Add support for Annotation Processors in the Javac Extension by PiIsRational · Pull Request #3686 · KeYProject/key

PiIsRational · 2025-11-18T20:41:44Z

Changes

Extended the Javac Extension to be able to load annotation processors, while the java code is getting checked
in KeY. This includes creating settings for the Javac Extension, to be able to set the checkers.
Also, the there are changes to the run step of the gradle script
to add (add-export and add-opens) directives to the java runtime such that annotations processors can access the internal java compiler data structures.
This is required to be done by hand when using KeY as a jar and would require the following (or similar) command:

java \
    --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 \
    -jar key-2.12.4-dev-exe.jar

Type of pull request

New feature (non-breaking change which adds functionality)
There are changes to the (Java) code
There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

I made sure that introduced/changed code is well documented (javadoc and inline comments).
I have tested the feature as follows:
- I used it with multiple annotation processors
- I loaded KeY with various settings to check if and when they are deleted
I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

@WolframPfeifer is involved in this pull request.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

key.ui/build.gradle

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

…figuration" This reverts commit 74af1d7.

codecov · 2025-12-08T14:07:03Z

Codecov Report

❌ Patch coverage is 0% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 50.34%. Comparing base (e5853a5) to head (7c4df33).
⚠️ Report is 95 commits behind head on main.

Files with missing lines	Patch %	Lines
...n/java/de/uka/ilkd/key/settings/Configuration.java	0.00%	1 Missing and 1 partial ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3686      +/-   ##
============================================
+ Coverage     47.98%   50.34%   +2.35%     
+ Complexity    16045    15902     -143     
============================================
  Files          1683     1597      -86     
  Lines         96046    91024    -5022     
  Branches      15388    14553     -835     
============================================
- Hits          46091    45823     -268     
+ Misses        44683    39988    -4695     
+ Partials       5272     5213      -59

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

wadoon · 2026-01-26T15:14:24Z

One solution to the exports-problem is to start javac in an external process. This means:

Writing a main function inside KeY
On call, use the current classpath and JRE, and start a new Java process which enters the new main function.
Capture the diagnostics in the new process, and send them in a structured way to stdout.
Read the stdout in the process spawner.

Externalize Javac into separate Java process for setting JMS directives

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

WolframPfeifer

Thanks for this PR, which will allow running Checker Framework checkers (e.g. for Nullness of Ownership) from the KeY GUI directly.

Also, thanks to @wadoon for the initial draft of the external checker, and @PiIsRational for polishing.

I have a few minor complaints about the use of var. When these are fixed, the PR would be ready from my point of view. Also, there is code smell in the unit test (check without assert), but we could also keep it like that.

WolframPfeifer · 2026-02-23T19:48:45Z

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

+     */
+    public static void main(String[] args) {
+        try (var input = new InputStreamReader(System.in)) {
+            var params = Configuration.load(CharStreams.fromReader(input));


We have the policy that the var keyword can be used in the code as long as the type is obvious (for example, when calling a constructor), otherwise it would decrease readability of the code. In this case, it is not in my opinion. Can you please make the type here explicit?

WolframPfeifer · 2026-02-23T19:49:21Z

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

+            var settings = new JavacSettings();
+            settings.readSettings(params);
+
+            var result = check(null,


Same as above: Make the type explicit for better readability please.

WolframPfeifer · 2026-02-23T19:50:43Z

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

+
+                // the KeY logging messages from `process` (currently not used)
+                var logs = Streams.toString(process.getInputStream());
+                var messages = Configuration.load(CharStreams.fromStream(process.getErrorStream()));


Here as well ...

WolframPfeifer · 2026-02-23T20:00:14Z

key.ui/src/test/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacadeTest.java

+    }
+
+    @Test
+    void compileExternal() throws ExecutionException, InterruptedException {


In my opinion, it is a bit of a code smell to have a test without any asserts (was already the case for the original test of this class). However, this can still count as some kind of smoke test, so I do not let it block the merge ...

PiIsRational added 6 commits November 17, 2025 18:25

extend the javac extension

ef77b66

updated the code and text to be clearer

2a5ca56

save proof independent settings, that are not used by the configuration

74af1d7

few changes

0ae4244

Merge branch 'main' into javac-extension

1931fe9

fix mistakes introduced by the merge

0f710eb

wadoon reviewed Nov 24, 2025

View reviewed changes

key.ui/build.gradle Outdated Show resolved Hide resolved

key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java Outdated Show resolved Hide resolved

PiIsRational added 2 commits December 6, 2025 18:31

Revert "save proof independent settings, that are not used by the con…

d84fb9f

…figuration" This reverts commit 74af1d7.

un-revert the name of the Javac Settings

7ca2241

update the javaCompilerCheckFacade interface and fix tests

ba35a99

PiIsRational mentioned this pull request Jan 26, 2026

Add the Universe Type Checker as a Dependency #3725

Draft

3 tasks

PiIsRational changed the title ~~Javac extension~~ Add support for Annotation Processors in the Javac Extension Jan 26, 2026

change the help messages in the settings provider

7a1658c

WolframPfeifer assigned PiIsRational Jan 26, 2026

WolframPfeifer added GUI Feature New feature or request Java Pull requests that update Java code labels Jan 26, 2026

WolframPfeifer added this to the v3.0.0 milestone Jan 26, 2026

PiIsRational and others added 3 commits January 30, 2026 12:30

make compiler errors acessible from the gui

4c5f41e

wip: Javac in separate process

0f42201

Externalize Javac into separate Java process for setting JMS directives

finish implementing the external java checks

622a300

wadoon reviewed Feb 23, 2026

View reviewed changes

key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java Outdated Show resolved Hide resolved

wadoon and others added 3 commits February 23, 2026 11:42

Merge branch 'main' into javac-extension

285af93

replace HashMap with a TreeMap

f89754d

minor fixups and comments

7c4df33

PiIsRational marked this pull request as ready for review February 23, 2026 17:15

WolframPfeifer requested changes Feb 23, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for Annotation Processors in the Javac Extension#3686

Add support for Annotation Processors in the Javac Extension#3686
PiIsRational wants to merge 16 commits intoKeYProject:mainfrom
PiIsRational:javac-extension

PiIsRational commented Nov 18, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Dec 8, 2025 •

edited

Loading

Uh oh!

wadoon commented Jan 26, 2026

Uh oh!

Uh oh!

WolframPfeifer left a comment

Uh oh!

WolframPfeifer Feb 23, 2026

Uh oh!

WolframPfeifer Feb 23, 2026

Uh oh!

WolframPfeifer Feb 23, 2026

Uh oh!

WolframPfeifer Feb 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

PiIsRational commented Nov 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Type of pull request

Ensuring quality

Additional information and contact(s)

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Dec 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

wadoon commented Jan 26, 2026

Uh oh!

Uh oh!

WolframPfeifer left a comment

Choose a reason for hiding this comment

Uh oh!

WolframPfeifer Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

WolframPfeifer Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

WolframPfeifer Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

WolframPfeifer Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

PiIsRational commented Nov 18, 2025 •

edited

Loading

codecov bot commented Dec 8, 2025 •

edited

Loading