JavaToLaurelCompiler: collapse reference comparison against null to a constant - #438
JavaToLaurelCompiler: collapse reference comparison against null to a constant#438tautschnig wants to merge 1 commit into
Conversation
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Adds an early rewrite in the Java→Laurel compiler to treat == null / != null as constant booleans (since the Laurel model has no null), avoiding literal conversion for BOT-typed null literals.
Changes:
- Detects
EQ/NEcomparisons where either operand is anullliteral (TypeTag.BOT) - Rewrites those comparisons to boolean constants prior to recursive operand conversion
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
In JVerify's array-as-map model an array-typed value is never null, so `arr == null` / `arr != null` (detected via a BOT-typed null literal operand) is folded to a boolean constant (false / true respectively) before operand conversion. This keeps the BOT-typed literal off the convertLiteral path. The fold is restricted to comparisons whose non-null operand is array-typed, so it does not silently mask the nullability of ordinary object references — those fall through to the normal conversion path. The degenerate `null == null` / `null != null` case folds to true / false respectively. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
2589d34 to
5270d6a
Compare
fabiomadge
left a comment
fabiomadge
left a comment
There was a problem hiding this comment.
This is unreachable until array support lands — array-typed operands error at translateType today (verified), so arr == null never reaches this fold. #441 (array support) is what makes it reachable, and notably #441 doesn't need this — it doesn't touch arr == null handling at all.
Suggestion: punt this until arrays land, and fold it into #441 (or a follow-up on top of it). Reasons: (1) it can't be tested in isolation today; (2) the "arrays are never null" assumption is only meaningful once #441's mapType(int, int) model exists — at which point it's verifiable; (3) the instanceof Type.ArrayType check would also match @Nullable int[], harmless now (@Nullable is a no-op — isNullable has zero call sites) but worth settling alongside the real array+null model rather than ahead of it.
The logic itself looks reasonable; it's just landing ahead of the thing it depends on.
In JVerify's array-as-map model an array-typed value is never null, so
arr == null/arr != null(detected via a BOT-typed null-literal operand) is folded to a boolean constant —false/truerespectively — before operand conversion. This keeps the BOT-typed null literal off theconvertLiteralpath.The fold is restricted to comparisons whose non-null operand is array-typed (map-backed), so it does not silently mask the nullability of ordinary object references — those fall through to the normal conversion path. The degenerate
null == null/null != nullcase folds totrue/falserespectively.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.