JavaToLaurel: support null / reference-constant comparisons and values

[tautschnig]

Object references translate to opaque Laurel compositeType sorts with no built-in null, so any use of the null literal (Java's BOT-typed null) hit convertConstantValue's default and crashed translation with "Unsupported constant type tag: BOT" — methods involving null or reference comparisons could not be emitted or verified.

Model null per reference sort: alongside each opaque composite sort S, declare an uninterpreted 0-arg function S$null : S — a distinguished, otherwise unconstrained element of the sort. Then:

• x == null / x != null on an object reference lower to eq(x, S$null) / neq(x, S$null); on an array (never null in the map model) they fold to a boolean; null == null folds.
• Standalone null values take their reference sort from the use-site expected type: return null; (return type), T a = null; (declared local type), a = null; (assignment target), foo(null) (callee parameter type).

S$null is uninterpreted, so this soundly models reference (in)equality with null without committing to a concrete identity. Helpers: nullRefForType (the S$null value), isNullLiteral (peels parens/casts so (T) null is recognised), convertNullable. Contexts with no known target type (ternary branches, array-element null) still reject a bare null, now with a clear diagnostic.

Adds NullReferenceTest (comparison + return/local/assignment/call-arg null, all verify). Front-end only; no Strata submodule change.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.

[Copilot]

Pull request overview

This PR updates the Java→Laurel front-end to support Java null in reference contexts by introducing a per-reference-sort distinguished null value (<sort>$null) and using that value for == null / != null comparisons and for standalone null where a target type is known. This prevents translation from crashing on BOT-typed null literals and adds a regression test covering the new behavior.

Changes:

• Emit a per-composite-sort uninterpreted null constant function (<sort>$null) and lower reference == null / != null to equality against it.
• Add “nullable” conversion in specific typed contexts (return, local init, assignment, call-arg) so standalone null picks up the expected reference sort.
• Add NullReferenceTest to verify null comparisons and typed null values translate and verify successfully.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java	Adds per-sort null modeling, typed-null conversion helpers, and special-casing for == null / != null.
verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceTest.java	New regression test exercising reference comparisons and typed standalone null uses.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[fabiomadge]

CI is red because this bumps the Strata submodule to 7c5a2132, which isn't pushed to the remote — checkout fails on both platforms (upload-pack: not our ref 7c5a2132…) before anything builds. Looks unintentional (the body says "no Strata submodule change"); resetting the pin to main's 24b8f04e should get CI green. Happy to review the null support then.

[keyboardDrummer]

This is a partial solution right? I don't know by heart but I imagine there are quite some cases that it doesn't handle. For example, it can't prove that a fresh object is not null, right? Could we add a few test-cases that show the limitations of this approach?

The solution I had in mind for supporting nullable types was on the Laurel side, but it will take quite a bit more time to implement it. Could we add comments to the code added in this PR to indicate that this solution is a stop-gap until Laurel has better support for this?

The Laurel support I have in mind is to support "implicit conversions" that allow Laurel to insert conversions to translate between types (Nullable<T> and T in this case) and to translate @Nullable Object x to var x: Nullable<Object>.

On top of that, we could even added dedicated Nullable support to Laurel, adding a Null value and a Nullable type.

[fabiomadge]

+1 on the Laurel plan and the stop-gap comment. One thing worth pinning beyond "temporary": S$null is per-sort (Base$null and Sub$null are distinct opaque elements), and composite sorts carry no subtyping (the composite(...) extends-slot is always empty). That's fine as long as a value of one reference sort never has to compare against another sort's $null. If subtyping/upcasting between composite sorts becomes expressible — a subtype value reaching a supertype-typed slot compared to its $null — the per-sort nulls would turn unsound (identical Java nulls appearing distinct). Worth a note at the S$null site recording that assumption; it's also why the eventual Laurel model wants a single shared Null.

Minor: no negative test — a should-fail case (o == null on an unconstrained o) would pin the model isn't over-permissive.

[tautschnig]

@fabiomadge Strata pin is back to main’s 24b8f04e in fe020b3 (front-end only, no submodule bump), so checkout should be green. Also added the per-sort/no-subtyping soundness note at the S$null site and a negative test (o == null / o != null on an unconstrained ref both fail to prove). Thanks!

[tautschnig]

@keyboardDrummer Agreed it’s a stop-gap — marked as such in the NULL_REF_SUFFIX doc, pointing at the Nullable<T> / shared-Null Laurel plan, and added NullReferenceLimitationsTest for the limits (unconstrained ref proved neither null nor non-null; a fresh object not provably non-null). All in fe020b3.

[keyboardDrummer]

Just a FYI: the design of JVerify is to assume that all reference variables are non-null, unless annotated with @Nullable.