Keep bounds-check temporaries that are still read after slice index reconstruction

[coord-e]

Fixes #319.

The problem, in MIR

Take this function:

fn last(slice: &[i32]) -> i32 {
    slice[slice.len() - 1]
}

At -C opt-level=0, rustc computes the length twice: once for the user's len() (_3) and once more for the bounds check (_4):

bb0: {
    _3 = PtrMetadata(copy _1);              // slice.len()
    _2 = Sub(move _3, const 1_usize);       // slice.len() - 1
    _4 = PtrMetadata(copy _1);              // length for the bounds check
    _5 = Lt(copy _2, copy _4);
    assert(move _5, "index out of bounds: ...", move _4, copy _2) -> bb1;
}
bb1: {
    _0 = copy (*_1)[_2];
    return;
}

At -C opt-level=1 and above, GVN merges the two, so the bounds check reuses the user's _3:

bb0: {
    _3 = PtrMetadata(copy _1);              // slice.len(), also used as the bounds check's length
    _2 = Sub(copy _3, const 1_usize);       // _3 is read here
    _4 = Lt(copy _2, copy _3);
    assert(move _4, "index out of bounds: ...", copy _3, copy _2) -> bb1;
}
bb1: {
    _0 = copy (*_1)[_2];
    return;
}

reconstruct_slice_indexing replaces the assert with an Index::index call. Then remove_bounds_check_setup turns into Nop every assignment in bb0 to the assert's condition (_4) and length (_3). On main, the result is:

bb0: {
    nop;                                    // was `_3 = PtrMetadata(copy _1)`
    _2 = Sub(copy _3, const 1_usize);       // reads _3, which now has no definition
    nop;                                    // was `_4 = Lt(copy _2, copy _3)`
    _5 = <[i32] as Index<usize>>::index(copy _1, copy _2) -> bb1;
}
bb1: {
    _0 = copy (*_5);
    return;
}

_3 is still read, but its definition is gone. The analysis then panics in FunctionType::remove_param:

refinement of the parameter being removed references its own value

At -C opt-level=0 none of this happens, because the deleted _4 and _5 are read only by the bounds check.

A user-written let n = a.len() whose n is used later is reused the same way. In let n = a.len(); let x = a[i]; x + n as i64, the assert reads _3, and so does _6 = copy _3 as i64 in the next block.

The fix

remove_bounds_check_setup now runs after the assert has been replaced by the call. It looks at each candidate local in turn: the condition, then the length, then the operand of PtrMetadata. A candidate is removed only if nothing in the body still reads it.

For last at -C opt-level=1, the result is:

bb0: {
    _3 = PtrMetadata(copy _1);              // kept: read by `_2 = Sub(..)`
    _2 = Sub(copy _3, const 1_usize);
    nop;                                    // `_4 = Lt(..)` removed: nothing reads it anymore
    _5 = <[i32] as Index<usize>>::index(copy _1, copy _2) -> bb1;
}

At -C opt-level=0, _5 (Lt) and _4 (PtrMetadata) are removed exactly as before. The receiver _1 is read by the new call, so it is always kept. That makes the old receiver special case unnecessary, and this PR removes it.

These decisions are logged at trace level (RUST_LOG=thrust::analyze::reconstruct_slice_indexing=trace):

	-C opt-level=0	-C opt-level=1
condition	_5 removed	_4 removed
length	_4 removed	_3 kept (still read)
PtrMetadata operand	_1 kept (receiver)	_1 kept (receiver)

Test

tests/ui/{pass,fail}/slice_index_len.rs check slice[slice.len() - 1] at -C opt-level=1. On main, both panic as shown above. With this PR, the pass test is safe and the fail test is Unsat.

Validation

• cargo fmt --all -- --check and cargo clippy -- -D warnings are clean.
• Locally, with Z3 5.0.0 and the PCSat version CI pins, cargo test passes: 392 UI tests plus the unit tests.

🤖 Generated with Claude Code

https://claude.ai/code/session_0171U9qC8QWRU95brd4pMBLX

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-03T21:44:18.646587Z	14f76ac	PR opened

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[coord-e]

The test check failed on tests/ui/fail/slice_split_first_mut_loop.rs. That test hit verification error: Timeout(60s) instead of Unsat, and every other test (391 of 392) passed.

This PR doesn't cause that failure. I generated the CHC system for this test with THRUST_OUTPUT_DIR, once with this branch and once with main's reconstruct_slice_indexing.rs. The two thrust_output.smt2 files are byte-identical, so PCSat gets exactly the same problem either way, and the difference is only solver time. I also saw this test time out once locally on unmodified main under a parallel cargo test run; it passed when I ran it alone.

No fix exists for this timeout yet. I've re-run the failed job once.

---

Generated by Claude Code