JavaToLaurelCompiler: fall back to a 1:1 position for unknown line maps

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 = "/<unknown>";
 
     private final JavaLowerer lowerer;
     private final MethodOrLoopContractCompiler contractCompiler;
@@ -93,6 +97,27 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List<Java
         FilesMap filesMap = (uri, offset) -> {
             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
+                // "<unknown>" 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<Parameter> 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<ReturnType> 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<RequiresClause> 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 "<unknown>" 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<String, String> 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 "<unknown>" 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<String, String>
                 MethodOrLoopContract loopContract = contractCompiler.getContract(loopBlock);
                 List<InvariantClause> 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<StmtExpr> stmts = new ArrayList<>();

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
+    /// "<unknown>" 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<JavaFileObject>, 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
+            // "<unknown>" 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

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 <unknown>} 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}.
+ *
+ * <p>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} <em>return</em> 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 <em>does</em>
+ * synthesize (parameters, return types, requires/ensures/invariant clauses).
+ * Hence this case exercises the residual, now-loud fallback.
+ *
+ * <p>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 <unknown> 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");
+    }
+}

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 <unknown>} 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 /<unknown>} path so the
+ * JavaToLaurelCompiler line-map fallback (a path-suffix match) triggers.
+ */
+class LaurelDriverUriTest {
+
+    @Test
+    void syntheticFileUriForUnknownPathIsConstructibleAndFallbackMatchable() {
+        URI uri = LaurelDriver.syntheticFileUri("<unknown>");
+        // getPath() decodes the percent-encoded '<'/'>' back.
+        assertEquals("/<unknown>", uri.getPath());
+        assertTrue(uri.getPath().endsWith("/<unknown>"),
+                "the line-map fallback matches on the /<unknown> path suffix");
+    }
+}