From 5270d6ab383819d09f535228c7f7c43179b2db2b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 9 Jun 2026 11:52:21 +0000 Subject: [PATCH] JavaToLaurelCompiler: collapse array-vs-null comparison to a constant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../laurel/JavaToLaurelCompiler.java | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) 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 5059012cb..0a6057e02 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 @@ -558,6 +558,36 @@ private StmtExpr convertConstantValue(SourceRange sr, TypeTag tag, Object v) { } private StmtExpr convertBinary(JCTree.JCBinary binary, Map renames) { + // Handle comparisons against the `null` literal before + // recursing into operand conversion. In JVerify's + // array-as-map model an array-typed value is never null, so + // `arr == null` / `arr != null` fold to a boolean constant + // (and the BOT-typed null literal stays off the + // convertLiteral path). The fold is restricted to array- + // typed operands so it can't silently mask the nullability + // of ordinary object references. + if (binary.getTag() == JCTree.Tag.EQ || binary.getTag() == JCTree.Tag.NE) { + boolean lhsNull = (binary.lhs instanceof JCTree.JCLiteral l) + && l.typetag == TypeTag.BOT; + boolean rhsNull = (binary.rhs instanceof JCTree.JCLiteral r) + && r.typetag == TypeTag.BOT; + if (lhsNull && rhsNull) { + // null == null -> true; null != null -> false. + SourceRange sr = toSourceRange(binary); + return literalBool(sr, binary.getTag() == JCTree.Tag.EQ); + } + if (lhsNull ^ rhsNull) { + // Only fold when the non-null operand is an array- + // typed (map-backed) expression; other reference + // comparisons fall through to the normal path. + var other = lhsNull ? binary.rhs : binary.lhs; + if (other.type instanceof com.sun.tools.javac.code.Type.ArrayType) { + // x == null -> false; x != null -> true. + SourceRange sr = toSourceRange(binary); + return literalBool(sr, binary.getTag() == JCTree.Tag.NE); + } + } + } StmtExpr lhs = convertExpression(binary.lhs, renames); StmtExpr rhs = convertExpression(binary.rhs, renames); SourceRange sr = toSourceRange(binary);