Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows

Summary

moved_locals in src/analyze/basic_block/drop_point.rs only treats a move operand as an ownership transfer when the moved place is a whole local (place.projection.is_empty()). When a value is moved out of a projection (a partial move, e.g. let b = s.0;), the source local is still considered dead-and-droppable at the move site, so the analyzer emits an implicit drop for it.

Env::drop_local → dropping_assumption (src/refine/env.rs) then walks the local's full type — including the part that was just moved away — and emits the prophecy-resolving assumption mut_final(t) = mut_current(t) for a mutable reference whose ownership (and drop obligation) actually transferred to the destination of the move. When the program later writes through the moved reference, its prophecy is resolved a second time to a different value, making the environment assumptions inconsistent (1 = 2), after which any assertion verifies.

The result is that Thrust verifies programs that panic at runtime.

Reproduction

fn main() {
    let mut a = 1_i64;
    let s = ((&mut a,),);
    let b = s.0;     // partial move: `(&mut a,)` moves out of `s`
    *b.0 = 2;
    assert!(a == 1); // false at runtime: a == 2
}

This program panics when compiled with plain rustc:

$ rustc -C debug-assertions=off partial_move.rs && ./partial_move
thread 'main' panicked at partial_move.rs:6:5:
assertion failed: a == 1

but Thrust (at 1d85b18, z3 4.13.4) accepts it:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false partial_move.rs && echo verified safe
verified safe

Control: the whole-local move is handled correctly

Replacing the partial move with a whole-local move (which is recorded by moved_locals) makes Thrust reject the program as expected:

fn main() {
    let mut a = 1_i64;
    let s = ((&mut a,),);
    let b = s;       // whole-local move: drop of `s` correctly suppressed
    *(b.0).0 = 2;
    assert!(a == 1);
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false whole_move.rs
error: verification error: Unsat

The only difference between the two programs is whether the move operand has a projection.

Analysis

The optimized MIR of the reproducer is:

bb0: {
    _1 = const 1_i64;            // a
    _4 = &mut _1;
    _3 = (move _4,);
    _2 = (move _3,);             // s
    _5 = move (_2.0: (&mut i64,)); // b — partial move out of s
    _8 = deref_copy (_5.0: &mut i64);
    (*_8) = const 2_i64;
    _6 = copy _1;
    switchInt(move _6) -> [1: bb2, otherwise: bb1];
}

With RUST_LOG=info, the analyzer logs:

implicitly dropped after statement local=_2 stmt_idx=4

i.e. s (_2) is implicitly dropped immediately after the partial move _5 = move (_2.0).

Two pieces interact:

moved_locals (src/analyze/basic_block/drop_point.rs, in fn moved_locals):
```
fn visit_operand(&mut self, operand: &mir::Operand<'tcx>, _location: mir::Location) {
    if let mir::Operand::Move(place) = operand {
        if place.projection.is_empty() && !self.body.local_decls[place.local].ty.is_ref() {
            self.locals.insert(place.local);
        }
    }
}
```
move (_2.0) has a non-empty projection, so _2 is not recorded as moved. Since _2 is dead after this statement (per MaybeLiveLocals), it lands in the implicit-drop set for stmt_idx = 4. The doc comment above this function even states the invariant being violated: 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" — but this is only enforced for whole-local moves.
dropping_assumption (src/refine/env.rs) is type-driven and walks the entire current type of the dropped local. For s it recurses tuple → own → tuple → own → mut and reaches the &mut i64 that was just moved into b, emitting:
```
builder.push_formula(term.clone().mut_final().equal_to(term.mut_current()));
```
i.e. final(a-borrow) = current(a-borrow) = 1. Because the environment binding for the moved-out field still points at the same temp-var chain that b's binding was derived from, the later assignment *b.0 = 2 resolves the same prophecy to 2. The CHC body now contains both final = 1 and final = 2, so the clause body is unsatisfiable and the false assertion a == 1 is "verified".

Note that the more common partial-move shape let b = s.0; where the field type is &mut T itself is not affected, because ReborrowVisitor::visit_operand turns moves of Ref-typed operands into reborrows. The hole is reachable whenever the moved projection's type is a non-reference type that (transitively) owns a mutable borrow — e.g. a tuple/struct field of type (&mut T,), Box<&mut T>, or a struct containing a &mut.

Expected behavior

A local that is partially moved must not have a dropping assumption emitted for the moved-out portion (or, conservatively, for any portion). Either:

record partially-moved locals in moved_locals (possibly tracking which projection was moved, so the remaining fields can still be dropped soundly), or
make dropping_assumption skip subtrees whose ownership has been transferred away.

Environment

thrust @ 1d85b18 ("Resolve named struct fields in formula translation (Resolve named struct fields in formula translation #118)")
rustc nightly-2025-09-08 (per rust-toolchain.toml)
z3 4.13.4, default solver configuration

Fix double-drop of partially-moved locals via PlaceSet drop points

Fix double-drop of partially-moved locals in drop points

Fix double-drop of partially-moved locals

The same hole is reachable through an enum variant field, and #155 as written does not close it

While looking for unsoundness in &mut-heavy real-world shapes I hit this bug again, but through a projection kind neither this issue nor #122 mentions: a Downcast + Field partial move, i.e. an ordinary match / if let that binds an enum payload by value.

This matters because it makes the hole reachable from completely idiomatic code — if let Some(x) = … where the payload is not itself a reference but owns one. Common std shapes with exactly that type:

slice::split_first_mut → Option<(&mut T, &mut [T])>
iter_mut().enumerate().next() → Option<(usize, &mut T)>
any Option<W> / Result<W, E> where W is a struct or tuple holding a &mut

Reproductions (thrust @ `35eea46`, rustc nightly-2025-09-08, z3 5.0.0)

All three are accepted; rustc -C debug-assertions=off panics on the first one.

// rep1.rs — Option payload is a tuple that owns a &mut
fn main() {
    let mut a = 1_i64;
    {
        let o: Option<(&mut i64,)> = Some((&mut a,));
        if let Some(t) = o {
            *t.0 = 2;
        }
    }
    assert!(a == 1); // false at runtime: a == 2
}

// rep2.rs — Option payload is a struct holding a &mut
struct Wrap<'a> { r: &'a mut i64 }
impl<'a> thrust_models::Model for Wrap<'a> { type Ty = Wrap<'a>; }

fn main() {
    let mut a = 1_i64;
    {
        let o: Option<Wrap> = Some(Wrap { r: &mut a });
        if let Some(w) = o {
            *w.r = 2;
        }
    }
    assert!(false); // accepted — the constraints are contradictory, not merely weak
}

// rep3.rs — nested enums: Result<Option<&mut i64>, i64>
fn main() {
    let mut a = 1_i64;
    {
        let o: Result<Option<&mut i64>, i64> = Ok(Some(&mut a));
        if let Ok(inner) = o {
            if let Some(r) = inner { *r = 2; }
        }
    }
    assert!(false); // accepted
}

$ ./thrust-rustc -Adead_code -C debug-assertions=false rep1.rs && echo safe
safe
$ rustc -C debug-assertions=off rep1.rs && ./rep1
thread 'main' panicked at rep1.rs:10:5:
assertion failed: a == 1

Control — when the payload is &mut i64 itself, ReborrowVisitor turns the move into a reborrow (as this issue already notes) and the program is correctly rejected:

fn main() {
    let mut a = 1_i64;
    { let o: Option<&mut i64> = Some(&mut a); if let Some(r) = o { *r = 2; } }
    assert!(a == 1); // correctly Unsat
}

Same root cause

rep1's NLL MIR has the partial move as a Downcast+Field projection:

bb2: {
    _8 = move ((_3 as Some).0: (&mut i64,));
    (*(_8.0: &mut i64)) = const 2_i64;
    ...
}

and RUST_LOG=info confirms the wholesale drop of the parent right after it:

INFO implicitly dropped after statement local=_2 stmt_idx=0 bb=bb1   # _2/_3 = the Option local

moved_locals' place.projection.is_empty() check misses it exactly as described in this issue, so s's &mut a prophecy is resolved both at the wholesale drop and at *t.0 = 2, and the clause body goes contradictory.

I confirmed the root cause by relaxing that one condition locally (dropping the projection.is_empty() requirement in moved_locals): all three reproductions then correctly report Unsat.

Why #155 does not fix it

I built PR #155 (a87b28e) and re-ran the three programs — all three are still accepted. The relevant part is the enum branch of dropping_formula_for_term:

// A field is reached through a matcher selector rather than a
// projection, so the walk stays at the enum's path and a
// moved-out field is not skipped.
body.push_conj(self.dropping_formula_for_term(
    existentials, &field_type, field_term,
    path,      // <- the enum's own path, not path.downcast(variant, field)
    except,
));

Moves::collect does record ((_3 as Some).0) as a partial move, and elaborated_path does build a Path::Downcast(Local(_3), Some, 0) for it — but since the walk keeps passing the enum's own Path::Local(_3) down into the variant fields, except.contains(path) can never match and the moved-out field's prophecy is resolved anyway. The carve-out in that comment is a soundness hole, not just an incompleteness.

Possible directions, in case they're useful:

Thread the field's Path::Downcast(path, variant, field) (the variant already carries discr/field_idx in FlowBinding::Enum, and Path::Downcast already exists) into the recursive call so except can match it, or
conservatively suppress the whole-local drop of an enum whose variant field was moved out — the sibling-drop concern that motivated per-field precision for tuples doesn't arise here, since only one variant's fields are live at a time.

Happy to open this as a separate issue instead if you'd rather track the enum case on its own.

Generated by Claude Code

Fix double-drop of partially-moved locals

Navigation Menu

Repository navigation

Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out `&mut` borrows #121

Summary

Reproduction

Control: the whole-local move is handled correctly

Analysis

Expected behavior

Environment

The same hole is reachable through an enum variant field, and #155 as written does not close it

Reproductions (thrust @ `35eea46`, rustc nightly-2025-09-08, z3 5.0.0)

Same root cause

Why #155 does not fix it

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121

Description

Summary

Reproduction

Control: the whole-local move is handled correctly

Analysis

Expected behavior

Environment

Activity

coord-e commented on Aug 29, 2026

The same hole is reachable through an enum variant field, and #155 as written does not close it

Reproductions (thrust @ 35eea46, rustc nightly-2025-09-08, z3 5.0.0)

Same root cause

Why #155 does not fix it

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out `&mut` borrows #121

Reproductions (thrust @ `35eea46`, rustc nightly-2025-09-08, z3 5.0.0)