From db0c5b02f883799fc4f874cde284c8b13ad8f3f5 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 9 Aug 2025 22:46:39 +0200 Subject: [PATCH 01/11] add missing standard annotations to JavaRedux --- .../de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT | 5 ++++- .../java/lang/annotation/Annotation.java | 5 ++++- .../java/lang/annotation/Documented.java | 4 ++++ .../java/lang/annotation/ElementType.java | 16 ++++++++++++++++ .../java/lang/annotation/Retention.java | 5 +++++ .../java/lang/annotation/RetentionPolicy.java | 7 +++++++ .../JavaRedux/java/lang/annotation/Target.java | 5 +++++ .../de/uka/ilkd/key/proof/rules/heapRules.key | 6 +++--- 8 files changed, 48 insertions(+), 5 deletions(-) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT index ece9cf04a53..a86564689ec 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT @@ -1,5 +1,9 @@ java.lang.Object java.lang.annotation.Annotation +java.lang.annotation.ElementType +java.lang.annotation.Retention +java.lang.annotation.RetentionPolicy +java.lang.annotation.Target java.lang.ArithmeticException java.lang.ArrayIndexOutOfBoundsException java.lang.ArrayStoreException @@ -58,4 +62,3 @@ java.util.ListIteratorImpl java.util.Date java.util.LinkedHashMap java.util.LinkedList - diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java index ed8b65547ec..a65813efb64 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java @@ -5,6 +5,9 @@ public interface Annotation { + public int hashCode(); - public java.lang.Class annotationType(); + public String toString(); + + public java.lang.Class annotationType(); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java new file mode 100644 index 00000000000..c068b55a50e --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java @@ -0,0 +1,4 @@ +package java.lang.annotation; + +public @interface Documented { +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java new file mode 100644 index 00000000000..4a09eb9312e --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java @@ -0,0 +1,16 @@ +package java.lang.annotation; + +public enum ElementType { + TYPE, + FIELD, + METHOD, + PARAMETER, + CONSTRUCTOR, + LOCAL_VARIABLE, + ANNOTATION_TYPE, + PACKAGE, + TYPE_PARAMETER, + TYPE_USE, + MODULE, + RECORD_COMPONENT +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java new file mode 100644 index 00000000000..bb54c77a35e --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java @@ -0,0 +1,5 @@ +package java.lang.annotation; + +public @interface Retention { + public RetentionPolicy value(); +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java new file mode 100644 index 00000000000..bcd9b9d8158 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java @@ -0,0 +1,7 @@ +package java.lang.annotation; + +public enum RetentionPolicy { + SOURCE, + CLASS, + RUNTIME +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java new file mode 100644 index 00000000000..f1e24a4cf6e --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java @@ -0,0 +1,5 @@ +package java.lang.annotation; + +public @interface Target { + public ElementType[] value(); +} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key index 6936e4daea1..fe79de150eb 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key +++ b/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) }; From 5d55191740865507d865ca746e15abc6196c0d72 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 8 Dec 2025 14:57:16 +0100 Subject: [PATCH 02/11] first try --- build.gradle | 4 +++- .../de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/build.gradle b/build.gradle index d7745aa8613..b9916232710 100644 --- a/build.gradle +++ b/build.gradle @@ -70,6 +70,7 @@ subprojects { } repositories { + mavenLocal() mavenCentral() maven { url = 'https://git.key-project.org/api/v4/projects/35/packages/maven' @@ -81,7 +82,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" @@ -91,6 +91,8 @@ subprojects { checkerFramework "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" + implementation "piisrational:universe:0.1" + testImplementation("ch.qos.logback:logback-classic:1.5.20") testImplementation("org.assertj:assertj-core:3.27.6") testImplementation("ch.qos.logback:logback-classic:1.5.20") diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index a36732b5390..799fe1c8207 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -150,7 +150,7 @@ private void loadProof(Proof selectedProof) throws RuntimeException { return; } - Path bootClassPath = jm.getBootClassPath() != null ? jm.getBootClassPath() : null; + Path bootClassPath = jm.getBootClassPath(); // may be null List classpath = jm.getClassPath(); JavacSettings settings = JavacSettingsProvider.getJavacSettings(); From 81dc0ab27df9aceab63e961e19dbddbc508a4de0 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 15 Dec 2025 13:58:49 +0100 Subject: [PATCH 03/11] update the build scripts and add the annotations to key --- build.gradle | 2 -- .../de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT | 9 +++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Any.java | 9 +++++++++ .../ilkd/key/java/JavaRedux/universe/qual/Bottom.java | 8 ++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Dom.java | 8 ++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Lost.java | 3 +++ .../ilkd/key/java/JavaRedux/universe/qual/Payload.java | 9 +++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Peer.java | 8 ++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Rep.java | 9 +++++++++ .../ilkd/key/java/JavaRedux/universe/qual/RepOnly.java | 9 +++++++++ .../uka/ilkd/key/java/JavaRedux/universe/qual/Self.java | 8 ++++++++ key.ui/build.gradle | 7 +++++++ 12 files changed, 87 insertions(+), 2 deletions(-) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Any.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Bottom.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Dom.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Lost.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Payload.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Peer.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Rep.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/RepOnly.java create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Self.java diff --git a/build.gradle b/build.gradle index b9916232710..8262aa061c6 100644 --- a/build.gradle +++ b/build.gradle @@ -91,8 +91,6 @@ subprojects { checkerFramework "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" - implementation "piisrational:universe:0.1" - testImplementation("ch.qos.logback:logback-classic:1.5.20") testImplementation("org.assertj:assertj-core:3.27.6") testImplementation("ch.qos.logback:logback-classic:1.5.20") diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT index a86564689ec..454ba20d94d 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT @@ -62,3 +62,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 diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Any.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Any.java new file mode 100644 index 00000000000..95be30c499a --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Bottom.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Bottom.java new file mode 100644 index 00000000000..b198769dcef --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Dom.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Dom.java new file mode 100644 index 00000000000..c9afc4df3ab --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Lost.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Lost.java new file mode 100644 index 00000000000..aaac7273087 --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Payload.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Payload.java new file mode 100644 index 00000000000..77c386ef380 --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Peer.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Peer.java new file mode 100644 index 00000000000..6110608e340 --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Rep.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Rep.java new file mode 100644 index 00000000000..079eaa20da0 --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/RepOnly.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/RepOnly.java new file mode 100644 index 00000000000..80174ee1b00 --- /dev/null +++ b/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 {} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Self.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/universe/qual/Self.java new file mode 100644 index 00000000000..cf047a60608 --- /dev/null +++ b/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 {} diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 5b94221ae2a..e5d7d13562f 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -18,6 +18,7 @@ dependencies { implementation project(":key.core.rifl") implementation("com.formdev:flatlaf:3.6.2") + implementation("piisrational:universe:0.1") implementation project(":key.core.proof_references") implementation project(":key.core.symbolic_execution") @@ -69,7 +70,13 @@ application { mainClass.set("de.uka.ilkd.key.core.Main") } +task copyToLib(type: Copy) { + into "$buildDir/output/libs" + from configurations.runtimeClasspath +} + run { + dependsOn(copyToLib) systemProperties["key.examples.dir"] = "$projectDir/examples" //systemProperties["slf4j.detectLoggerNameMismatch"] = true //systemProperties["KeyDebugFlag"] = "on" From 834ec52b490cdcdd247a36dceade6b7a2f01c452 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 4 Jan 2026 19:08:06 +0100 Subject: [PATCH 04/11] universe typechecking works without adding anything to the classpath! --- .gitignore | 1 + key.ui/build.gradle | 7 +------ .../gui/plugins/javac/JavaCompilerCheckFacade.java | 11 +++++++++++ keyext.isabelletranslation/build.gradle | 6 +++++- 4 files changed, 18 insertions(+), 7 deletions(-) diff --git a/.gitignore b/.gitignore index 894015b1c6c..d29b77f1797 100644 --- a/.gitignore +++ b/.gitignore @@ -51,6 +51,7 @@ bin/ .settings .project .classpath +*/.factorypath # Files generated by IntelliJ ANTLR plugin key.core/src/main/gen diff --git a/key.ui/build.gradle b/key.ui/build.gradle index e5d7d13562f..bebf11fb157 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -19,6 +19,7 @@ dependencies { implementation("com.formdev:flatlaf:3.6.2") implementation("piisrational:universe:0.1") + implementation("io.github.eisop:checker:3.42.0-eisop3") implementation project(":key.core.proof_references") implementation project(":key.core.symbolic_execution") @@ -70,13 +71,7 @@ application { mainClass.set("de.uka.ilkd.key.core.Main") } -task copyToLib(type: Copy) { - into "$buildDir/output/libs" - from configurations.runtimeClasspath -} - run { - dependsOn(copyToLib) systemProperties["key.examples.dir"] = "$projectDir/examples" //systemProperties["slf4j.detectLoggerNameMismatch"] = true //systemProperties["KeyDebugFlag"] = "on" diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java index 15a19f60fc9..d5d577a0e67 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java +++ b/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 javac * via @@ -101,7 +103,12 @@ public class JavaCompilerCheckFacade { .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"); options.add("-processor"); options.add(processors.stream().collect(Collectors.joining(","))); } @@ -125,6 +132,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(); diff --git a/keyext.isabelletranslation/build.gradle b/keyext.isabelletranslation/build.gradle index e2119425bdb..6cb49424322 100644 --- a/keyext.isabelletranslation/build.gradle +++ b/keyext.isabelletranslation/build.gradle @@ -14,4 +14,8 @@ dependencies { */ configurations.configureEach { exclude group: 'org.slf4j', module: 'slf4j-simple' -} \ No newline at end of file + + // interferes with the checker framework used by the universe checker + // but is not used by the dependency + exclude group: 'org.checkerframework', module: 'checker-qual:3.42.0' +} From 7c4726f32d04c29afdfb4bba0c1959af914c1b3a Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 4 Jan 2026 21:46:22 +0100 Subject: [PATCH 05/11] removing the other checkerframework is not necessary --- keyext.isabelletranslation/build.gradle | 4 ---- 1 file changed, 4 deletions(-) diff --git a/keyext.isabelletranslation/build.gradle b/keyext.isabelletranslation/build.gradle index 6cb49424322..0a75bb1bb8b 100644 --- a/keyext.isabelletranslation/build.gradle +++ b/keyext.isabelletranslation/build.gradle @@ -14,8 +14,4 @@ dependencies { */ configurations.configureEach { exclude group: 'org.slf4j', module: 'slf4j-simple' - - // interferes with the checker framework used by the universe checker - // but is not used by the dependency - exclude group: 'org.checkerframework', module: 'checker-qual:3.42.0' } From c3060714f80c9695a1651f51871c07220f9a830e Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 10 Jan 2026 14:14:31 +0100 Subject: [PATCH 06/11] update build.gradle --- key.ui/build.gradle | 1 + 1 file changed, 1 insertion(+) diff --git a/key.ui/build.gradle b/key.ui/build.gradle index bebf11fb157..d18ac60e602 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -18,6 +18,7 @@ dependencies { implementation project(":key.core.rifl") implementation("com.formdev:flatlaf:3.6.2") + // implementation("io.github.piisrational:universe:0.1.0") implementation("piisrational:universe:0.1") implementation("io.github.eisop:checker:3.42.0-eisop3") From d9dc07fcaac47464780767ed0514bf8272c30787 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Tue, 13 Jan 2026 15:17:29 +0100 Subject: [PATCH 07/11] fix a bug concerning the javac extension classpaths --- key.ui/build.gradle | 2 +- .../key/gui/plugins/javac/JavaCompilerCheckFacade.java | 6 ++++-- .../uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 10 ++++++++-- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/key.ui/build.gradle b/key.ui/build.gradle index d18ac60e602..f60107416d4 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -19,7 +19,7 @@ dependencies { implementation("com.formdev:flatlaf:3.6.2") // implementation("io.github.piisrational:universe:0.1.0") - implementation("piisrational:universe:0.1") + implementation("piisrational:universe:0.1.0") implementation("io.github.eisop:checker:3.42.0-eisop3") implementation project(":key.core.proof_references") diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java index d5d577a0e67..d9d70ab3841 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java @@ -109,8 +109,10 @@ public class JavaCompilerCheckFacade { // there is no guarantee that remove is supported else processors = new LinkedList<>(processors); universe = processors.remove("universe.UniverseChecker"); - options.add("-processor"); - options.add(processors.stream().collect(Collectors.joining(","))); + if (!processors.isEmpty()) { + options.add("-processor"); + options.add(processors.stream().collect(Collectors.joining(","))); + } } ArrayList files = new ArrayList<>(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index 799fe1c8207..a0ca18c5526 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/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. *

@@ -158,8 +161,11 @@ private void loadProof(Proof selectedProof) throws RuntimeException { 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())); } From f055f55a002cfd62437bf15e1a2102bbb0e923e9 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 25 Jan 2026 22:07:26 +0100 Subject: [PATCH 08/11] use the universe checker on maven central --- build.gradle | 1 - key.ui/build.gradle | 3 +-- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/build.gradle b/build.gradle index 8262aa061c6..c3c929e7e56 100644 --- a/build.gradle +++ b/build.gradle @@ -70,7 +70,6 @@ subprojects { } repositories { - mavenLocal() mavenCentral() maven { url = 'https://git.key-project.org/api/v4/projects/35/packages/maven' diff --git a/key.ui/build.gradle b/key.ui/build.gradle index f60107416d4..4748da7396c 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -18,8 +18,7 @@ dependencies { implementation project(":key.core.rifl") implementation("com.formdev:flatlaf:3.6.2") - // implementation("io.github.piisrational:universe:0.1.0") - implementation("piisrational:universe:0.1.0") + implementation("io.github.piisrational.universe:universe:0.1.0") implementation("io.github.eisop:checker:3.42.0-eisop3") implementation project(":key.core.proof_references") From 47dfe9c84916f16dc90920dbfac22efdea031b2e Mon Sep 17 00:00:00 2001 From: PiisRational Date: Fri, 30 Jan 2026 12:42:06 +0100 Subject: [PATCH 09/11] remove unnessecary previously added javaredux classes --- .../de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT | 4 ---- .../java/lang/annotation/Annotation.java | 4 ---- .../java/lang/annotation/Documented.java | 4 ---- .../java/lang/annotation/ElementType.java | 16 ---------------- .../java/lang/annotation/Retention.java | 5 ----- .../java/lang/annotation/RetentionPolicy.java | 7 ------- .../JavaRedux/java/lang/annotation/Target.java | 5 ----- 7 files changed, 45 deletions(-) delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java delete mode 100644 key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT index 454ba20d94d..4bc27ab05d4 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT @@ -1,9 +1,5 @@ java.lang.Object java.lang.annotation.Annotation -java.lang.annotation.ElementType -java.lang.annotation.Retention -java.lang.annotation.RetentionPolicy -java.lang.annotation.Target java.lang.ArithmeticException java.lang.ArrayIndexOutOfBoundsException java.lang.ArrayStoreException diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java index a65813efb64..54fa274f138 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Annotation.java @@ -5,9 +5,5 @@ public interface Annotation { - public int hashCode(); - public String toString(); - - public java.lang.Class annotationType(); } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java deleted file mode 100644 index c068b55a50e..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Documented.java +++ /dev/null @@ -1,4 +0,0 @@ -package java.lang.annotation; - -public @interface Documented { -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java deleted file mode 100644 index 4a09eb9312e..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/ElementType.java +++ /dev/null @@ -1,16 +0,0 @@ -package java.lang.annotation; - -public enum ElementType { - TYPE, - FIELD, - METHOD, - PARAMETER, - CONSTRUCTOR, - LOCAL_VARIABLE, - ANNOTATION_TYPE, - PACKAGE, - TYPE_PARAMETER, - TYPE_USE, - MODULE, - RECORD_COMPONENT -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java deleted file mode 100644 index bb54c77a35e..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Retention.java +++ /dev/null @@ -1,5 +0,0 @@ -package java.lang.annotation; - -public @interface Retention { - public RetentionPolicy value(); -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java deleted file mode 100644 index bcd9b9d8158..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/RetentionPolicy.java +++ /dev/null @@ -1,7 +0,0 @@ -package java.lang.annotation; - -public enum RetentionPolicy { - SOURCE, - CLASS, - RUNTIME -} diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java deleted file mode 100644 index f1e24a4cf6e..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/lang/annotation/Target.java +++ /dev/null @@ -1,5 +0,0 @@ -package java.lang.annotation; - -public @interface Target { - public ElementType[] value(); -} From 82a54dfb6d8b3f294e0b5d2d359dfbf26a7801de Mon Sep 17 00:00:00 2001 From: PiisRational Date: Tue, 3 Feb 2026 15:08:01 +0100 Subject: [PATCH 10/11] add tests for the javac check facade --- .../javac/JavaCompilerCheckFacadeTest.java | 33 +++- .../test/resources/plugins/javac/Correct.java | 141 ++++++++++++++++++ .../resources/plugins/javac/Incorrect.java | 7 + 3 files changed, 177 insertions(+), 4 deletions(-) create mode 100644 key.ui/src/test/resources/plugins/javac/Correct.java create mode 100644 key.ui/src/test/resources/plugins/javac/Incorrect.java diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java index 5cae7320876..79ad95d8ee4 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java @@ -4,15 +4,24 @@ 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) @@ -20,7 +29,24 @@ 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/recources/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/recources/plugins/javac/Incorrect.java"); + assertEquals(checkFile(src, Collections.emptyList()).size(), 0); + assertEquals(checkFile(src, Arrays.asList("universe.UniverseChecker")).size(), 1); + } + + List checkFile(Path src, List 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(); } - } diff --git a/key.ui/src/test/resources/plugins/javac/Correct.java b/key.ui/src/test/resources/plugins/javac/Correct.java new file mode 100644 index 00000000000..195a49c866a --- /dev/null +++ b/key.ui/src/test/resources/plugins/javac/Correct.java @@ -0,0 +1,141 @@ +import universe.qual.Rep; +import universe.qual.Peer; +import universe.qual.Payload; + +class Client { + /*@ normal_behaviour + @ requires t1 != t2; + @ requires t2.isConst(0); + @ requires \invariant_for(t1) && \invariant_for(t2); + @ ensures t2.isConst(0); + */ + void increment(@Rep Tree t1, @Rep Tree t2) { + t1.increment(); + } + + /*@ normal_behaviour + @ requires t1 != t2; + @ requires t2.isConst(t2.value); + @ requires \invariant_for(t1); + @ requires \invariant_for(t2); + @ requires t1.isConst(t1.value); + @ ensures t1.value == \old(t1.value) + 1; + @ ensures t1.isConst(t1.value); + @ ensures t2.isConst(\old(t2.value)); + */ + void increment2(@Rep Tree t1, @Rep Tree t2) { + t1.increment(); + } + + /*@ normal_behaviour + @ requires t1 != t2; + @ requires t2.isConst(t2.value); + @ requires \invariant_for(t2); + @ requires \invariant_for(t1); + @ ensures t1.contains(value); + @ ensures t2.isConst(\old(t2.value)); + */ + void append(@Rep Tree t1, int value, @Rep Tree t2) { + t1.append(value); + } + + /*@ normal_behaviour + @ requires t1 != t2; + @ requires t2.isConst(t2.value); + @ requires \invariant_for(t2); + @ requires \invariant_for(t1); + @ requires t1.contains(0); + @ ensures t1.contains(1); + @ ensures t2.isConst(\old(t2.value)); + */ + void append(@Rep Tree t1, @Rep Tree t2) { + t1.increment(); + } +} + +final class Tree { + public @Rep /*@ nullable */ Tree left; + public @Rep /*@ nullable */ Tree right; + public int value; + + //@ public ghost \dl_tree t; + //@ public accessible \inv: \dl_createdRepfp(this); + //@ public invariant t == \dl_Node(left == null ? \dl_Leaf() : left.t, value, right == null ? \dl_Leaf() : right.t); + //@ public invariant \dl_tree_count(t) >= 0; + //@ public invariant left != null ==> \invariant_for(left); + //@ public invariant right != null ==> \invariant_for(right); + //@ public invariant left != null && right != null ==> right != left; + + /*@ public normal_behaviour + @ ensures left == null && right == null && value == v; + @ ensures t == \dl_Node(\dl_Leaf(), v, \dl_Leaf()); + @*/ + public /*@ pure */ Tree(int v) { + left = null; + right = null; + value = v; + //@ set t = \dl_Node(\dl_Leaf(), v, \dl_Leaf()); + } + + /*@ public normal_behaviour + @ ensures \result == \dl_tree_is_const(t, v); + @ measured_by \dl_tree_count(t); + @ accessible \dl_createdRepfp(this); + @*/ + public /*@ pure */ boolean isConst(int v) { + if (value != v) return false; + if (left != null && !left.isConst(v)) return false; + if (right != null && !right.isConst(v)) return false; + return true; + } + + /*@ public normal_behaviour + @ ensures \result == \dl_tree_contains(t, v); + @ measured_by \dl_tree_count(t); + @ accessible \dl_createdRepfp(this); + @*/ + public /*@ pure */ boolean contains(int v) { + if (value == v) return true; + if (left != null && left.contains(v)) return true; + if (right != null && right.contains(v)) return true; + return false; + } + + /*@ public normal_behaviour + @ ensures t == \dl_tree_append(\old(t), v); + @ ensures \dl_tree_count(t) == \dl_tree_count(\old(t)) + 1; + @ measured_by \dl_tree_count(t); + @ assignable \dl_createdRepfp(this); + @*/ + public void append(int v) { + if (v <= value) { + if (left == null) { + left = new @Rep Tree(v); + } else { + left.append(v); + } + } else { + if (right == null) { + right = new @Rep Tree(v); + } else { + right.append(v); + } + } + + //@ set t = \dl_Node(left == null ? \dl_Leaf() : left.t, value, right == null ? \dl_Leaf() : right.t); + } + + /*@ public normal_behaviour + @ ensures t == \dl_tree_increment(\old(t)); + @ ensures \dl_tree_count(t) == \dl_tree_count(\old(t)); + @ measured_by \dl_tree_count(t); + @ assignable \dl_createdRepfp(this); + @*/ + public void increment() { + value++; + if (left != null) left.increment(); + if (right != null) right.increment(); + + //@ set t = \dl_Node(left == null ? \dl_Leaf() : left.t, value, right == null ? \dl_Leaf() : right.t); + } +} diff --git a/key.ui/src/test/resources/plugins/javac/Incorrect.java b/key.ui/src/test/resources/plugins/javac/Incorrect.java new file mode 100644 index 00000000000..31187ea8bfe --- /dev/null +++ b/key.ui/src/test/resources/plugins/javac/Incorrect.java @@ -0,0 +1,7 @@ +import universe.qual.*; + +class Client { + void client(@Rep Object t1, @Peer Object t2) { + t1 = t2; + } +} From 5578ea17a8aea621eca273ba9e6f16b12fb40158 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Tue, 3 Feb 2026 15:30:48 +0100 Subject: [PATCH 11/11] fix the java compuler check facade tests --- key.ui/build.gradle | 22 +++++++++++++++++++ .../javac/JavaCompilerCheckFacadeTest.java | 4 ++-- 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 4748da7396c..6e26800c6a0 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -53,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") diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java index 79ad95d8ee4..d3851cd755b 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java @@ -35,13 +35,13 @@ void compile1() throws ExecutionException, InterruptedException { @Test void compileUniverseCorrect() throws ExecutionException, InterruptedException { - Path src = Paths.get("src/test/recources/plugins/javac/Correct.java"); + 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/recources/plugins/javac/Incorrect.java"); + 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); }