From ef77b66780b5b2646f1b099de10d678b74f9b4e1 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 8 Jun 2025 11:52:42 +0200 Subject: [PATCH 01/16] extend the javac extension --- key.ui/build.gradle | 22 ++++- .../javac/JavaCompilerCheckFacade.java | 11 ++- .../key/gui/plugins/javac/JavacExtension.java | 24 ++++- .../key/gui/plugins/javac/JavacSettings.java | 96 +++++++++++++++++++ .../plugins/javac/JavacSettingsProvider.java | 80 ++++++++++++++++ 5 files changed, 229 insertions(+), 4 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 5ec55a4a26b..f5db1e9eb11 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -69,7 +69,27 @@ 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 ", + "--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" + ] } task runWithProfiler(type: 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 01759d83660..d93f294efd8 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 @@ -56,11 +56,13 @@ public class JavaCompilerCheckFacade { * @param classPath the {@link List} of {@link File}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 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, - File bootClassPath, List classPath, File javaPath) { + File bootClassPath, List classPath, File 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 +88,7 @@ public class JavaCompilerCheckFacade { // gather configured bootstrap classpath and regular classpath List options = new ArrayList<>(); + if (bootClassPath != null) { options.add("-Xbootclasspath"); options.add(bootClassPath.getAbsolutePath()); @@ -95,6 +98,12 @@ public class JavaCompilerCheckFacade { options.add( classPath.stream().map(File::getAbsolutePath).collect(Collectors.joining(":"))); } + + if (processors != null && !processors.isEmpty()) { + options.add("-processor"); + options.add(processors.stream().collect(Collectors.joining(","))); + } + ArrayList files = new ArrayList<>(); if (javaPath.isDirectory()) { try (var s = Files.walk(javaPath.toPath())) { 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 c8d62a2e080..38a4937fbd5 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 @@ -5,6 +5,9 @@ import java.awt.*; import java.io.File; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Arrays; import java.util.Collections; import java.util.List; import java.util.TreeSet; @@ -24,6 +27,7 @@ import de.uka.ilkd.key.gui.fonticons.MaterialDesignRegular; import de.uka.ilkd.key.proof.JavaModel; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.gui.settings.SettingsProvider; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -42,7 +46,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. */ @@ -147,6 +151,18 @@ private void loadProof(Proof selectedProof) throws RuntimeException { File bootClassPath = jm.getBootClassPath() != null ? new File(jm.getBootClassPath()) : null; List classpath = jm.getClassPathEntries(); + JavacSettings settings = JavacSettingsProvider.getJavacSettings(); + + List checkers = null; + if (settings.getUseCheckers()) { + if (classpath == null) classpath = new ArrayList<>(); + + classpath.addAll(Arrays.asList(settings.getCheckerPaths().split(System.lineSeparator())) + .stream().map(p -> new File(p)).toList()); + + checkers = Arrays.asList(settings.getCheckers().split(System.lineSeparator())); + } + File javaPath = new File(jm.getModelDir()); lblStatus.setForeground(Color.black); @@ -154,7 +170,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, checkers); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); @@ -227,6 +243,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..a68e6070f4d --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -0,0 +1,96 @@ +/* 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 { + + public static final String CATEGORY = "Type Checking"; + + /** + * Config key for {@link #checkers}. + */ + private static final String KEY_USE_CHECKERS = "useCheckers"; + + /** + * Config key for {@link #checkers}. + */ + private static final String KEY_CHECKERS = "checkers"; + + /** + * Config key for {@link #checkerPaths}. + */ + private static final String KEY_CHECKER_PATHS = "checkerPaths"; + + /** + * The type checkers (processors) to be run. + */ + private final PropertyEntry useCheckers = + createBooleanProperty(KEY_USE_CHECKERS, false); + + /** + * The type checkers (processors) to be run. + */ + private final PropertyEntry checkers = + createStringProperty(KEY_CHECKERS, ""); + + /** + * The paths needed for the checkers (processors). + */ + private final PropertyEntry checkerPaths = + createStringProperty(KEY_CHECKER_PATHS, ""); + + public JavacSettings() { + super(CATEGORY); + } + + /** + * @param useCheckers if the type checkers should be used + */ + public void setUseCheckers(boolean useCheckers) { + this.useCheckers.set(useCheckers); + } + + /** + * @param checkers the type checkers to use + */ + public void setCheckers(String checkers) { + this.checkers.set(checkers); + } + + /** + * @param paths the paths on which the type checkers are + */ + public void setCheckerPaths(String paths) { + this.checkerPaths.set(paths); + } + + /** + * @return true iff the checkers should be used + */ + public boolean getUseCheckers() { + return useCheckers.get(); + } + + /** + * @return all the checkers in a comma separated string + */ + public String getCheckers() { + return checkers.get(); + } + + /** + * @return all checker paths spearated by a colon + */ + public String getCheckerPaths() { + return checkerPaths.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..dffebd2b728 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java @@ -0,0 +1,80 @@ +/* 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; + +/** + * Settings for the javac extension. + * + * @author Daniel Grévent + */ +public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { + /** + * Singleton instance of the slicing settings. + */ + private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); + + private static final String USE_CHECKERS_INFO = "If enabled the type checkers will be run in addition to the default java type checker."; + private static final String CHECKERS_INFO = "The list of type checkers to run in addition to the default Java type checker. Each checkers should be written on a new line."; + private static final String CHECKER_PATHS_INFO = "The list of paths to the type checkers and their dependencies. Each path should be absolute and be written on a new line."; + + private final JCheckBox useCheckers; + private final JTextArea checkers; + private final JTextArea paths; + + /** + * Construct a new settings provider. + */ + public JavacSettingsProvider() { + useCheckers = addCheckBox( + "use checkers", USE_CHECKERS_INFO, false, e -> {}); + checkers = addTextArea("checkers", "", CHECKERS_INFO, e -> {}); + paths = addTextArea("checker paths", "", CHECKER_PATHS_INFO, e -> {}); + + setHeaderText("Javac Options"); + } + + @Override + public String getDescription() { + return "Java Type Checking"; + } + + public static JavacSettings getJavacSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(JAVAC_SETTINGS); + return JAVAC_SETTINGS; + } + + + @Override + public JPanel getPanel(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + useCheckers.setSelected(settings.getUseCheckers()); + checkers.setText(settings.getCheckers()); + paths.setText(settings.getCheckerPaths()); + + return this; + } + + @Override + public void applySettings(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + settings.setUseCheckers(useCheckers.isSelected()); + settings.setCheckers(checkers.getText()); + settings.setCheckerPaths(paths.getText()); + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} From 2a5ca567df5feed6878be6204cbf29f77962461c Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 17 Nov 2025 19:20:42 +0100 Subject: [PATCH 02/16] updated the code and text to be clearer --- .../key/gui/plugins/javac/JavacExtension.java | 10 +-- .../key/gui/plugins/javac/JavacSettings.java | 66 +++++++++---------- .../plugins/javac/JavacSettingsProvider.java | 59 ++++++++++++----- 3 files changed, 80 insertions(+), 55 deletions(-) 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 38a4937fbd5..a98db9c985e 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 @@ -153,14 +153,14 @@ private void loadProof(Proof selectedProof) throws RuntimeException { List classpath = jm.getClassPathEntries(); JavacSettings settings = JavacSettingsProvider.getJavacSettings(); - List checkers = null; - if (settings.getUseCheckers()) { + List processors = null; + if (settings.getUseProcessors()) { if (classpath == null) classpath = new ArrayList<>(); - classpath.addAll(Arrays.asList(settings.getCheckerPaths().split(System.lineSeparator())) + classpath.addAll(Arrays.asList(settings.getClassPaths().split(System.lineSeparator())) .stream().map(p -> new File(p)).toList()); - checkers = Arrays.asList(settings.getCheckers().split(System.lineSeparator())); + processors = Arrays.asList(settings.getProcessors().split(System.lineSeparator())); } File javaPath = new File(jm.getModelDir()); @@ -170,7 +170,7 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setIcon(ICON_WAIT.get(16)); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, checkers); + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, processors); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); 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 index a68e6070f4d..96488e6fa38 100644 --- 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 @@ -16,81 +16,81 @@ public class JavacSettings extends AbstractPropertiesSettings { public static final String CATEGORY = "Type Checking"; /** - * Config key for {@link #checkers}. + * Config key for {@link #useProcessors}. */ - private static final String KEY_USE_CHECKERS = "useCheckers"; + private static final String KEY_USE_PROCESSORS = "useProcessors"; /** - * Config key for {@link #checkers}. + * Config key for {@link #processors}. */ - private static final String KEY_CHECKERS = "checkers"; + private static final String KEY_PROCESSORS = "processors"; /** - * Config key for {@link #checkerPaths}. + * Config key for {@link #classPaths}. */ - private static final String KEY_CHECKER_PATHS = "checkerPaths"; + private static final String KEY_CLASS_PATHS = "classPaths"; /** - * The type checkers (processors) to be run. + * The type annotation processors to be run. */ - private final PropertyEntry useCheckers = - createBooleanProperty(KEY_USE_CHECKERS, false); + private final PropertyEntry useProcessors = + createBooleanProperty(KEY_USE_PROCESSORS, false); /** - * The type checkers (processors) to be run. + * The type annotation processors to be run. */ - private final PropertyEntry checkers = - createStringProperty(KEY_CHECKERS, ""); + private final PropertyEntry processors = + createStringProperty(KEY_PROCESSORS, ""); /** - * The paths needed for the checkers (processors). + * Additional class paths, needed for example by annotation processors */ - private final PropertyEntry checkerPaths = - createStringProperty(KEY_CHECKER_PATHS, ""); + private final PropertyEntry classPaths = + createStringProperty(KEY_CLASS_PATHS, ""); public JavacSettings() { super(CATEGORY); } /** - * @param useCheckers if the type checkers should be used + * @param useProcessors if the annotation processors should be run */ - public void setUseCheckers(boolean useCheckers) { - this.useCheckers.set(useCheckers); + public void setUseProcessors(boolean useProcessors) { + this.useProcessors.set(useProcessors); } /** - * @param checkers the type checkers to use + * @param processor the annotation processors to run */ - public void setCheckers(String checkers) { - this.checkers.set(checkers); + public void setProcessors(String processor) { + this.processors.set(processor); } /** - * @param paths the paths on which the type checkers are + * @param paths the additional class paths */ - public void setCheckerPaths(String paths) { - this.checkerPaths.set(paths); + public void setClassPaths(String paths) { + this.classPaths.set(paths); } /** - * @return true iff the checkers should be used + * @return true iff the annotation processors should be used */ - public boolean getUseCheckers() { - return useCheckers.get(); + public boolean getUseProcessors() { + return useProcessors.get(); } /** - * @return all the checkers in a comma separated string + * @return the annotation processors separated by newlines */ - public String getCheckers() { - return checkers.get(); + public String getProcessors() { + return processors.get(); } /** - * @return all checker paths spearated by a colon + * @return the additional class paths separated by newlines */ - public String getCheckerPaths() { - return checkerPaths.get(); + 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 index dffebd2b728..6ad05aba32e 100644 --- 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 @@ -10,6 +10,8 @@ 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. * @@ -17,33 +19,56 @@ */ public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { /** - * Singleton instance of the slicing settings. + * Singleton instance of the javac settings. */ private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); - private static final String USE_CHECKERS_INFO = "If enabled the type checkers will be run in addition to the default java type checker."; - private static final String CHECKERS_INFO = "The list of type checkers to run in addition to the default Java type checker. Each checkers should be written on a new line."; - private static final String CHECKER_PATHS_INFO = "The list of paths to the type checkers and their dependencies. Each path should be absolute and be written on a new line."; + /** + * 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 useCheckers; - private final JTextArea checkers; + private final JCheckBox useProcessors; + private final JTextArea processors; private final JTextArea paths; /** * Construct a new settings provider. */ public JavacSettingsProvider() { - useCheckers = addCheckBox( - "use checkers", USE_CHECKERS_INFO, false, e -> {}); - checkers = addTextArea("checkers", "", CHECKERS_INFO, e -> {}); - paths = addTextArea("checker paths", "", CHECKER_PATHS_INFO, e -> {}); + 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 "Java Type Checking"; + return "Javac Options"; } public static JavacSettings getJavacSettings() { @@ -56,9 +81,9 @@ public static JavacSettings getJavacSettings() { public JPanel getPanel(MainWindow window) { JavacSettings settings = getJavacSettings(); - useCheckers.setSelected(settings.getUseCheckers()); - checkers.setText(settings.getCheckers()); - paths.setText(settings.getCheckerPaths()); + useProcessors.setSelected(settings.getUseProcessors()); + processors.setText(settings.getProcessors()); + paths.setText(settings.getClassPaths()); return this; } @@ -67,9 +92,9 @@ public JPanel getPanel(MainWindow window) { public void applySettings(MainWindow window) { JavacSettings settings = getJavacSettings(); - settings.setUseCheckers(useCheckers.isSelected()); - settings.setCheckers(checkers.getText()); - settings.setCheckerPaths(paths.getText()); + settings.setUseProcessors(useProcessors.isSelected()); + settings.setProcessors(processors.getText()); + settings.setClassPaths(paths.getText()); } From 74af1d7a68d15eb278cad28dc7cb1d2c51225750 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Tue, 18 Nov 2025 20:59:07 +0100 Subject: [PATCH 03/16] save proof independent settings, that are not used by the configuration --- .../uka/ilkd/key/settings/Configuration.java | 4 +-- .../settings/ProofIndependentSettings.java | 27 ++++++++++++------- .../key/gui/plugins/javac/JavacExtension.java | 3 +++ .../key/gui/plugins/javac/JavacSettings.java | 5 +++- 4 files changed, 26 insertions(+), 13 deletions(-) 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.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 a98db9c985e..480eb2e2c8f 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 @@ -178,6 +178,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); } } 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 index 96488e6fa38..95827169cba 100644 --- 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 @@ -13,7 +13,10 @@ */ public class JavacSettings extends AbstractPropertiesSettings { - public static final String CATEGORY = "Type Checking"; + /** + * The name of the category in the settings. + */ + public static final String CATEGORY = "Javac Extension"; /** * Config key for {@link #useProcessors}. From 0ae4244a00008863c8b28639b1b464b4c1151450 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 24 Nov 2025 16:37:42 +0100 Subject: [PATCH 04/16] few changes --- key.ui/build.gradle | 5 ++++- .../de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/key.ui/build.gradle b/key.ui/build.gradle index f5db1e9eb11..6c0f5f87cac 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -69,8 +69,11 @@ 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 " + + // this is needed to be able to load checker framework checkers in the javac + // extension jvmArgs += [ - "-Dsun.awt.disablegrab=true ", "--add-exports", "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", "--add-exports", 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 480eb2e2c8f..c66567ec51d 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 @@ -33,7 +33,7 @@ import org.slf4j.LoggerFactory; /** - * 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. * From 0f710eb359420d65fe7307b45f8b59893e8a870c Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 24 Nov 2025 17:08:46 +0100 Subject: [PATCH 05/16] fix mistakes introduced by the merge --- .../uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java | 2 +- .../java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) 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 cccfd859de0..15a19f60fc9 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 @@ -61,7 +61,7 @@ public class JavaCompilerCheckFacade { */ 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"); 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 ede47a3bce8..a36732b5390 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 @@ -6,6 +6,7 @@ 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; From db0c5b02f883799fc4f874cde284c8b13ad8f3f5 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 9 Aug 2025 22:46:39 +0200 Subject: [PATCH 06/16] 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 07/16] 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 08/16] 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 09/16] 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 10/16] 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 11/16] 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 12/16] 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 13/16] 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 14/16] 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 15/16] 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 16/16] 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); }