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 2d2a7dc66..5c27dab74 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 @@ -93,13 +93,70 @@ SourceRange toSourceRange(JCTree node) { } private List getPredefinedTypes() { - return List.of( + var commands = new ArrayList(List.of( makeConstrainedType("int8", -128L, 127L), makeConstrainedType("int16", -32768L, 32767L), makeConstrainedType("int32", -2147483648L, 2147483647L), makeConstrainedType("int64", -9223372036854775808L, 9223372036854775807L), makeConstrainedType("char", 0L, 65535L) - ); + )); + + // Uninterpreted-function declaration for the array-as-map + // model. `arr.length` (JCFieldAccess in contract positions, + // where ArrayCompiler doesn't intercept) translates to a call + // against this. Strata's resolver requires a declaration; the + // empty body makes the function uninterpreted, so the only + // relation Strata enforces is "same input -> same output". + var arrayMap = mapType(intType(), intType()); + commands.add(procedureCommand(function( + "lengthOf", + List.of(parameter("arr", arrayMap)), + Optional.of(returnType(intType())), + Optional.empty(), List.of(), Optional.empty(), + Optional.empty(), Optional.empty() + ))); + // arrayGet(arr, idx) reads element `idx` from the Map + // that models the array. Used by both body-level `arr[i]` (via + // the JArray.get lowering) and contract-position array reads. + // Uninterpreted: same (arr, idx) yields the same value. + commands.add(procedureCommand(function( + "arrayGet", + List.of(parameter("arr", arrayMap), + parameter("idx", intType())), + Optional.of(returnType(intType())), + Optional.empty(), List.of(), Optional.empty(), + Optional.empty(), Optional.empty() + ))); + // arrayNew_1(N) returns a fresh Map for a 1-D + // `new int[N]` allocation. ArrayCompiler also lowers + // `{v0, v1, ...}` literals to JArray.create(N) (the literal + // element values are dropped, only the length is retained). + // Uninterpreted same-input -> same-output function; + // multi-dimensional and richer arities can be added on demand. + commands.add(procedureCommand(function( + "arrayNew_1", + List.of(parameter("d0", intType())), + Optional.of(returnType(arrayMap)), + Optional.empty(), List.of(), Optional.empty(), + Optional.empty(), Optional.empty() + ))); + // arraySet(arr, idx, value) returns a fresh Map + // representing arr with the (idx -> value) mapping updated. + // Standard pure-functional map "store"; matches the JArray.set + // call ArrayCompiler emits for `arr[i] = v`. Uninterpreted (no + // congruence axioms beyond same-input -> same-output); a future + // refinement can add the read-after-write axiom + // (`arrayGet(arraySet(a, i, v), i) == v`). + commands.add(procedureCommand(function( + "arraySet", + List.of(parameter("arr", arrayMap), + parameter("idx", intType()), + parameter("value", intType())), + Optional.of(returnType(arrayMap)), + Optional.empty(), List.of(), Optional.empty(), + Optional.empty(), Optional.empty() + ))); + return commands; } private Command makeConstrainedType(String name, long min, long max) { @@ -119,6 +176,19 @@ private static StmtExpr longLiteral(SourceRange sr, long val) { } private LaurelType translateType(com.sun.tools.javac.code.Type type) { + // Array types: encoded as a Laurel MapType(int, int) — the + // standard Boogie/SMT array model. The element type is + // deliberately erased to int (the type the array prelude + // functions in getPredefinedTypes are declared over), so every + // array, regardless of element type, type-checks uniformly + // against lengthOf / arrayGet / arraySet / arrayNew_1. This is + // sound for the int-family element types (int/short/byte/char, + // which are int-backed) and is a deliberate imprecision for + // wider (long), reference (Object[]), and nested array element + // types in this foundation. + if (type instanceof com.sun.tools.javac.code.Type.ArrayType) { + return mapType(intType(), intType()); + } return switch (type.getTag()) { case INT -> compositeType("int32"); case SHORT -> compositeType("int16"); @@ -543,7 +613,60 @@ private StmtExpr convertExpression(JCTree.JCExpression expr, Map } var methodSym = (Symbol.MethodSymbol) TreeInfo.symbol(invocation.getMethodSelect()); String calleeName = qualifiedMethodName(methodSym); + String simpleName = methodSym.getSimpleName().toString(); + // Recognise the synthetic JArray.get call that + // ArrayCompiler emits for body-level `arr[i]`. We + // route get -> arrayGet (declared in the prelude + // with same-input/same-output semantics). + String ownerName = methodSym.owner != null + ? methodSym.owner.getQualifiedName().toString() + : ""; + // Match either the qualified-name form + // (org.strata.jverify.builtin.JArray) or its + // post-MoveStaticMethodsToStaticType form + // (org.strata.jverify.builtin.JArray?static). + // The `?static` suffix is appended by the + // simplification that hoists static methods to + // a synthetic static-type, which runs after + // ArrayCompiler. + String ownerStem = ownerName.endsWith("?static") + ? ownerName.substring(0, ownerName.length() - "?static".length()) + : ownerName; + boolean isJArray = + ownerStem.equals("org.strata.jverify.builtin.JArray") + || ownerStem.endsWith(".JArray"); + boolean prependArrayReceiver = false; + if (isJArray) { + if (simpleName.equals("get")) { + calleeName = "arrayGet"; + prependArrayReceiver = true; + } else if (simpleName.equals("create")) { + // ArrayCompiler lowers `new int[N]` and + // `{v0, ...}` to JArray.create(N). We + // rewrite to arrayNew_1 (declared in + // the prelude) so Strata's resolver + // picks it up. + calleeName = "arrayNew_1"; + } else if (simpleName.equals("set")) { + // ArrayCompiler lowers `arr[i] = v` to the + // rebinding `arr = arr.set(i, v)`. We route + // the set call to the pure map-store arraySet + // (declared in the prelude); the surrounding + // assignment makes the update observable to + // later reads of `arr`. + calleeName = "arraySet"; + prependArrayReceiver = true; + } + } List args = new ArrayList<>(); + // get/set are instance methods on the array; their + // receiver is the array (a Map) and must be the first + // argument of arrayGet/arraySet. (create is static, so + // its array argument is already in invocation.args.) + if (prependArrayReceiver + && invocation.getMethodSelect() instanceof JCTree.JCFieldAccess receiverAccess) { + args.add(convertExpression(receiverAccess.selected, renames)); + } for (var arg : invocation.args) { args.add(convertExpression(arg, renames)); } @@ -570,6 +693,70 @@ yield call(toSourceRange(invocation), // expression's type. case JCTree.JCFieldAccess fa when fa.type.constValue() != null -> convertConstantValue(toSourceRange(fa), fa.type.getTag(), fa.type.constValue()); + case JCTree.JCFieldAccess fieldAccess -> { + SourceRange sr = toSourceRange(fieldAccess); + // Special-case `arr.length` for array-typed receivers. + // In JVerify's array-as-map model there is no + // intrinsic length; translate to a call to the + // uninterpreted Laurel function `lengthOf` we + // declare in the prelude (see getPredefinedTypes). + // Strata's resolver requires a declaration, so a + // pure free identifier wouldn't work; the + // declaration also gives same-input/same-output + // semantics so multiple references to the same + // `arr.length` are consistent. + if (fieldAccess.name.toString().equals("length") + && fieldAccess.selected.type instanceof + com.sun.tools.javac.code.Type.ArrayType) { + StmtExpr arr = convertExpression(fieldAccess.selected, renames); + yield call(sr, identifier(sr, "lengthOf"), + java.util.List.of(arr)); + } + throw new JavaViolationException( + "Unsupported field access: " + fieldAccess); + } + case JCTree.JCArrayAccess arrayAccess -> { + // `arr[i]` for a single-dimension array reads + // from the Map we use to model the + // array. Translate to an `arrayGet(arr, i)` + // call against the Laurel function we declare + // in the prelude. Note: ArrayCompiler often + // intercepts these in the body and rewrites to + // JArray.get; this case is the fallback for + // contract-position array reads. + SourceRange sr = toSourceRange(arrayAccess); + StmtExpr arr = convertExpression(arrayAccess.indexed, renames); + StmtExpr idx = convertExpression(arrayAccess.index, renames); + yield call(sr, identifier(sr, "arrayGet"), + java.util.List.of(arr, idx)); + } + case JCTree.JCNewArray newArray -> { + // Two source forms reach here: + // `new int[N]` — dims=[N], elems=null + // `{v0, v1, ...}` (or `new int[]{v0, ...}`) + // — dims=[], elems=[v0, ...] + // Both are modelled length-only via the uninterpreted + // arrayNew_1 prelude function: the initializer-list + // element values are not captured (matching + // ArrayCompiler's lowering). Only single-dimension + // arrays are supported; multi-dimensional allocations + // are rejected with a clear error rather than emitting + // an undeclared arrayNew_ symbol. + SourceRange sr = toSourceRange(newArray); + if (newArray.elems != null) { + // Initializer-list form `{v0, v1, ...}`: a fresh + // array of the literal length. + yield call(sr, identifier(sr, "arrayNew_1"), + java.util.List.of(longLiteral(sr, newArray.elems.size()))); + } + if (newArray.dims.size() != 1) { + throw new JavaViolationException( + "Only single-dimension array creation is supported, but got " + + newArray.dims.size() + " dimensions"); + } + StmtExpr dim = convertExpression(newArray.dims.head, renames); + yield call(sr, identifier(sr, "arrayNew_1"), java.util.List.of(dim)); + } default -> throw new JavaViolationException("Unsupported expression: " + expr.getClass().getSimpleName()); }; } diff --git a/verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/ArrayCompiler.java b/verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/ArrayCompiler.java index 570e3bf47..749c58a17 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/ArrayCompiler.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/ArrayCompiler.java @@ -22,6 +22,7 @@ public class ArrayCompiler extends TreeTranslator { private final TreeMaker maker; private final JavacElements elements; private final Names names; + private final com.sun.tools.javac.code.Symtab symtab; public java.util.List transform(java.util.List envs) { for (var env : envs) { @@ -34,6 +35,7 @@ public ArrayCompiler(Context context) { this.maker = TreeMaker.instance(context); this.elements = JavacElements.instance(context); this.names = Names.instance(context); + this.symtab = com.sun.tools.javac.code.Symtab.instance(context); this.reporter = Reporter.instance(context); arraySymbol = elements.getTypeElement(COM_AWS_JVERIFY_BUILTIN_JARRAY); @@ -65,11 +67,36 @@ public void visitNewClass(JCTree.JCNewClass tree) { public void visitAssign(JCTree.JCAssign tree) { if (tree.lhs instanceof JCTree.JCArrayAccess arrayAccess) { maker.pos = tree.pos; + var arrayExpr = arrayAccess.getExpression(); tree.rhs = translate(tree.rhs); - result = maker.App(maker.Select(arrayAccess.getExpression(), setMethodSymbol), - List.of(arrayAccess.getIndex(), tree.rhs)); - result.type = tree.type; + if (arrayExpr instanceof JCTree.JCIdent ident) { + // `arr[i] = v` lowers to the pure map-store `arr.set(i, v)` + // (modelled in Laurel as arraySet, which returns a fresh + // map). To make the write observable by later reads we + // rebind the array variable: `arr = arr.set(i, v)`. + var setCall = maker.App( + maker.Select(maker.Ident(ident.sym), setMethodSymbol), + List.of(arrayAccess.getIndex(), tree.rhs)); + setCall.type = arrayExpr.type; + var rebind = maker.Assign(maker.Ident(ident.sym), setCall); + rebind.type = arrayExpr.type; + result = rebind; + } else { + // We can only rebind a simple (assignable) local-variable + // array. For any other array expression — a field access, + // a method-call result, a nested index, etc. — we cannot + // make the store observable, so reject it with a clear + // error rather than silently dropping the write (which + // would mis-model the program). + reporter.reportError(tree, "notSupported", + "array element assignment whose array is not a simple local variable"); + var setCall = maker.App( + maker.Select(arrayExpr, setMethodSymbol), + List.of(arrayAccess.getIndex(), tree.rhs)); + setCall.type = tree.type; + result = setCall; + } } else { super.visitAssign(tree); @@ -103,8 +130,22 @@ public void visitNewArray(JCTree.JCNewArray newArray) { maker.pos = newArray.pos; JCTree.JCExpression size; if (newArray.getInitializers() != null && !newArray.getInitializers().isEmpty()) { - reporter.reportError(newArray, "notSupported", "new array with initializers"); - size = maker.Literal(0); + // Initializer-list form `{v0, v1, ...}` (or + // `new int[]{v0, ...}`): we lower this to + // `JArray.create(N)` where N is the literal length. + // The contents are then unconstrained — Strata sees a + // fresh array of the right length but nondet entries. + // This is coarse but lets verification proceed; users + // who rely on the literal contents (rather than just + // bounds-style reasoning) will need to add explicit + // assumptions or wait for a per-arity arrayInit_N + // axiomatization on the JavaToLaurelCompiler side. + JCTree.JCLiteral sizeLit = + maker.Literal(newArray.getInitializers().size()); + // Set the literal's type so downstream attribution + // (line-map resolution, etc.) doesn't trip. + sizeLit.type = symtab.intType; + size = sizeLit; } else { size = newArray.getDimensions().head; } diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/AcceptArrayParam.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/AcceptArrayParam.java new file mode 100644 index 000000000..5ca0dc798 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/AcceptArrayParam.java @@ -0,0 +1,16 @@ +package org.strata.jverify.verifier.tests.javasupport; + +import org.strata.jverify.testengine.JVerifyTest; + +/** + * A method with an array-typed parameter is accepted and verifies: the array + * is modelled as a Laurel Map. (Element-level get/set translate and + * type-check but do not fully verify yet — the element type is erased to an + * unbounded int rather than int32; full element-level verification is deferred + * to typed-array support, Strata#1073.) + */ +@JVerifyTest(methodsVerified = 2, errorCount = 0) +class AcceptArrayParam { + static void acceptArrayParam(int[] a) { + } +} diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/ResolutionErrorsStringMethods.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/ResolutionErrorsStringMethods.java index 323b14e6b..050f066fe 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/ResolutionErrorsStringMethods.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/ResolutionErrorsStringMethods.java @@ -4,11 +4,11 @@ import static org.strata.jverify.JVerify.*; -@JVerifyTest(exitCode = 2) +@JVerifyTest(exitCode = 4) class ResolutionErrorsStringMethods { static void stringFormatted() { check("hello %s".formatted("world").length() == 11); // ^ warning: missing contract for method 'formatted' in class 'java.lang.String' -// ^ error: new array with initializers is not supported +// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Resolution failed: 'String_length' is not defined } }