Add test for Java parsing coverage (#3916)

Author: wadoon

key.core/src/test/java/de/uka/ilkd/key/java/JavaFeatureCoverageTest.java

@@ -0,0 +1,143 @@
+/* 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.java;
+
+import java.io.IOException;
+import java.net.URISyntaxException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.speclang.PositionedString;
+import de.uka.ilkd.key.util.ExceptionTools;
+
+import org.junit.jupiter.api.Assumptions;
+import org.junit.jupiter.api.DynamicTest;
+import org.junit.jupiter.api.TestFactory;
+
+import static org.junit.jupiter.api.Assertions.fail;
+
+/**
+ * Pins down which Java language features KeY's front-end
+ * ({@link de.uka.ilkd.key.java.loader.JP2KeYConverter} and the transformation pipeline) currently
+ * accepts. This backs the "Java Coverage" support table in the user documentation.
+ * <p>
+ * The examples live under {@code src/test/resources/de/uka/ilkd/key/java/coverage} in two folders:
+ * <ul>
+ * <li>{@code supported/} — one directory per feature that KeY <em>parses</em> today. Each is loaded
+ * and must keep loading; a failure here is a parser regression.</li>
+ * <li>{@code rejected/} — one directory per feature that KeY does <em>not</em> parse today (it
+ * throws at load time, usually "Unsupported element detected given by Java Parser"). Each must keep
+ * being rejected; if one starts loading, the feature has become supported and the test (plus the
+ * documentation table) must be updated.</li>
+ * </ul>
+ * Every example also compiles with {@code javac} 21, so a load failure reflects KeY's front-end and
+ * not malformed Java. Note this checks <em>parseability</em>, not sound reasoning: a few
+ * {@code supported/} features (e.g. autoboxing, try-with-resources) load but are not soundly
+ * modelled, as noted in the documentation.
+ *
+ * @see de.uka.ilkd.key.java.loader.JP2KeYConverter
+ */
+public class JavaFeatureCoverageTest {
+
+    /** Each directory here must keep parsing; a throw is a front-end regression. */
+    @TestFactory
+    public Stream<DynamicTest> supportedFeaturesStayParseable() throws Exception {
+        return featureDirs("supported")
+                .map(dir -> DynamicTest.dynamicTest(dir.getFileName().toString(),
+                    () -> {
+                        Throwable error = tryLoad(dir);
+                        if (error != null) {
+                            fail("Regression: the Java feature '" + dir.getFileName()
+                                + "' no longer parses, although it is listed as supported. "
+                                + "If dropping it is intended, move it to 'coverage/rejected/' and update "
+                                + "the Java Coverage documentation table. Load error: "
+                                + firstMessage(error));
+                        }
+                    }));
+    }
+
+    /**
+     * Each directory here must keep being rejected. If one starts to parse, the feature is now
+     * supported and both this test and the documentation must be updated.
+     */
+    @TestFactory
+    public Stream<DynamicTest> unsupportedFeaturesStayRejected() throws Exception {
+        return featureDirs("rejected")
+                .map(dir -> DynamicTest.dynamicTest(dir.getFileName().toString(),
+                    () -> {
+                        Throwable error = tryLoad(dir);
+                        if (error == null) {
+                            fail("'" + dir.getFileName()
+                                + "' is now supported and the test should be "
+                                + "modified to reflect the new addition: move it from 'coverage/rejected/' "
+                                + "to 'coverage/supported/' and update the Java Coverage documentation "
+                                + "table (mark the feature as supported).");
+                        }
+                    }));
+    }
+
+    // --- helpers -----------------------------------------------------------------------------
+
+    private static Stream<Path> featureDirs(String kind) throws IOException, URISyntaxException {
+        Path base = coverageRoot().resolve(kind);
+        Assumptions.assumeTrue(Files.isDirectory(base),
+            "coverage examples not found at " + base.toAbsolutePath());
+        try (Stream<Path> s = Files.list(base)) {
+            // Materialise so the directory stream is closed before the dynamic tests run.
+            List<Path> dirs = s.filter(Files::isDirectory).sorted().collect(Collectors.toList());
+            return dirs.stream();
+        }
+    }
+
+    private static Path coverageRoot() throws URISyntaxException {
+        // Prefer the copied test resources on the classpath (location-independent),
+        // fall back to the module-relative source path.
+        var url = JavaFeatureCoverageTest.class.getResource("/de/uka/ilkd/key/java/coverage");
+        if (url != null) {
+            return Paths.get(url.toURI());
+        }
+        return Paths.get("src/test/resources/de/uka/ilkd/key/java/coverage");
+    }
+
+    /** Loads the feature's {@code problem.key}; returns {@code null} on success, else the error. */
+    private static Throwable tryLoad(Path featureDir) {
+        Path problem = featureDir.resolve("problem.key");
+        KeYEnvironment<?> env = null;
+        try {
+            env = KeYEnvironment.load(problem);
+            return null;
+        } catch (Throwable t) {
+            return t;
+        } finally {
+            if (env != null) {
+                try {
+                    env.dispose();
+                } catch (Throwable ignore) {
+                }
+            }
+        }
+    }
+
+    private static String firstMessage(Throwable t) {
+        List<String> msgs = new ArrayList<>();
+        try {
+            for (PositionedString ps : ExceptionTools.getMessages(t)) {
+                msgs.add(ps.getText());
+            }
+        } catch (Throwable ignore) {
+        }
+        String joined = String.join(" | ", msgs);
+        if (joined.isBlank()) {
+            joined = t.getClass().getSimpleName()
+                    + (t.getMessage() != null ? ": " + t.getMessage() : "");
+        }
+        return joined.replaceAll("\\s+", " ").trim();
+    }
+}

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/README.md

@@ -0,0 +1,65 @@
+# Java feature coverage examples
+
+Fixtures for `de.uka.ilkd.key.java.JavaFeatureCoverageTest`, which pins down
+which Java language features KeY's front-end currently parses. They also back
+the **Java Coverage** support table in the user documentation
+(*User Guide > Supported Language Features > Java Coverage*).
+
+Layout: one directory per feature, each with a small `.java` file plus a
+`problem.key` (`\javaSource "."; \problem { true }`) that makes KeY parse it:
+
+- `supported/`: features KeY **parses** today. The test loads each and fails
+  if one stops parsing (a front-end regression).
+- `rejected/`: features KeY does **not** parse today (loading throws, usually
+  *"Unsupported element detected given by Java Parser"*). The test fails if one
+  starts parsing, which means the feature became supported and both the test
+  and the documentation table must be updated.
+
+Every `.java` file also compiles with `javac` 21, and uses only types available
+in KeY's default classpath (`JavaRedux`) or types it declares itself, so a load
+failure reflects KeY's front-end and not malformed Java or a missing type.
+
+## Why each rejected example is rejected
+
+Each example isolates a single construct, so its rejection is attributable to
+the feature under test (verified by loading each and inspecting the error):
+
+| Example | Rejected because |
+|---|---|
+| `generics-*` (plain, bounded, wildcard, method, diamond) | converter aborts with *"Unexpected type to convert"* on the type parameter/argument |
+| `local-class` | `Unsupported element: LocalClassDeclarationStmt` |
+| `static-import` | `Unsupported element: ImportDeclaration` (the `static` import) |
+| `annotation-declaration` | `Unsupported element: AnnotationDeclaration` (the `@interface`) |
+| `multi-catch` | `Unsupported element: UnionType` |
+| `lambda` | `Unsupported element: LambdaExpr` |
+| `method-reference` | `Unsupported element: MethodReferenceExpr` |
+| `instanceof-pattern` | `Unsupported element: TypePatternExpr` (the bound pattern) |
+| `switch-expression` | parser rejects `yield` / arrow-switch (syntax error) |
+| `switch-pattern-type` | `Unsupported element: TypePatternExpr` (`case Integer i`) |
+| `switch-pattern-record` | `Unsupported element: TypePatternExpr` (record component of `case Point(...)`) |
+| `record-pattern` | `Unsupported element: TypePatternExpr` (record pattern via `instanceof`) |
+| `switch-enum-unqualified` | KeY cannot resolve the **unqualified** `case RED` label (the enum is declared in the file, so this is the label form, not a missing type) |
+| `module-declaration` | `module-info` currently triggers an internal error (`IndexOutOfBoundsException`) |
+| `var-reference-type` | a `var` with a `String` initializer currently triggers an internal `NullPointerException` |
+
+Because the host construct is otherwise supported (a `switch` statement,
+`instanceof`, a normal class), the failure lands on the tested feature, not on
+its surroundings.
+
+## Notes
+
+- `switch-enum-qualified` vs `switch-enum-unqualified` capture a real quirk: a
+  `switch` over an `enum` only loads with *qualified* case labels
+  (`case E.C:`); the standard unqualified `case C:` fails to resolve.
+- Pattern matching for `switch` is split by pattern kind:
+  `switch-pattern-type` and `switch-pattern-record` are rejected, but a bare
+  `case null` label (`switch-null-label`) actually parses, so it lives in
+  `supported/`. The examples use `switch` *statements*, not `switch`
+  *expressions*, so the failure is attributed to the pattern and not to the
+  (also unsupported) switch-expression form.
+- `var-primitive` / `var-in-for` load, but `var-reference-type` does not.
+- Generics come in five variants (`plain`, `bounded`, `wildcard`, `method`,
+  `diamond`), all rejected.
+- "Parses" is not "soundly reasoned about": `autoboxing` and
+  `try-with-resources` sit in `supported/` because they load, but KeY does not
+  model them soundly (see the documentation's *Comments* column).

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/annotation-declaration/AnnDecl.java

@@ -0,0 +1,4 @@
+public class AnnDecl {
+    @interface Marker { int value() default 0; }
+    @Marker(3) int x;
+}

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/annotation-declaration/problem.key

@@ -0,0 +1,3 @@
+\javaSource ".";
+
+\problem { true }

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-bounded/GenBounded.java

@@ -0,0 +1,6 @@
+public class GenBounded {
+    interface S { }
+    static class Box<T extends S> { T v; }
+    static class Impl implements S { }
+    Box<Impl> b = new Box<Impl>();
+}

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-bounded/problem.key

@@ -0,0 +1,3 @@
+\javaSource ".";
+
+\problem { true }

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-diamond/GenDiamond.java

@@ -0,0 +1,4 @@
+public class GenDiamond {
+    static class Box<T> { T v; }
+    Box<String> b = new Box<>();
+}

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-diamond/problem.key

@@ -0,0 +1,3 @@
+\javaSource ".";
+
+\problem { true }

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-method/GenMethod.java

@@ -0,0 +1,4 @@
+public class GenMethod {
+    <T> T id(T x) { return x; }
+    String f() { return id("hi"); }
+}

key.core/src/test/resources/de/uka/ilkd/key/java/coverage/rejected/generics-method/problem.key

@@ -0,0 +1,3 @@
+\javaSource ".";
+
+\problem { true }