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 d84fb9f3c76f404863fdc61e800747dc62915013 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 6 Dec 2025 18:31:19 +0100 Subject: [PATCH 06/16] Revert "save proof independent settings, that are not used by the configuration" This reverts commit 74af1d7a68d15eb278cad28dc7cb1d2c51225750. --- .../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, 13 insertions(+), 26 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 b6dbb981ecd..8efef1a3e1b 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 12b64dadf06..0646074f4af 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 lastReadProperties; - private Configuration lastReadConfiguration; + private Properties lastReadedProperties; + private Configuration lastReadedConfiguration; 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 (lastReadProperties != null) { - settings.readSettings(lastReadProperties); + if (lastReadedProperties != null) { + settings.readSettings(lastReadedProperties); } - if (lastReadConfiguration != null) { - settings.readSettings(lastReadConfiguration); + if (lastReadedConfiguration != null) { + settings.readSettings(lastReadedConfiguration); } } } @@ -106,22 +106,19 @@ private void load(File file) throws IOException { for (Settings settings : settings) { settings.readSettings(properties); } - lastReadProperties = properties; + lastReadedProperties = properties; } } else { - this.lastReadConfiguration = Configuration.load(file); + this.lastReadedConfiguration = Configuration.load(file); for (Settings settings : settings) { - settings.readSettings(lastReadConfiguration); + settings.readSettings(lastReadedConfiguration); } } } public void saveSettings() { if (!filename.getName().endsWith(".json")) { - Properties result = lastReadProperties == null - ? new Properties() - : new Properties(lastReadProperties); - + Properties result = new Properties(); for (Settings settings : settings) { settings.writeSettings(result); } @@ -138,10 +135,6 @@ 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 a36732b5390..6dbe5220512 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 @@ -179,9 +179,6 @@ 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 95827169cba..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 @@ -13,10 +13,7 @@ */ public class JavacSettings extends AbstractPropertiesSettings { - /** - * The name of the category in the settings. - */ - public static final String CATEGORY = "Javac Extension"; + public static final String CATEGORY = "Type Checking"; /** * Config key for {@link #useProcessors}. From 7ca22418fc511ee6d7c7c90d513ce26cf77229ea Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 6 Dec 2025 18:34:28 +0100 Subject: [PATCH 07/16] un-revert the name of the Javac Settings --- .../de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 ba35a995a0f8b7247d9a71f92f5906fe45bab778 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 19 Jan 2026 13:53:56 +0100 Subject: [PATCH 08/16] update the javaCompilerCheckFacade interface and fix tests --- .gitignore | 1 + .../javac/JavaCompilerCheckFacade.java | 32 +++++++++++++++---- .../key/gui/plugins/javac/JavacExtension.java | 21 +++--------- .../key/gui/plugins/javac/JavacSettings.java | 7 ++-- .../plugins/javac/JavacSettingsProvider.java | 26 ++++++++------- .../javac/JavaCompilerCheckFacadeTest.java | 2 +- 6 files changed, 50 insertions(+), 39 deletions(-) diff --git a/.gitignore b/.gitignore index 894015b1c6c..05e1ef6c942 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/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..3fd0127f2b5 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 @@ -12,6 +12,7 @@ import java.nio.charset.Charset; import java.nio.file.Files; import java.nio.file.Path; +import java.nio.file.Paths; import java.util.*; import java.util.concurrent.CompletableFuture; import java.util.stream.Collectors; @@ -56,13 +57,14 @@ public class JavaCompilerCheckFacade { * @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 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 + * @param settings the {@link JavacSettings} that describe what other options the compiler + * should be called with * @return future providing the list of diagnostics */ public static @NonNull CompletableFuture> check( ProblemInitializer.ProblemInitializerListener listener, Path bootClassPath, List classPath, Path javaPath, - List processors) { + JavacSettings settings) { if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) { LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); return CompletableFuture.completedFuture(Collections.emptyList()); @@ -89,10 +91,32 @@ public class JavaCompilerCheckFacade { // gather configured bootstrap classpath and regular classpath List options = new ArrayList<>(); + if (settings.getUseProcessors()) { + + String newlineClassPath = settings.getClassPaths(); + if (!newlineClassPath.isEmpty()) { + List processorClassPath = + Arrays.asList(newlineClassPath.split(System.lineSeparator())) + .stream().map(p -> Paths.get(p)).toList(); + + classPath = new ArrayList<>(classPath); + classPath.addAll(processorClassPath); + } + + List processors = Arrays.asList(settings.getProcessors() + .split(System.lineSeparator())); + + if (!processors.isEmpty()) { + options.add("-processor"); + options.add(processors.stream().collect(Collectors.joining(","))); + } + } + if (bootClassPath != null) { options.add("-Xbootclasspath"); options.add(bootClassPath.toAbsolutePath().toString()); } + if (classPath != null && !classPath.isEmpty()) { options.add("-classpath"); options.add( @@ -101,10 +125,6 @@ public class JavaCompilerCheckFacade { .collect(Collectors.joining(":"))); } - if (processors != null && !processors.isEmpty()) { - options.add("-processor"); - options.add(processors.stream().collect(Collectors.joining(","))); - } ArrayList files = new ArrayList<>(); if (Files.isDirectory(javaPath)) { 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 6dbe5220512..588d89c80ce 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,11 +4,7 @@ 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; @@ -26,10 +22,10 @@ import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.fonticons.IconFontProvider; import de.uka.ilkd.key.gui.fonticons.MaterialDesignRegular; +import de.uka.ilkd.key.gui.settings.SettingsProvider; 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; @@ -152,17 +148,6 @@ private void loadProof(Proof selectedProof) throws RuntimeException { Path bootClassPath = jm.getBootClassPath() != null ? jm.getBootClassPath() : null; List classpath = jm.getClassPath(); - JavacSettings settings = JavacSettingsProvider.getJavacSettings(); - - List processors = null; - if (settings.getUseProcessors()) { - if (classpath == null) classpath = new ArrayList<>(); - - classpath.addAll(Arrays.asList(settings.getClassPaths().split(System.lineSeparator())) - .stream().map(p -> Paths.get(p)).toList()); - - processors = Arrays.asList(settings.getProcessors().split(System.lineSeparator())); - } Path javaPath = jm.getModelDir(); @@ -170,8 +155,10 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setText("Javac runs"); lblStatus.setIcon(ICON_WAIT.get(16)); + JavacSettings settings = JavacSettingsProvider.getJavacSettings(); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, processors); + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, + settings); 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 95827169cba..09c42adc887 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 @@ -2,7 +2,6 @@ * 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; @@ -36,19 +35,19 @@ public class JavacSettings extends AbstractPropertiesSettings { /** * The type annotation processors to be run. */ - private final PropertyEntry useProcessors = + private final PropertyEntry useProcessors = createBooleanProperty(KEY_USE_PROCESSORS, false); /** * The type annotation processors to be run. */ - private final PropertyEntry processors = + private final PropertyEntry processors = createStringProperty(KEY_PROCESSORS, ""); /** * Additional class paths, needed for example by annotation processors */ - private final PropertyEntry classPaths = + private final PropertyEntry classPaths = createStringProperty(KEY_CLASS_PATHS, ""); public JavacSettings() { 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 6ad05aba32e..15b1f5e6a51 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 @@ -26,28 +26,29 @@ public class JavacSettingsProvider extends SettingsPanel implements SettingsProv /** * 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."; + 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 = + 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."""; + 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."""; + 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; @@ -59,9 +60,12 @@ public class JavacSettingsProvider extends SettingsPanel implements SettingsProv 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 -> {}); + "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"); } @@ -76,7 +80,7 @@ public static JavacSettings getJavacSettings() { return JAVAC_SETTINGS; } - + @Override public JPanel getPanel(MainWindow window) { JavacSettings settings = getJavacSettings(); 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..77a5d4253d3 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 @@ -48,7 +48,7 @@ public void reportException(Object sender, ProofOblInput input, Exception e) {} }; var promise = JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), - src.toPath()); + src.toPath(), new JavacSettings()); promise.get(); } From 7a1658c7db0a77fa4433822ae42201f09981f481 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 26 Jan 2026 14:35:31 +0100 Subject: [PATCH 09/16] change the help messages in the settings provider --- .../uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 15b1f5e6a51..b1d21a52b4f 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 @@ -27,7 +27,7 @@ public class JavacSettingsProvider extends SettingsPanel implements SettingsProv * 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."; + "This allows to run the Java compiler when loading java files with additional processes such as Nullness or Ownership checkers."; /** * Information message for the {@link #useProcessors} checkbox. @@ -64,7 +64,7 @@ public JavacSettingsProvider() { }); processors = addTextArea("Annotation Processors", "", PROCESSORS_INFO, e -> { }); - paths = addTextArea("Class Paths", "", CLASS_PATHS_INFO, e -> { + paths = addTextArea("Processor Class Paths", "", CLASS_PATHS_INFO, e -> { }); setHeaderText("Javac Options"); From 4c5f41e1e92cd6add135e9e311072bd9bedaec38 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Fri, 30 Jan 2026 12:30:09 +0100 Subject: [PATCH 10/16] make compiler errors acessible from the gui --- .../javac/JavaCompilerCheckFacade.java | 24 ++++++++++++------- .../plugins/javac/JavacSettingsProvider.java | 8 +++---- 2 files changed, 20 insertions(+), 12 deletions(-) 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 3fd0127f2b5..7fce4d69fbe 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 @@ -94,17 +94,23 @@ public class JavaCompilerCheckFacade { if (settings.getUseProcessors()) { String newlineClassPath = settings.getClassPaths(); - if (!newlineClassPath.isEmpty()) { - List processorClassPath = - Arrays.asList(newlineClassPath.split(System.lineSeparator())) - .stream().map(p -> Paths.get(p)).toList(); - + List processorClassPath = + Arrays.asList(newlineClassPath.split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .map(Paths::get) + .toList(); + + if (!processorClassPath.isEmpty()) { classPath = new ArrayList<>(classPath); classPath.addAll(processorClassPath); } - List processors = Arrays.asList(settings.getProcessors() - .split(System.lineSeparator())); + List processors = + Arrays.asList(settings.getProcessors().split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .toList(); if (!processors.isEmpty()) { options.add("-processor"); @@ -156,7 +162,9 @@ public class JavaCompilerCheckFacade { it -> new PositionedIssueString( it.getMessage(Locale.ENGLISH), new Location( - fileManager.asPath(it.getSource()).toFile().toPath().toUri(), + it.getSource() == null + ? null + : fileManager.asPath(it.getSource()).toFile().toPath().toUri(), it.getPosition() != Diagnostic.NOPOS ? Position.newOneBased((int) it.getLineNumber(), (int) it.getColumnNumber()) 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 b1d21a52b4f..d1fe5b77dd6 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 @@ -27,26 +27,26 @@ public class JavacSettingsProvider extends SettingsPanel implements SettingsProv * 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 Nullness or Ownership checkers."; + "This allows to run the Java compiler when loading Java files with additional processes such as Nullness 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."; + "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. + 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. + 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."""; From 0f42201da88e110e26b4a695f624132c71e123cd Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 8 Feb 2026 01:26:42 +0100 Subject: [PATCH 11/16] wip: Javac in separate process Externalize Javac into separate Java process for setting JMS directives --- .../uka/ilkd/key/settings/Configuration.java | 4 + key.ui/build.gradle | 23 -- .../javac/JavaCompilerCheckFacade.java | 220 ++++++++++++++---- .../key/gui/plugins/javac/JavacExtension.java | 3 +- .../key/gui/plugins/javac/JavacSettings.java | 4 +- .../javac/JavaCompilerCheckFacadeTest.java | 86 +++++-- 6 files changed, 252 insertions(+), 88 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..79463f7978f 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 @@ -466,6 +466,10 @@ public ConfigurationWriter printIndent() { } public ConfigurationWriter printComment(String comment) { + if (comment == null) { + return this; + } + if (comment.contains("\n")) { out.format("/* %s */\n", comment); } else { diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 5b94221ae2a..0bd1325fc2a 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -81,29 +81,6 @@ 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 += [ - "--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 7fce4d69fbe..9ed84e88a0a 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 @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.plugins.javac; -import java.io.File; -import java.io.IOException; -import java.io.OutputStream; -import java.io.StringWriter; +import java.io.*; import java.net.URI; import java.net.URISyntaxException; import java.nio.charset.Charset; @@ -15,14 +12,25 @@ import java.nio.file.Paths; import java.util.*; import java.util.concurrent.CompletableFuture; +import java.util.concurrent.ExecutionException; import java.util.stream.Collectors; import javax.tools.*; +import com.formdev.flatlaf.json.Json; import de.uka.ilkd.key.gui.PositionedIssueString; import de.uka.ilkd.key.java.Position; +import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.parser.Location; +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.settings.Configuration; +import org.antlr.v4.runtime.CharStream; +import org.antlr.v4.runtime.CharStreams; +import org.checkerframework.checker.units.qual.C; +import org.key_project.util.Streams; + import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -44,21 +52,145 @@ * @version 1 (14.10.22) */ public class JavaCompilerCheckFacade { + private JavaCompilerCheckFacade() { + /* This utility class should not be instantiated */ + } + private static final Logger LOGGER = LoggerFactory.getLogger(JavaCompilerCheckFacade.class); + + public static void main(String[] args) { + try (var input = new InputStreamReader(System.in)) { + var params = ParsingFacade.readConfigurationFile(CharStreams.fromReader(input)); + + var settings = new JavacSettings(); + settings.readSettings(params); + + var result = check(new ProblemInitializer.ProblemInitializerListener() { + @Override + public void proofCreated(ProblemInitializer sender, ProofAggregate proofAggregate) { + + } + + @Override + public void progressStarted(Object sender) { + + } + + @Override + public void progressStopped(Object sender) { + + } + + @Override + public void reportStatus(Object sender, String status, int progress) { + LOGGER.info(status); + } + + @Override + public void reportStatus(Object sender, String status) { + LOGGER.info(status); + } + + @Override + public void resetStatus(Object sender) { + + } + + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + + } + }, + Paths.get(params.getString("bootClassPath")), + params.getStringList("classPath").stream().map(Paths::get).toList(), + Paths.get(params.getString("javaPath")), settings).get(); + + var out = new Configuration(); + out.set("messages", + result.stream().map(it -> + { + return Map.of("message", it.text, + "kind", it.getKind().toString(), + "line", it.location.getPosition().line(), + "fileUri", it.location.fileUri().toString(), + "column", it.location.getPosition().column() + ); + } + + ).toList() + ); + out.save(new OutputStreamWriter(System.err), null); + } catch (Exception e) { + LOGGER.error("Error during execution.", e); + } + } + + public static @NonNull CompletableFuture> checkExternally( + ProblemInitializer.ProblemInitializerListener listener, + Path bootClassPath, List classPath, Path javaPath, + JavacSettings settings) { + if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) { + LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); + return CompletableFuture.completedFuture(Collections.emptyList()); + } + + var params = new Configuration(); + params.set("bootClassPath", Objects.toString(bootClassPath)); + params.set("classPath", classPath.stream().map(Path::toAbsolutePath).map(Path::toString).toList()); + params.set("javaPath", Objects.toString(javaPath)); + settings.writeSettings(params); + + String classpath = System.getProperty("java.class.path"); + String path = Paths.get(System.getProperty("java.home"), "bin", "java").toAbsolutePath().toString(); + ProcessBuilder processBuilder = + new ProcessBuilder(path, + "--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", + "-cp", + classpath, + JavaCompilerCheckFacade.class.getCanonicalName()); + return CompletableFuture.supplyAsync(() -> { + try { + var process = processBuilder.start(); + params.save(process.outputWriter(), null); + process.outputWriter().close(); + + + List strings; + var cfg = ParsingFacade.parseConfigurationFile(CharStreams.fromStream(process.getErrorStream())); + var errors = Streams.toString(process.getInputStream()); + process.waitFor(); + + // TODO weigl, transform Configuration back to PositionedIssueString + return List.of(); + } catch (IOException | InterruptedException e) { + throw new RuntimeException(e); + } + }); + } + + /** * initiates the compilation check on the target Java source (the Java program to be verified) * and * reports any issues to the provided listener * - * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed - * about any issues found in the target Java program + * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed + * about any issues found in the target Java program * @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 Path} to the source of the target Java program - * @param settings the {@link JavacSettings} that describe what other options the compiler - * should be called with + * @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 Path} to the source of the target Java program + * @param settings the {@link JavacSettings} that describe what other options the compiler + * should be called with * @return future providing the list of diagnostics */ public static @NonNull CompletableFuture> check( @@ -81,9 +213,9 @@ public class JavaCompilerCheckFacade { } JavaFileManagerDelegate fileManager = - new JavaFileManagerDelegate( - compiler.getStandardFileManager( - diagnostics, Locale.ENGLISH, Charset.defaultCharset())); + new JavaFileManagerDelegate( + compiler.getStandardFileManager( + diagnostics, Locale.ENGLISH, Charset.defaultCharset())); StringWriter output = new StringWriter(); List classes = new ArrayList<>(); @@ -95,11 +227,11 @@ public class JavaCompilerCheckFacade { String newlineClassPath = settings.getClassPaths(); List processorClassPath = - Arrays.asList(newlineClassPath.split(System.lineSeparator())) - .stream() - .filter(s -> !s.isBlank()) - .map(Paths::get) - .toList(); + Arrays.asList(newlineClassPath.split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .map(Paths::get) + .toList(); if (!processorClassPath.isEmpty()) { classPath = new ArrayList<>(classPath); @@ -107,10 +239,10 @@ public class JavaCompilerCheckFacade { } List processors = - Arrays.asList(settings.getProcessors().split(System.lineSeparator())) - .stream() - .filter(s -> !s.isBlank()) - .toList(); + Arrays.asList(settings.getProcessors().split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .toList(); if (!processors.isEmpty()) { options.add("-processor"); @@ -126,9 +258,9 @@ public class JavaCompilerCheckFacade { if (classPath != null && !classPath.isEmpty()) { options.add("-classpath"); options.add( - classPath.stream().map(Path::toAbsolutePath) - .map(Objects::toString) - .collect(Collectors.joining(":"))); + classPath.stream().map(Path::toAbsolutePath) + .map(Objects::toString) + .collect(Collectors.joining(":"))); } @@ -146,10 +278,10 @@ public class JavaCompilerCheckFacade { } Iterable compilationUnits = - fileManager.getJavaFileObjects(files.toArray(new Path[0])); + fileManager.getJavaFileObjects(files.toArray(new Path[0])); JavaCompiler.CompilationTask task = compiler.getTask(output, fileManager, diagnostics, - options, classes, compilationUnits); + options, classes, compilationUnits); return CompletableFuture.supplyAsync(() -> { long start = System.currentTimeMillis(); @@ -159,17 +291,17 @@ public class JavaCompilerCheckFacade { LOGGER.info("{}", diagnostic); } return diagnostics.getDiagnostics().stream().map( - it -> new PositionedIssueString( - it.getMessage(Locale.ENGLISH), - new Location( - it.getSource() == null - ? null - : fileManager.asPath(it.getSource()).toFile().toPath().toUri(), - it.getPosition() != Diagnostic.NOPOS - ? Position.newOneBased((int) it.getLineNumber(), - (int) it.getColumnNumber()) - : Position.UNDEFINED), - it.getCode() + " " + it.getKind())) + it -> new PositionedIssueString( + it.getMessage(Locale.ENGLISH), + new Location( + it.getSource() == null + ? null + : fileManager.asPath(it.getSource()).toFile().toPath().toUri(), + it.getPosition() != Diagnostic.NOPOS + ? Position.newOneBased((int) it.getLineNumber(), + (int) it.getColumnNumber()) + : Position.UNDEFINED), + it.getCode() + " " + it.getKind())) .collect(Collectors.toList()); }); } @@ -251,7 +383,7 @@ public void setLocationFromPaths(Location location, Collection p @Override public void setLocationForModule(Location location, String moduleName, - Collection paths) throws IOException { + Collection paths) throws IOException { fileManager.setLocationForModule(location, moduleName, paths); } @@ -282,7 +414,7 @@ public ClassLoader getClassLoader(Location location) { @Override public Iterable list(Location location, String packageName, - Set kinds, boolean recurse) throws IOException { + Set kinds, boolean recurse) throws IOException { return fileManager.list(location, packageName, kinds, recurse); } @@ -303,13 +435,13 @@ public boolean hasLocation(Location location) { @Override public JavaFileObject getJavaFileForInput(Location location, String className, - JavaFileObject.Kind kind) throws IOException { + JavaFileObject.Kind kind) throws IOException { return fileManager.getJavaFileForInput(location, className, kind); } @Override public JavaFileObject getJavaFileForOutput(Location location, String className, - JavaFileObject.Kind kind, FileObject sibling) throws IOException { + JavaFileObject.Kind kind, FileObject sibling) throws IOException { if (kind == JavaFileObject.Kind.CLASS && location == StandardLocation.CLASS_OUTPUT) { // do not save compiled .class files on disk try { @@ -330,7 +462,7 @@ public FileObject getFileForInput(Location location, String packageName, String @Override public FileObject getFileForOutput(Location location, String packageName, String relativeName, - FileObject sibling) throws IOException { + FileObject sibling) throws IOException { return fileManager.getFileForOutput(location, packageName, relativeName, sibling); } 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 588d89c80ce..ae3e4364835 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 @@ -157,7 +157,8 @@ private void loadProof(Proof selectedProof) throws RuntimeException { JavacSettings settings = JavacSettingsProvider.getJavacSettings(); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, + JavaCompilerCheckFacade.checkExternally(mediator.getUI(), bootClassPath, classpath, + javaPath, settings); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { 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 09c42adc887..ad10348691e 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 @@ -5,12 +5,14 @@ import de.uka.ilkd.key.settings.AbstractPropertiesSettings; +import java.io.Serializable; + /** * Settings for the javac extention. * * @author Daniel Grévent */ -public class JavacSettings extends AbstractPropertiesSettings { +public class JavacSettings extends AbstractPropertiesSettings implements Serializable { /** * The name of the category in the settings. 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 77a5d4253d3..d3e43e68337 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 @@ -23,32 +23,80 @@ void compile1() throws ExecutionException, InterruptedException { File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile(); System.out.println(src); ProblemInitializer.ProblemInitializerListener emptyListener = - new ProblemInitializer.ProblemInitializerListener() { - @Override - public void proofCreated(ProblemInitializer sender, - ProofAggregate proofAggregate) {} + new ProblemInitializer.ProblemInitializerListener() { + @Override + public void proofCreated(ProblemInitializer sender, + ProofAggregate proofAggregate) { + } - @Override - public void progressStarted(Object sender) {} + @Override + public void progressStarted(Object sender) { + } - @Override - public void progressStopped(Object sender) {} + @Override + public void progressStopped(Object sender) { + } - @Override - public void reportStatus(Object sender, String status, int progress) {} + @Override + public void reportStatus(Object sender, String status, int progress) { + } - @Override - public void reportStatus(Object sender, String status) {} + @Override + public void reportStatus(Object sender, String status) { + } - @Override - public void resetStatus(Object sender) {} + @Override + public void resetStatus(Object sender) { + } - @Override - public void reportException(Object sender, ProofOblInput input, Exception e) {} - }; + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + } + }; var promise = - JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), - src.toPath(), new JavacSettings()); + JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), + src.toPath(), new JavacSettings()); + promise.get(); + } + + @Test + void compileExternal() throws ExecutionException, InterruptedException { + File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile(); + System.out.println(src); + ProblemInitializer.ProblemInitializerListener emptyListener = + new ProblemInitializer.ProblemInitializerListener() { + @Override + public void proofCreated(ProblemInitializer sender, + ProofAggregate proofAggregate) { + } + + @Override + public void progressStarted(Object sender) { + } + + @Override + public void progressStopped(Object sender) { + } + + @Override + public void reportStatus(Object sender, String status, int progress) { + } + + @Override + public void reportStatus(Object sender, String status) { + } + + @Override + public void resetStatus(Object sender) { + } + + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + } + }; + var promise = + JavaCompilerCheckFacade.checkExternally(emptyListener, null, Collections.emptyList(), + src.toPath(), new JavacSettings()); promise.get(); } From 622a300954615487019956664f1f4b9688cb324a Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 22 Feb 2026 19:33:02 +0100 Subject: [PATCH 12/16] finish implementing the external java checks --- .../javac/JavaCompilerCheckFacade.java | 238 ++++++++---------- .../key/gui/plugins/javac/JavacExtension.java | 11 +- .../key/gui/plugins/javac/JavacSettings.java | 4 +- .../javac/JavaCompilerCheckFacadeTest.java | 128 +++++----- 4 files changed, 180 insertions(+), 201 deletions(-) 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 9ed84e88a0a..bc2f403d82b 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 @@ -12,25 +12,18 @@ import java.nio.file.Paths; import java.util.*; import java.util.concurrent.CompletableFuture; -import java.util.concurrent.ExecutionException; import java.util.stream.Collectors; import javax.tools.*; -import com.formdev.flatlaf.json.Json; import de.uka.ilkd.key.gui.PositionedIssueString; import de.uka.ilkd.key.java.Position; -import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.parser.Location; -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.settings.Configuration; -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.checkerframework.checker.units.qual.C; + import org.key_project.util.Streams; +import org.antlr.v4.runtime.CharStreams; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -58,69 +51,37 @@ private JavaCompilerCheckFacade() { private static final Logger LOGGER = LoggerFactory.getLogger(JavaCompilerCheckFacade.class); - public static void main(String[] args) { try (var input = new InputStreamReader(System.in)) { - var params = ParsingFacade.readConfigurationFile(CharStreams.fromReader(input)); + var params = Configuration.load(CharStreams.fromReader(input)); var settings = new JavacSettings(); settings.readSettings(params); - var result = check(new ProblemInitializer.ProblemInitializerListener() { - @Override - public void proofCreated(ProblemInitializer sender, ProofAggregate proofAggregate) { - - } - - @Override - public void progressStarted(Object sender) { - - } - - @Override - public void progressStopped(Object sender) { - - } - - @Override - public void reportStatus(Object sender, String status, int progress) { - LOGGER.info(status); - } - - @Override - public void reportStatus(Object sender, String status) { - LOGGER.info(status); - } - - @Override - public void resetStatus(Object sender) { - - } - - @Override - public void reportException(Object sender, ProofOblInput input, Exception e) { - - } - }, - Paths.get(params.getString("bootClassPath")), - params.getStringList("classPath").stream().map(Paths::get).toList(), - Paths.get(params.getString("javaPath")), settings).get(); + var result = check(null, + Paths.get(params.getString("bootClassPath")), + params.getStringList("classPath").stream().map(Paths::get).toList(), + Paths.get(params.getString("javaPath")), settings).get(); var out = new Configuration(); out.set("messages", - result.stream().map(it -> - { - return Map.of("message", it.text, - "kind", it.getKind().toString(), - "line", it.location.getPosition().line(), - "fileUri", it.location.fileUri().toString(), - "column", it.location.getPosition().column() - ); - } - - ).toList() - ); - out.save(new OutputStreamWriter(System.err), null); + result.stream().map(it -> { + var map = Map.of( + "message", it.text, + "kind", it.getKind().toString(), + "line", it.location.getPosition().line(), + "column", it.location.getPosition().column(), + "additionalInfo", it.getAdditionalInfo()); + if (it.location.fileUri() != null) { + map = new HashMap<>(map); + map.put("fileUri", it.location.fileUri().toString()); + } + return map; + }).toList()); + + Writer writer = new OutputStreamWriter(System.err); + out.save(writer, null); + writer.close(); } catch (Exception e) { LOGGER.error("Error during execution.", e); } @@ -134,63 +95,78 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); return CompletableFuture.completedFuture(Collections.emptyList()); } - + LOGGER.info("External Javac check is triggered."); var params = new Configuration(); params.set("bootClassPath", Objects.toString(bootClassPath)); - params.set("classPath", classPath.stream().map(Path::toAbsolutePath).map(Path::toString).toList()); + params.set("classPath", + classPath.stream().map(Path::toAbsolutePath).map(Path::toString).toList()); params.set("javaPath", Objects.toString(javaPath)); settings.writeSettings(params); String classpath = System.getProperty("java.class.path"); - String path = Paths.get(System.getProperty("java.home"), "bin", "java").toAbsolutePath().toString(); + String path = + Paths.get(System.getProperty("java.home"), "bin", "java").toAbsolutePath().toString(); ProcessBuilder processBuilder = - new ProcessBuilder(path, - "--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", - "-cp", - classpath, - JavaCompilerCheckFacade.class.getCanonicalName()); + new ProcessBuilder(path, + "--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", + "-cp", + classpath, + JavaCompilerCheckFacade.class.getCanonicalName()); return CompletableFuture.supplyAsync(() -> { try { var process = processBuilder.start(); params.save(process.outputWriter(), null); process.outputWriter().close(); - - List strings; - var cfg = ParsingFacade.parseConfigurationFile(CharStreams.fromStream(process.getErrorStream())); - var errors = Streams.toString(process.getInputStream()); + var errors = Streams.toString(process.getInputStream()); // what should be done with + // the errors ?? + var cfg = Configuration.load(CharStreams.fromStream(process.getErrorStream())); process.waitFor(); - // TODO weigl, transform Configuration back to PositionedIssueString - return List.of(); - } catch (IOException | InterruptedException e) { + return cfg.getList("messages").stream() + .map(msgObj -> { + Configuration msg = (Configuration) msgObj; + return new PositionedIssueString( + msg.getString("message"), + new Location( + msg.exists("fileUri") + ? URI.create(msg.getString("fileUri")) + : null, + msg.getInt("line") == -1 || msg.getInt("column") == -1 + ? Position.UNDEFINED + : Position.newOneBased( + msg.getInt("line"), + msg.getInt("column"))), + msg.getString("additionalInfo"), + PositionedIssueString.Kind.valueOf(msg.getString("kind"))); + }).toList(); + } catch (IOException | InterruptedException e) { throw new RuntimeException(e); } }); } - /** * initiates the compilation check on the target Java source (the Java program to be verified) * and * reports any issues to the provided listener * - * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed - * about any issues found in the target Java program + * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed + * about any issues found in the target Java program * @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 Path} to the source of the target Java program - * @param settings the {@link JavacSettings} that describe what other options the compiler - * should be called with + * @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 Path} to the source of the target Java program + * @param settings the {@link JavacSettings} that describe what other options the compiler + * should be called with * @return future providing the list of diagnostics */ public static @NonNull CompletableFuture> check( @@ -208,14 +184,16 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { if (compiler == null) { LOGGER.info("Javac is not available in current java runtime. Javac check skipped"); - listener.reportStatus(null, "No javac compiler found. Java check disabled."); + if (listener != null) { + listener.reportStatus(null, "No javac compiler found. Java check disabled."); + } return CompletableFuture.completedFuture(Collections.emptyList()); } JavaFileManagerDelegate fileManager = - new JavaFileManagerDelegate( - compiler.getStandardFileManager( - diagnostics, Locale.ENGLISH, Charset.defaultCharset())); + new JavaFileManagerDelegate( + compiler.getStandardFileManager( + diagnostics, Locale.ENGLISH, Charset.defaultCharset())); StringWriter output = new StringWriter(); List classes = new ArrayList<>(); @@ -224,14 +202,13 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { List options = new ArrayList<>(); if (settings.getUseProcessors()) { - String newlineClassPath = settings.getClassPaths(); List processorClassPath = - Arrays.asList(newlineClassPath.split(System.lineSeparator())) - .stream() - .filter(s -> !s.isBlank()) - .map(Paths::get) - .toList(); + Arrays.asList(newlineClassPath.split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .map(Paths::get) + .toList(); if (!processorClassPath.isEmpty()) { classPath = new ArrayList<>(classPath); @@ -239,10 +216,10 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { } List processors = - Arrays.asList(settings.getProcessors().split(System.lineSeparator())) - .stream() - .filter(s -> !s.isBlank()) - .toList(); + Arrays.asList(settings.getProcessors().split(System.lineSeparator())) + .stream() + .filter(s -> !s.isBlank()) + .toList(); if (!processors.isEmpty()) { options.add("-processor"); @@ -251,19 +228,18 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { } if (bootClassPath != null) { - options.add("-Xbootclasspath"); + options.add("-bootclasspath"); options.add(bootClassPath.toAbsolutePath().toString()); } if (classPath != null && !classPath.isEmpty()) { options.add("-classpath"); options.add( - classPath.stream().map(Path::toAbsolutePath) - .map(Objects::toString) - .collect(Collectors.joining(":"))); + classPath.stream().map(Path::toAbsolutePath) + .map(Objects::toString) + .collect(Collectors.joining(":"))); } - ArrayList files = new ArrayList<>(); if (Files.isDirectory(javaPath)) { try (var s = Files.walk(javaPath)) { @@ -278,10 +254,10 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { } Iterable compilationUnits = - fileManager.getJavaFileObjects(files.toArray(new Path[0])); + fileManager.getJavaFileObjects(files.toArray(new Path[0])); JavaCompiler.CompilationTask task = compiler.getTask(output, fileManager, diagnostics, - options, classes, compilationUnits); + options, classes, compilationUnits); return CompletableFuture.supplyAsync(() -> { long start = System.currentTimeMillis(); @@ -291,17 +267,17 @@ public void reportException(Object sender, ProofOblInput input, Exception e) { LOGGER.info("{}", diagnostic); } return diagnostics.getDiagnostics().stream().map( - it -> new PositionedIssueString( - it.getMessage(Locale.ENGLISH), - new Location( - it.getSource() == null - ? null - : fileManager.asPath(it.getSource()).toFile().toPath().toUri(), - it.getPosition() != Diagnostic.NOPOS - ? Position.newOneBased((int) it.getLineNumber(), - (int) it.getColumnNumber()) - : Position.UNDEFINED), - it.getCode() + " " + it.getKind())) + it -> new PositionedIssueString( + it.getMessage(Locale.ENGLISH), + new Location( + it.getSource() == null + ? null + : fileManager.asPath(it.getSource()).toFile().toPath().toUri(), + it.getPosition() != Diagnostic.NOPOS + ? Position.newOneBased((int) it.getLineNumber(), + (int) it.getColumnNumber()) + : Position.UNDEFINED), + it.getCode() + " " + it.getKind())) .collect(Collectors.toList()); }); } @@ -383,7 +359,7 @@ public void setLocationFromPaths(Location location, Collection p @Override public void setLocationForModule(Location location, String moduleName, - Collection paths) throws IOException { + Collection paths) throws IOException { fileManager.setLocationForModule(location, moduleName, paths); } @@ -414,7 +390,7 @@ public ClassLoader getClassLoader(Location location) { @Override public Iterable list(Location location, String packageName, - Set kinds, boolean recurse) throws IOException { + Set kinds, boolean recurse) throws IOException { return fileManager.list(location, packageName, kinds, recurse); } @@ -435,13 +411,13 @@ public boolean hasLocation(Location location) { @Override public JavaFileObject getJavaFileForInput(Location location, String className, - JavaFileObject.Kind kind) throws IOException { + JavaFileObject.Kind kind) throws IOException { return fileManager.getJavaFileForInput(location, className, kind); } @Override public JavaFileObject getJavaFileForOutput(Location location, String className, - JavaFileObject.Kind kind, FileObject sibling) throws IOException { + JavaFileObject.Kind kind, FileObject sibling) throws IOException { if (kind == JavaFileObject.Kind.CLASS && location == StandardLocation.CLASS_OUTPUT) { // do not save compiled .class files on disk try { @@ -462,7 +438,7 @@ public FileObject getFileForInput(Location location, String packageName, String @Override public FileObject getFileForOutput(Location location, String packageName, String relativeName, - FileObject sibling) throws IOException { + FileObject sibling) throws IOException { return fileManager.getFileForOutput(location, packageName, relativeName, sibling); } 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 ae3e4364835..12bb82ad939 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 @@ -156,10 +156,13 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setIcon(ICON_WAIT.get(16)); JavacSettings settings = JavacSettingsProvider.getJavacSettings(); - CompletableFuture> task = - JavaCompilerCheckFacade.checkExternally(mediator.getUI(), bootClassPath, classpath, - javaPath, - settings); + CompletableFuture> task = settings.getUseProcessors() + ? JavaCompilerCheckFacade.checkExternally(mediator.getUI(), bootClassPath, + classpath, + javaPath, + settings) + : JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, + javaPath, settings); 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 ad10348691e..bd3d821a6c1 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 @@ -3,10 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.plugins.javac; -import de.uka.ilkd.key.settings.AbstractPropertiesSettings; - import java.io.Serializable; +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + /** * Settings for the javac extention. * 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 d3e43e68337..00b8eb4f118 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 @@ -23,39 +23,39 @@ void compile1() throws ExecutionException, InterruptedException { File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile(); System.out.println(src); ProblemInitializer.ProblemInitializerListener emptyListener = - new ProblemInitializer.ProblemInitializerListener() { - @Override - public void proofCreated(ProblemInitializer sender, - ProofAggregate proofAggregate) { - } - - @Override - public void progressStarted(Object sender) { - } - - @Override - public void progressStopped(Object sender) { - } - - @Override - public void reportStatus(Object sender, String status, int progress) { - } - - @Override - public void reportStatus(Object sender, String status) { - } - - @Override - public void resetStatus(Object sender) { - } - - @Override - public void reportException(Object sender, ProofOblInput input, Exception e) { - } - }; + new ProblemInitializer.ProblemInitializerListener() { + @Override + public void proofCreated(ProblemInitializer sender, + ProofAggregate proofAggregate) { + } + + @Override + public void progressStarted(Object sender) { + } + + @Override + public void progressStopped(Object sender) { + } + + @Override + public void reportStatus(Object sender, String status, int progress) { + } + + @Override + public void reportStatus(Object sender, String status) { + } + + @Override + public void resetStatus(Object sender) { + } + + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + } + }; var promise = - JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), - src.toPath(), new JavacSettings()); + JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), + src.toPath(), new JavacSettings()); promise.get(); } @@ -64,39 +64,39 @@ void compileExternal() throws ExecutionException, InterruptedException { File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile(); System.out.println(src); ProblemInitializer.ProblemInitializerListener emptyListener = - new ProblemInitializer.ProblemInitializerListener() { - @Override - public void proofCreated(ProblemInitializer sender, - ProofAggregate proofAggregate) { - } - - @Override - public void progressStarted(Object sender) { - } - - @Override - public void progressStopped(Object sender) { - } - - @Override - public void reportStatus(Object sender, String status, int progress) { - } - - @Override - public void reportStatus(Object sender, String status) { - } - - @Override - public void resetStatus(Object sender) { - } - - @Override - public void reportException(Object sender, ProofOblInput input, Exception e) { - } - }; + new ProblemInitializer.ProblemInitializerListener() { + @Override + public void proofCreated(ProblemInitializer sender, + ProofAggregate proofAggregate) { + } + + @Override + public void progressStarted(Object sender) { + } + + @Override + public void progressStopped(Object sender) { + } + + @Override + public void reportStatus(Object sender, String status, int progress) { + } + + @Override + public void reportStatus(Object sender, String status) { + } + + @Override + public void resetStatus(Object sender) { + } + + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + } + }; var promise = - JavaCompilerCheckFacade.checkExternally(emptyListener, null, Collections.emptyList(), - src.toPath(), new JavacSettings()); + JavaCompilerCheckFacade.checkExternally(emptyListener, null, Collections.emptyList(), + src.toPath(), new JavacSettings()); promise.get(); } From f89754d9dc44dac45c8537669377fde339ec9ba1 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 23 Feb 2026 15:04:27 +0100 Subject: [PATCH 13/16] replace HashMap with a TreeMap --- .../uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java | 2 +- 1 file changed, 1 insertion(+), 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 bc2f403d82b..60f4782995b 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 @@ -73,7 +73,7 @@ public static void main(String[] args) { "column", it.location.getPosition().column(), "additionalInfo", it.getAdditionalInfo()); if (it.location.fileUri() != null) { - map = new HashMap<>(map); + map = new TreeMap<>(map); map.put("fileUri", it.location.fileUri().toString()); } return map; From 7c4df333e2d6532f70f56b99d6145d088d823591 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 23 Feb 2026 18:14:32 +0100 Subject: [PATCH 14/16] minor fixups and comments --- .../javac/JavaCompilerCheckFacade.java | 30 +++++++++++++++---- .../plugins/javac/JavacSettingsProvider.java | 8 +++++ 2 files changed, 33 insertions(+), 5 deletions(-) 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 60f4782995b..a008a628782 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 @@ -51,6 +51,9 @@ private JavaCompilerCheckFacade() { private static final Logger LOGGER = LoggerFactory.getLogger(JavaCompilerCheckFacade.class); + /** + * This main method be exclusively used by `checkExternally` to perform javac checks + */ public static void main(String[] args) { try (var input = new InputStreamReader(System.in)) { var params = Configuration.load(CharStreams.fromReader(input)); @@ -79,6 +82,7 @@ public static void main(String[] args) { return map; }).toList()); + // send the data over stderr to not interfere with the log messages Writer writer = new OutputStreamWriter(System.err); out.save(writer, null); writer.close(); @@ -87,6 +91,21 @@ public static void main(String[] args) { } } + /** + * initiates the compilation check on the target Java source (the Java program to be verified) + * in a separate process (with another java runtime) and + * reports any issues to the provided listener + * + * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed + * about any issues found in the target Java program + * @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 Path} to the source of the target Java program + * @param settings the {@link JavacSettings} that describe what other options the compiler + * should be called with + * @return future providing the list of diagnostics + */ public static @NonNull CompletableFuture> checkExternally( ProblemInitializer.ProblemInitializerListener listener, Path bootClassPath, List classPath, Path javaPath, @@ -95,7 +114,8 @@ public static void main(String[] args) { LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); return CompletableFuture.completedFuture(Collections.emptyList()); } - LOGGER.info("External Javac check is triggered."); + LOGGER.info( + "External Javac check is triggered. To disable use property -PKEY_JAVAC_DISABLE=true"); var params = new Configuration(); params.set("bootClassPath", Objects.toString(bootClassPath)); params.set("classPath", @@ -126,12 +146,12 @@ public static void main(String[] args) { params.save(process.outputWriter(), null); process.outputWriter().close(); - var errors = Streams.toString(process.getInputStream()); // what should be done with - // the errors ?? - var cfg = Configuration.load(CharStreams.fromStream(process.getErrorStream())); + // the KeY logging messages from `process` (currently not used) + var logs = Streams.toString(process.getInputStream()); + var messages = Configuration.load(CharStreams.fromStream(process.getErrorStream())); process.waitFor(); - return cfg.getList("messages").stream() + return messages.getList("messages").stream() .map(msgObj -> { Configuration msg = (Configuration) msgObj; return new PositionedIssueString( 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 d1fe5b77dd6..ee7c3beabbc 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 @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.plugins.javac; +import java.awt.event.ItemEvent; +import java.awt.event.ItemListener; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -62,6 +64,12 @@ public JavacSettingsProvider() { useProcessors = addCheckBox( "Enable Annotation Processing", USE_PROCESSORS_INFO, false, e -> { }); + useProcessors.addItemListener(new ItemListener() { + public void itemStateChanged(ItemEvent itemEvent) { + processors.setEnabled(itemEvent.getStateChange() == ItemEvent.SELECTED); + paths.setEnabled(itemEvent.getStateChange() == ItemEvent.SELECTED); + } + }); processors = addTextArea("Annotation Processors", "", PROCESSORS_INFO, e -> { }); paths = addTextArea("Processor Class Paths", "", CLASS_PATHS_INFO, e -> { From 495123b7c9c101c0b72c342581db43d8e7a91cb1 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 2 Mar 2026 15:10:54 +0100 Subject: [PATCH 15/16] replace unclear var declarations --- .../key/gui/plugins/javac/JavaCompilerCheckFacade.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 a008a628782..652c947b888 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,12 +56,12 @@ private JavaCompilerCheckFacade() { */ public static void main(String[] args) { try (var input = new InputStreamReader(System.in)) { - var params = Configuration.load(CharStreams.fromReader(input)); + Configuration params = Configuration.load(CharStreams.fromReader(input)); var settings = new JavacSettings(); settings.readSettings(params); - var result = check(null, + List result = check(null, Paths.get(params.getString("bootClassPath")), params.getStringList("classPath").stream().map(Paths::get).toList(), Paths.get(params.getString("javaPath")), settings).get(); @@ -147,8 +147,8 @@ public static void main(String[] args) { process.outputWriter().close(); // the KeY logging messages from `process` (currently not used) - var logs = Streams.toString(process.getInputStream()); - var messages = Configuration.load(CharStreams.fromStream(process.getErrorStream())); + String logs = Streams.toString(process.getInputStream()); + Configuration messages = Configuration.load(CharStreams.fromStream(process.getErrorStream())); process.waitFor(); return messages.getList("messages").stream() From 3f01c36be3019042381878e58779477cc7be1d04 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 2 Mar 2026 15:12:27 +0100 Subject: [PATCH 16/16] run spotless --- .../ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java | 3 ++- 1 file 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 652c947b888..81ba30a64fa 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 @@ -148,7 +148,8 @@ public static void main(String[] args) { // the KeY logging messages from `process` (currently not used) String logs = Streams.toString(process.getInputStream()); - Configuration messages = Configuration.load(CharStreams.fromStream(process.getErrorStream())); + Configuration messages = + Configuration.load(CharStreams.fromStream(process.getErrorStream())); process.waitFor(); return messages.getList("messages").stream()