Support static array literals, &[T;N] → &[T] coercion, and &mut [T] element writes#123
Draft
coord-e wants to merge 11 commits into
Draft
Support static array literals, &[T;N] → &[T] coercion, and &mut [T] element writes#123coord-e wants to merge 11 commits into
coord-e wants to merge 11 commits into
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
coord-e
force-pushed
the
claude/static-arrays-slices-y6hmtr
branch
from
7f78620 to
ac84456
Compare
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 Rvalue::Len to always use the Tuple (Seq) branch. Use result.len() instead of result.1 in slice test annotations, and 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
ac84456 to
fec1c05
Compare
…any pointer
Adds two capabilities needed for element access on &mut [T] slices:
1. Rvalue::RawPtr(FakeForPtrMetadata, place): the MIR idiom for extracting
fat-pointer metadata during bounds checks on mutable slices. Strip Subtype
("(fake)") projections and model as an immutable Seq reference so that the
PtrMetadata handler can extract the length.
2. PtrMetadata: relax the check from Ref(Immut) to any pointer kind pointing at
a Tuple (Seq<T>). Both &[T] and the raw ptr produced by FakeForPtrMetadata
now yield the length field.
Tests: array_literal_3 pass/fail pair — read element from &mut [T] and assert
the value, with a false assertion in the fail case.
… T elements Three new capabilities for arrays of mutable references ([&mut T; N]): 1. Rvalue::CopyForDeref: copies a mutable reference out of an aggregate (e.g. deref_copy arr[i]). Treated as a regular Copy for the model. 2. mir::Const::Ty: type-level constants (e.g. array bounds written as `const 2_usize`). Extracted via try_to_scalar_int() and delegated to const_value_ty as a scalar integer. 3. PtrMetadata generalization (also in the FakeForPtrMetadata commit): accepts any pointer-to-Tuple, so &mut [T] and raw ptrs from FakeForPtrMetadata both yield the length field. Tests: array_literal_4 pass/fail pair — build [&mut i32; 2], read both elements through the mutable references, and assert the correct values. Write-back through indexed mutable references ((*arr[i]) = val) requires per-element flow bindings in locate_place, which is left for future work.
Add assign_to_slice_index to handle (*s)[i] = val patterns where s: &mut [T]. The reborrow visitor cannot handle [Deref, Index] projections via locate_place (elaborate_place_for_borrow asserts the last element is Deref), so we intercept these statements in analyze_statements before the reborrow visitor runs. The implementation: - Creates a fresh TempVar for the post-write Seq - Constrains it to store(old_arr, idx, val) while preserving the length - Advances s's "current" binding via swap_mut_current so subsequent reads through s see the new value (same mechanism as scalar reborrow) Handles two local shapes: - Direct FlowBinding::Mut (is_mut_local = false) - Box-wrapped: FlowBinding::Box(content) where content has FlowBinding::Mut (is_mut_local = true; bind_local wraps &mut Seq in an Own box) Update array_literal_3 tests to actually exercise mutation through &mut [T]: - pass: s[0] = 42; assert!(s[0] == 42 && s[1] == 2) - fail: s[0] = 42; assert!(s[0] == 1) // old value → Unsat Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
coord-e
changed the title
…row visitor Instead of assign_to_slice_index (which encoded Seq tuple structure directly in the analyzer), ReborrowVisitor now rewrites (*s)[idx]=val into *ptr=val where ptr is produced by type_slice_index_mut — a call to the existing <[T] as IndexMut<usize>>::index_mut extern spec. This keeps all Seq-model knowledge in std.rs and removes swap_mut_current from env.rs. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
Remove the Seq-specific assign_to_slice_index from basic_block.rs and the corresponding swap_mut_current from env.rs. Instead, ReborrowVisitor now handles (*s)[idx]=val by: 1. reborrowing *s → s1 (updating s's current, as for any &mut write) 2. constructing a func operand for <[T] as IndexMut<usize>>::index_mut 3. calling the existing type_call to apply the extern spec 4. rewriting the place to *ptr so super_assign handles the rest All Seq-model knowledge stays in the _extern_spec_slice_index_mut spec. Also revert accidental .gitignore modification. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BV92ggaKvAp7oNknvVmGsM
…tatements
Move the (*s)[idx]=val rewrite out of ReborrowVisitor (where drop semantics
are inaccessible) into a new preprocess_slice_index_assign step called before
visit_statement in analyze_statements. The preprocessor:
1. Detects Assign with projection [Deref, Index] on &mut [T]
2. Resolves <[T] as IndexMut<usize>>::index_mut
3. Builds a synthetic TerminatorKind::Call and feeds it through
reborrow_visitor().visit_terminator() + analyze_terminator_binds()
4. Rewrites the statement to *ptr = val
5. Returns ptr_local so the caller can drop_local(ptr) after the write,
closing the prophecy chain through the extern spec
The drop is essential: ptr.final == ptr.current causes the extern spec
constraint !slice == Seq((*slice).0.store(index, !result), (*slice).1)
to propagate the written value back into the slice's CHC model.
Co-Authored-By: Claude <noreply@anthropic.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
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
Six commits, each paired with pass/fail tests:
Basic support (
a28ad57) —Seq<T>as unified model for[T]/[T;N]/Vec<T>;PlaceElem::Indexinenv.rsresolves(*s)[i]to aselectconstraint on the CHC array term. Handles both slice (Tuple→proj 0→deref) and raw Array types.Construction support (
311e771) —AggregateKind::Arrayarm: array literals[1, 2, 3]producerty::Type::Array(Int, T)with element values pinned viastorefolds. Tests:s[0] == 1passes,s[0] == 99→ Unsat.Coercion support (
fec1c05) —PointerCoercion::Unsizearm:&[T; N] → &[T]is identity onSeq<T>(array and length already in the right shape). Tests: index 3 on a 4-element slice passes, index 4 → Unsat.Mutable slice reads (
5ced28a) —RawPtr(FakeForPtrMetadata)for bounds checks on&mut [T];PtrMetadataextended to any pointer-to-Tuple. Enables reading through&mut [T]slices.[&mut T]array support (92f553d) —Rvalue::CopyForDerefandmir::Const::Tyfor array length constants. Supports[&mut i32; N]element arrays.Mutable slice writes (
ba8f02d) —(*s)[i] = valwheres: &mut [T]. Intercepts[Deref, Index]assignments before the reborrow visitor (which cannot handleIndexprojections). Advancess's current Seq binding viaenv.swap_mut_currentso subsequent reads see the new value. Tests:s[0] = 42; assert!(s[0] == 42)passes,s[0] = 42; assert!(s[0] == 1)→ Unsat.Test plan
cargo test— no regressions against pre-existing baselinearray_literal_1— element values tracked through literal + coercionarray_literal_2— length from coercion enables bounds verificationarray_literal_3— mutation through&mut [T]: write then read-backarray_literal_4—[&mut T]element arraysKnown limitations (out of scope)
[&mut T](would requirePlaceElem::Indexinlocate_place)unimplemented!)