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`

[coord-e]

Summary

<[T]>::len is lowered by rustc to PtrMetadata. When the receiver is a &mut [T], ReborrowVisitor::visit_operand first rewrites the operand into a fresh &mut reborrow of the slice, and analyze_assignment's PtrMetadata branch then throws that reborrow away — it takes a new shared borrow of the reborrow's referent and passes that to slice_len instead. Nothing ever resolves the discarded &mut reborrow's prophecy, and because borrowing a place replaces its value with the borrow's prophecy, *v is havoc'd for the rest of the function.

Consequence: after a single v.len() on a &mut [T], every later fact about (*v) — including the length that len() itself just returned — is lost. The guard if i < v.len() therefore no longer discharges the index < (*slice).length precondition of _extern_spec_slice_index/_extern_spec_slice_index_mut, and trivially safe programs are rejected with Unsat.

At -C opt-level=0 rustc always routes the metadata read through an explicit shared reborrow (_5 = &(*_1); _4 = PtrMetadata(move _5)), so the &mut operand shape — and the bug — never appears. From -C opt-level=1 upward (including -O, -C opt-level=s, -C opt-level=z) rustc emits _4 = PtrMetadata(copy _1) directly on the &mut [T] local and the bug fires. Thrust's verdict therefore depends on the optimization level: the same source is safe in a debug build and Unsat in a release build.

This is a completeness failure (over-rejection), not an unsoundness — the havoc'd referent is genuinely free, so false assertions after such a call are still correctly rejected (see "Not vacuity" below).

Minimal reproducer

fn main() {}

#[thrust::callable]
fn check(v: &mut [i32], i: usize) {
 if i < v.len() {
 let x = v[i];
 assert!(x == x);
 }
}

$ cargo run -- -Adead_code -C debug-assertions=false min.rs && echo safe
safe

$ cargo run -- -Adead_code -C debug-assertions=false -C opt-level=2 min.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

The index is guarded by the immediately preceding v.len(), so v[i] is in bounds by construction.

Changing the parameter to a shared slice makes the program verify at every optimization level:

#[thrust::callable]
fn check(v: &[i32], i: usize) { // &[i32] instead of &mut [i32]
 if i < v.len() {
 let x = v[i];
 assert!(x == x);
 }
}

A realistic case — the standard "walk a mutable slice by index" loop:

fn double_all(v: &mut [i32]) {
 let mut i = 0;
 while i < v.len() {
 v[i] = v[i] * 2;
 i += 1;
 }
}

#[thrust::callable]
fn check(v: &mut [i32]) {
 double_all(v);
}

fn main() {}

safe at the default optimization level, Unsat at -C opt-level=2.

Behavior matrix (all with -Adead_code -C debug-assertions=false)

-C opt-level	&mut [i32] reader (min.rs)	&[i32] reader	&mut [i32] writer (if i < v.len() { v[i] = 5; })	double_all
0 (default)	safe ✔	safe ✔	safe ✔	safe ✔
1	Unsat ❌	safe ✔	Unsat ❌	Unsat ❌
2	Unsat ❌	safe ✔	Unsat ❌	Unsat ❌
3	Unsat ❌	safe ✔	Unsat ❌	Unsat ❌
s / z	Unsat ❌	safe ✔	Unsat ❌	Unsat ❌

Programs that only read the length keep working at -O (let n = v.len(); let m = v.len(); assert!(n == m);, if i < v.len() { assert!(i < v.len()); }): rustc CSEs the two metadata reads into one, so nothing reads *v after the reborrow. It is specifically a read of (*v) after a len() — which every indexing operation performs, since the reconstructed Index::index receiver is &(*v) — that observes the havoc.

Root cause

v.len() is PtrMetadata in MIR. The two shapes rustc emits for a &mut [i32] receiver:

// -C opt-level=0
bb0: {
 _5 = &(*_1); // shared reborrow, inserted by rustc
 _4 = PtrMetadata(move _5); // operand type: &[i32] -> ReborrowVisitor does nothing
 ...
}

// -C opt-level=1 and above
bb0: {
 _4 = PtrMetadata(copy _1); // operand type: &mut [i32] -> ReborrowVisitor reborrows it
 ...
}

analyze_statements runs ReborrowVisitor on the statement before analyze_assignment sees it. ReborrowVisitor::visit_operand (src/analyze/basic_block/visitor/reborrow.rs) reborrows every &mut-typed operand:

if m.is_mut() {
 let new_local = self.insert_reborrow(self.tcx.mk_place_deref(p), *inner_ty);
 *operand = mir::Operand::Move(new_local.into());
}

so the statement becomes _4 = PtrMetadata(move _new) with _new = &mut (*_1). insert_reborrow binds _new via borrow_place_, which allocates a prophecy and — as everywhere in the prophecy encoding — replaces the value of *_1 with that prophecy.

analyze_assignment then takes the mutable branch (src/analyze/basic_block.rs):

let operand = if mutability.is_mut() {
 let place = operand.place().expect("mutable slice metadata operand must be a place");
 ...
 let rty = self.immut_borrow_place(self.tcx.mk_place_deref(place)); // &(*_new)
 self.bind_local(local, rty);
 Operand::Copy(local.into())
} else {
 operand.clone()
};

It reads _new's current half through a fresh shared borrow (so _4 is the correct, pre-borrow length) and never touches _new again. _new is a synthetic local that does not exist in the MIR the liveness-based DropPoints was computed from, so it is never passed to drop_local and its prophecy is never equated to its current value. ReborrowVisitor::insert_reborrow/insert_borrow do not call drop_after_terminator either (only visitor/rust_call.rs does that, for closure receivers).

Every later read of (*_1) — in particular the _7 = &(*_1) receiver that reconstruct_slice_indexing::receiver_operand inserts for the reconstructed Index::index call — therefore reads that unconstrained prophecy.

CHC evidence

For the minimal reproducer at -C opt-level=2, the query clause for the index precondition (THRUST_OUTPUT_DIR, clause c2) contains, among the assumptions:

; the length the guard was taken on: len = tuple_proj.1(current half of _1 at the PtrMetadata)
(= v11 (< v10 v12)) ; _3 = Lt(_2, _4)
(not (= v11 false)) ; the `if` was taken
(= (mut (tuple v21 v22) v20) (mut (tuple v15 v16) v19)) ; current = (v15,v16), final = v19

; the receiver of Index::index is built from v19, the *final* half above
(= (mut (tuple v3 v4) v2) (mut v19 v14))
(= v8 (mut_current (mut (tuple v3 v4) v2)))
(= v1 v8)

and the head obliges (< v0 (tuple_proj<...>.1 v1)), i.e. _2 < v4. The guard gives v10 < v12 with v12 = tuple_proj.1(tuple(v15, v16)) = v16, but the receiver's length is v4, taken from v19 — the unresolved prophecy. Nothing in the system relates v19 to tuple(v15, v16), so the obligation is unprovable and the system is unsat.

Confirmed by experiment

Resolving the discarded reborrow right after the shared borrow is taken:

 let rty = self.immut_borrow_place(self.tcx.mk_place_deref(place));
 self.bind_local(local, rty);
+ self.drop_local(place.local);
 Operand::Copy(local.into())

makes every reproducer above verify as safe at -C opt-level=0..3, while the unsafe variants stay rejected (if i < v.len() { v[i] = 7; assert!(v[i] == 8); } → Unsat, unguarded v[i] → Unsat, assert!(false) after the call → Unsat). This is offered as evidence for the diagnosis, not as a proposed patch — not reborrowing the operand of a read-only PtrMetadata in ReborrowVisitor at all looks like the cleaner place to fix it.

Not vacuity

The havoc is a genuine over-approximation, so the failure mode is only over-rejection:

• if i < v.len() { let x = v[i]; assert!(false); } → Unsat at -C opt-level=2 (the env is not made inconsistent).
• if i < v.len() { v[i] = 7; assert!(v[i] == 8); } → Unsat at both optimization levels.
• unguarded let x = v[i]; → Unsat at both optimization levels.

Notes

• No existing test covers this: tests/ui/pass/slice_index_mut.rs, slice_first_mut.rs, slice_last_mut.rs and slice_methods_mut.rs all verify at -C opt-level=2 too, because they index a #[thrust::trusted] slice at constant positions and never guard a symbolic index with v.len(). The suite otherwise runs at the default optimization level, so CI never sees the PtrMetadata(copy <&mut>) shape at all — even though tests/ui/pass/list_sum_const.rs shows -C opt-level=3 is a supported configuration.
• The mutability.is_mut() branch in analyze_assignment exists precisely for this optimized shape; in every -C opt-level=0 MIR I inspected (v.len(), (*v).len(), <[T]>::len(v), &mut &mut [T], indexing loops) the PtrMetadata operand is a shared &[T], so the branch appears to be reachable only with optimizations enabled.
• Distinct from Incompleteness: a &mut stored in a Vec (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as Unsat #202 (a &mut stored in a Seq/array-backed container never has its prophecy resolved at drop): here the unresolved &mut is a synthetic reborrow of the container itself, created by ReborrowVisitor, and the referent it havocs is the slice's own (array, length) model.
• Distinct from Incompleteness: unsigned integer types (usize/u32/u64) are modeled as unconstrained integers, so their >= 0 lower bound is not assumed and safe programs are wrongly rejected #165 (usize modeled as an unconstrained integer): the reproducers are rejected even though the guard i < v.len() supplies the upper bound directly, and the identical program with &[i32] verifies.
• Numerical-range / overflow concerns are not involved.

Environment

• branch main @ cd6b330
• solver: Z3 5.0.0 (HORN / Spacer)