Add foundational array support

verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java

@@ -93,13 +93,70 @@ SourceRange toSourceRange(JCTree node) {
     }
 
     private List<Command> getPredefinedTypes() {
-        return List.of(
+        var commands = new ArrayList<Command>(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<int,elem>
+        // 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<int,int> 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<int,int>
+        // 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<String, String>
                     }
                     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<StmtExpr> 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<int, elem> 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_<k> 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());
             };
         }

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<JCTree.JCCompilationUnit> transform(java.util.List<JCTree.JCCompilationUnit> 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;
         }

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<int, int>. (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) {
+    }
+}

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
     }
 }