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/build.gradle b/build.gradle index d7745aa8613..c3c929e7e56 100644 --- a/build.gradle +++ b/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" diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1b..b6dbb981ecd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 0646074f4af..12b64dadf06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -53,8 +53,8 @@ public class ProofIndependentSettings { private final List 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()) { 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..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 @@ -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 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..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 @@ -6,5 +6,4 @@ public interface Annotation { - public java.lang.Class annotationType(); } 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.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) }; diff --git a/key.ui/build.gradle b/key.ui/build.gradle index fc29de9bcee..6e26800c6a0 100644 --- a/key.ui/build.gradle +++ b/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) { 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 a2cc0f81440..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 @@ -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 @@ -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> check( ProblemInitializer.ProblemInitializerListener listener, - Path bootClassPath, List classPath, Path javaPath) { + Path bootClassPath, List classPath, Path javaPath, + List 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 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 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(); 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 009a53a28de..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 @@ -4,7 +4,11 @@ package de.uka.ilkd.key.gui.plugins.javac; import java.awt.*; + import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.List; import java.util.TreeSet; @@ -25,12 +29,16 @@ import de.uka.ilkd.key.proof.JavaModel; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.gui.settings.SettingsProvider; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.util.stream.Collectors; +import java.util.Objects; + /** - * Extensions provides Javac checks for recent-loaded Java files. + * Extension provides Javac checks for recent-loaded Java files. *

* Provides an entry in the status line for access. * @@ -43,7 +51,7 @@ experimental = false) public class JavacExtension implements KeYGuiExtension, KeYGuiExtension.StatusLine, KeYGuiExtension.Startup, - KeYSelectionListener { + KeYSelectionListener, KeYGuiExtension.Settings { /** * Color used for the label if javac didn't produce any diagnostics. */ @@ -145,8 +153,23 @@ 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(); + + List processors = null; + if (settings.getUseProcessors()) { + if (classpath == null) classpath = new ArrayList<>(); + + 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())); + } + Path javaPath = jm.getModelDir(); lblStatus.setForeground(Color.black); @@ -154,7 +177,7 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setIcon(ICON_WAIT.get(16)); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath); + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, processors); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); @@ -162,6 +185,9 @@ private void loadProof(Proof selectedProof) throws RuntimeException { updateLabel(data); })).get(); } catch (InterruptedException | ExecutionException ex) { + lblStatus.setForeground(COLOR_ERROR.get()); + lblStatus.setIcon(ICON_ERROR.get(16)); + lblStatus.setText("Javac error"); throw new RuntimeException(ex); } } @@ -227,6 +253,10 @@ public void selectedNodeChanged(KeYSelectionEvent e) { public void selectedProofChanged(KeYSelectionEvent e) { loadProof(e.getSource().getSelectedProof()); } + + public SettingsProvider getSettings() { + return new JavacSettingsProvider(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java new file mode 100644 index 00000000000..95827169cba --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -0,0 +1,99 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.javac; +import java.lang.Boolean; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + +/** + * Settings for the javac extention. + * + * @author Daniel Grévent + */ +public class JavacSettings extends AbstractPropertiesSettings { + + /** + * The name of the category in the settings. + */ + public static final String CATEGORY = "Javac Extension"; + + /** + * Config key for {@link #useProcessors}. + */ + private static final String KEY_USE_PROCESSORS = "useProcessors"; + + /** + * Config key for {@link #processors}. + */ + private static final String KEY_PROCESSORS = "processors"; + + /** + * Config key for {@link #classPaths}. + */ + private static final String KEY_CLASS_PATHS = "classPaths"; + + /** + * The type annotation processors to be run. + */ + private final PropertyEntry useProcessors = + createBooleanProperty(KEY_USE_PROCESSORS, false); + + /** + * The type annotation processors to be run. + */ + private final PropertyEntry processors = + createStringProperty(KEY_PROCESSORS, ""); + + /** + * Additional class paths, needed for example by annotation processors + */ + private final PropertyEntry classPaths = + createStringProperty(KEY_CLASS_PATHS, ""); + + public JavacSettings() { + super(CATEGORY); + } + + /** + * @param useProcessors if the annotation processors should be run + */ + public void setUseProcessors(boolean useProcessors) { + this.useProcessors.set(useProcessors); + } + + /** + * @param processor the annotation processors to run + */ + public void setProcessors(String processor) { + this.processors.set(processor); + } + + /** + * @param paths the additional class paths + */ + public void setClassPaths(String paths) { + this.classPaths.set(paths); + } + + /** + * @return true iff the annotation processors should be used + */ + public boolean getUseProcessors() { + return useProcessors.get(); + } + + /** + * @return the annotation processors separated by newlines + */ + public String getProcessors() { + return processors.get(); + } + + /** + * @return the additional class paths separated by newlines + */ + public String getClassPaths() { + return classPaths.get(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java new file mode 100644 index 00000000000..6ad05aba32e --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java @@ -0,0 +1,105 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.javac; + +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.settings.SettingsPanel; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +import net.miginfocom.layout.CC; + +/** + * Settings for the javac extension. + * + * @author Daniel Grévent + */ +public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { + /** + * Singleton instance of the javac settings. + */ + private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); + + /** + * Text for the explanaition. + */ + private static final String INTRO_LABEL = "This allows to run the Java compiler when loading java files with additional processes such as Nulness or Ownership checkers."; + + /** + * Information message for the {@link #useProcessors} checkbox. + */ + private static final String USE_PROCESSORS_INFO = + "If enabled the annotation processors will be run with the java compiler while performing type checking of newly loaded sources."; + + /** + * Information message for the {@link #processors} text area. + */ + private static final String PROCESSORS_INFO = """ + A list of annotation processors to run while type checking with the java compiler. + Each checkers should be written on a new line."""; + + /** + * Information message for the {@link #paths} text area. + */ + private static final String CLASS_PATHS_INFO = """ + A list of additional class paths to be used by the java compiler while type checking. + These could for example be needed for certain annotation processors. + Each path should be absolute and be written on a new line."""; + + private final JCheckBox useProcessors; + private final JTextArea processors; + private final JTextArea paths; + + /** + * Construct a new settings provider. + */ + public JavacSettingsProvider() { + pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); + useProcessors = addCheckBox( + "Enable Annotation Processing", USE_PROCESSORS_INFO, false, e -> {}); + processors = addTextArea("Annotation Processors", "", PROCESSORS_INFO, e -> {}); + paths = addTextArea("Class Paths", "", CLASS_PATHS_INFO, e -> {}); + + setHeaderText("Javac Options"); + } + + @Override + public String getDescription() { + return "Javac Options"; + } + + public static JavacSettings getJavacSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(JAVAC_SETTINGS); + return JAVAC_SETTINGS; + } + + + @Override + public JPanel getPanel(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + useProcessors.setSelected(settings.getUseProcessors()); + processors.setText(settings.getProcessors()); + paths.setText(settings.getClassPaths()); + + return this; + } + + @Override + public void applySettings(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + settings.setUseProcessors(useProcessors.isSelected()); + settings.setProcessors(processors.getText()); + settings.setClassPaths(paths.getText()); + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} 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..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 @@ -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/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 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; + } +} diff --git a/keyext.isabelletranslation/build.gradle b/keyext.isabelletranslation/build.gradle index e2119425bdb..0a75bb1bb8b 100644 --- a/keyext.isabelletranslation/build.gradle +++ b/keyext.isabelletranslation/build.gradle @@ -14,4 +14,4 @@ dependencies { */ configurations.configureEach { exclude group: 'org.slf4j', module: 'slf4j-simple' -} \ No newline at end of file +}