From fe020b394c77ac05a8b615964f0dc972283657b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Jun 2026 21:02:23 +0000 Subject: [PATCH] JavaToLaurel: support `null` / reference-constant comparisons and values MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. Per review feedback (keyboardDrummer, fabiomadge): this per-sort null encoding is a stop-gap until Laurel gains first-class nullable support (a shared `Null` value + `Nullable` with implicit conversions). The `NULL_REF_SUFFIX` doc records that plan, and a note at the `S$null` emission site records the soundness assumption it relies on — per-sort nulls are sound only while composite sorts carry no subtyping, so a value of one sort is never compared against another sort's null; if upcasting between composite sorts becomes expressible this would turn unsound, motivating the eventual single shared `Null`. Adds NullReferenceLimitationsTest pinning the deliberate limitations as should-fail: an unconstrained reference is proved neither null nor non-null, and a freshly allocated object is not provably non-null. Co-authored-by: Kiro --- .../laurel/JavaToLaurelCompiler.java | 161 +++++++++++++++++- .../NullReferenceLimitationsTest.java | 49 ++++++ .../tests/javasupport/NullReferenceTest.java | 57 +++++++ 3 files changed, 263 insertions(+), 4 deletions(-) create mode 100644 verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceLimitationsTest.java create mode 100644 verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceTest.java 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 b2756003..9d439d89 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 @@ -34,6 +34,27 @@ public class JavaToLaurelCompiler { /// 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 = "/"; + /// Suffix for the per-sort uninterpreted null-reference function + /// (`$null`) used to model `x == null` / `x != null` and standalone + /// `null` values on object references (which translate to opaque + /// composite sorts). + /// + ///

STOP-GAP. This per-sort null encoding is a front-end workaround + /// until Laurel gains first-class nullable support. The intended Laurel + /// model is: + ///

    + ///
  • a shared {@code Null} value and a {@code Nullable} type; and
    • + ///
  • implicit conversions between {@code Nullable} and {@code T}, so + /// the front-end can translate {@code @Nullable Object x} to + /// {@code var x: Nullable} and let Laurel insert the + /// conversions. + /// + /// Until then, {@code null} is modelled here as a distinguished element + /// {@code $null} of each reference sort. This should be removed in + /// favour of the Laurel model once it lands. See {@code NullReferenceTest} + /// for what this supports and {@code NullReferenceLimitationsTest} for what + /// it deliberately does not. + private static final String NULL_REF_SUFFIX = "$null"; private final JavaLowerer lowerer; private final MethodOrLoopContractCompiler contractCompiler; @@ -85,6 +106,30 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List$null` yields a distinguished value of the sort, so + // `x == null` / `x != null` and standalone null on a + // reference of this type can be modelled. Uninterpreted, so + // the only fact is that it is one fixed element of the sort. + // + // SOUNDNESS ASSUMPTION: `$null` is per-sort — + // `Base$null` and `Sub$null` are distinct opaque elements. + // Composite sorts currently carry NO subtyping (the + // extends-slot passed to `composite(...)` above is always + // Optional.empty()), so a value of one reference sort is + // never compared against another sort's `$null`, and the + // distinct per-sort nulls are sound. If subtyping/upcasting + // between composite sorts ever becomes expressible (a + // subtype value reaching a supertype-typed slot, compared to + // that slot's `$null`), this turns UNSOUND: two equal Java + // nulls would appear distinct. That is exactly the case the + // eventual single shared Laurel `Null` value is meant to + // cover (see NULL_REF_SUFFIX). + commands.add(procedureCommand(function( + typeName + NULL_REF_SUFFIX, List.of(), + Optional.of(returnType(compositeType(typeName))), + Optional.empty(), List.of(), Optional.empty(), + Optional.empty(), Optional.empty()))); } } for (var proc : visitor.procedures) { @@ -279,6 +324,9 @@ private static String qualifiedMethodName(Symbol.MethodSymbol sym) { private class StaticMethodCollector extends TreeScanner { final List procedures = new ArrayList<>(); private int labelCounter = 0; + // Resolved return type of the method currently being translated (null + // for void / none). Used to pick the reference sort for a `return null`. + private com.sun.tools.javac.code.Type currentMethodReturnType = null; /** Label stack entry for break/continue resolution. */ private record LabelEntry(String javaLabel, String breakLabel, String continueLabel) {} @@ -386,6 +434,7 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) { } Optional retType = Optional.empty(); + currentMethodReturnType = (method.restype != null) ? method.restype.type : null; if (method.restype != null && method.restype.type != null && method.restype.type.getTag() != TypeTag.VOID) { retType = Optional.of(returnType(toSourceRange(method.restype), translateType(method.restype.type))); @@ -577,7 +626,7 @@ private StmtExpr convertStatement(JCTree.JCStatement statement, Map { LaurelType type = translateType(varDecl.type, varDecl.mods); Optional optAssign = varDecl.init != null - ? Optional.of(initializer(convertExpression(varDecl.init, renames))) + ? Optional.of(initializer(convertNullable(varDecl.init, varDecl.type, renames))) : Optional.empty(); yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), Optional.of(typeAnnotation(type)), optAssign); @@ -596,7 +645,7 @@ yield varDecl(toSourceRange(varDecl), varDecl.name.toString(), } case JCTree.JCReturn retStmt -> { Optional value = retStmt.expr != null - ? Optional.of(convertExpression(retStmt.expr, renames)) + ? Optional.of(convertNullable(retStmt.expr, currentMethodReturnType, renames)) : Optional.empty(); yield return_(toSourceRange(retStmt), value); } @@ -756,7 +805,8 @@ private StmtExpr convertExpression(JCTree.JCExpression expr, Map case JCTree.JCBinary binary -> convertBinary(binary, renames); case JCTree.JCUnary unary -> convertUnary(unary, renames); case JCTree.JCAssign asgn -> - assign(toSourceRange(asgn), convertExpression(asgn.lhs, renames), convertExpression(asgn.rhs, renames)); + assign(toSourceRange(asgn), convertExpression(asgn.lhs, renames), + convertNullable(asgn.rhs, asgn.lhs.type, renames)); case JCTree.JCConditional cond -> ifThenElse(toSourceRange(cond), convertExpression(cond.cond, renames), convertExpression(cond.truepart, renames), @@ -769,8 +819,32 @@ private StmtExpr convertExpression(JCTree.JCExpression expr, Map var methodSym = (Symbol.MethodSymbol) TreeInfo.symbol(invocation.getMethodSelect()); String calleeName = qualifiedMethodName(methodSym); List args = new ArrayList<>(); + // Per-argument expected types from the resolved callee, so + // a `null` argument picks up the parameter's reference sort. + var calleeSym = com.sun.tools.javac.tree.TreeInfo.symbol(invocation.meth); + List paramTypes = + (calleeSym instanceof Symbol.MethodSymbol ms) + ? ms.type.getParameterTypes() : null; + int argIdx = 0; for (var arg : invocation.args) { - args.add(convertExpression(arg, renames)); + com.sun.tools.javac.code.Type expected; + if (paramTypes != null && argIdx < paramTypes.size()) { + expected = paramTypes.get(argIdx); + } else if (paramTypes != null && !paramTypes.isEmpty() + && calleeSym instanceof Symbol.MethodSymbol vms && vms.isVarArgs() + && paramTypes.get(paramTypes.size() - 1) + instanceof com.sun.tools.javac.code.Type.ArrayType vat) { + // Spread argument beyond the declared parameters: + // it takes the varargs element type, so a `null` + // here picks up the element's reference sort. + expected = vat.elemtype; + } else { + expected = null; + } + args.add(expected != null + ? convertNullable(arg, expected, renames) + : convertExpression(arg, renames)); + argIdx++; } yield call(toSourceRange(invocation), identifier(toSourceRange(invocation), calleeName), args); @@ -859,11 +933,90 @@ private StmtExpr convertConstantValue(SourceRange sr, TypeTag tag, Object v) { return switch (tag) { case BOOLEAN -> literalBool(sr, ((Number) v).intValue() != 0); case CHAR, INT, SHORT, BYTE, LONG -> longLiteral(sr, ((Number) v).longValue()); + case BOT -> throw new JavaViolationException( + "could not determine a concrete class/interface reference type for this `null`. " + + "`null` is supported in `== null` / `!= null` comparisons and, where the target " + + "type is a class/interface reference, in `return`, local initialisers, " + + "assignments, and call arguments; array and type-variable targets are not yet " + + "supported as a standalone `null`"); default -> throw new JavaViolationException("Unsupported constant type tag: " + tag); }; } + /// The distinguished null value of an object reference type: + /// `$null`, an uninterpreted element of the (otherwise opaque) + /// composite sort. Returns {@code null} when {@code type} is not an + /// object reference, so callers can fall back to the normal path. + private StmtExpr nullRefForType(SourceRange sr, com.sun.tools.javac.code.Type type) { + if (type instanceof com.sun.tools.javac.code.Type.ClassType ct) { + String sortName = ct.tsym.getQualifiedName().toString().replace('$', '.'); + referencedCompositeTypes.add(sortName); + return call(sr, identifier(sr, sortName + NULL_REF_SUFFIX), List.of()); + } + return null; + } + + /// Whether {@code expr} is the {@code null} literal (Java's BOT-typed + /// null), peeling enclosing parentheses and casts (e.g. {@code (T) null}). + private static boolean isNullLiteral(JCTree.JCExpression expr) { + JCTree.JCExpression e = expr; + while (true) { + if (e instanceof JCTree.JCParens p) { + e = p.expr; + } else if (e instanceof JCTree.JCTypeCast c && c.expr instanceof JCTree.JCExpression inner) { + e = inner; + } else { + break; + } + } + return e instanceof JCTree.JCLiteral l && l.typetag == TypeTag.BOT; + } + + /// Convert an expression that may be the {@code null} literal, using + /// {@code expectedType} (the use-site target type) to pick the reference + /// sort for a standalone null. Non-null expressions, and bare nulls whose + /// expected type is not an object reference, fall back to the normal path. + private StmtExpr convertNullable(JCTree.JCExpression expr, + com.sun.tools.javac.code.Type expectedType, Map renames) { + if (isNullLiteral(expr)) { + StmtExpr nullRef = nullRefForType(toSourceRange(expr), expectedType); + if (nullRef != null) { + return nullRef; + } + } + return convertExpression(expr, renames); + } + private StmtExpr convertBinary(JCTree.JCBinary binary, Map renames) { + // Reference comparisons against the `null` literal. Object refs + // translate to opaque composite sorts with no built-in null, so a + // comparison is lowered against the sort's distinguished + // `$null` value (see nullRefForType); arrays are never null in + // the map model and fold to a boolean; `null == null` also folds. + if (binary.getTag() == JCTree.Tag.EQ || binary.getTag() == JCTree.Tag.NE) { + boolean lhsNull = isNullLiteral(binary.lhs); + boolean rhsNull = isNullLiteral(binary.rhs); + if (lhsNull && rhsNull) { + SourceRange sr = toSourceRange(binary); + return literalBool(sr, binary.getTag() == JCTree.Tag.EQ); + } + if (lhsNull ^ rhsNull) { + var other = lhsNull ? binary.rhs : binary.lhs; + SourceRange sr = toSourceRange(binary); + if (other.type instanceof com.sun.tools.javac.code.Type.ArrayType) { + return literalBool(sr, binary.getTag() == JCTree.Tag.NE); + } + StmtExpr nullRef = nullRefForType(sr, other.type); + if (nullRef != null) { + StmtExpr otherExpr = convertExpression(other, renames); + return binary.getTag() == JCTree.Tag.EQ + ? eq(sr, otherExpr, nullRef) + : neq(sr, otherExpr, nullRef); + } + // Other reference comparisons (e.g. type variables) fall + // through to the normal path, which surfaces a clear error. + } + } StmtExpr lhs = convertExpression(binary.lhs, renames); StmtExpr rhs = convertExpression(binary.rhs, renames); SourceRange sr = toSourceRange(binary); diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceLimitationsTest.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceLimitationsTest.java new file mode 100644 index 00000000..a1f10ac8 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceLimitationsTest.java @@ -0,0 +1,49 @@ +package org.strata.jverify.verifier.tests.javasupport; + +import org.strata.jverify.testengine.JVerifyTest; + +import static org.strata.jverify.JVerify.check; + +/** + * Deliberate limitations of the stop-gap per-sort {@code $null} null + * model (see {@code JavaToLaurelCompiler.NULL_REF_SUFFIX}). These are the cases + * the eventual Laurel nullable model is meant to handle; pinning them as + * should-fail shows the current model is neither unsound nor over-permissive: + * it treats an unconstrained reference as possibly-{@code null} and + * possibly-non-{@code null}, and cannot invent non-nullness. + * + *

    Companion to {@code NullReferenceTest}, which covers what does + * work. + */ +@JVerifyTest(exitCode = 4, methodsVerified = 1, errorCount = 3) +class NullReferenceLimitationsTest { + + /** + * Not over-permissive: an unconstrained reference cannot be proved + * non-null — it may be the sort's {@code $null} element. + */ + static void cannotProveParamNonNull(Object o) { + check(o != null); +// ^^^^^^^^^^^^^^^^ Error: assertion does not hold + } + + /** + * ...and, symmetrically, cannot be proved null. The model is agnostic + * about an unconstrained reference, not biased either way. + */ + static void cannotProveParamNull(Object o) { + check(o == null); +// ^^^^^^^^^^^^^^^^ Error: assertion does not hold + } + + /** + * A freshly allocated object is not provably non-null: {@code new T(...)} + * lowers to an opaque {@code new_(T)} value carrying no fact that it + * differs from {@code T$null}. + */ + static void cannotProveFreshObjectNonNull() { + Object o = new Object(); + check(o != null); +// ^^^^^^^^^^^^^^^^ Error: assertion does not hold + } +} diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceTest.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceTest.java new file mode 100644 index 00000000..d8219a74 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/NullReferenceTest.java @@ -0,0 +1,57 @@ +package org.strata.jverify.verifier.tests.javasupport; + +import org.strata.jverify.Pure; +import org.strata.jverify.testengine.JVerifyTest; + +import static org.strata.jverify.JVerify.postcondition; +import static org.strata.jverify.JVerify.precondition; + +/** + * Reference comparisons against the {@code null} literal, and standalone + * {@code null} values, now translate to Laurel instead of crashing with + * "Unsupported constant type tag: BOT". + * + *

    An object reference is compared to / assigned the sort's distinguished + * {@code $null} value (an uninterpreted element of the otherwise-opaque + * reference sort). A standalone null picks up its reference sort from the + * use-site expected type (return type, declared local type, assignment target, + * or callee parameter type). + */ +@JVerifyTest(methodsVerified = 7, errorCount = 0) +public class NullReferenceTest { + + /** `o != null` in a precondition. */ + int withNonNullPrecondition(Object o) { + precondition(o != null); + return 5; + } + + /** `o == null` as a value, mirrored in the postcondition. */ + boolean isNull(Object o) { + postcondition((boolean r) -> r == (o == null)); + return o == null; + } + + /** `return null` — sort taken from the return type. */ + Object returnsNull() { + return null; + } + + /** Local initialised to null, then compared (folds to true). */ + boolean localNull() { + postcondition((boolean r) -> r); + Object a = null; + return a == null; + } + + /** Passing `null` as an argument — sort taken from the parameter type. */ + boolean callWithNull() { + postcondition((boolean r) -> r); + return acceptsRef(null); + } + + @Pure + boolean acceptsRef(Object o) { + return o == null; + } +}