Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 24 additions & 1 deletion key.ui/build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This requirement makes this PR unusable in practice. The normal execution is java -jar key-...-exe.jar.

Using start scripts, it would be possible, but #3638 is not discussed.

"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) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should it not be JavacSettings instance here for later extensibility?

if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) {
LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE");
return CompletableFuture.completedFuture(Collections.emptyList());
Expand All @@ -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());
Expand All @@ -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)) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.
*
Expand All @@ -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.
*/
Expand Down Expand Up @@ -147,14 +152,26 @@ 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");
Expand Down Expand Up @@ -227,6 +244,10 @@ public void selectedNodeChanged(KeYSelectionEvent<Node> e) {
public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
loadProof(e.getSource().getSelectedProof());
}

public SettingsProvider getSettings() {
return new JavacSettingsProvider();
}
}


Expand Down
Original file line number Diff line number Diff line change
@@ -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();
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
/* 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;

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 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 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 -> {});
processors = addTextArea("Annotation Processors", "", PROCESSORS_INFO, e -> {});
paths = addTextArea("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;
}
}
Loading