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/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")

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
@@ -101,9 +103,16 @@ public class JavaCompilerCheckFacade {
                         .collect(Collectors.joining(":")));
         }
 
+        boolean universe = false;
+
         if (processors != null && !processors.isEmpty()) {
-            options.add("-processor");
-            options.add(processors.stream().collect(Collectors.joining(",")));
+            // 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<>();
@@ -125,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();

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

@@ -34,6 +34,9 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.util.stream.Collectors;
+import java.util.Objects;
+
 /**
  * Extension provides Javac checks for recent-loaded Java files.
  * <p>
@@ -150,16 +153,19 @@ private void loadProof(Proof selectedProof) throws RuntimeException {
                 return;
             }
 
-            Path bootClassPath = jm.getBootClassPath() != null ? jm.getBootClassPath() : null;
+            Path bootClassPath = jm.getBootClassPath(); // may be null
             List<Path> classpath = jm.getClassPath();
             JavacSettings settings = JavacSettingsProvider.getJavacSettings();
 
             List<String> processors = null;
             if (settings.getUseProcessors()) {
                 if (classpath == null) classpath = new ArrayList<>();
 
-                classpath.addAll(Arrays.asList(settings.getClassPaths().split(System.lineSeparator()))
-                    .stream().map(p -> Paths.get(p)).toList());
+                String classpaths = settings.getClassPaths();
+                if (!classpaths.isEmpty()) {
+                    classpath.addAll(Arrays.asList(classpaths.split(System.lineSeparator()))
+                        .stream().map(p -> Paths.get(p)).toList());
+                }
 
                 processors = Arrays.asList(settings.getProcessors().split(System.lineSeparator()));
             }

key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java

@@ -4,23 +4,49 @@
 package de.uka.ilkd.key.gui.plugins.javac;
 
 import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.List;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.concurrent.ExecutionException;
 
 import de.uka.ilkd.key.proof.ProofAggregate;
 import de.uka.ilkd.key.proof.init.ProblemInitializer;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
+import de.uka.ilkd.key.gui.PositionedIssueString;
 
 import org.junit.jupiter.api.Test;
 
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
 /**
  * @author Alexander Weigl
  * @version 1 (29.01.23)
  */
 class JavaCompilerCheckFacadeTest {
     @Test
     void compile1() throws ExecutionException, InterruptedException {
-        File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile();
+        Path src = Paths.get("examples/firstTouch/06-BinarySearch/src/");
+        assertEquals(checkFile(src, Collections.emptyList()).size(), 0);
+    }
+
+    @Test 
+    void compileUniverseCorrect() throws ExecutionException, InterruptedException { 
+        Path src = Paths.get("src/test/resources/plugins/javac/Correct.java");
+        assertEquals(checkFile(src, Arrays.asList("universe.UniverseChecker")).size(), 0);
+    }
+
+    @Test
+    void compileUniverseIncorrect() throws ExecutionException, InterruptedException, IOException {
+        Path src = Paths.get("src/test/resources/plugins/javac/Incorrect.java");
+        assertEquals(checkFile(src, Collections.emptyList()).size(), 0);
+        assertEquals(checkFile(src, Arrays.asList("universe.UniverseChecker")).size(), 1);
+    }
+
+    List<PositionedIssueString> checkFile(Path src, List<String> processors) throws ExecutionException, InterruptedException  {
         System.out.println(src);
         ProblemInitializer.ProblemInitializerListener emptyListener =
             new ProblemInitializer.ProblemInitializerListener() {
@@ -48,8 +74,7 @@ public void reportException(Object sender, ProofOblInput input, Exception e) {}
             };
         var promise =
             JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(),
-                src.toPath());
-        promise.get();
+                src, processors);
+        return promise.get();
     }
-
 }