From 773d5ffdeef02d5d210ba609a22cc058e98d2f56 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Jun 2026 11:51:55 +0000 Subject: [PATCH 1/2] JavaToLaurelCompiler: fall back to a 1:1 position for the synthetic URI Strata reports diagnostics for trees injected by a simplification pass against a synthesized "" source path (extracted to the SYNTHETIC_UNKNOWN_PATH constant). Previously a missing line map threw, which masked the real Strata error in the user's verdict. Return a fallback Position(1,1) for that specific synthetic URI so the diagnostic surfaces as a user-visible Verifier error with a stable location (the URI is still reported). Any other unmapped URI keeps the previous fail-fast behaviour, since that indicates a real line-map collection bug we do not want to hide behind a misleading 1:1 location. The synthetic "" path is also not a legal filesystem path on every platform ('<' and '>' are illegal on Windows), so LaurelDriver must not route it through Paths.get: that threw InvalidPathException on windows-2022 (while parsing fine on Linux) before the line-map fallback was ever reached. When Paths.get rejects the path, build the file URI directly via the multi-argument URI constructor (which percent-encodes the illegal characters); getPath() decodes them back, so the fallback's "/" path-suffix match still triggers. StrataDiagnostic.filename() likewise takes the segment after the last '/' instead of Paths.get(...).getFileName(), which had the same latent Windows crash. Adds UnknownLineMapFallbackTest, which drives the verifier on a method with a parameter named `result` (whose Strata `result` collision is reported against the synthetic URI) and asserts the diagnostic surfaces instead of crashing with "Could not find line map"; and LaurelDriverUriTest, a cross-platform unit test locking the synthetic URI construction. Note: that `result` collision is the same one PR #431 fixes (by renaming the user parameter), so the test relies on pre-#431 behaviour to reach the synthetic-URI path; the two PRs are complementary (this surfaces the error, #431 removes the collision). Co-authored-by: Kiro --- .../laurel/JavaToLaurelCompiler.java | 21 +++++++ .../jverify/verifier/laurel/LaurelDriver.java | 42 ++++++++++++- .../verifier/UnknownLineMapFallbackTest.java | 59 +++++++++++++++++++ .../verifier/laurel/LaurelDriverUriTest.java | 28 +++++++++ 4 files changed, 148 insertions(+), 2 deletions(-) create mode 100644 verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java create mode 100644 verifier/src/test/java/org/strata/jverify/verifier/laurel/LaurelDriverUriTest.java diff --git a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java index 60c210d16..29165893b 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java @@ -30,6 +30,10 @@ public class JavaToLaurelCompiler { /// clauses. A 1-parameter postcondition lambda's parameter is renamed /// to this so the clause refers to the return value correctly. private static final String LAUREL_RESULT_BINDING = "result"; + /// javac's synthetic source path for trees injected by a + /// simplification pass; Strata reports diagnostics for them against + /// this URI, which has no entry in our line map. + private static final String SYNTHETIC_UNKNOWN_PATH = "/"; private final JavaLowerer lowerer; private final MethodOrLoopContractCompiler contractCompiler; @@ -93,6 +97,23 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List { var lineMap = lineMaps.get(uri); if (lineMap == null) { + // Strata reports diagnostics for trees injected by a + // simplification pass against a synthesized "" + // source path (e.g. ArrayCompiler's lowering of an + // initializer-list array). For that specific synthetic + // URI, return a 1:1 fallback Position so the diagnostic + // still threads through and surfaces as a user-visible + // Verifier error instead of being masked by an + // exception (the URI is still reported, so a developer + // inspecting raw_stderr can see the synthetic origin). + // + // For any other unmapped URI we keep failing fast: that + // indicates a real line-map collection bug, which we do + // not want to hide behind a misleading 1:1 location. + String path = uri.getPath(); + if (path != null && path.endsWith(SYNTHETIC_UNKNOWN_PATH)) { + return new Position(1, 1); + } throw new RuntimeException("Could not find line map for " + uri); } long line = lineMap.getLineNumber(offset); diff --git a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java index 8831f5cfb..d48c6bd57 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/laurel/LaurelDriver.java @@ -18,7 +18,9 @@ import javax.tools.JavaFileObject; import java.io.IOException; import java.net.URI; +import java.net.URISyntaxException; import java.nio.file.Files; +import java.nio.file.InvalidPathException; import java.nio.file.Paths; import java.util.ArrayList; import java.util.List; @@ -202,7 +204,7 @@ private JVerifyResults parseStrataOutput(FilesMap filesMap, // the source location (reported as 1:1). var uri = filePath.startsWith("file:") ? URI.create(filePath) - : Paths.get(filePath).toUri(); + : toDiagnosticUri(filePath); var range = new Range( filesMap.computePositionFromFileOffset(uri, startOffset), @@ -270,6 +272,36 @@ private JVerifyResults parseStrataOutput(FilesMap filesMap, } + /// Build a URI for a Strata diagnostic's (non-`file:`) source path. + /// Normally this is a real filesystem path, but Strata also reports + /// diagnostics for simplification-injected trees against a synthetic + /// "" path, which is not a legal filesystem path on every + /// platform ('<' and '>' are illegal on Windows). Fall back to a + /// directly constructed file URI in that case so the diagnostic still + /// threads through to the JavaToLaurelCompiler line-map fallback + /// instead of crashing with InvalidPathException. + private static URI toDiagnosticUri(String filePath) { + try { + return Paths.get(filePath).toUri(); + } catch (InvalidPathException e) { + return syntheticFileUri(filePath); + } + } + + /// Construct a `file:` URI from a path that is not a legal filesystem + /// path on this platform. The multi-argument URI constructor + /// percent-encodes illegal characters; getPath() decodes them back, so + /// the line-map fallback's path-suffix match still triggers. + static URI syntheticFileUri(String filePath) { + String path = filePath.startsWith("/") ? filePath : "/" + filePath; + try { + return new URI("file", null, path, null); + } catch (URISyntaxException e) { + throw new RuntimeException( + "Could not construct URI for diagnostic path: " + filePath, e); + } + } + public static class StrataDiagnostic implements Diagnostic, DiagnosticWithRange { private static final int SEVERITY_ERROR = 1; private static final int SEVERITY_WARNING = 2; @@ -307,7 +339,13 @@ public String filePath() { @Override public String filename() { - return Paths.get(uri.getPath()).getFileName().toString(); + // Avoid Paths.get here: the diagnostic URI may be the synthetic + // "" path, which is not a legal filesystem path on + // every platform. URI paths always use '/', so the file name is + // the segment after the last '/'. + String path = uri.getPath(); + int slash = path.lastIndexOf('/'); + return slash >= 0 ? path.substring(slash + 1) : path; } @Override diff --git a/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java b/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java new file mode 100644 index 000000000..d2744309d --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java @@ -0,0 +1,59 @@ +package org.strata.jverify.verifier; + +import org.junit.jupiter.api.Test; +import org.strata.jverify.testengine.JVerifyTestEngine; + +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.List; + +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertNotEquals; + +/** + * Locks the JavaToLaurelCompiler line-map fallback for the synthetic + * {@code } URI: a Strata diagnostic reported against it must surface + * as a user-visible Verifier error rather than crashing with + * "Could not find line map". + * + *

The trigger is a parameter named {@code result}: JVerify renames the + * postcondition lambda's parameter to Strata's canonical {@code result}, so + * both bind {@code result} in the same scope and Strata reports a + * "Duplicate definition 'result'" diagnostic — against the synthetic + * {@code } URI, which has no line-map entry. + * + *

Note: the underlying collision is fixed by #431 (which renames the user + * parameter), so this test relies on the pre-#431 behaviour to exercise the + * synthetic-URI fallback path. A marked-source {@code @JVerifyTest} resource + * is a poor fit here because the diagnostic lands at the synthetic position + * {@code 1:1}, which positional markup can't express cleanly. + */ +public class UnknownLineMapFallbackTest { + + @Test + public void syntheticUnknownUriSurfacesDiagnosticInsteadOfCrashing() throws Exception { + String source = """ + import static org.strata.jverify.JVerify.*; + class ResultParam { + static int identity(int result) { + postcondition((int r) -> r == result); + return result; + } + } + """; + var sourceFile = new SourceFile(Path.of("ResultParam.java"), source); + var options = JVerifyTestEngine.getVerifierOptions( + JVerifyTestEngine.makeJVerifyTestAnnotation(0, 0), null); + + // Without the fallback, the synthetic URI has no line map + // and this throws "Could not find line map"; with it, the Strata + // diagnostic threads through instead. + var results = Driver.getDriver(options) + .verifyJavaFiles(new ArrayList<>(List.of(sourceFile))); + + assertNotEquals(0, results.exitCode(), + "the result-parameter collision should surface as a Verifier error"); + assertFalse(results.diagnostics().isEmpty(), + "a user-visible diagnostic should be reported, not masked by a crash"); + } +} diff --git a/verifier/src/test/java/org/strata/jverify/verifier/laurel/LaurelDriverUriTest.java b/verifier/src/test/java/org/strata/jverify/verifier/laurel/LaurelDriverUriTest.java new file mode 100644 index 000000000..bd990d363 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/laurel/LaurelDriverUriTest.java @@ -0,0 +1,28 @@ +package org.strata.jverify.verifier.laurel; + +import org.junit.jupiter.api.Test; + +import java.net.URI; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Windows-safety regression (#439): a Strata diagnostic reported against the + * synthetic {@code } source path must not be routed through + * {@code Paths.get}, which throws {@code InvalidPathException} on Windows + * ({@code '<'}/{@code '>'} are illegal filename characters). The directly + * constructed URI must still expose a {@code /} path so the + * JavaToLaurelCompiler line-map fallback (a path-suffix match) triggers. + */ +class LaurelDriverUriTest { + + @Test + void syntheticFileUriForUnknownPathIsConstructibleAndFallbackMatchable() { + URI uri = LaurelDriver.syntheticFileUri(""); + // getPath() decodes the percent-encoded '<'/'>' back. + assertEquals("/", uri.getPath()); + assertTrue(uri.getPath().endsWith("/"), + "the line-map fallback matches on the / path suffix"); + } +} From 204bd2cec27fce7f1302e21216ab986ebd2d0fac Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Jun 2026 12:08:28 +0000 Subject: [PATCH 2/2] Thread source ranges into synthesized contract nodes; make the line-map fallback loud Addresses review feedback (keyboardDrummer): a diagnostic on a generated node indicates a synthesis bug, and synthesized nodes should carry a source location from their generating context rather than degrading to 1:1. - JavaToLaurelCompiler now threads toSourceRange(...) from the originating Java tree into every node it synthesizes: method parameters, return types, and the requires / ensures / loop-invariant clauses (previously built with the no-source builder overloads, i.e. SourceRange.NONE). Invariant ranges in particular pair with Strata's per-invariant source ranges (#1361). So a Strata diagnostic on any jverify-synthesized node now points at the user's code. - The line-map fallback is kept as a defense-in-depth net for the residual case where a diagnostic still lands on a node jverify does not construct -- e.g. the result-parameter collision, which Strata reports against its own implicit "result" return binding -- but it is now LOUD: it prints a "[jverify] internal: ... source-less synthesized node" warning naming it a synthesis bug instead of silently returning a misleading 1:1. UnknownLineMapFallbackTest is re-pointed to assert both that the diagnostic surfaces (no crash) and that the residual fallback is flagged loudly. Full verifier suite green (131 run, 0 failures). Co-authored-by: Kiro --- .../laurel/JavaToLaurelCompiler.java | 49 ++++++++++------ .../verifier/UnknownLineMapFallbackTest.java | 56 ++++++++++++------- 2 files changed, 68 insertions(+), 37 deletions(-) diff --git a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java index 29165893b..b2756003b 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java @@ -97,21 +97,25 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List { var lineMap = lineMaps.get(uri); if (lineMap == null) { - // Strata reports diagnostics for trees injected by a - // simplification pass against a synthesized "" - // source path (e.g. ArrayCompiler's lowering of an - // initializer-list array). For that specific synthetic - // URI, return a 1:1 fallback Position so the diagnostic - // still threads through and surfaces as a user-visible - // Verifier error instead of being masked by an - // exception (the URI is still reported, so a developer - // inspecting raw_stderr can see the synthetic origin). + // jverify threads a source range from the generating Java + // tree into every synthesized clause/binding (see the + // requires/ensures/invariant construction above), so a + // diagnostic should normally carry a real user-source + // location. If one still arrives against Strata's synthetic + // "" path, some synthesis site failed to thread its + // source -- a jverify bug. Surface it LOUDLY (so it is not + // hidden behind a misleading location) but do not crash: a + // 1:1 fallback keeps the underlying Strata diagnostic visible + // to the user instead of masking it with an exception. // - // For any other unmapped URI we keep failing fast: that - // indicates a real line-map collection bug, which we do - // not want to hide behind a misleading 1:1 location. + // Any OTHER unmapped URI indicates a real line-map collection + // bug; keep failing fast there. String path = uri.getPath(); if (path != null && path.endsWith(SYNTHETIC_UNKNOWN_PATH)) { + System.err.println("[jverify] internal: a Strata diagnostic was reported " + + "against a source-less synthesized node (" + uri + "); a synthesis " + + "pass did not thread a source range from its generating context. " + + "Falling back to 1:1 -- please report this as a jverify bug."); return new Position(1, 1); } throw new RuntimeException("Could not find line map for " + uri); @@ -378,13 +382,13 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) { List params = new ArrayList<>(); for (var param : method.params) { - params.add(parameter(param.name.toString(), translateType(param.type, param.mods))); + params.add(parameter(toSourceRange(param), param.name.toString(), translateType(param.type, param.mods))); } Optional retType = Optional.empty(); if (method.restype != null && method.restype.type != null && method.restype.type.getTag() != TypeTag.VOID) { - retType = Optional.of(returnType(translateType(method.restype.type))); + retType = Optional.of(returnType(toSourceRange(method.restype), translateType(method.restype.type))); } List requires = new ArrayList<>(); @@ -398,7 +402,11 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) { StmtExpr converted = (preExpr instanceof JCTree.JCLambda lambda) ? convertLambdaBody(lambda, Map.of()) : convertExpression(preExpr); - requires.add(requiresClause(converted, Optional.empty())); + // Thread the originating clause's source range so a + // Strata diagnostic on this (possibly renamed/synthesized) + // clause points at the user's precondition rather than the + // synthetic "" path. + requires.add(requiresClause(toSourceRange(preExpr), converted, Optional.empty())); } for (var post : contract.postconditions()) { var postExpr = post.get(); @@ -412,9 +420,14 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) { Map renames = lambda.params.size() == 1 ? Map.of(lambda.params.getFirst().name.toString(), LAUREL_RESULT_BINDING) : Map.of(); - ensures.add(ensuresClause(convertLambdaBody(lambda, renames), Optional.empty())); + // Thread the postcondition lambda's source range: when + // the renamed `result` binding collides with a user + // parameter, Strata's duplicate-definition diagnostic + // then points at this `ensures` clause instead of the + // synthetic "" path. + ensures.add(ensuresClause(toSourceRange(postExpr), convertLambdaBody(lambda, renames), Optional.empty())); } else { - ensures.add(ensuresClause(convertExpression(postExpr), Optional.empty())); + ensures.add(ensuresClause(toSourceRange(postExpr), convertExpression(postExpr), Optional.empty())); } } @@ -717,7 +730,7 @@ private LoopParts extractLoopParts(JCTree.JCStatement body, Map MethodOrLoopContract loopContract = contractCompiler.getContract(loopBlock); List invariants = new ArrayList<>(); for (var inv : loopContract.loopInvariants()) { - invariants.add(invariantClause(convertExpression(inv.get(), renames))); + invariants.add(invariantClause(toSourceRange(inv.get()), convertExpression(inv.get(), renames))); } var implStatements = MethodOrLoopContractCompiler.getImplementationStatements(loopBlock); List stmts = new ArrayList<>(); diff --git a/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java b/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java index d2744309d..976174c95 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java @@ -3,35 +3,41 @@ import org.junit.jupiter.api.Test; import org.strata.jverify.testengine.JVerifyTestEngine; +import java.io.ByteArrayOutputStream; +import java.io.PrintStream; +import java.nio.charset.StandardCharsets; import java.nio.file.Path; import java.util.ArrayList; import java.util.List; import static org.junit.jupiter.api.Assertions.assertFalse; import static org.junit.jupiter.api.Assertions.assertNotEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; /** - * Locks the JavaToLaurelCompiler line-map fallback for the synthetic - * {@code } URI: a Strata diagnostic reported against it must surface - * as a user-visible Verifier error rather than crashing with - * "Could not find line map". + * Locks the JavaToLaurelCompiler behaviour when Strata reports a diagnostic + * against the synthetic {@code } URI (a node with no source in our + * line map): it must (1) surface as a user-visible Verifier error rather than + * crashing with "Could not find line map", and (2) be flagged LOUDLY as a + * synthesis bug rather than silently degrading to a misleading {@code 1:1}. * *

The trigger is a parameter named {@code result}: JVerify renames the - * postcondition lambda's parameter to Strata's canonical {@code result}, so - * both bind {@code result} in the same scope and Strata reports a - * "Duplicate definition 'result'" diagnostic — against the synthetic - * {@code } URI, which has no line-map entry. + * postcondition lambda's parameter to Strata's canonical {@code result}, so it + * collides with Strata's implicit {@code result} return binding and + * Strata reports "Duplicate definition 'result'". That diagnostic lands on the + * return binding — a node JVerify does not construct, so it has no source even + * though JVerify now threads source ranges into everything it does + * synthesize (parameters, return types, requires/ensures/invariant clauses). + * Hence this case exercises the residual, now-loud fallback. * - *

Note: the underlying collision is fixed by #431 (which renames the user - * parameter), so this test relies on the pre-#431 behaviour to exercise the - * synthetic-URI fallback path. A marked-source {@code @JVerifyTest} resource - * is a poor fit here because the diagnostic lands at the synthetic position - * {@code 1:1}, which positional markup can't express cleanly. + *

Note: the underlying collision is removed by #431 (which renames the user + * parameter), so this test relies on pre-#431 behaviour to reach the + * synthetic-URI path. */ public class UnknownLineMapFallbackTest { @Test - public void syntheticUnknownUriSurfacesDiagnosticInsteadOfCrashing() throws Exception { + public void syntheticUnknownUriSurfacesDiagnosticLoudlyInsteadOfCrashing() throws Exception { String source = """ import static org.strata.jverify.JVerify.*; class ResultParam { @@ -45,15 +51,27 @@ static int identity(int result) { var options = JVerifyTestEngine.getVerifierOptions( JVerifyTestEngine.makeJVerifyTestAnnotation(0, 0), null); - // Without the fallback, the synthetic URI has no line map - // and this throws "Could not find line map"; with it, the Strata - // diagnostic threads through instead. - var results = Driver.getDriver(options) - .verifyJavaFiles(new ArrayList<>(List.of(sourceFile))); + // Capture stderr to assert the fallback flags the synthesis bug loudly. + var captured = new ByteArrayOutputStream(); + var savedErr = System.err; + JVerifyResults results; + try { + System.setErr(new PrintStream(captured, true, StandardCharsets.UTF_8)); + // Without the fallback the synthetic URI has no line map + // and this throws "Could not find line map"; with it, the Strata + // diagnostic threads through instead. + results = Driver.getDriver(options) + .verifyJavaFiles(new ArrayList<>(List.of(sourceFile))); + } finally { + System.setErr(savedErr); + } assertNotEquals(0, results.exitCode(), "the result-parameter collision should surface as a Verifier error"); assertFalse(results.diagnostics().isEmpty(), "a user-visible diagnostic should be reported, not masked by a crash"); + assertTrue(captured.toString(StandardCharsets.UTF_8).contains("source-less synthesized node"), + "the residual synthetic-URI fallback must be flagged loudly as a synthesis bug, " + + "not silently degraded to a 1:1 location"); } }