Panic at -C opt-level >= 1 on a[a.len() - 1] (and let n = a.len(); … a[i] … n): slice-index reconstruction deletes the program's own len() local because rustc reuses it as the bounds check's length #319

Summary

With optimizations enabled (-C opt-level=1 and above, which covers -O and cargo's --release), indexing a slice by an expression that uses the slice's own length makes Thrust panic:

thread 'rustc' panicked at src/rty.rs:311:21:
refinement of the parameter being removed references its own value

The common a[a.len() - 1] idiom is enough to trigger it, as is computing let n = a.len(); in the same basic block as an index a[i] and then using n. At -C opt-level=0 the same programs verify correctly, both ways (safe when safe, Unsat when the assertion is false).

This isn't a missing feature. It comes from a MIR rewrite in Thrust that deletes a statement the program still needs.

Reproducer

#[thrust::trusted]
#[thrust_macros::requires(true)]
#[thrust_macros::ensures(
    (*result).len() == 3
        && (*result)[0] == 10
        && (*result)[1] == 20
        && (*result)[2] == 30
)]
fn slice() -> &'static [i32] {
    unimplemented!()
}

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

fn main() {
    let slice = slice();
    assert!(last(slice) == 30);
}

$ THRUST_SOLVER=tests/thrust-pcsat-wrapper cargo run -- -C debug-assertions=false last.rs && echo safe
safe
$ THRUST_SOLVER=tests/thrust-pcsat-wrapper cargo run -- -C debug-assertions=false -C opt-level=1 last.rs
thread 'rustc' panicked at src/rty.rs:311:21:
refinement of the parameter being removed references its own value

A second shape with the same cause:

fn g(a: &[i64], i: usize) -> i64 { let n = a.len(); let x = a[i]; x + n as i64 }

Root cause

At -C opt-level>=1, GVN makes the bounds check reuse the length the program already computed. The optimized MIR of g:

bb0: {
    _3 = PtrMetadata(copy _1);          // the user's `let n = a.len()`
    _5 = Lt(copy _2, copy _3);
    assert(move _5, "index out of bounds: ...", copy _3, copy _2) -> bb1;
}
bb1: {
    _4 = copy (*_1)[_2];
    _6 = copy _3 as i64 (IntToInt);     // `n` is still used here
    _0 = Add(copy _4, move _6);
    return;
}

For slice[slice.len() - 1], the index itself is computed from that local in the same block (_3 = PtrMetadata(copy _1); _4 = Sub(copy _3, const 1_usize); _5 = Lt(copy _4, copy _3); assert(...)).

reconstruct_slice_indexing::remove_bounds_check_setup replaces the bounds check with an Index::index call. It then turns into Nop every assignment in the assert block to the assert's condition local, its len local, and the PtrMetadata operand. It assumes all of these are temporaries that only the bounds check used. Here _3 is the program's own n, so its definition disappears while _3 is still read: by _4 = Sub(_3, 1) in the same block, or by _3 as i64 in bb1. The now-undefined local then shows up as live where it was never bound, and FunctionType::remove_param panics when the analysis tries to remove it.

The receiver is the only exception the function already makes ("When PtrMetadata is applied directly to the slice reference (the receiver), that local must not be NOP'd"). The len local and the condition local can be reused in the same way.

Fix

Remove a bounds-check temporary only when nothing in the body still reads it. This also covers the existing receiver special case, because the reconstructed call reads the receiver. Do the removal after the assert terminator has been replaced, in dependency order (condition, then length, then the PtrMetadata operand). With that change, every row of the table above gives the -C opt-level=0 result at -C opt-level=1 and 3, and the full test suite passes. PR to follow.

Not related

• Incompleteness: v.len() on a &mut [T] leaves an unresolved reborrow that havocs the referent, so every safe &mut slice program that guards an index with len() is rejected at any -C opt-level >= 1 #240 (closed): the PtrMetadata operand being reborrowed when it is &mut. This issue is about the result of PtrMetadata being deleted, and it also happens with shared slices.
• Slicing with a range (&v[1..], &v[..n], &v[a..b], &v[..]) ICEs: the refinement-spec table is keyed by DefId alone, so _extern_spec_slice_index's usize signature is applied to every I: SliceIndex instantiation of the one shared Index::index impl method #281: range slicing (&v[1..]) keyed by DefId. This issue only involves usize indexing.
• No numeric-range or overflow reasoning is involved.

Environment

• main @ 67a1cc4
• PCSat (thrust-pcsat-wrapper-49ed9fe340, as in CI), Z3 5.0.0