fix ProofBundleIOTest (and setting classpath/bootclasspath in .key files): make sure that Java files are always read through FileRepo, set bcp/cp earlier, remove String.key from bundle

Author: WolframPfeifer

key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java

@@ -114,6 +114,7 @@ public class JavaService {
     @NonNull
     private final Path bootClassPath;
 
+    private final FileRepo fileRepo;
 
     /**
      * A list of {@link File} objects that describes the classpath to be searched
@@ -123,11 +124,12 @@ public class JavaService {
     private final Collection<Path> libraryPath;
 
     public JavaService(Services services, @NonNull Path bootClassPath,
-            @NonNull Collection<Path> libraryPath) {
+            @NonNull Collection<Path> libraryPath, FileRepo fileRepo) {
         this.services = services;
         this.mapping = new KeYJPMapping();
         this.bootClassPath = bootClassPath;
         this.libraryPath = libraryPath;
+        this.fileRepo = fileRepo;
         programFactory = new JavaParserFactory(services);
         typeConverter = new JP2KeYTypeConverter(services, programFactory.getTypeSolver(), mapping);
         converter = new JP2KeYConverter(services, new Namespace<>());
@@ -137,6 +139,8 @@ private JavaService(JavaService o, Services services) {
         this.services = services;
         this.bootClassPath = o.bootClassPath;
         this.libraryPath = o.libraryPath;
+        // TODO: copy filerepo instead?
+        this.fileRepo = o.fileRepo;
         this.mapping = o.mapping.copy();
         programFactory = o.programFactory.copy(services);
         typeConverter = new JP2KeYTypeConverter(services, programFactory.getTypeSolver(), mapping);
@@ -238,7 +242,7 @@ public List<de.uka.ilkd.key.java.ast.CompilationUnit> readCompilationUnits(
             Path parent,
             Collection<Path> files, FileRepo repo)
             throws IOException, BuildingExceptions {
-        parseSpecialClasses();
+        parseSpecialClasses(repo);
         var cus = new ArrayList<CompilationUnit>(files.size());
         for (Path file : files) {
             var cu = unwrapParseResult(file.toString(), parseCompilationUnit(file, repo));
@@ -732,7 +736,9 @@ private com.github.javaparser.ast.type.Type keyType2JPType(Type type) {
      * @return the parsed and resolved recoder statement block
      */
     Node parseBlock(String input, JPContext context) {
-        parseSpecialClasses();
+        // ensure bootclasspath/classpath are read (needed for resolution in modalities in taclets)
+        parseSpecialClasses(fileRepo);
+
         // TODO javaparser change grammar of the parser to allow blocks without context information
         // Context-block
         Node original;

key.core/src/main/java/de/uka/ilkd/key/java/Services.java

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.proof.*;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
+import de.uka.ilkd.key.proof.io.consistency.FileRepo;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 import de.uka.ilkd.key.util.KeYResourceManager;
 
@@ -473,19 +474,19 @@ public JavaService getJavaService() {
     }
 
     private JavaService activateJavaPath(@NonNull Path bootClassPath,
-            @NonNull Collection<Path> libraryPaths) {
+            @NonNull Collection<Path> libraryPaths, FileRepo fileRepo) {
         if (javaService != null && javaService.getBootClassPath().equals(bootClassPath)
                 && CollectionUtil.containsSame(javaService.getLibraryPath(), libraryPaths)) {
             return javaService;
         }
         LOGGER.info("activate java with {} and {}", bootClassPath, libraryPaths);
-        javaService = new JavaService(this, bootClassPath, libraryPaths);
+        javaService = new JavaService(this, bootClassPath, libraryPaths, fileRepo);
         javaInfo = new JavaInfo(new KeYProgModelInfo(javaService), this);
         return javaService;
     }
 
     public JavaService activateJava(@Nullable Path bootClassPath,
-            @NonNull Collection<Path> libraryPaths) {
+            @NonNull Collection<Path> libraryPaths, FileRepo fileRepo) {
         Path path;
         if (bootClassPath != null) {
             path = bootClassPath;
@@ -497,11 +498,11 @@ public JavaService activateJava(@Nullable Path bootClassPath,
             libraryPaths = Collections.emptyList();
         }
 
-        return activateJavaPath(path, libraryPaths);
+        return activateJavaPath(path, libraryPaths, fileRepo);
     }
 
     public void activateJava(@Nullable Path bootClassPath) {
-        activateJava(bootClassPath, Collections.emptyList());
+        activateJava(bootClassPath, Collections.emptyList(), null);
     }
 
     public static Path getReduxPath() {

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -708,9 +708,14 @@ public Object visit(FieldAccessExpr n, Void arg) {
                 return new FieldReference(pi, c, variable, translatePackageReference(n.getScope()));
             }
         } catch (UnsolvedSymbolException e) {
-            ResolvedType type = n.calculateResolvedType();
-            var keyType = getKeYJavaType(type);
-            return new TypeRef(keyType);
+            try {
+                ResolvedType type = n.calculateResolvedType();
+                var keyType = getKeYJavaType(type);
+                return new TypeRef(keyType);
+            } catch (UnsolvedSymbolException e1) {
+                throw new ParserException("Name could not be resolved '" + n + "'",
+                    Location.fromNode(n));
+            }
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -238,8 +238,9 @@ private void readJava(EnvInput envInput, InitConfig initConfig) throws ProofInpu
         if (fileRepo != null) {
             // set the paths in the FileRepo (all three methods can deal with null parameters)
             fileRepo.setJavaPath(javaPath);
-            fileRepo.setClassPath(classPath);
-            fileRepo.setBootClassPath(bootClassPath);
+            // cp and bcp should have been set earlier (in activateJava)
+            //fileRepo.setClassPath(classPath);
+            //fileRepo.setBootClassPath(bootClassPath);
         }
 
         // weigl: 2021-01, Early including the includes of the KeYUserProblemFile,
@@ -406,11 +407,17 @@ private void setUpProofHelper(ProofOblInput problem, ProofAggregate pl)
         }
     }
 
-    private void activateInitConfigJava(InitConfig config, EnvInput envInput) {
+    private void activateInitConfigJava(InitConfig config, EnvInput envInput, FileRepo fileRepo) {
         var bootClassPath = envInput.readBootClassPath();
         var classPath = envInput.readClassPath();
         config.getServices().activateJava(bootClassPath,
-            classPath != null ? classPath : Collections.emptyList());
+            classPath != null ? classPath : Collections.emptyList(), fileRepo);
+
+        if (fileRepo != null) {
+            fileRepo.setClassPath(classPath);
+            fileRepo.setBootClassPath(bootClassPath);
+            config.setFileRepo(fileRepo);
+        }
     }
 
     /**
@@ -428,7 +435,7 @@ private InitConfig createInitConfigFor(EnvInput envInput) throws ProofInputExcep
         }
 
         InitConfig config = new InitConfig(services);
-        activateInitConfigJava(config, envInput);
+        activateInitConfigJava(config, envInput, fileRepo);
 
         // the first time, read in standard rules
         ImmutableList<RuleSource> tacletBases = profile.getStandardRules().getTacletBase();

key.core/src/test/java/KeyJavaPipelineTest.java

@@ -51,7 +51,7 @@ public KeYJavaPipeline createPipelineTest(Path testFolder) throws IOException {
         assertNotNull(nss.sorts().lookup("int"));
         assertNotNull(nss.sorts().lookup("boolean"));
         var inputFolder = testFolder.resolve("input");
-        var js = services.activateJava(null, Collections.singleton(inputFolder));
+        var js = services.activateJava(null, Collections.singleton(inputFolder), null);
         js.parseSpecialClasses();
 
         final var jp = js.getProgramFactory().createJavaParser();