Unsound: moving a `&mut`-capturing closure out of a tuple/struct field into a by-value `FnOnce`/`FnMut` verifies panicking programs as `safe`

[coord-e]

Summary

When a non-Copy closure that captures a &mut is moved out of a tuple or struct field (a place with a projection) and passed by value to a higher-order function taking FnOnce/FnMut, Thrust produces a contradictory (⊥) post-state. Everything after the call then verifies vacuously — including assert!(false) — so Thrust reports panicking programs as safe.

This is unsound: the program below always panics at runtime, yet Thrust accepts it.

Reproduction (minimal)

fn apply<F: FnOnce()>(f: F) { f(); }

fn main() {
 let mut x = 0;
 let r = &mut x;
 let t = (|| { *r += 1; },); // &mut-capturing closure, stored in a 1-tuple
 apply(t.0); // moved out of the tuple field (a projection)
 assert!(false); // unreachable-for-Thrust, but ALWAYS panics at runtime
}

$ THRUST_SOLVER=z3 cargo run -q -- -Adead_code -C debug-assertions=false repro.rs ; echo "exit:$?"
exit:0 # Thrust: SAFE

$ rustc --edition 2021 repro.rs -o repro && ./repro ; echo "exit:$?"
thread 'main' panicked at repro.rs:7:5:
assertion failed: false
exit:101 # actually panics

assert!(false) verifying as safe is the tell-tale of a vacuous (bottom) typing environment: after apply(t.0), Thrust's assumptions are unsatisfiable, so any assertion passes.

A more "natural" version that panics for an ordinary reason (the closure runs, so x == 1, not 2) is also wrongly accepted:

fn apply<F: FnOnce()>(f: F) { f(); }
fn main() {
 let mut x = 0;
 let r = &mut x;
 let t = (|| { *r += 1; },);
 apply(t.0);
 assert!(x == 2); // false at runtime (x == 1); Thrust: SAFE
}

What isolates the cause

Program	Thrust verdict	Correct?
let t = (|| { *r += 1; },); apply(t.0); assert!(false);	safe	✗ (always panics)
let w = W { f: || { *r += 1; } }; apply(w.f); assert!(false); (struct field)	safe	✗
apply bound F: FnMut instead of FnOnce, same tuple-field move	safe	✗
Control: let c = || { *r += 1; }; apply(c); assert!(x == 2); (projection-less move)	Unsat (rejected)	✓

The only difference between the last two rows is whether the closure is moved out of a field (t.0 / w.f) or through a projection-less local (c). The projection-less path is handled correctly; the field path is not.

Mechanism

src/analyze/basic_block/visitor/rust_call.rs, "case 3" ({closure} → &mut {closure}, lines ~118-136):

// case 3: {closure} -> &mut {closure}
let borrowed_closure_local = self.insert_mut_borrow(arg_closure_place, arg_closure_ty);
args[0].node = mir::Operand::Move(borrowed_closure_local.into());
// FnOnce::call_once consumes the closure, but the resolved function only borrows it:
// drop the borrow and the environment after the call to resolve the prophecies of the
// captured mutable borrows.
self.analyzer.drop_after_terminator(borrowed_closure_local);
// The original MIR moves the closure into the call, so `moved_locals` dropped its drop
// obligation, expecting the callee to consume it; we must restore it. `moved_locals` only
// steals whole-local moves, so we only restore those: with a projection the obligation was
// never stolen and the normal drop machinery still handles it (re-adding it would
// double-drop). In practice a non-`Copy` closure (the only kind reaching this case) is
// always moved through a projection-less temporary.
if arg_closure_place.projection.is_empty() {
 self.analyzer.drop_after_terminator(arg_closure_place.local);
}

The comment's closing assumption — "a non-Copy closure … is always moved through a projection-less temporary" — does not hold. When the closure is moved out of a tuple/struct field, arg_closure_place is _t.0 (non-empty projection), so the if is skipped. The captured &mut x's prophecy is then never resolved consistently for the enclosing local, and the post-call environment collapses to ⊥ (which is exactly why assert!(false) passes). The projection-less control case takes the if branch and is sound.

The same faulty path is reached whether the consumer is bound FnOnce or FnMut, and whether the field is a tuple element or a named struct field.

Notes

• Valid, safe Rust: the reproducers compile and run under rustc (they panic at runtime, as intended — the point is that Thrust fails to see the panic).
• Distinct from the aggregate/partial-move prophecy issues (Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121, Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122): those concern dropping partially-moved data aggregates; this is about moving a closure out of an aggregate field into a by-value closure-consuming call, and the resulting ⊥ post-state.

Environment

• thrust @ af7cd99 (current main)
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.16.0