Support static array literals and &[T;N] → &[T] coercion#123
Draft
coord-e wants to merge 4 commits into
Draft
Conversation
coord-e
force-pushed
the
claude/static-arrays-slices-y6hmtr
branch
from
4df27b4 to
7f78620
Compare
Add `model::Slice<T>` and `Model` impls for `[T]`, `model::Slice<T>`, and `[T; N]` so that the existing Model-trait normalization pipeline handles these types without changes to the core type-builder logic: - `[T]` normalizes to `model::Slice<T::Ty>` = `(Array<Int,T>, Int)`, matching the Vec model (`.0` = array, `.1` = length) - `[T; N]` normalizes to `model::Array<Int, T::Ty>`, reusing the existing array model (N is statically known, written directly in specs) - `&[T]` and `&mut [T]` flow through the existing reference handling Add `Rvalue::Len` handling in `basic_block.rs` (slice length comes from fat-pointer metadata in MIR, not a function call): - For slice model (TupleType): project element 1 then deref the box - For static array model (ArrayType): evaluate the const N from MIR Add `UnOp::PtrMetadata` handling for `&[T]` references: extract the length by deref → tuple_proj(1) → deref. Add extern specs for `<[T]>::len`, `<[T]>::index`, `<[T]>::index_mut`, and `<[T]>::is_empty`, mirroring the existing Vec specs. Add test cases: - `tests/ui/pass/slice_1.rs`: safe indexing with non-empty slice - `tests/ui/fail/slice_1.rs`: out-of-bounds access (empty slice) - `tests/ui/pass/slice_2.rs`: two-element slice, two safe indices https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
Switch [T] and [T;N] to both use model::Seq<T> (replacing model::Slice<T> and model::Array<Int,T>). Remove the Slice<T> struct from std.rs and update the index_mut extern spec constructor accordingly. Now both static arrays and slices share the same (Array<Int,T>, Int) logical representation. Add Path::Index / path_type() arm in env.rs: MIR (*s)[i] projections resolve to a select on the Seq's inner array (field 0 → deref → select). Simplify PlaceElem::Len to always use the Tuple (Seq) branch. Add tests/ui/fail/slice_2.rs pairing the existing pass: s[2] on a slice guaranteed only len >= 2 cannot be proven safe → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
Handle AggregateKind::Array in rvalue_type(): fold store operations over a base existential to build a CHC array term, then wrap with the concrete element count to produce Seq<T> = (Array<Int,T>, N). Element type for empty arrays is read from AggregateKind::Array(ty) directly. Paired tests: pass asserts s[0]==1 (correct), fail asserts s[0]==99 → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
Since both [T;N] and [T] now model as Seq<T>, the PointerCoercion::Unsize cast is a model-level identity: just pass through the operand's place type. Paired tests: pass accesses index 3 on a 4-element slice (safe), fail accesses index 4 → Unsat. https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
coord-e
force-pushed
the
claude/static-arrays-slices-y6hmtr
branch
from
7f78620 to
ac84456
Compare
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
2 participants
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.
Summary
Three commits, each paired with a pass/fail test:
Basic support —
PlaceElem::Indexinsrc/refine/env.rs: MIR place projections(*s)[i]now resolve to aselectconstraint on the underlying CHC array term. Handles both slice (Tuple → proj 0 → deref) and rawArraytypes. Addstests/ui/fail/slice_2.rsto pair the existing pass test.Construction support —
AggregateKind::Arrayarm insrc/analyze/basic_block.rs: array literals[1, 2, 3]producerty::Type::Array(Int, T)with element values pinned viastorefolds over a base existential. Element type for empty arrays is read directly fromAggregateKind::Array(ty)rather than derived from elements. Paired tests:s[0] == 1passes,s[0] == 99→ Unsat.Coercion support —
PointerCoercion::Unsizearm insrc/analyze/basic_block.rs:&[T; N] → &[T]coercions wrap the array place type in a(Array<Int,T>, N)tuple with the concrete length, enabling bounds verification. Paired tests: index 3 on a 4-element slice passes, index 4 → Unsat.Test plan
cargo test— all existing tests continue to pass; 4 new tests passtests/ui/pass/array_literal_1.rs—s[0] == 1verifiestests/ui/fail/array_literal_1.rs—s[0] == 99reports Unsattests/ui/pass/array_literal_2.rs—s[3]on 4-element slice is safetests/ui/fail/array_literal_2.rs—s[4]on 4-element slice reports Unsattests/ui/fail/slice_2.rs—s[2]with onlylen >= 2guaranteed reports UnsatKnown limitations (out of scope)
[x; N]repeat syntax compiles toRvalue::Repeat, not handled herearr[i]as array place, not slice) is not exercised by these tests