diff --git a/.gitignore b/.gitignore index df03685c259..6624464d29e 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.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 31acea8acba..c6ca789dfef 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 @@ -508,7 +508,6 @@ public ConfigurationWriter printComment(@Nullable 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 8bc57b2200d..9a9527fcc7a 100644 --- a/key.ui/build.gradle +++ b/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 " } 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 7180b655d1d..6415e899821 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,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; @@ -20,8 +18,11 @@ import de.uka.ilkd.key.gui.PositionedIssueString; 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; @@ -33,8 +34,6 @@ *

* For setting up javac it uses the KeY project information about the bootpath and * classpath. - * Any issues found in the compilation are reported to a provided listener of type - * {@link ProblemInitializer.ProblemInitializerListener}. *

* Checking the target Java code can be enabled / disabled by providing the property * -PKEY_JAVAC_DISABLE=true / -PKEY_JAVAC_DISABLE=false on startup of KeY. @@ -43,24 +42,146 @@ * @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)) { + Configuration params = Configuration.load(CharStreams.fromReader(input)); + + var settings = new JavacSettings(); + settings.readSettings(params); + + List result = check( + 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) + * + * @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( + 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()); + } + 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) + String logs = Streams.toString(process.getInputStream()); + Configuration 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 listener * - * @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> check( - ProblemInitializer.ProblemInitializerListener listener, - Path bootClassPath, List classPath, Path javaPath) { + 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()); @@ -72,7 +193,6 @@ 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."); return CompletableFuture.completedFuture(Collections.emptyList()); } @@ -86,10 +206,39 @@ public class JavaCompilerCheckFacade { // gather configured bootstrap classpath and regular classpath 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(); + + if (!processorClassPath.isEmpty()) { + classPath = new ArrayList<>(classPath); + classPath.addAll(processorClassPath); + } + + List 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("-bootclasspath"); - options.add(bootClassPath.toAbsolutePath().toString()); + // options.add("-bootclasspath"); + // options.add(bootClassPath.toAbsolutePath().toString()); + LOGGER.info("The \"bootclasspath\" Option is set but not supported."); } + if (classPath != null && !classPath.isEmpty()) { options.add("-classpath"); options.add( @@ -97,6 +246,7 @@ public class JavaCompilerCheckFacade { .map(Objects::toString) .collect(Collectors.joining(":"))); } + ArrayList files = new ArrayList<>(); if (Files.isDirectory(javaPath)) { try (var s = Files.walk(javaPath)) { @@ -113,6 +263,10 @@ public class JavaCompilerCheckFacade { Iterable compilationUnits = fileManager.getJavaFileObjects(files.toArray(new Path[0])); + LOGGER.info( + "running Javac check with following\n\toptions: {},\n\tclasses: {},\n\tcompilation units: {},", + options, classes, compilationUnits); + JavaCompiler.CompilationTask task = compiler.getTask(output, fileManager, diagnostics, options, classes, compilationUnits); @@ -127,7 +281,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/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index 009a53a28de..2f18a27cd47 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 @@ -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. *

* 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 classpath = jm.getClassPath(); + Path javaPath = jm.getModelDir(); lblStatus.setForeground(Color.black); lblStatus.setText("Javac runs"); lblStatus.setIcon(ICON_WAIT.get(16)); - CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath); + JavacSettings settings = JavacSettingsProvider.getJavacSettings(); + CompletableFuture> task = settings.getUseProcessors() + ? JavaCompilerCheckFacade.checkExternally(bootClassPath, + classpath, + javaPath, + settings) + : JavaCompilerCheckFacade.check(bootClassPath, classpath, + javaPath, settings); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); @@ -227,6 +235,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..bd3d821a6c1 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -0,0 +1,100 @@ +/* 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.io.Serializable; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + +/** + * Settings for the javac extention. + * + * @author Daniel Grévent + */ +public class JavacSettings extends AbstractPropertiesSettings implements Serializable { + + /** + * The name of the category in the settings. + */ + public static final String CATEGORY = "Javac Extension"; + + /** + * Config key for {@link #useProcessors}. + */ + private static final String KEY_USE_PROCESSORS = "useProcessors"; + + /** + * Config key for {@link #processors}. + */ + private static final String KEY_PROCESSORS = "processors"; + + /** + * Config key for {@link #classPaths}. + */ + private static final String KEY_CLASS_PATHS = "classPaths"; + + /** + * The type annotation processors to be run. + */ + private final PropertyEntry useProcessors = + createBooleanProperty(KEY_USE_PROCESSORS, false); + + /** + * The type annotation processors to be run. + */ + private final PropertyEntry processors = + createStringProperty(KEY_PROCESSORS, ""); + + /** + * Additional class paths, needed for example by annotation processors + */ + private final PropertyEntry classPaths = + createStringProperty(KEY_CLASS_PATHS, ""); + + public JavacSettings() { + super(CATEGORY); + } + + /** + * @param useProcessors if the annotation processors should be run + */ + public void setUseProcessors(boolean useProcessors) { + this.useProcessors.set(useProcessors); + } + + /** + * @param processor the annotation processors to run + */ + public void setProcessors(String processor) { + this.processors.set(processor); + } + + /** + * @param paths the additional class paths + */ + public void setClassPaths(String paths) { + this.classPaths.set(paths); + } + + /** + * @return true iff the annotation processors should be used + */ + public boolean getUseProcessors() { + return useProcessors.get(); + } + + /** + * @return the annotation processors separated by newlines + */ + public String getProcessors() { + return processors.get(); + } + + /** + * @return the additional class paths separated by newlines + */ + public String getClassPaths() { + return classPaths.get(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java new file mode 100644 index 00000000000..ee7c3beabbc --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java @@ -0,0 +1,117 @@ +/* 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.awt.event.ItemEvent; +import java.awt.event.ItemListener; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.settings.SettingsPanel; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +import net.miginfocom.layout.CC; + +/** + * Settings for the javac extension. + * + * @author Daniel Grévent + */ +public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { + /** + * Singleton instance of the javac settings. + */ + private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); + + /** + * Text for the explanaition. + */ + private static final String INTRO_LABEL = + "This allows to run the Java compiler when loading Java files with additional processes such as 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."; + + /** + * Information message for the {@link #processors} text area. + */ + private static final String PROCESSORS_INFO = """ + A list of annotation processors to run while type checking with the Java compiler. + Each checkers should be written on a new line."""; + + /** + * Information message for the {@link #paths} text area. + */ + private static final String CLASS_PATHS_INFO = """ + A list of additional class paths to be used by the Java compiler while type checking. + These could for example be needed for certain annotation processors. + Each path should be absolute and be written on a new line."""; + + private final JCheckBox useProcessors; + private final JTextArea processors; + private final JTextArea paths; + + /** + * Construct a new settings provider. + */ + public JavacSettingsProvider() { + pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); + useProcessors = addCheckBox( + "Enable Annotation Processing", USE_PROCESSORS_INFO, false, e -> { + }); + 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 -> { + }); + + setHeaderText("Javac Options"); + } + + @Override + public String getDescription() { + return "Javac Options"; + } + + public static JavacSettings getJavacSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(JAVAC_SETTINGS); + return JAVAC_SETTINGS; + } + + + @Override + public JPanel getPanel(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + useProcessors.setSelected(settings.getUseProcessors()); + processors.setText(settings.getProcessors()); + paths.setText(settings.getClassPaths()); + + return this; + } + + @Override + public void applySettings(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + settings.setUseProcessors(useProcessors.isSelected()); + settings.setProcessors(processors.getText()); + settings.setClassPaths(paths.getText()); + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java index 5cae7320876..f731d7adf6a 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 @@ -7,12 +7,10 @@ import java.util.Collections; import java.util.concurrent.ExecutionException; -import de.uka.ilkd.key.proof.ProofAggregate; -import de.uka.ilkd.key.proof.init.ProblemInitializer; -import de.uka.ilkd.key.proof.init.ProofOblInput; - import org.junit.jupiter.api.Test; +import static org.junit.jupiter.api.Assertions.assertTrue; + /** * @author Alexander Weigl * @version 1 (29.01.23) @@ -22,34 +20,21 @@ class JavaCompilerCheckFacadeTest { 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) {} - }; var promise = - JavaCompilerCheckFacade.check(emptyListener, null, Collections.emptyList(), - src.toPath()); - promise.get(); + JavaCompilerCheckFacade.check(null, Collections.emptyList(), + src.toPath(), new JavacSettings()); + var result = promise.get(); + assertTrue(result.isEmpty()); } + @Test + void compileExternal() throws ExecutionException, InterruptedException { + File src = new File("examples/firstTouch/06-BinarySearch/src/").getAbsoluteFile(); + System.out.println(src); + var promise = + JavaCompilerCheckFacade.checkExternally(null, Collections.emptyList(), + src.toPath(), new JavacSettings()); + var result = promise.get(); + assertTrue(result.isEmpty()); + } }