Add support for Annotation Processors in the Javac Extension

.gitignore

@@ -51,6 +51,7 @@ bin/
 .settings
 .project
 .classpath
+.factorypath
 
 # Files generated by IntelliJ ANTLR plugin
 key.core/src/main/gen

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

@@ -497,6 +497,10 @@ public ConfigurationWriter printIndent() {
         }
 
         public ConfigurationWriter printComment(String comment) {
+            if (comment == null) {
+                return this;
+            }
+
             if (comment.contains("\n")) {
                 out.format("/* %s */\n", comment);
             } else {

key.ui/build.gradle

@@ -83,7 +83,7 @@ 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 "
 }
 
 tasks.register('runWithProfiler', JavaExec) {

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

@@ -3,15 +3,13 @@
  * 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;
 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;
@@ -21,7 +19,11 @@
 import de.uka.ilkd.key.java.Position;
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.proof.init.ProblemInitializer;
+import de.uka.ilkd.key.settings.Configuration;
 
+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;
@@ -43,24 +45,154 @@
  * @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);
 
+    /**
+     * 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));
+
+            var settings = new JavacSettings();
+            settings.readSettings(params);
+
+            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 -> {
+                    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 TreeMap<>(map);
+                        map.put("fileUri", it.location.fileUri().toString());
+                    }
+                    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();
+        } catch (Exception e) {
+            LOGGER.error("Error during execution.", e);
+        }
+    }
+
+    /**
+     * 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 <code>listener</code>
+     *
+     * @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<List<PositionedIssueString>> checkExternally(
+            ProblemInitializer.ProblemInitializerListener listener,
+            Path bootClassPath, List<Path> 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());
+        }
+        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",
+            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();
+
+                // 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 messages.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 <code>listener</code>
      *
      * @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 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<List<PositionedIssueString>> check(
             ProblemInitializer.ProblemInitializerListener listener,
-            Path bootClassPath, List<Path> classPath, Path javaPath) {
+            Path bootClassPath, List<Path> 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());
@@ -72,7 +204,9 @@ public class JavaCompilerCheckFacade {
 
         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());
         }
 
@@ -86,17 +220,46 @@ public class JavaCompilerCheckFacade {
 
         // gather configured bootstrap classpath and regular classpath
         List<String> options = new ArrayList<>();
+
+        if (settings.getUseProcessors()) {
+            String newlineClassPath = settings.getClassPaths();
+            List<Path> 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<String> processors =
+                Arrays.asList(settings.getProcessors().split(System.lineSeparator()))
+                        .stream()
+                        .filter(s -> !s.isBlank())
+                        .toList();
+
+            if (!processors.isEmpty()) {
+                options.add("-processor");
+                options.add(processors.stream().collect(Collectors.joining(",")));
+            }
+        }
+
         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(":")));
         }
+
         ArrayList<Path> files = new ArrayList<>();
         if (Files.isDirectory(javaPath)) {
             try (var s = Files.walk(javaPath)) {
@@ -127,7 +290,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())

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

@@ -22,6 +22,7 @@
 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;
@@ -30,7 +31,7 @@
 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 +44,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,14 +148,21 @@ private void loadProof(Proof selectedProof) throws RuntimeException {
 
             Path bootClassPath = jm.getBootClassPath() != null ? jm.getBootClassPath() : null;
             List<Path> classpath = jm.getClassPath();
+
             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);
+            JavacSettings settings = JavacSettingsProvider.getJavacSettings();
+            CompletableFuture<List<PositionedIssueString>> 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");
@@ -227,6 +235,10 @@ public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
     public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
         loadProof(e.getSource().getSelectedProof());
     }
+
+    public SettingsProvider getSettings() {
+        return new JavacSettingsProvider();
+    }
 }