Add the Universe Type Checker as a Dependency

.gitignore

@@ -51,6 +51,7 @@ bin/
 .settings
 .project
 .classpath
+*/.factorypath
 
 # Files generated by IntelliJ ANTLR plugin
 key.core/src/main/gen

build.gradle

@@ -81,7 +81,6 @@ subprojects {
         implementation("org.slf4j:slf4j-api:2.0.17")
         testImplementation("ch.qos.logback:logback-classic:1.5.20")
 
-
         compileOnly("org.jspecify:jspecify:1.0.0")
         testCompileOnly("org.jspecify:jspecify:1.0.0")
         def eisop_version = "3.49.3-eisop1"

key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java

@@ -525,7 +525,7 @@ private ConfigurationWriter printMap(Map<?, ?> value) {
             }
             indent -= 4;
             newline().printIndent();
-            out.format(" }");
+            out.format("}");
             return this;
         }
 
@@ -555,7 +555,7 @@ private ConfigurationWriter printSeq(Collection<?> value) {
             }
             indent -= 4;
             newline().printIndent();
-            out.format(" ]");
+            out.format("]");
             return this;
         }
 

key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java

@@ -53,8 +53,8 @@ public class ProofIndependentSettings {
     private final List<Settings> settings = new LinkedList<>();
 
     private final PropertyChangeListener settingsListener = e -> saveSettings();
-    private Properties lastReadedProperties;
-    private Configuration lastReadedConfiguration;
+    private Properties lastReadProperties;
+    private Configuration lastReadConfiguration;
 
     private ProofIndependentSettings() {
         addSettings(smtSettings);
@@ -74,11 +74,11 @@ public void addSettings(Settings settings) {
         if (!this.settings.contains(settings)) {
             this.settings.add(settings);
             settings.addPropertyChangeListener(settingsListener);
-            if (lastReadedProperties != null) {
-                settings.readSettings(lastReadedProperties);
+            if (lastReadProperties != null) {
+                settings.readSettings(lastReadProperties);
             }
-            if (lastReadedConfiguration != null) {
-                settings.readSettings(lastReadedConfiguration);
+            if (lastReadConfiguration != null) {
+                settings.readSettings(lastReadConfiguration);
             }
         }
     }
@@ -106,19 +106,22 @@ private void load(File file) throws IOException {
                 for (Settings settings : settings) {
                     settings.readSettings(properties);
                 }
-                lastReadedProperties = properties;
+                lastReadProperties = properties;
             }
         } else {
-            this.lastReadedConfiguration = Configuration.load(file);
+            this.lastReadConfiguration = Configuration.load(file);
             for (Settings settings : settings) {
-                settings.readSettings(lastReadedConfiguration);
+                settings.readSettings(lastReadConfiguration);
             }
         }
     }
 
     public void saveSettings() {
         if (!filename.getName().endsWith(".json")) {
-            Properties result = new Properties();
+            Properties result = lastReadProperties == null 
+                ? new Properties()
+                : new Properties(lastReadProperties);
+
             for (Settings settings : settings) {
                 settings.writeSettings(result);
             }
@@ -135,6 +138,10 @@ public void saveSettings() {
         }
 
         Configuration config = new Configuration();
+        if (lastReadConfiguration != null) {
+            config.overwriteWith(lastReadConfiguration);
+        }
+
         for (var settings : settings)
             settings.writeSettings(config);
         if (!filename.exists()) {

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT

@@ -58,4 +58,12 @@ java.util.ListIteratorImpl
 java.util.Date
 java.util.LinkedHashMap
 java.util.LinkedList
-
+universe.qual.Any
+universe.qual.Dom
+universe.qual.Payload
+universe.qual.Rep
+universe.qual.Self
+universe.qual.Bottom
+universe.qual.Lost
+universe.qual.Peer
+universe.qual.RepOnly

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java

@@ -6,5 +6,4 @@
 public interface Annotation
 {
 
-   public java.lang.Class annotationType();
 }

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Any.java

@@ -0,0 +1,9 @@
+package universe.qual;
+
+/**
+ * The Any modifier expresses no static ownership information, the referenced object can have any
+ * owner.
+ *
+ * @author wmdietl
+ */
+public @interface Any {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Bottom.java

@@ -0,0 +1,8 @@
+package universe.qual;
+
+/**
+ * The bottom of the type hierarchy is only used internally.
+ *
+ * @author wmdietl
+ */
+public @interface Bottom {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Dom.java

@@ -0,0 +1,8 @@
+package universe.qual;
+
+/**
+ * The referenced object is dominated by the current object.
+ *
+ * @author PiisRational
+ */
+public @interface Dom {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Lost.java

@@ -0,0 +1,3 @@
+package universe.qual;
+
+public @interface Lost {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Payload.java

@@ -0,0 +1,9 @@
+package universe.qual;
+
+
+/**
+ * The Payload modifier expresses that the underlying object cannot be accessed in any way.
+ *
+ * @author Daniel Grévent
+ */
+public @interface Payload {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Peer.java

@@ -0,0 +1,8 @@
+package universe.qual;
+
+/**
+ * The referenced object has the same owner as the current object.
+ *
+ * @author wmdietl
+ */
+public @interface Peer {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Rep.java

@@ -0,0 +1,9 @@
+package universe.qual;
+
+
+/**
+ * The current object owns the referenced object.
+ *
+ * @author wmdietl
+ */
+public @interface Rep {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/RepOnly.java

@@ -0,0 +1,9 @@
+package universe.qual;
+
+/**
+ * The RepOnly modifier expresses that a method can only access owned fields and other RepOnly
+ * methods.
+ *
+ * @author Daniel Grévent
+ */
+public @interface RepOnly {}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Self.java

@@ -0,0 +1,8 @@
+package universe.qual;
+
+/**
+ * A special annotation to distinguish the current object "this" from other objects.
+ *
+ * @author wmdietl
+ */
+public @interface Self {}

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key

@@ -1366,7 +1366,7 @@
 
         \replacewith(alpha::final(o,f))
 
-	\heuristics(simplify)
+	      \heuristics(simplify)
     };
 
 
@@ -1391,7 +1391,7 @@
         \schemaVar \term Object o;
         \schemaVar \term int idx;
 
-	\assumes( ==> o = null )
+	      \assumes( ==> o = null )
 
         \find(beta::final(o,arr(idx))) \sameUpdateLevel
 
@@ -1400,7 +1400,7 @@
 
         \replacewith(alpha::final(o,arr(idx)))
 
-	\heuristics(simplify)
+	      \heuristics(simplify)
     };
 
 

key.ui/build.gradle

@@ -18,6 +18,8 @@ dependencies {
     implementation project(":key.core.rifl")
 
     implementation("com.formdev:flatlaf:3.6.2")
+    implementation("io.github.piisrational.universe:universe:0.1.0")
+    implementation("io.github.eisop:checker:3.42.0-eisop3")
 
     implementation project(":key.core.proof_references")
     implementation project(":key.core.symbolic_execution")
@@ -51,6 +53,28 @@ tasks.register('createExamplesZip', Zip) {
 
 processResources.dependsOn << createExamplesZip
 
+tasks.withType(Test).configureEach {
+    jvmArgs += [
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
+        "--add-opens", 
+        "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED" 
+    ]
+}
 
 shadowJar {
     archiveClassifier.set("exe")
@@ -80,7 +104,30 @@ run {
 
     // this can be used to solve a problem where the OS hangs during debugging of popup menus
     // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425)
-    jvmArgs += "-Dsun.awt.disablegrab=true"
+    jvmArgs += "-Dsun.awt.disablegrab=true "
+
+    // this is needed to be able to load checker framework checkers in the javac
+    // extension
+    jvmArgs += [
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
+        "--add-opens", 
+        "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED" 
+    ]
 }
 
 tasks.register('runWithProfiler', JavaExec) {

key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java

@@ -26,6 +26,8 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import universe.UniverseChecker;
+
 /**
  * This facade checks whether the Java program to be verified is compilable using <code>javac</code>
  * via
@@ -52,15 +54,17 @@ public class JavaCompilerCheckFacade {
      *
      * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed
      *        about any issues found in the target Java program
-     * @param bootClassPath the {@link File} referring to the path containing the core Java classes
-     * @param classPath the {@link List} of {@link File}s referring to the directory that make up
+     * @param bootClassPath the {@link Path} referring to the path containing the core Java classes
+     * @param classPath the {@link List} of {@link Path}s referring to the directory that make up
      *        the target Java programs classpath
-     * @param javaPath the {@link String} with the path to the source of the target Java program
+     * @param javaPath the {@link Path} to the source of the target Java program
+     * @param processors the {@link List} of {@link String}s referring to the annotation processors to be run
      * @return future providing the list of diagnostics
      */
     public static @NonNull CompletableFuture<List<PositionedIssueString>> check(
             ProblemInitializer.ProblemInitializerListener listener,
-            Path bootClassPath, List<Path> classPath, Path javaPath) {
+            Path bootClassPath, List<Path> classPath, Path javaPath,
+            List<String> processors) {
         if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) {
             LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE");
             return CompletableFuture.completedFuture(Collections.emptyList());
@@ -86,6 +90,7 @@ public class JavaCompilerCheckFacade {
 
         // gather configured bootstrap classpath and regular classpath
         List<String> options = new ArrayList<>();
+
         if (bootClassPath != null) {
             options.add("-Xbootclasspath");
             options.add(bootClassPath.toAbsolutePath().toString());
@@ -97,6 +102,19 @@ public class JavaCompilerCheckFacade {
                         .map(Objects::toString)
                         .collect(Collectors.joining(":")));
         }
+
+        boolean universe = false;
+
+        if (processors != null && !processors.isEmpty()) {
+            // there is no guarantee that remove is supported else
+            processors = new LinkedList<>(processors); 
+            universe = processors.remove("universe.UniverseChecker");
+            if (!processors.isEmpty()) {
+                options.add("-processor");
+                options.add(processors.stream().collect(Collectors.joining(",")));
+            }
+        }
+
         ArrayList<Path> files = new ArrayList<>();
         if (Files.isDirectory(javaPath)) {
             try (var s = Files.walk(javaPath)) {
@@ -116,6 +134,10 @@ public class JavaCompilerCheckFacade {
         JavaCompiler.CompilationTask task = compiler.getTask(output, fileManager, diagnostics,
             options, classes, compilationUnits);
 
+        if (universe) {
+            task.setProcessors(Collections.singletonList(new UniverseChecker()));
+        }
+
         return CompletableFuture.supplyAsync(() -> {
             long start = System.currentTimeMillis();
             var b = task.call();