JavaToLaurelCompiler: inline static final compile-time constants - #442
Draft
tautschnig wants to merge 7 commits into
Draft
JavaToLaurelCompiler: inline static final compile-time constants#442tautschnig wants to merge 7 commits into
tautschnig wants to merge 7 commits into
Conversation
Encode a Java array type `T[]` as a Laurel `Map<int, T>` (the standard Boogie/SMT array model), so an array-typed parameter such as `int[] xs` is accepted and becomes a `Map<int, int>` that Strata can reason about via its map-theory axioms. This is the foundation the body- and contract-level array operations build on. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Translate `arr.length` on an array-typed receiver to a call to a new uninterpreted Laurel prelude function `lengthOf(arr)`. The array-as-map model has no intrinsic length, and Strata's resolver needs a declared symbol; an empty-body (uninterpreted) function also gives same-input/ same-output semantics so repeated `arr.length` references stay consistent. The new unguarded JCFieldAccess switch arm is placed after the existing guarded compile-time-constant arm so the latter is not dominated. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Read a single-dimension array element via a new uninterpreted Laurel prelude function `arrayGet(arr, idx)`. A contract-position `arr[i]` (JCArrayAccess) translates directly; body-level `arr[i]` that ArrayCompiler has lowered to `JArray.get(arr, i)` is routed to the same `arrayGet` symbol. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Match the JArray owner by stem so the synthetic-static rewrite that appends a `?static` suffix (MoveStaticMethodsToStaticType, which runs after ArrayCompiler) is still recognized, and accept any `.JArray` nested form. Without this the JArray.* routing silently fails once the hoisting pass has run. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
ArrayCompiler now lowers an initializer-list array `{v0, v1, ...}` to
`JArray.create(N)` (length-only; element values are dropped) instead of
rejecting it, setting the synthetic size literal's type so downstream
attribution succeeds.
JavaToLaurelCompiler declares an uninterpreted `arrayNew_1(N)` prelude
function returning a fresh Map<int,int>, routes JArray.create to it, and
translates JCNewArray: the sized form `new int[N]` to arrayNew_1 and the
initializer-list form to arrayInit_<n> (per-arity axioms can be added on
demand).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ay.set) Declare an uninterpreted `arraySet(arr, idx, value)` prelude function (pure-functional map store) and route the JArray.set call that ArrayCompiler emits for `arr[i] = v` to it. The original routing guarded on calleeName (the qualified "JArray_set" form) rather than the simple name, so the branch never fired; this uses simpleName, consistent with the get/create routing, so the write is actually translated. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Read a static final field access whose VarSymbol carries a constant value (javac folds `static final int X = ...` initialisers) and emit the corresponding Laurel boolean/integer literal, rather than failing on the field access. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Read a static final field access whose VarSymbol carries a constant value (javac folds
static final int X = ...initialisers) and emit the corresponding Laurel boolean/integer literal, rather than failing on the field access.Builds on #441, kept in draft until that is merged (and this one is rebased).
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.