Add support for Annotation Processors in the Javac Extension

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;
         }
 

key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java

@@ -53,8 +53,8 @@ public class ProofIndependentSettings {
     private final List<Settings> 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()) {

key.ui/build.gradle

@@ -80,7 +80,30 @@ run {
 
     // this can be used to solve a problem where the OS hangs during debugging of popup menus
     // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425)
-    jvmArgs += "-Dsun.awt.disablegrab=true"
+    jvmArgs += "-Dsun.awt.disablegrab=true "
+
+    // this is needed to be able to load checker framework checkers in the javac
+    // extension
+    jvmArgs += [
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
+        "--add-exports", 
+        "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
+        "--add-opens", 
+        "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED" 
+    ]
 }
 
 tasks.register('runWithProfiler', JavaExec) {

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

@@ -52,15 +52,17 @@ public class JavaCompilerCheckFacade {
      *
      * @param listener the {@link ProblemInitializer.ProblemInitializerListener} to be informed
      *        about any issues found in the target Java program
-     * @param bootClassPath the {@link File} referring to the path containing the core Java classes
-     * @param classPath the {@link List} of {@link File}s referring to the directory that make up
+     * @param bootClassPath the {@link Path} referring to the path containing the core Java classes
+     * @param classPath the {@link List} of {@link Path}s referring to the directory that make up
      *        the target Java programs classpath
-     * @param javaPath the {@link String} with the path to the source of the target Java program
+     * @param javaPath the {@link Path} to the source of the target Java program
+     * @param processors the {@link List} of {@link String}s referring to the annotation processors to be run
      * @return future providing the list of diagnostics
      */
     public static @NonNull CompletableFuture<List<PositionedIssueString>> check(
             ProblemInitializer.ProblemInitializerListener listener,
-            Path bootClassPath, List<Path> classPath, Path javaPath) {
+            Path bootClassPath, List<Path> classPath, Path javaPath,
+            List<String> 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<String> options = new ArrayList<>();
+
         if (bootClassPath != null) {
             options.add("-Xbootclasspath");
             options.add(bootClassPath.toAbsolutePath().toString());
@@ -97,6 +100,12 @@ public class JavaCompilerCheckFacade {
                         .map(Objects::toString)
                         .collect(Collectors.joining(":")));
         }
+
+        if (processors != null && !processors.isEmpty()) {
+            options.add("-processor");
+            options.add(processors.stream().collect(Collectors.joining(",")));
+        }
+
         ArrayList<Path> files = new ArrayList<>();
         if (Files.isDirectory(javaPath)) {
             try (var s = Files.walk(javaPath)) {

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

@@ -4,7 +4,11 @@
 package de.uka.ilkd.key.gui.plugins.javac;
 
 import java.awt.*;
+
 import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.List;
 import java.util.TreeSet;
@@ -25,12 +29,13 @@
 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;
 
 /**
- * Extensions provides Javac checks for recent-loaded Java files.
+ * Extension provides Javac checks for recent-loaded Java files.
  * <p>
  * Provides an entry in the status line for access.
  *
@@ -43,7 +48,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,21 +152,36 @@ private void loadProof(Proof selectedProof) throws RuntimeException {
 
             Path bootClassPath = jm.getBootClassPath() != null ? jm.getBootClassPath() : null;
             List<Path> classpath = jm.getClassPath();
+            JavacSettings settings = JavacSettingsProvider.getJavacSettings();
+
+            List<String> processors = null;
+            if (settings.getUseProcessors()) {
+                if (classpath == null) classpath = new ArrayList<>();
+
+                classpath.addAll(Arrays.asList(settings.getClassPaths().split(System.lineSeparator()))
+                    .stream().map(p -> Paths.get(p)).toList());
+
+                processors = Arrays.asList(settings.getProcessors().split(System.lineSeparator()));
+            }
+
             Path javaPath = jm.getModelDir();
 
             lblStatus.setForeground(Color.black);
             lblStatus.setText("Javac runs");
             lblStatus.setIcon(ICON_WAIT.get(16));
 
             CompletableFuture<List<PositionedIssueString>> task =
-                JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath);
+                JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, processors);
             try {
                 task.thenAccept(it -> SwingUtilities.invokeLater(() -> {
                     lblStatus.setText("Javac finished");
                     data.issues = it;
                     updateLabel(data);
                 })).get();
             } catch (InterruptedException | ExecutionException ex) {
+                lblStatus.setForeground(COLOR_ERROR.get());
+                lblStatus.setIcon(ICON_ERROR.get(16));
+                lblStatus.setText("Javac error");
                 throw new RuntimeException(ex);
             }
         }
@@ -227,6 +247,10 @@ public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
     public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
         loadProof(e.getSource().getSelectedProof());
     }
+
+    public SettingsProvider getSettings() {
+        return new JavacSettingsProvider();
+    }
 }
 
 

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

@@ -0,0 +1,99 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.gui.plugins.javac;
+import java.lang.Boolean;
+
+import de.uka.ilkd.key.settings.AbstractPropertiesSettings;
+
+/**
+ * Settings for the javac extention.
+ *
+ * @author Daniel Grévent
+ */
+public class JavacSettings extends AbstractPropertiesSettings {
+
+    /**
+     * The name of the category in the settings.
+     */
+    public static final String CATEGORY = "Javac Extension";
+
+    /**
+     * Config key for {@link #useProcessors}.
+     */
+    private static final String KEY_USE_PROCESSORS = "useProcessors";
+
+    /**
+     * Config key for {@link #processors}.
+     */
+    private static final String KEY_PROCESSORS = "processors";
+
+    /**
+     * Config key for {@link #classPaths}.
+     */
+    private static final String KEY_CLASS_PATHS = "classPaths";
+
+    /**
+     * The type annotation processors to be run.
+     */
+    private final PropertyEntry<Boolean> useProcessors = 
+        createBooleanProperty(KEY_USE_PROCESSORS, false);
+
+    /**
+     * The type annotation processors to be run.
+     */
+    private final PropertyEntry<String> processors = 
+        createStringProperty(KEY_PROCESSORS, "");
+
+    /**
+     * Additional class paths, needed for example by annotation processors
+     */
+    private final PropertyEntry<String> classPaths = 
+        createStringProperty(KEY_CLASS_PATHS, "");
+
+    public JavacSettings() {
+        super(CATEGORY);
+    }
+
+    /**
+     * @param useProcessors if the annotation processors should be run
+     */
+    public void setUseProcessors(boolean useProcessors) {
+        this.useProcessors.set(useProcessors);
+    }
+
+    /**
+     * @param processor the annotation processors to run
+     */
+    public void setProcessors(String processor) {
+        this.processors.set(processor);
+    }
+
+    /**
+     * @param paths the additional class paths
+     */
+    public void setClassPaths(String paths) {
+        this.classPaths.set(paths);
+    }
+
+    /**
+     * @return true iff the annotation processors should be used
+     */
+    public boolean getUseProcessors() {
+        return useProcessors.get();
+    }
+
+    /**
+     * @return the annotation processors separated by newlines
+     */
+    public String getProcessors() {
+        return processors.get();
+    }
+
+    /**
+     * @return the additional class paths separated by newlines
+     */
+    public String getClassPaths() {
+        return classPaths.get();
+    }
+}