Unsound: at `-C opt-level >= 1` a compound assignment through a `&mut` that sits behind a projection is reborrowed twice, the two prophecy resolutions contradict the write, and the function verifies vacuously — even `assert!(false)` is `safe`

[coord-e]

Summary

ReborrowVisitor::visit_operand (src/analyze/basic_block/visitor/reborrow.rs:109-128) turns every &mut-typed operand place into a fresh reborrow and rewrites the operand to Move(new_local):

fn visit_operand(&mut self, operand: &mut mir::Operand<'tcx>, location: mir::Location) {
    let Some(p) = operand.place() else { ... };
    let mir_ty::TyKind::Ref(_, inner_ty, m) = p.ty(&self.analyzer.local_decls, self.tcx).ty.kind() else { ... };
    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());
    }
    ...
}

operand.place() matches Operand::Move and Operand::Copy. For a Move this is right — Rust's &mut is not Copy, so the source is consumed and the new reborrow is the only live handle. But MIR optimizations do produce Operand::Copy of a &mut-typed place: Derefer hoists the base of a deref chain into a temp _t = deref_copy P (Rvalue::CopyForDeref), and GVN rewrites that into _t = copy P (GVN runs from mir_opt_level >= 2, i.e. from -C opt-level=1 upward — the same rewrite that #244 reports for Box).

Such a temp is a pointer copy that exists only to be dereferenced, not an aliasing use. When a single statement carries two of them for the same reference — which is exactly what a compound assignment *p += e through a &mut that sits behind a projection lowers to — Thrust creates two simultaneously-live reborrows of the same reference. At the end of the block both are dropped and each prophecy is resolved to the identity, while the write constrains one of them to current + 1. The three constraints are jointly unsatisfiable, so the block's Horn clause has a false body, its exit predicate is left unconstrained, and every obligation downstream of the call is discharged vacuously.

The result is a silent, unsound, optimization-level-dependent safe: with -C opt-level=1 (also s and z, and 2/3 when the closure crosses a function boundary) a program that panics at run time verifies as safe, and so does assert!(false).

At -C opt-level=0 the temp is still Rvalue::CopyForDeref, which is not an Operand and therefore never reaches visit_operand; rvalue_type binds it with place_type(elaborate_place(P)), a single reborrow is created, and the prophecy is threaded correctly.

Minimal reproduction

No annotations, no Box, no slices:

fn main() {
    let mut cnt = 0_i64;
    let mut f = || { cnt += 1; };
    f();
    assert!(false);        // <- unreachable only if the environment is inconsistent
}

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

error: aborting due to 1 previous error

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

assert!(false) verifying is the clearest statement of the problem, but the same holds for an assertion that is merely false about the program:

fn main() {
    let mut cnt = 0_i64;
    let mut f = || { cnt += 1; };
    f();
    assert!(cnt == 100);   // false: cnt == 1
}

$ rustc -Adead_code --edition 2021 -O -o min min.rs && ./min
thread 'main' panicked at min.rs:5:5:
assertion failed: cnt == 100
$ cargo run -q -- -Adead_code -C debug-assertions=false -C opt-level=1 min.rs && echo safe
safe

This is vacuity, not a wrong value

Unlike #244, the accepting side here is not "the environment says something else"; the environment is inconsistent, so every mutually contradictory assertion is accepted at once at -C opt-level=1:

assertion after f()	opt-level 0	opt-level 1
assert!(cnt == 1) (true)	safe ✔	safe
assert!(cnt == 100) (false)	Unsat ✔	safe ❌
assert!(false)	Unsat ✔	safe ❌

A closure is not required

Any &mut reached through one more projection reproduces it — the closure upvar is just the most common such place. Both of these are ordinary Rust:

// &mut field of a struct, mutated through a &mut to the struct
struct H<'a> { m: &'a mut i64 }
impl<'a> thrust_models::Model for H<'a> { type Ty = Self; }

fn bump(h: &mut H) { *h.m += 1; }

fn main() {
    let mut x = 0_i64;
    { let mut h = H { m: &mut x }; bump(&mut h); }
    assert!(x == 100);   // false: x == 1 — `safe` at -C opt-level=1
}

// &mut in a tuple, mutated through a &mut to the tuple
fn bump(t: &mut (&mut i64,)) { *t.0 += 1; }

fn main() {
    let mut x = 0_i64;
    { let mut t = (&mut x,); bump(&mut t); }
    assert!(x == 100);   // false: x == 1 — `safe` at -C opt-level=1
}

Both panic under rustc -O (exit 101) and both verify as safe at -C opt-level=1.

Behaviour matrix

All with -Adead_code -C debug-assertions=off. A = the closure reproducer, B = the struct-field one, C = the tuple one, E = the closure passed to a generic HOF (fn call<F: FnMut() -> i64>(mut f: F) -> i64 { f() }), D = let mut r = &mut x; let rr = &mut r; **rr += 1;.

program	0	1	2	3	s	z
A assert!(cnt == 100) — false	Unsat ✔	safe ❌	Unsat ✔	Unsat ✔	safe ❌	safe ❌
A assert!(false)	Unsat ✔	safe ❌	Unsat ✔	Unsat ✔	safe ❌	safe ❌
A assert!(cnt == 1) — true	safe ✔	safe	safe ✔	safe ✔	safe	safe
B assert!(x == 100) — false	Unsat ✔	safe ❌	Unsat ✔	Unsat ✔	safe ❌	safe ❌
C assert!(x == 100) — false	Unsat ✔	safe ❌	Unsat ✔	Unsat ✔	safe ❌	safe ❌
E assert!(r == 100) — false	Unsat ✔	safe ❌	safe ❌	safe ❌	safe ❌	safe ❌
D assert!(x == 100) — false	Unsat ✔	ICE	ICE	ICE	ICE	ICE

2/3 recover for A/B/C only because the callee is inlined into main there (scope 3 (inlined main::{closure#0}) in the -Zunpretty=mir output), which folds *_2 = Add(copy (*_3), 1) back onto the caller's own &mut local and makes the two-temp shape disappear; as soon as the closure crosses a function boundary that inlining cannot undo (row E) the wrong safe is back at every level from 1 to z.

Row D (&mut &mut) instead ICEs at src/refine/env.rs:1014 with borrowing unbound var from -C opt-level=1 upward — noted as an observation, not as a claim that it is the same defect.

Root cause, step by step

cnt += 1 inside the closure lowers to two deref temps for the upvar. At -C opt-level=0:

fn main::{closure#0}(_1: &mut {closure@min.rs:3:17: 3:19}) -> () {
    _2 = deref_copy ((*_1).0: &mut i64);      // Rvalue::CopyForDeref
    _3 = deref_copy ((*_1).0: &mut i64);      // Rvalue::CopyForDeref
    (*_2) = Add(copy (*_3), const 1_i64);

At -C opt-level=1 GVN rewrites both:

-    _2 = deref_copy ((*_1).0: &mut i64);
-    _3 = deref_copy ((*_1).0: &mut i64);
+    _2 = copy ((*_1).0: &mut i64);
+    _3 = copy ((*_1).0: &mut i64);
     (*_2) = Add(copy (*_3), const 1_i64);

Rvalue::CopyForDeref holds a Place, not an Operand, so at 0 the visitor never sees it. At 1 both statements are Rvalue::Use(Operand::Copy(place)) with place: &mut i64, so visit_operand fires on each. RUST_LOG=thrust=info shows exactly that — one reborrow of the upvar at 0, two at 1:

### opt0
implicitly reborrowed old_place=(*((*_1).0: &mut i64)) new_local=_4 def=main::{closure#0}

### opt1
implicitly reborrowed old_place=(*((*_1).0: &mut i64)) new_local=_4 def=main::{closure#0}
implicitly reborrowed old_place=(*((*_1).0: &mut i64)) new_local=_5 def=main::{closure#0}
implicitly reborrowed old_place=(*_2)                  new_local=_6 def=main::{closure#0}

CHC evidence

The closure body's clause (c4 in THRUST_OUTPUT_DIR) at -C opt-level=1, with the mut equalities propagated:

(= (mut v6 v5)  (mut v2 v4))    ; reborrow #1 of the upvar       -> v6 = v2, v5 = v4
(= (mut v8 v7)  (mut v6 v5))    ;                                -> v8 = v2, v7 = v4
(= (mut v11 v10)(mut v4 v9))    ; reborrow #2 of the upvar       -> v11 = v4, v10 = v9
(= (mut v13 v12)(mut v11 v10))  ;                                -> v13 = v4, v12 = v9
(= (mut v16 v15)(mut v8 v14))   ; reborrow of _2                 -> v16 = v2, v15 = v14
(= v18 (mut_current (mut v13 v12)))          ; the read:  v18 = v4
(= (mut_final (mut v16 v15)) (+ v18 1))      ; the write: v15 = v4 + 1
(= (mut_final (mut v14 v7)) (mut_current …)) ; drop:      v7  = v14, and v7 = v4  =>  v14 = v4
(= (mut_final (mut v13 v12)) (mut_current …)); drop:      v12 = v13

v15 = v14 = v4 from the drops, and v15 = v4 + 1 from the write. The body is unsatisfiable, so c4 says nothing about its head p3; p3 may be false, which makes the caller's clause c1 vacuous, p5 unconstrained, and the panic clause c2 (head false) trivially satisfiable. The system is sat — reported as safe.

At -C opt-level=0 the same clause has a single reborrow and is satisfiable:

(= (mut v6 v5) (mut v2 v4))                  ; the one reborrow
(= v8 (mut_current (mut v6 v5)))             ; v8 = v2
(= (mut_final (mut v6 v5)) (+ v8 1))         ; v4 = v2 + 1
(= (mut_final (mut (tuple (mut v4 v1)) v0)) (mut_current …))   ; upvar resolved once

The two copies must overlap

Writing the increment so the two temps do not live at the same time is handled correctly at every level, which pins the trigger to the overlap rather than to the rewrite alone:

let mut f = || { cnt = cnt + 1; };   // Unsat at 0 and at 1 — correct
let mut f = || { cnt = 1; };         // Unsat at 0 and at 1 — correct
let mut f = || { cnt += 1; };        // Unsat at 0, safe at 1 — the bug

MIR for the middle one at -C opt-level=1 still contains two copy ((*_1).0) statements, but the first temp is read and dead before the second is created, so the reborrows are created and resolved one at a time.

Distinct from the known issues

• Unsound: at -C opt-level >= 1 GVN rewrites the Box deref temp from deref_copy to copy, so unelaborate_derefs misses it and every write through a nested Box lands on a copy — panicking programs verify as safe #244 / PR Unelaborate the Box deref temps GVN rewrites into copies #245 share the trigger (GVN rewriting a deref_copy temp into a copy) but nothing else. Unsound: at -C opt-level >= 1 GVN rewrites the Box deref temp from deref_copy to copy, so unelaborate_derefs misses it and every write through a nested Box lands on a copy — panicking programs verify as safe #244 is about Box: extract_elaborated_deref fails to unelaborate the deref chain, Box is modeled by value, and the write lands on an independent copy — a wrong value, explicitly not vacuity. Here there is no Box anywhere, nothing goes through unelaborate_derefs, and the failure is an inconsistent environment. I built the Unelaborate the Box deref temps GVN rewrites into copies #245 branch (9d842ec) and re-ran every reproducer above: all of them still report safe at -C opt-level=1. That is expected — Unelaborate the Box deref temps GVN rewrites into copies #245's new Use(Copy) case is gated on box_deref_temps, a set populated only from ElaborateBoxDerefs Transmute chains, and a &mut i64 temp is never in it.
• 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 is the other optimization-level-dependent one: a ReborrowVisitor-created reborrow whose prophecy is never resolved, which havocs the referent and only ever over-rejects, triggered by PtrMetadata on &mut [T]. Here the prophecies are all resolved — too many times — and the result is a wrong safe. No slices and no len() are involved.
• Unsound: a two-phase borrow (v.push(v.len())) havocs the receiver before the arguments are evaluated, so reads in the argument see the prophecy — panicking programs verify as safe #209 (two-phase borrows) needs a method call taking &mut self with the receiver read in an argument; these reproducers have no two-phase borrow and no such call, and they behave correctly at -C opt-level=0.
• Unsound: moving a &mut-capturing closure out of a tuple/struct field into a by-value FnOnce/FnMut verifies panicking programs as safe #177 / Unsound: moving a &mut-capturing closure out of any aggregate (incl. enum/Option), with no higher-order call, drops its prophecy and verifies panicking programs as safe (generalizes #177) #207 are about a &mut-capturing closure moved out of an aggregate; here the closure is called directly (row A) or absent entirely (rows B, C), and the verdict is correct at the default optimization level.
• Not a numerical-range, overflow or unsigned issue: the only values are 0, 1 and 100.

Reachable from the existing suite

tests/ui/pass/closure_mut_capture_pre_post.rs is row E. It verifies at every optimization level, but from -C opt-level=1 upward it does so vacuously: appending assert!(false); to its main still gives safe at 1, 2, 3, s and z, and Unsat only at 0. CI never notices because the suite runs at the default optimization level.

A sweep of the whole tests/ui/pass suite with assert!(false) appended to main finds no vacuous test at -C opt-level=0 — 168 of the 169 tests are correctly Unsat there (the 16 pcsat-backed ones included; iterators/annot_range_next.rs is the one the mechanical injection could not apply to) — and exactly this one at -C opt-level=2.

Environment

• reproduced on main @ cd6b330, on 35eea46, and on the Unelaborate the Box deref temps GVN rewrites into copies #245 branch @ 9d842ec
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration