Unsound: the drop-flag edge of a conditionally-moved value still gets a liveness-derived implicit drop, so the consumed path's `&mut` prophecy is re-resolved and that path vanishes — `if flag { f(); }` over an `FnOnce` verifies panicking programs as `safe`

[coord-e]

Summary

When a local that owns a &mut prophecy is moved on one path but not another (if cond { consume(v); }), rustc's drop elaboration inserts a drop flag and a conditional drop in a later block:

bb0: _5 = const true;  switchInt(flag) -> [0: bb3, otherwise: bb1]
bb1: _5 = const false; _4 = move _1; consume(move _4) -> bb2   // moved: no drop needed
bb3/bb2: goto -> bb4
bb4: switchInt(_5) -> [0: bb5, otherwise: bb6]                 // _5 == false  <=>  already moved
bb5: return
bb6: drop(_1) -> bb5

DropPoints computes the drops on a terminator edge purely as a liveness difference (src/analyze/basic_block/drop_point.rs:167-172) and, unlike the per-statement sets, never subtracts moved locals. _1 is live at the end of bb4 (because bb6 drops it) and dead at bb5, so the analyzer emits an implicit drop_local(_1) on the bb4 -> bb5 edge — which is exactly the edge the program takes when _1 was already consumed.

Env::drop_local → dropping_assumption then emits mut_final(t) = mut_current(t) for the &mut that the callee already took ownership of and wrote through. The two resolutions of the same prophecy contradict each other, so the "value was consumed" path becomes an unsatisfiable clause body and silently disappears from the analysis. The caller is left reasoning as if the callback/consumer had never run, and programs that panic at runtime verify as safe.

This is the accepts-unsafe (false negative) direction, at the default -C opt-level=0, with no annotations involved.

Minimal reproduction (closure — the idiomatic shape)

repro.rs:

fn maybe<F: FnOnce()>(f: F, flag: bool) {
    if flag {
        f();
    }
}

#[thrust::callable]
fn check(a: i64, flag: bool) {
    let mut x = a;
    maybe(|| { x += 1; }, flag);
    assert!(x == a);   // FALSE at runtime whenever `flag`
}

fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs && echo safe
safe                                    # <- WRONG

Expected: Unsat. Actual: safe.

Ground truth (runnable)

fn maybe<F: FnOnce()>(f: F, flag: bool) { if flag { f(); } }
fn check(a: i64, flag: bool) {
    let mut x = a;
    maybe(|| { x += 1; }, flag);
    assert!(x == a);
}
fn main() { check(0, true); }

$ rustc -Adead_code --edition 2021 -C debug-assertions=off -o gt gt.rs && ./gt
thread 'main' panicked at gt.rs:5:5:
assertion failed: x == a

The bug is not about closures

The same hole is reachable with a plain by-value struct, as long as it (a) owns a &mut and (b) has drop glue, so drop elaboration emits a flag:

struct W<'a> { r: &'a mut i64, tag: Box<i64> }
impl<'a> thrust_models::Model for W<'a> {
    type Ty = (
        thrust_models::model::Mut<thrust_models::model::Int>,
        thrust_models::model::Box<thrust_models::model::Int>,
    );
}

fn consume(w: W) { *w.r = 1; }
fn maybe(w: W, flag: bool) { if flag { consume(w); } }

#[thrust::callable]
fn check(a: i64, flag: bool) {
    let mut x = a;
    maybe(W { r: &mut x, tag: Box::new(0) }, flag);
    assert!(x == a);   // FALSE at runtime when `flag` and `a != 1`
}

fn main() {}

check(5, true) panics under plain rustc; Thrust reports safe.

Real-world shape

The pattern "consume the callback only on one branch" is exactly what a hand-written lazy default looks like, and it is silently mis-verified:

fn or_else<F: FnOnce() -> i64>(o: Option<i64>, f: F) -> i64 {
    match o {
        Some(v) => v,
        None => f(),
    }
}

#[thrust::callable]
fn check(a: i64, o: Option<i64>) {
    let mut x = a;
    let _r = or_else(o, || { x += 1; 0 });
    assert!(x == a);   // FALSE when `o == None`; Thrust says `safe`
}

Any user-written unwrap_or_else / map_or_else / run_if / early-return-before-the-callback helper has this shape. std's own combinators are unaffected only because they are covered by #[thrust::extern_spec_fn] summaries in std.rs.

Isolation

All rows are the closure reproduction above, differing only in the marked part.

Case	Verdict	Correct?
if flag { f(); }, assert!(x == a)	safe	❌ bug (panics when flag)
same, assert!(x == a + 1)	Unsat	✅ (not true when !flag)
same, assert!(false)	Unsat	✅ — the surviving !flag path still refutes it
same, assert!(x == a || x == a + 1)	safe	✅
flag is the literal true: maybe(|| { x += 1; }, true), assert!(false)	safe	❌ bug — the !flag path is infeasible too, so the body is fully vacuous
unconditional call: fn always<F: FnOnce()>(f: F) { f(); }, assert!(x == a)	Unsat	✅ — whole-local move handled by moved_locals
both branches consume: if flag { consume(w) } else { consume(w) }	Unsat	✅ — no drop flag is generated
F: FnMut with mut f: F (callee borrows instead of moving)	Unsat	✅ — no conditional move
F: Fn, closure captures by shared ref	Unsat	✅
conditionally-moved value without a &mut inside	safe	✅ (nothing to double-resolve)

So the trigger is precisely: a local owning a &mut prophecy that is moved on some but not all paths, i.e. whenever MIR drop elaboration introduces a drop flag. Note the fifth row: with a statically-known condition the not-taken branch is infeasible as well, and then every assertion after the call verifies, assert!(false) included.

Root cause

DropPointsBuilder::build (src/analyze/basic_block/drop_point.rs):

let edge_drops = {
    let mut t = live_locals_after_terminator.clone();
    t.subtract(&self.bb_ins_cache[&succ_bb]);
    t
};
after_terminator.insert(succ_bb, edge_drops);           // :167-172  — liveness only
...
after_statements[statement_index] = {
    let mut t = live_locals.clone();
    ...
    t.subtract(&moved_locals(self.body, bb, statement_index));   // :195  — moves excluded here
    t
};

The per-statement set excludes locals whose ownership was transferred (moved_locals, whose doc comment states the invariant: a moved local's "drop obligation (including resolving any mutable-borrow prophecies it owns) moves to the destination and it must not be dropped at the move site"). The edge set has no such exclusion — and it could not have one locally, because the move happens in an earlier block (bb1) while the spurious drop is emitted on an edge of a later one (bb4 -> bb5). Move/initializedness state is not propagated across basic blocks at all; the block type at the join re-binds _1 from liveness alone.

analyze_terminator_goto then consumes that set for SwitchInt (src/analyze/basic_block.rs:1374-1385) — and likewise for Call, Drop and Assert targets — calling drop_local for each local.

With RUST_LOG=info on the non-closure variant:

INFO ... implicitly dropped for target local=_1 target=bb5 def=maybe bb=bb4
         term=switchInt(copy _5) -> [0: bb5, otherwise: bb6]

_5 is the drop flag; _5 == false means "_1 was moved in bb1, do not drop". Thrust drops it anyway.

The resulting contradiction is visible in the emitted CHCs (THRUST_OUTPUT_DIR): the clause for the bb4 -> bb5 edge carries (= (mut_final<Int> (tuple_proj<Mut<Int>>.0 v0)) (mut_current<Int> (tuple_proj<Mut<Int>>.0 v0))) on the very same v0 that the callee's postcondition constrains with (= (mut_final<Int> ...) (+ ... 1)).

This is distinct from #121/#122, which are about partial moves (move (_1.0), a projection) being missed by moved_locals within one block: here the move is a plain whole-local move _1 that moved_locals does record, and the fixes proposed there (track partially-moved sub-places / skip moved subtrees in dropping_assumption) do not cover a drop scheduled on a later block's edge. It is also distinct from #177/#207, which need the closure to be moved out of an aggregate.

Expected behavior

An implicit drop must only be emitted for a local that is still initialized on that edge. rustc's MaybeInitializedPlaces dataflow gives exactly this information and is already pulled into local_def.rs (for reassign_local_mutabilities), so the edge-drop set could be intersected with the maybe-initialized set at the successor's entry. Alternatively, since drop elaboration already materialized the decision as a drop flag, the liveness-derived drop could be suppressed for locals that MIR itself drops conditionally, leaving the explicit TerminatorKind::Drop in bb6 as the single drop point.

Whatever the mechanism, no path may resolve a &mut prophecy that a callee has already taken ownership of — otherwise the path is not merely imprecise but removed from the analysis.

Environment

• thrust @ 35eea46
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration, -C opt-level=0 (default)
• Uses only supported features (i64, &mut, FnOnce, if, assert!); no numeric-range/overflow/unsigned involvement — the constants are 0, 1, 5.