Add basic slice support

[coord-e]

Summary

• model [T] with the existing Seq model
• add extern specs for basic slice operations, including len, get, get_mut, first, first_mut, last, last_mut, Index, and IndexMut
• apply those specs to slice metadata and first-class MIR indexing operations
• add paired pass/fail UI tests and compiler-backed unit tests for MIR reconstruction

Design

Knowledge that slices are modeled as Seq remains in std.rs. The analyzer only maps slice-specific MIR operations back to standard slice operations and applies their registered function types; it never constructs Seq terms for slices.

Slice length and indexing use different integration points because they have different MIR shapes:

• Slice length is lowered to the atomic PtrMetadata(slice) rvalue. It already has a local input/output boundary, so assignment analysis can invoke type_call with [T]::len and bind the scalar result directly. Reconstructing a real call here would require splitting the basic block and inserting a new call terminator without improving borrow or prophecy handling.
• Slice indexing is distributed across a bounds-check terminator and a later PlaceElem::Index use. Mutable indexing also produces a reference whose prophecy and environment transition should use the normal call machinery. The reconstruction pass therefore recognizes this canonical MIR shape, replaces it with an Index::index or IndexMut::index_mut call, and rewrites the indexed place to dereference the returned reference.

Reconstruction is an implementation choice rather than a semantic requirement: direct indexed-place analysis could also remain model-independent, but it would require making place elaboration effectful and threading call, borrow, and prophecy handling through those paths.

Validation

• cargo check
• compiler-backed unit tests for shared indexing, mutable indexing, and shared indexing through a mutable slice
• all paired slice UI tests with the default Spacer solver

[Copilot]

Pull request overview

Adds first-class support for Rust slices ([T]) in Thrust’s modeling + MIR analysis pipeline by (a) mapping slices to the existing Seq model and (b) recognizing slice-specific MIR lowering patterns (length via PtrMetadata, indexing via bounds-check + PlaceElem::Index) and reifying them back into standard library operations so existing call/type machinery applies.

Changes:

• Model [T] as model::Seq<T> and add extern specs for common slice operations (len, get/get_mut, first/last, Index/IndexMut) in std.rs.
• Add a MIR reconstruction pass that rewrites lowered slice indexing back into Index::index / IndexMut::index_mut calls and hook it into analysis.
• Add paired UI pass/fail tests plus compiler-backed unit tests for the reconstruction behavior; enable library unit tests.

Reviewed changes

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

Show a summary per file

File	Description
tests/ui/pass/slice_methods.rs	UI coverage for basic shared slice methods and trait-based Index::index.
tests/ui/pass/slice_methods_mut.rs	UI coverage for get_mut and subsequent readback.
tests/ui/pass/slice_last_mut.rs	UI coverage for last_mut + last consistency.
tests/ui/pass/slice_index.rs	UI coverage for len() and slice[idx] desugaring.
tests/ui/pass/slice_index_mut.rs	UI coverage for slice[idx] += 1 via IndexMut.
tests/ui/pass/slice_first_mut.rs	UI coverage for first_mut + first consistency.
tests/ui/fail/slice_methods.rs	Negative UI coverage for incorrect last() expectation.
tests/ui/fail/slice_methods_mut.rs	Negative UI coverage for incorrect post-mutation value.
tests/ui/fail/slice_last_mut.rs	Negative UI coverage for incorrect last() expectation after mutation.
tests/ui/fail/slice_index.rs	Negative UI coverage for out-of-bounds indexing.
tests/ui/fail/slice_index_mut.rs	Negative UI coverage for incorrect IndexMut result expectation.
tests/ui/fail/slice_first_mut.rs	Negative UI coverage for incorrect first() expectation after mutation.
std.rs	Adds [T] model + extern specs for slice ops used by analysis/reconstruction.
src/lib.rs	Adds rustc_driver import behind cfg(test) for compiler-backed unit tests.
src/analyze/reconstruct_slice_indexing.rs	New pass to reconstruct slice indexing calls from optimized MIR patterns.
src/analyze/reconstruct_slice_indexing/tests.rs	New compiler-backed unit tests validating reconstructed MIR call shapes.
src/analyze/local_def.rs	Runs the reconstruction pass as part of analysis pipeline.
src/analyze/basic_block.rs	Recognizes slice len() lowered to PtrMetadata and types it as a call.
src/analyze.rs	Registers the new analysis module and adds an internal fn_operand helper.
Cargo.toml	Enables lib unit tests so the new reconstruction tests can run.

---

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit:40d296d9e0

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Gate slice get specs to usize indices

Because extern specs are registered by the target DefId, this contract for the generic <[T]>::get method is reused for every SliceIndex instantiation, not just usize. A valid call like slice.get(0..2) then tries to type a range argument against this usize/index-element contract and can panic during subtyping instead of either falling back or using range-slice semantics; the mirrored get_mut spec below has the same issue.

Useful? React with 👍 / 👎.

[coord-e]

that is indeed TODO 74906dd