JavaToLaurelCompiler: fall back to a 1:1 position for unknown line maps - #439
Conversation
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Adjusts Java→Laurel analysis error handling so Strata diagnostics tied to synthetic/unknown URIs surface to users instead of being masked by an internal exception.
Changes:
- Replace a hard failure on missing
lineMapwith a fallbackPosition(1, 1)and explanatory comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
308b9d1 to
d8af4ee
Compare
fabiomadge
left a comment
fabiomadge
left a comment
There was a problem hiding this comment.
Correct and well-scoped — narrowing the fallback to the synthetic /<unknown> URI (and keeping fail-fast for any other unmapped URI) is the right call; a blanket 1:1 fallback would hide real line-map collection bugs.
Verified it does what it claims: applied it alone and re-ran a case that previously crashed with Could not find line map (a method with a result parameter, from #431). It now surfaces the real Strata diagnostic — Duplicate definition 'result' is already defined in this scope — instead of throwing. So this also unmasks the underlying error in #431's scenario; the two are complementary (this makes it visible, #431 fixes the collision).
Two small things: (1) no test — since the whole point is "diagnostic instead of crash," a test that hits the synthetic path and asserts a user-visible error would lock it (the result-param case reliably triggers it); (2) endsWith("/<unknown>") couples to javac's synthetic filename — fine, but a brittle string match.
d8af4ee to
193d5da
Compare
Both addressed in 193d5da. |
6df0ed4 to
88fcc96
Compare
| /// 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 |
There was a problem hiding this comment.
For context, I think that reporting a diagnostic on a generated node indicates a compiler bug. Do you feel the same?
Secondly, I think that despite the above characterization of a bug, that for debugging purposes, it's better to give all synthesis nodes a source location. That source location should originate from the context that is generating the node. Getting a (1,1) diagnostic at any point is quite frustrating for debugging. What do you think?
There was a problem hiding this comment.
Agreed on both counts.
(1) Yes — a user-facing diagnostic on a source-less generated node is a defect on our side. Here it was mostly that JavaToLaurelCompiler built parameters, return types, and the requires/ensures/invariant clauses through the no-source builder overloads (SourceRange.NONE) despite the originating Java tree having a real range.
(2) Agreed — fixed in 204bd2c: it now threads toSourceRange(<originating tree>) into everything it synthesizes (parameters, return types, requires/ensures/loop-invariant clauses; the invariant ranges pair with #1361). So a diagnostic on any node jverify constructs now points at the user's code.
Honest caveat: this PR's result-collision trigger isn't reported against a node jverify builds — Strata raises it against its own implicit result return binding, which we never construct, so there's no source to thread. For that residual class I kept the fallback but made it loud (a [jverify] internal: … source-less synthesized node … warning naming it a synthesis bug) rather than a silent 1:1 — surfacing (1) instead of hiding it. (#431 removes this collision anyway -- I'll return to that PR next, trying to address it at the Laurel source as suggested in #431.)
…unknown> URI
Strata reports diagnostics for trees injected by a simplification pass
against a synthesized "<unknown>" 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 "<unknown>" 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
"/<unknown>" 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 <unknown> 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 strata-org#431 fixes (by renaming
the user parameter), so the test relies on pre-strata-org#431 behaviour to reach
the synthetic-URI path; the two PRs are complementary (this surfaces the
error, strata-org#431 removes the collision).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ap 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 <unknown> 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 <kiro-agent@users.noreply.github.com>
88fcc96 to
204bd2c
Compare
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Looks good, thanks!
|
|
||
| @Test | ||
| public void syntheticUnknownUriSurfacesDiagnosticLoudlyInsteadOfCrashing() throws Exception { | ||
| String source = """ |
There was a problem hiding this comment.
I'm guessing this test will break when we solve the Laurel/Strata bug, right?
There was a problem hiding this comment.
It actually should, yes.
What was changed?
When Strata reports a diagnostic for a node that carries no source location, it serializes it against a synthesized
<unknown>source path, which has no entry in our line map. Previously a missing line map threw, masking the real Strata error in the user's verdict.This PR addresses that at the root:
JavaToLaurelCompilernow threads a source range from the originating Java tree into every node it synthesizes — method parameters, return types, and therequires/ensures/ loop-invariant clauses (all previously constructed with the no-source builder overloads, i.e.SourceRange.NONE). The loop-invariant ranges pair with Strata's per-invariant source ranges (#1361). So a Strata diagnostic on any node jverify constructs now points at the user's code instead of<unknown>.For the residual case where a diagnostic still lands on a node jverify does not construct (e.g. Strata's implicit
resultreturn binding — see the test below), the<unknown>fallback is kept as defense-in-depth but is now loud: it emits a[jverify] internal: … source-less synthesized node …warning naming it a synthesis bug, instead of silently returning a misleading1:1. 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.How has this been tested?
UnknownLineMapFallbackTestdrives the verifier on a method with a parameter namedresult(whose Strataresultcollision is reported against the synthetic<unknown>URI) and asserts the diagnostic surfaces — rather than crashing withCould not find line map— and that the residual fallback is flagged loudly. Full verifier suite green (131 run, 0 failures). Verified it fails (with the crash) when the fallback is removed.Note: coupling with #431
The
result-parameter collision used as the trigger is the same one PR #431 fixes (by renaming the user parameter). The two are complementary — this one makes the error visible (and points jverify-synthesized diagnostics at real locations), #431 removes the collision. Consequently the test relies on pre-#431 behaviour to reach the synthetic-URI path.