Fix double-drop of partially-moved locals

A local with a partial field move (e.g. `move (_2.0)`) was still dropped
wholesale, so dropping it walked into the moved-out sub-place and resolved
the `&mut` prophecy it owns a second time. The two resolutions contradict,
making the clause body unsatisfiable, after which any assertion -- including
false ones -- "verifies" (#121, #122).

`Moves::collect` gathers all non-reference `move`d operands in one body
traversal: whole-local moves (keyed by location, where the local also dies)
and, keyed by parent local, the partial field moves. A dying local is dropped
whole, but its partial-move sub-places are passed to the drop as `except`: the
drop walk skips those subtrees (they are resolved at the move destination) and
resolves the still-owned siblings, so the fix is both sound and complete.

`Env::dropping_assumption` gains the `except` set and `Path::same_place`. The
comparison peels `Deref`, because the drop walk inserts a `Deref` for every
`own`-box the type elaboration introduces (mut locals, and every tuple field)
while the moved-out places come straight from MIR without them; moved-out
places never contain a real deref, so peeling cannot conflate distinct places.

Adds regression tests: the two original shapes (#121, #122), plus a
partially-moved local with a still-owned sibling (completeness) and a soundness
guard where the moved part is used and the sibling is reborrowed.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NU1g7aHMxcSEZgeKProDr1

Author: claude

src/analyze/basic_block.rs

@@ -1,5 +1,5 @@
 use std::borrow::Cow;
-use std::collections::{HashMap, HashSet};
+use std::collections::HashMap;
 
 use rustc_hir::def::DefKind;
 use rustc_index::IndexVec;
@@ -1008,10 +1008,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
     }
 
-    fn drop_places(&mut self, places: HashSet<mir::Place<'tcx>>) {
-        for place in places {
-            tracing::info!(?place, "implicitly dropped");
-            self.env.drop_place(place);
+    fn drop_places(&mut self, set: drop_point::DropSet<'tcx>) {
+        let except: Vec<mir::Place<'tcx>> = set.except.into_iter().collect();
+        for place in set.drops {
+            tracing::info!(?place, ?except, "implicitly dropped");
+            self.env.drop_place(place, &except);
         }
     }
 

src/analyze/basic_block/drop_point.rs

@@ -1,95 +1,134 @@
 use std::collections::{HashMap, HashSet};
 
 use rustc_index::bit_set::DenseBitSet;
-use rustc_middle::mir::{self, BasicBlock, Body, Local};
+use rustc_middle::mir::{self, BasicBlock, Body, Local, Location};
+use rustc_middle::ty::TyCtxt;
 use rustc_mir_dataflow::{impls::MaybeLiveLocals, ResultsCursor};
 
-/// Implicit-drop targets. A drop is a `Place`; a whole-local drop is just a
-/// place with an empty projection (semantically a bare `Local`).
+/// A set of implicit-drop targets: `drops` are places to drop; `except` are
+/// moved-out sub-places to skip when a drop walks into them.
+#[derive(Debug, Clone, Default)]
+pub struct DropSet<'tcx> {
+    pub drops: HashSet<mir::Place<'tcx>>,
+    pub except: HashSet<mir::Place<'tcx>>,
+}
+
+impl<'tcx> DropSet<'tcx> {
+    pub fn insert(&mut self, place: mir::Place<'tcx>) {
+        self.drops.insert(place);
+    }
+
+    fn extend(&mut self, other: &DropSet<'tcx>) {
+        self.drops.extend(other.drops.iter().copied());
+        self.except.extend(other.except.iter().copied());
+    }
+}
+
 #[derive(Debug, Clone, Default)]
 pub struct DropPoints<'tcx> {
-    pub before_statements: HashSet<mir::Place<'tcx>>,
-    after_statements: Vec<HashSet<mir::Place<'tcx>>>,
-    after_terminator: HashMap<BasicBlock, HashSet<mir::Place<'tcx>>>,
-    /// Drops scheduled after the terminator regardless of the target, in
-    /// addition to the liveness-derived sets above.
-    after_terminator_extra: HashSet<mir::Place<'tcx>>,
+    pub before_statements: DropSet<'tcx>,
+    after_statements: Vec<DropSet<'tcx>>,
+    after_terminator: HashMap<BasicBlock, DropSet<'tcx>>,
+    after_terminator_extra: DropSet<'tcx>,
 }
 
 impl DropPoints<'_> {
-    pub fn builder<'mir, 'tcx>(body: &'mir Body<'tcx>) -> DropPointsBuilder<'mir, 'tcx> {
+    pub fn builder<'mir, 'tcx>(
+        tcx: TyCtxt<'tcx>,
+        body: &'mir Body<'tcx>,
+    ) -> DropPointsBuilder<'mir, 'tcx> {
         DropPointsBuilder {
             body,
             bb_ins_cache: HashMap::new(),
+            moves: Moves::collect(tcx, body),
         }
     }
 }
 
 impl<'tcx> DropPoints<'tcx> {
-    pub fn after_statement(&self, statement_index: usize) -> HashSet<mir::Place<'tcx>> {
+    pub fn after_statement(&self, statement_index: usize) -> DropSet<'tcx> {
         self.after_statements[statement_index].clone()
     }
 
     pub fn insert_after_terminator(&mut self, place: mir::Place<'tcx>) {
         self.after_terminator_extra.insert(place);
     }
 
-    pub fn after_terminator(&self, target: &BasicBlock) -> HashSet<mir::Place<'tcx>> {
+    pub fn after_terminator(&self, target: &BasicBlock) -> DropSet<'tcx> {
         let mut set = self.after_terminator[target].clone();
-        set.extend(self.after_statements.last().unwrap().iter().copied());
-        set.extend(self.after_terminator_extra.iter().copied());
+        set.extend(self.after_statements.last().unwrap());
+        set.extend(&self.after_terminator_extra);
         set
     }
 }
 
-#[derive(Debug, Clone)]
+#[derive(Clone)]
 pub struct DropPointsBuilder<'mir, 'tcx> {
     body: &'mir Body<'tcx>,
     bb_ins_cache: HashMap<BasicBlock, DenseBitSet<Local>>,
+    moves: Moves<'tcx>,
 }
 
-/// Locals whose ownership is fully transferred away by the statement (or
-/// terminator) at `statement_index`. Such a local is left uninitialized, so its
-/// 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 `move`d operands of a body, excluding reference-typed places.
 ///
-/// Only owned (non-reference) operands are reported: `move`d references are
-/// turned into reborrows by `ReborrowVisitor`/`RustCallVisitor`, so the source
-/// local remains live and must still be dropped.
-fn moved_locals<'tcx>(
-    body: &Body<'tcx>,
-    bb: BasicBlock,
-    statement_index: usize,
-) -> DenseBitSet<Local> {
-    struct Visitor<'a, 'tcx> {
-        body: &'a Body<'tcx>,
-        locals: DenseBitSet<Local>,
-    }
-    impl<'tcx> mir::visit::Visitor<'tcx> for Visitor<'_, 'tcx> {
-        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`d references are turned into reborrows by
+/// `ReborrowVisitor`/`RustCallVisitor`, so the source still owns its prophecy
+/// and must be dropped normally; they are therefore not recorded here.
+///
+/// A whole-local move leaves the local uninitialized, transferring its entire
+/// drop obligation (including resolving any mutable-borrow prophecies it owns)
+/// to the destination, so it must not be dropped at the move site — where the
+/// local also becomes dead, hence the per-location keying. A partial (projected)
+/// field move transfers only a sub-place, but the parent stays live until its
+/// remaining parts die later; dropping it wholesale at that point would walk
+/// into the moved-out sub-place and resolve its `&mut` prophecy a second time,
+/// so a partially-moved local is excluded from dropping entirely.
+#[derive(Clone, Default)]
+struct Moves<'tcx> {
+    /// Whole-local moves, keyed by the location performing the move.
+    whole: HashMap<Location, DenseBitSet<Local>>,
+    /// Partial field moves, keyed by the parent local.
+    partial: HashMap<Local, Vec<mir::Place<'tcx>>>,
+}
+
+impl<'tcx> Moves<'tcx> {
+    fn collect(tcx: TyCtxt<'tcx>, body: &Body<'tcx>) -> Moves<'tcx> {
+        struct Visitor<'a, 'tcx> {
+            tcx: TyCtxt<'tcx>,
+            body: &'a Body<'tcx>,
+            moves: Moves<'tcx>,
+        }
+        impl<'tcx> mir::visit::Visitor<'tcx> for Visitor<'_, 'tcx> {
+            fn visit_operand(&mut self, operand: &mir::Operand<'tcx>, location: Location) {
+                let mir::Operand::Move(place) = operand else {
+                    return;
+                };
+                if place.ty(&self.body.local_decls, self.tcx).ty.is_ref() {
+                    return;
+                }
+                if place.projection.is_empty() {
+                    self.moves
+                        .whole
+                        .entry(location)
+                        .or_insert_with(|| DenseBitSet::new_empty(self.body.local_decls.len()))
+                        .insert(place.local);
+                } else {
+                    let entry = self.moves.partial.entry(place.local).or_default();
+                    if !entry.contains(place) {
+                        entry.push(*place);
+                    }
                 }
             }
         }
+        let mut visitor = Visitor {
+            tcx,
+            body,
+            moves: Moves::default(),
+        };
+        use mir::visit::Visitor as _;
+        visitor.visit_body(body);
+        visitor.moves
     }
-    let mut visitor = Visitor {
-        body,
-        locals: DenseBitSet::new_empty(body.local_decls.len()),
-    };
-    let loc = mir::Location {
-        statement_index,
-        block: bb,
-    };
-    let data = &body.basic_blocks[bb];
-    use mir::visit::Visitor as _;
-    if statement_index < data.statements.len() {
-        visitor.visit_statement(&data.statements[statement_index], loc);
-    } else if let Some(tmnt) = &data.terminator {
-        visitor.visit_terminator(tmnt, loc);
-    }
-    visitor.locals
 }
 
 fn def_local<'tcx>(data: &mir::BasicBlockData<'tcx>, statement_index: usize) -> Option<Local> {
@@ -121,6 +160,21 @@ fn def_local<'tcx>(data: &mir::BasicBlockData<'tcx>, statement_index: usize) ->
 }
 
 impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
+    /// Turn a set of locals that become dead into the drop targets. A local with
+    /// a partial field move is excluded: dropping it wholesale would resolve the
+    /// moved-out sub-place's `&mut` prophecy a second time (it is resolved at the
+    /// move destination instead).
+    fn drop_set(&self, locals: DenseBitSet<Local>) -> DropSet<'tcx> {
+        let mut set = DropSet::default();
+        for local in locals.iter() {
+            set.drops.insert(local.into());
+            if let Some(moved) = self.moves.partial.get(&local) {
+                set.except.extend(moved.iter().copied());
+            }
+        }
+        set
+    }
+
     pub fn build(
         &mut self,
         results: &mut ResultsCursor<'mir, 'tcx, MaybeLiveLocals>,
@@ -130,7 +184,7 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
 
         let mut after_terminator = HashMap::new();
         let mut after_statements = Vec::new();
-        after_statements.resize_with(data.statements.len() + 1, HashSet::new);
+        after_statements.resize_with(data.statements.len() + 1, DropSet::default);
 
         results.seek_to_block_end(bb);
         let live_locals_after_terminator = results.get().clone();
@@ -147,7 +201,7 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
                 t.subtract(&self.bb_ins_cache[&succ_bb]);
                 t
             };
-            after_terminator.insert(succ_bb, edge_drops.iter().map(Into::into).collect());
+            after_terminator.insert(succ_bb, self.drop_set(edge_drops));
             ins.union(&self.bb_ins_cache[&succ_bb]);
         }
 
@@ -170,8 +224,10 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
                     t.insert(def);
                 }
                 t.subtract(&last_live_locals);
-                t.subtract(&moved_locals(self.body, bb, statement_index));
-                t.iter().map(Into::into).collect()
+                if let Some(moved) = self.moves.whole.get(&loc) {
+                    t.subtract(moved);
+                }
+                self.drop_set(t)
             };
             last_live_locals = live_locals;
         }
@@ -185,10 +241,10 @@ impl<'mir, 'tcx> DropPointsBuilder<'mir, 'tcx> {
             "analyzed implicit drop points"
         );
         DropPoints {
-            before_statements: HashSet::default(),
+            before_statements: DropSet::default(),
             after_statements,
             after_terminator,
-            after_terminator_extra: HashSet::default(),
+            after_terminator_extra: DropSet::default(),
         }
     }
 }

src/analyze/local_def.rs

@@ -1065,7 +1065,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .iterate_to_fixpoint(self.tcx, &self.body, None)
             .into_results_cursor(&self.body);
 
-        let mut builder = analyze::basic_block::DropPoints::builder(&self.body);
+        let mut builder = analyze::basic_block::DropPoints::builder(self.tcx, &self.body);
         for (bb, _data) in mir::traversal::postorder(&self.body) {
             let span = tracing::info_span!("refine_basic_block", ?bb);
             let _guard = span.enter();

src/refine/env.rs

@@ -1087,6 +1087,26 @@ impl Path {
     fn tuple_proj(self, idx: usize) -> Self {
         Path::TupleProj(Box::new(self), idx)
     }
+
+    /// Structural place equality for the drop walk's except-skip. `Deref` is
+    /// treated as transparent on both sides: the drop walk inserts a `Deref`
+    /// for every `own`-box the type elaboration introduces (mut locals, and
+    /// every tuple field), whereas the moved-out places this is compared against
+    /// come straight from MIR and carry no such derefs. Moved-out places never
+    /// contain a real deref (reference moves are excluded upstream), so peeling
+    /// derefs cannot conflate distinct owned places here.
+    fn same_place(&self, other: &Path) -> bool {
+        match (self, other) {
+            (Path::Deref(a), _) => a.same_place(other),
+            (_, Path::Deref(b)) => self.same_place(b),
+            (Path::Local(a), Path::Local(b)) => a == b,
+            (Path::TupleProj(a, i), Path::TupleProj(b, j)) => i == j && a.same_place(b),
+            (Path::Downcast(a, va, fa), Path::Downcast(b, vb, fb)) => {
+                va == vb && fa == fb && a.same_place(b)
+            }
+            _ => false,
+        }
+    }
 }
 
 impl<T> Env<T>
@@ -1110,18 +1130,21 @@ where
         self.path_type(&place.into())
     }
 
-    fn dropping_assumption(&mut self, path: &Path) -> Assumption {
+    fn dropping_assumption(&mut self, path: &Path, except: &[Path]) -> Assumption {
+        if except.iter().any(|e| e.same_place(path)) {
+            return Assumption::default();
+        }
         let ty = self.path_type(path);
         if ty.ty.is_mut() {
             let mut builder = PlaceTypeBuilder::default();
             let (_, term) = builder.subsume(ty);
             builder.push_formula(term.clone().mut_final().equal_to(term.mut_current()));
             builder.build_assumption()
         } else if ty.ty.is_own() {
-            self.dropping_assumption(&path.clone().deref())
+            self.dropping_assumption(&path.clone().deref(), except)
         } else if let Some(tty) = ty.ty.as_tuple() {
             (0..tty.elems.len())
-                .map(|i| self.dropping_assumption(&path.clone().tuple_proj(i)))
+                .map(|i| self.dropping_assumption(&path.clone().tuple_proj(i), except))
                 .collect()
         } else if let Some(ety) = ty.ty.as_enum() {
             let enum_def = self.enum_defs.enum_def(&ety.symbol);
@@ -1174,7 +1197,7 @@ where
                 let Assumption {
                     existentials: assumption_existentials,
                     body: assumption_body,
-                } = self.dropping_assumption(&Path::PlaceTy(Box::new(field_pty)));
+                } = self.dropping_assumption(&Path::PlaceTy(Box::new(field_pty)), except);
                 // dropping assumption should not generate any existential
                 assert!(assumption_existentials.is_empty());
                 formula.push_conj(assumption_body);
@@ -1189,14 +1212,11 @@ where
         }
     }
 
-    pub fn drop_place(&mut self, place: Place<'_>) {
-        let assumption = self.dropping_assumption(&place.into());
+    pub fn drop_place(&mut self, place: Place<'_>, except: &[Place<'_>]) {
+        let except: Vec<Path> = except.iter().map(|p| Path::from(*p)).collect();
+        let assumption = self.dropping_assumption(&place.into(), &except);
         if !assumption.is_top() {
             self.assume(assumption);
         }
     }
-
-    pub fn drop_local(&mut self, local: Local) {
-        self.drop_place(local.into());
-    }
 }

tests/ui/fail/partial_move_drop.rs

@@ -0,0 +1,15 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+// Regression test for #121: a local that is partially moved must not have a
+// dropping assumption emitted for the moved-out portion. Here `(&mut a,)` is
+// moved out of `s` into `b`; dropping `s` wholesale used to resolve the
+// moved-out `&mut a` prophecy a second time, making the constraints
+// contradictory so that this false assertion was wrongly accepted.
+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
+}