Add foundational array support

[tautschnig]

What was changed?

Adds foundational array support to the Java → Laurel front end (JavaToLaurelCompiler + ArrayCompiler). Java arrays are modelled as Laurel maps — every array becomes a Map<int, int> (the standard Boogie/SMT array model) — with element operations translated to a small set of uninterpreted prelude functions (lengthOf, arrayGet, arraySet, arrayNew_1).

Commits:

1. Translate array types to Laurel map types — every T[] → Map<int, int>; the element type is erased to int so all arrays type-check uniformly against the prelude functions. Adds AcceptArrayParam, a test showing an array-typed parameter method verifies.
2. arr.length → lengthOf(arr).
3. Array element reads arr[i] / JArray.get → arrayGet(arr, idx).
4. Recognise JArray after the ?static hoisting pass.
5. Array creation new int[N] / {…} → arrayNew_1 (length-only); multi-dimensional allocation rejected with a clear error.
6. Array element writes arr[i] = v / JArray.set → rebound arr = arraySet(arr, i, v) so the store is observable.
7. Pass the array receiver to arrayGet/arraySet — get/set are instance methods, so the array is the call receiver; it must be the first argument. Without this, arr.get(i) lowered to arrayGet(i) and Strata rejected it with a type error.

Scope: what verifies vs. what's deferred

This is a deliberately partial foundation:

• Array-typed parameter acceptance verifies (see AcceptArrayParam).
• Element get/set translate and type-check (commit 7 fixes the receiver type error), but do not fully verify yet: the element type is erased to an unbounded int, whereas Java int is the constrained int32, so a[i] is not provably int32 (and Strata does not allow constrained function return types, so arrayGet can't simply return int32). Bridging that needs int↔int32 handling at element sites.

So the bar here is "accepts and translates" for element operations, not full element-level verification. That, plus the Map<int,int> model itself, is expected to be superseded by typed-array support (Strata#1073, Array<T>/Seq<T>) — element-level verification is deferred to that work rather than completed against the map model.

Other known limitations

• Initializer-list arrays retain only their length; element values are dropped. Only single-dimension allocation is supported.
• Element-type erasure makes wider (long), reference (Object[]), and nested array elements imprecise.

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

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

This PR updates the Java→Laurel lowering to support a map-based array model, including array length, allocation, and reads/writes, and adjusts array literal handling to preserve only length.

Changes:

• Lower array initializer lists to allocate an array of the right length (dropping element values) in ArrayCompiler.
• Introduce Laurel prelude declarations and expression rewrites for array operations (lengthOf, arrayGet, arrayNew_1, arraySet).
• Translate Java array types to Laurel map types (Map<int, elem>).

Reviewed changes

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

File	Description
verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/ArrayCompiler.java	Lowers array initializer lists to length-only allocation and sets literal type via Symtab.
verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java	Adds array map prelude functions and rewrites array operations/typing during Laurel generation.

---

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

[fabiomadge]

Tried this locally (origin/main, same Strata e115b8ec): array element access doesn't verify — both reads and writes exit with a Strata type error rather than a verification result:

static int get0(int[] a) { return a[0]; }   // exit 1
// Type checking error. Impossible to unify (arrow (Map int int) (arrow int int)) with (arrow int $__ty69)

Same for a[i] = v. The arrayGet/arraySet calls don't match the Map<int,int> prelude declarations; a non-array control verifies fine through the same path.

Two things: (1) is element get/set meant to verify yet, or is "translates and proceeds" the bar for now? (2) No array test in the PR (only an unrelated ResolutionErrorsStringMethods tweak), so CI doesn't catch it — one read/write test would. Also worth noting the overlap with Strata#1073 (typed Array<T>/Seq<T>), which may supersede the Map<int,int> model.

[tautschnig]

@fabiomadge Applied the smallish fixes, but indeed the right thing might be to wait for strata-org/Strata#1073.

[fabiomadge]

Confirmed prependArrayReceiver fixes the type error — element get/set type-check now, but still don't verify: arrayGet returns unbounded int while a Java int target is constrained int32, leaving an undischarged range-assert. Front-end tightening is Strata-blocked: arrayGet : int32 → "constrained return types on functions not supported"; an in-range ensures is dropped (function postconditions still open, #1173/#668). The procedure route (#1215 merged, #1352 open) is more promising but needs a Strata bump + remodeling.

Re #1073: it adds bounds-checking and value/reference semantics, but still needs one of those postcondition paths to verify element facts, and its Array<T> is T = int only (general element types wait on Laurel polymorphism). So it supersedes #441 for int arrays without fully closing the gap. The type-check fix is a fine incremental step regardless.