From 85521d34e9d6f740b5b96c502f8ed10af203e315 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 6 Oct 2026 20:02:41 +0100 Subject: [PATCH 1/3] Raise Spoon compliance level from 8 to 17 At level 8, Java 9+ syntax (`var`, `try (r)`, switch expressions) fails to compile, so verification runs on a broken model (e.g. `var` becomes a class `testSuite.var`). 17 is the highest level Spoon 10.4.2's JDT accepts. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/CorrectModernJavaSyntax.java | 32 +++++++++++++++++++ .../liquidjava/api/CommandLineLauncher.java | 2 +- 2 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectModernJavaSyntax.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectModernJavaSyntax.java b/liquidjava-example/src/main/java/testSuite/CorrectModernJavaSyntax.java new file mode 100644 index 000000000..5c310fab2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectModernJavaSyntax.java @@ -0,0 +1,32 @@ +package testSuite; + +import java.io.StringReader; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class CorrectModernJavaSyntax { + + // local variable type inference (Java 10) + void localVar() { + var n = 5; + @Refinement("_ > 0") + int p = n; + } + + // resource reference in try-with-resources (Java 9) + void resourceReference() throws Exception { + StringReader reader = new StringReader("a"); + try (reader) { + reader.read(); + } + } + + // switch expression (Java 14) + int switchExpression(int k) { + return switch (k) { + case 0 -> 1; + default -> 2; + }; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 621e8c2b0..49dc58be1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -70,7 +70,7 @@ public static void launch(String... paths) { env.setSourceClasspath( new String[] { new File(Refinement.class.getProtectionDomain().getCodeSource().getLocation().getFile()) .getAbsolutePath() }); - env.setComplianceLevel(8); + env.setComplianceLevel(17); boolean buildSuccess = launcher.getModelBuilder().build(); if (!buildSuccess && (env.getErrorCount() > 0 || env.getWarningCount() > 0)) { From 29e8641f6c87173b99db65f5f21669e9dfa71a10 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 7 Oct 2026 11:32:49 +0100 Subject: [PATCH 2/3] Read the compliance level from the project's pom.xml Spoon's compliance level is now taken from the nearest pom.xml of the verified paths (compiler plugin release/source, then the maven.compiler.release/source properties, walking up to enclosing poms). It defaults to 19 when no pom declares one and is capped at 19, the highest level Spoon 10.4.2's JDT accepts. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/api/CommandLineLauncher.java | 6 +- .../java/liquidjava/api/ComplianceLevel.java | 148 ++++++++++++++++++ .../api/tests/TestComplianceLevel.java | 72 +++++++++ 3 files changed, 225 insertions(+), 1 deletion(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 49dc58be1..f10d9abef 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -3,6 +3,7 @@ import java.io.File; import java.util.Arrays; +import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.warnings.CustomWarning; @@ -70,7 +71,10 @@ public static void launch(String... paths) { env.setSourceClasspath( new String[] { new File(Refinement.class.getProtectionDomain().getCodeSource().getLocation().getFile()) .getAbsolutePath() }); - env.setComplianceLevel(17); + int complianceLevel = ComplianceLevel.resolve(paths); + if (DebugLog.enabled()) + System.out.println("Java compliance level: " + complianceLevel); + env.setComplianceLevel(complianceLevel); boolean buildSuccess = launcher.getModelBuilder().build(); if (!buildSuccess && (env.getErrorCount() > 0 || env.getWarningCount() > 0)) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java b/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java new file mode 100644 index 000000000..dfbfb4dd4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java @@ -0,0 +1,148 @@ +package liquidjava.api; + +import java.io.File; +import java.io.FileReader; +import java.util.List; +import java.util.Optional; +import java.util.Properties; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import org.apache.maven.model.Build; +import org.apache.maven.model.Model; +import org.apache.maven.model.Plugin; +import org.apache.maven.model.io.xpp3.MavenXpp3Reader; +import org.codehaus.plexus.util.xml.Xpp3Dom; + +/** + * Resolves the Java compliance level used by Spoon to parse the verified sources, read from the nearest Maven + * {@code pom.xml} of each input path. + */ +public final class ComplianceLevel { + + /** Highest level accepted by Spoon 10.4.2 (JDT 3.33); higher levels make the model builder throw */ + public static final int MAX_SUPPORTED = 19; + + /** Level used when no {@code pom.xml} declares one */ + public static final int DEFAULT = MAX_SUPPORTED; + + private static final Pattern PROPERTY_REF = Pattern.compile("\\$\\{([^}]+)\\}"); + + private ComplianceLevel() { + } + + /** + * Returns the highest level declared by the poms of the given paths, capped at {@link #MAX_SUPPORTED}, or + * {@link #DEFAULT} if none declares one + */ + public static int resolve(String... paths) { + int level = -1; + for (String path : paths) { + Optional declared = fromMaven(new File(path)); + if (declared.isPresent()) + level = Math.max(level, declared.get()); + } + if (level < 0) + return DEFAULT; + return Math.min(level, MAX_SUPPORTED); + } + + /** + * Searches upwards from the path for a {@code pom.xml} that declares a Java version, so a module without one + * inherits it from the enclosing project + */ + static Optional fromMaven(File path) { + File dir = path.getAbsoluteFile(); + if (!dir.isDirectory()) + dir = dir.getParentFile(); + for (; dir != null; dir = dir.getParentFile()) { + File pom = new File(dir, "pom.xml"); + if (pom.isFile()) { + Optional level = readPom(pom); + if (level.isPresent()) + return level; + } + } + return Optional.empty(); + } + + /** + * Reads the Java version from the compiler plugin configuration or the {@code maven.compiler.*} properties, + * preferring {@code release} over {@code source} as Maven does + */ + static Optional readPom(File pom) { + Model model; + try (FileReader reader = new FileReader(pom)) { + model = new MavenXpp3Reader().read(reader); + } catch (Exception e) { + return Optional.empty(); + } + Properties properties = model.getProperties(); + Xpp3Dom config = compilerConfiguration(model.getBuild()); + String[] candidates = { childValue(config, "release"), properties.getProperty("maven.compiler.release"), + childValue(config, "source"), properties.getProperty("maven.compiler.source") }; + for (String candidate : candidates) { + Optional level = parseLevel(interpolate(candidate, properties)); + if (level.isPresent()) + return level; + } + return Optional.empty(); + } + + private static Xpp3Dom compilerConfiguration(Build build) { + if (build == null) + return null; + Xpp3Dom config = compilerConfiguration(build.getPlugins()); + if (config == null && build.getPluginManagement() != null) + config = compilerConfiguration(build.getPluginManagement().getPlugins()); + return config; + } + + private static Xpp3Dom compilerConfiguration(List plugins) { + for (Plugin plugin : plugins) { + if ("maven-compiler-plugin".equals(plugin.getArtifactId()) && plugin.getConfiguration() instanceof Xpp3Dom) + return (Xpp3Dom) plugin.getConfiguration(); + } + return null; + } + + private static String childValue(Xpp3Dom config, String name) { + if (config == null || config.getChild(name) == null) + return null; + return config.getChild(name).getValue(); + } + + /** + * Replaces {@code ${name}} references with the pom properties, leaving unknown ones in place + */ + private static String interpolate(String value, Properties properties) { + if (value == null) + return null; + for (int i = 0; i < 10; i++) { + Matcher matcher = PROPERTY_REF.matcher(value); + if (!matcher.find()) + break; + String replacement = properties.getProperty(matcher.group(1)); + if (replacement == null) + break; + value = matcher.replaceFirst(Matcher.quoteReplacement(replacement)); + } + return value; + } + + /** + * Parses a Java version such as {@code 17} or {@code 1.8} + */ + static Optional parseLevel(String value) { + if (value == null) + return Optional.empty(); + String version = value.trim(); + if (version.startsWith("1.")) + version = version.substring(2); + try { + return Optional.of(Integer.parseInt(version)); + } catch (NumberFormatException e) { + return Optional.empty(); + } + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java new file mode 100644 index 000000000..5a9b01e33 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java @@ -0,0 +1,72 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.io.TempDir; + +import liquidjava.api.ComplianceLevel; + +class TestComplianceLevel { + + @TempDir + Path project; + + private Path source() throws IOException { + Path src = Files.createDirectories(project.resolve("src/main/java")); + return Files.writeString(src.resolve("A.java"), "class A {}"); + } + + private void writePom(Path dir, String properties, String compilerConfig) throws IOException { + String plugin = compilerConfig == null ? "" + : "maven-compiler-plugin" + + compilerConfig + ""; + Files.writeString(dir.resolve("pom.xml"), + "4.0.0ga" + + "1" + properties + "" + plugin + ""); + } + + @Test + void defaultsWithoutPom() throws IOException { + assertEquals(ComplianceLevel.DEFAULT, ComplianceLevel.resolve(source().toString())); + } + + @Test + void readsCompilerProperties() throws IOException { + writePom(project, "11", null); + assertEquals(11, ComplianceLevel.resolve(source().toString())); + } + + @Test + void prefersReleaseOverSource() throws IOException { + writePom(project, + "1117", + null); + assertEquals(17, ComplianceLevel.resolve(source().toString())); + } + + @Test + void readsPluginConfigurationWithPropertyReference() throws IOException { + writePom(project, "1.8", "${java.version}"); + assertEquals(8, ComplianceLevel.resolve(source().toString())); + } + + @Test + void inheritsFromEnclosingPom() throws IOException { + writePom(project, "16", null); + Path module = Files.createDirectories(project.resolve("module")); + writePom(module, "", null); + Path src = Files.createDirectories(module.resolve("src")); + assertEquals(16, ComplianceLevel.resolve(src.toString())); + } + + @Test + void capsAtMaxSupported() throws IOException { + writePom(project, "25", null); + assertEquals(ComplianceLevel.MAX_SUPPORTED, ComplianceLevel.resolve(source().toString())); + } +} From 9a75214ea8b0061955655e0d5054ea3b8c7edbd7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 7 Oct 2026 11:51:03 +0100 Subject: [PATCH 3/3] Simplify ComplianceLevel to read only the maven.compiler properties Co-Authored-By: Claude Opus 5.5 --- .../java/liquidjava/api/ComplianceLevel.java | 142 +++--------------- .../api/tests/TestComplianceLevel.java | 53 +------ 2 files changed, 26 insertions(+), 169 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java b/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java index dfbfb4dd4..901824246 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/ComplianceLevel.java @@ -2,147 +2,41 @@ import java.io.File; import java.io.FileReader; -import java.util.List; +import java.util.Arrays; import java.util.Optional; import java.util.Properties; -import java.util.regex.Matcher; -import java.util.regex.Pattern; -import org.apache.maven.model.Build; -import org.apache.maven.model.Model; -import org.apache.maven.model.Plugin; import org.apache.maven.model.io.xpp3.MavenXpp3Reader; -import org.codehaus.plexus.util.xml.Xpp3Dom; /** - * Resolves the Java compliance level used by Spoon to parse the verified sources, read from the nearest Maven - * {@code pom.xml} of each input path. + * Java compliance level used by Spoon, read from the {@code maven.compiler.release} or {@code maven.compiler.source} + * property of the nearest {@code pom.xml} of the verified paths */ public final class ComplianceLevel { - /** Highest level accepted by Spoon 10.4.2 (JDT 3.33); higher levels make the model builder throw */ + /** Highest level accepted by Spoon 10.4.2 (JDT 3.33), also used when no pom declares one */ public static final int MAX_SUPPORTED = 19; - /** Level used when no {@code pom.xml} declares one */ - public static final int DEFAULT = MAX_SUPPORTED; - - private static final Pattern PROPERTY_REF = Pattern.compile("\\$\\{([^}]+)\\}"); - - private ComplianceLevel() { - } - - /** - * Returns the highest level declared by the poms of the given paths, capped at {@link #MAX_SUPPORTED}, or - * {@link #DEFAULT} if none declares one - */ public static int resolve(String... paths) { - int level = -1; - for (String path : paths) { - Optional declared = fromMaven(new File(path)); - if (declared.isPresent()) - level = Math.max(level, declared.get()); - } - if (level < 0) - return DEFAULT; - return Math.min(level, MAX_SUPPORTED); + return Arrays.stream(paths).map(path -> fromPom(new File(path).getAbsoluteFile())).flatMap(Optional::stream) + .max(Integer::compare).map(level -> Math.min(level, MAX_SUPPORTED)).orElse(MAX_SUPPORTED); } - /** - * Searches upwards from the path for a {@code pom.xml} that declares a Java version, so a module without one - * inherits it from the enclosing project - */ - static Optional fromMaven(File path) { - File dir = path.getAbsoluteFile(); - if (!dir.isDirectory()) - dir = dir.getParentFile(); - for (; dir != null; dir = dir.getParentFile()) { + private static Optional fromPom(File path) { + for (File dir = path; dir != null; dir = dir.getParentFile()) { File pom = new File(dir, "pom.xml"); - if (pom.isFile()) { - Optional level = readPom(pom); - if (level.isPresent()) - return level; + if (!pom.isFile()) + continue; + try (FileReader reader = new FileReader(pom)) { + Properties properties = new MavenXpp3Reader().read(reader).getProperties(); + String version = properties.getProperty("maven.compiler.release", + properties.getProperty("maven.compiler.source")); + if (version != null) + return Optional.of(Integer.parseInt(version.trim().replaceFirst("^1\\.", ""))); + } catch (Exception ignored) { + // unreadable pom or non-numeric version: keep searching enclosing poms } } return Optional.empty(); } - - /** - * Reads the Java version from the compiler plugin configuration or the {@code maven.compiler.*} properties, - * preferring {@code release} over {@code source} as Maven does - */ - static Optional readPom(File pom) { - Model model; - try (FileReader reader = new FileReader(pom)) { - model = new MavenXpp3Reader().read(reader); - } catch (Exception e) { - return Optional.empty(); - } - Properties properties = model.getProperties(); - Xpp3Dom config = compilerConfiguration(model.getBuild()); - String[] candidates = { childValue(config, "release"), properties.getProperty("maven.compiler.release"), - childValue(config, "source"), properties.getProperty("maven.compiler.source") }; - for (String candidate : candidates) { - Optional level = parseLevel(interpolate(candidate, properties)); - if (level.isPresent()) - return level; - } - return Optional.empty(); - } - - private static Xpp3Dom compilerConfiguration(Build build) { - if (build == null) - return null; - Xpp3Dom config = compilerConfiguration(build.getPlugins()); - if (config == null && build.getPluginManagement() != null) - config = compilerConfiguration(build.getPluginManagement().getPlugins()); - return config; - } - - private static Xpp3Dom compilerConfiguration(List plugins) { - for (Plugin plugin : plugins) { - if ("maven-compiler-plugin".equals(plugin.getArtifactId()) && plugin.getConfiguration() instanceof Xpp3Dom) - return (Xpp3Dom) plugin.getConfiguration(); - } - return null; - } - - private static String childValue(Xpp3Dom config, String name) { - if (config == null || config.getChild(name) == null) - return null; - return config.getChild(name).getValue(); - } - - /** - * Replaces {@code ${name}} references with the pom properties, leaving unknown ones in place - */ - private static String interpolate(String value, Properties properties) { - if (value == null) - return null; - for (int i = 0; i < 10; i++) { - Matcher matcher = PROPERTY_REF.matcher(value); - if (!matcher.find()) - break; - String replacement = properties.getProperty(matcher.group(1)); - if (replacement == null) - break; - value = matcher.replaceFirst(Matcher.quoteReplacement(replacement)); - } - return value; - } - - /** - * Parses a Java version such as {@code 17} or {@code 1.8} - */ - static Optional parseLevel(String value) { - if (value == null) - return Optional.empty(); - String version = value.trim(); - if (version.startsWith("1.")) - version = version.substring(2); - try { - return Optional.of(Integer.parseInt(version)); - } catch (NumberFormatException e) { - return Optional.empty(); - } - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java index 5a9b01e33..d99feb161 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestComplianceLevel.java @@ -16,57 +16,20 @@ class TestComplianceLevel { @TempDir Path project; - private Path source() throws IOException { - Path src = Files.createDirectories(project.resolve("src/main/java")); - return Files.writeString(src.resolve("A.java"), "class A {}"); - } - - private void writePom(Path dir, String properties, String compilerConfig) throws IOException { - String plugin = compilerConfig == null ? "" - : "maven-compiler-plugin" - + compilerConfig + ""; - Files.writeString(dir.resolve("pom.xml"), - "4.0.0ga" - + "1" + properties + "" + plugin + ""); - } - - @Test - void defaultsWithoutPom() throws IOException { - assertEquals(ComplianceLevel.DEFAULT, ComplianceLevel.resolve(source().toString())); - } - - @Test - void readsCompilerProperties() throws IOException { - writePom(project, "11", null); - assertEquals(11, ComplianceLevel.resolve(source().toString())); - } - - @Test - void prefersReleaseOverSource() throws IOException { - writePom(project, - "1117", - null); - assertEquals(17, ComplianceLevel.resolve(source().toString())); - } - - @Test - void readsPluginConfigurationWithPropertyReference() throws IOException { - writePom(project, "1.8", "${java.version}"); - assertEquals(8, ComplianceLevel.resolve(source().toString())); + private int resolveWithRelease(String release) throws IOException { + Files.writeString(project.resolve("pom.xml"), + "4.0.0" + release + + ""); + return ComplianceLevel.resolve(Files.createDirectories(project.resolve("src")).toString()); } @Test - void inheritsFromEnclosingPom() throws IOException { - writePom(project, "16", null); - Path module = Files.createDirectories(project.resolve("module")); - writePom(module, "", null); - Path src = Files.createDirectories(module.resolve("src")); - assertEquals(16, ComplianceLevel.resolve(src.toString())); + void readsLevelFromPom() throws IOException { + assertEquals(8, resolveWithRelease("1.8")); } @Test void capsAtMaxSupported() throws IOException { - writePom(project, "25", null); - assertEquals(ComplianceLevel.MAX_SUPPORTED, ComplianceLevel.resolve(source().toString())); + assertEquals(ComplianceLevel.MAX_SUPPORTED, resolveWithRelease("30")); } }