Support static array literals and &[T;N] → &[T] coercion#123
Draft
coord-e wants to merge 4 commits into
Draft
Conversation
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
Add Path::Index variant and path_type() arm in env.rs so that MIR place projections of the form (*s)[i] resolve to a select constraint on the underlying CHC array term. Handles both slice (Tuple → proj 0 → deref) and raw Array types. Add tests/ui/fail/slice_2.rs: accessing index 2 on a slice guaranteed only len >= 2 cannot be proven safe → Unsat, pairing the existing pass. 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 with each element constrained to its concrete value. Elements are not boxed — they go directly into the array. For empty arrays, element type 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
… model Add PointerCoercion::Unsize arm in rvalue_type(): reads N from the MIR source type before consuming the operand, then wraps the array place type in a (Array<Int,T>, N) tuple to produce the slice model with concrete length. 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
4df27b4 to
7f78620
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