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..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 @@ -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,27 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List { var lineMap = lineMaps.get(uri); if (lineMap == null) { + // 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. + // + // 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); } long line = lineMap.getLineNumber(offset); @@ -357,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<>(); @@ -377,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(); @@ -391,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())); } } @@ -696,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/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..976174c95 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/UnknownLineMapFallbackTest.java @@ -0,0 +1,77 @@ +package org.strata.jverify.verifier; + +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 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 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 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 syntheticUnknownUriSurfacesDiagnosticLoudlyInsteadOfCrashing() 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); + + // 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"); + } +} 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"); + } +}