From f3e4a91974b75f82b11224b07912cbcb58940d5f Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 13 Jun 2026 07:39:06 +0000 Subject: [PATCH] fix: don't drop partially-moved sub-places (resolves #121, #122) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `moved_locals` only excluded whole-local moves from the implicit-drop set, so a local with a partial field move (e.g. `move (_2.0)`) was still dropped wholesale. `Env::dropping_assumption` then walked the moved-out subtree and resolved the `&mut` prophecy it owns a second time, yielding contradictory constraints (`final = 1` and `final = 2`) under which any assertion — including false ones — verifies. Track partial field-moves per local (skipping ref-typed moves, which become reborrows and keep the source live) and skip the moved-out subtree when emitting the dropping assumption for the parent. Adds pass/fail regression tests for both the partial-move-into-local (#121) and partial-move-into-call (#122) shapes. https://claude.ai/code/session_01Fovh1a8R5EtDd98ic9EJfR --- src/analyze/basic_block.rs | 12 ++++++- src/analyze/basic_block/drop_point.rs | 41 ++++++++++++++++++++++++ src/refine/env.rs | 41 +++++++++++++++++++++--- tests/ui/fail/partial_move_drop.rs | 15 +++++++++ tests/ui/fail/partial_move_field_call.rs | 22 +++++++++++++ tests/ui/pass/partial_move_drop.rs | 13 ++++++++ tests/ui/pass/partial_move_field_call.rs | 19 +++++++++++ 7 files changed, 157 insertions(+), 6 deletions(-) create mode 100644 tests/ui/fail/partial_move_drop.rs create mode 100644 tests/ui/fail/partial_move_field_call.rs create mode 100644 tests/ui/pass/partial_move_drop.rs create mode 100644 tests/ui/pass/partial_move_field_call.rs diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index b76fb1a3..fd4c4e96 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -145,6 +145,10 @@ pub struct Analyzer<'tcx, 'ctx> { local_decls: IndexVec>, // TODO: remove this prophecy_vars: HashMap, + /// Sub-places partially moved out of a local somewhere in the body, keyed by + /// that local. Consulted when dropping so a wholesale drop does not + /// re-resolve a moved-out `&mut` prophecy. Recomputed from `body`. + partial_moves: HashMap>>, } impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { @@ -952,7 +956,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } fn drop_local(&mut self, local: Local) { - self.env.drop_local(local); + match self.partial_moves.get(&local) { + Some(moved) => self.env.drop_local_with_moved(local, moved), + None => self.env.drop_local(local), + } } fn add_prophecy_var(&mut self, statement_index: usize, ty: mir_ty::Ty<'tcx>) { @@ -1335,6 +1342,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let local_decls = body.local_decls.clone(); let prophecy_vars = Default::default(); let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id()); + let partial_moves = drop_point::partial_moved_places(tcx, &body); Self { ctx, tcx, @@ -1346,6 +1354,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { env, local_decls, prophecy_vars, + partial_moves, } } @@ -1357,6 +1366,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { pub fn body(&mut self, body: Body<'tcx>) -> &mut Self { self.local_decls = body.local_decls.clone(); self.body = Cow::Owned(body); + self.partial_moves = drop_point::partial_moved_places(self.tcx, &self.body); self } diff --git a/src/analyze/basic_block/drop_point.rs b/src/analyze/basic_block/drop_point.rs index 919acb3b..616998cc 100644 --- a/src/analyze/basic_block/drop_point.rs +++ b/src/analyze/basic_block/drop_point.rs @@ -101,6 +101,47 @@ fn moved_locals<'tcx>( visitor.locals } +/// For each local, the places (with a non-empty projection) that are moved out +/// of it somewhere in `body` — i.e. partial field moves. +/// +/// A wholesale drop of the parent would otherwise walk into such a moved-out +/// sub-place and resolve the `&mut` prophecy it owns a second time (see +/// `Env::dropping_assumption`). Whole-local moves are already excluded from the +/// drop set by `moved_locals`; this captures the partial-move case it misses. +/// +/// Moves of reference-typed places are skipped for the same reason as in +/// `moved_locals`: `ReborrowVisitor`/`RustCallVisitor` turn them into reborrows, +/// so the source still owns its prophecy and must be dropped normally. +pub fn partial_moved_places<'tcx>( + tcx: rustc_middle::ty::TyCtxt<'tcx>, + body: &Body<'tcx>, +) -> HashMap>> { + struct Visitor<'a, 'tcx> { + tcx: rustc_middle::ty::TyCtxt<'tcx>, + body: &'a Body<'tcx>, + moves: HashMap>>, + } + 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() + && !place.ty(&self.body.local_decls, self.tcx).ty.is_ref() + { + self.moves.entry(place.local).or_default().push(*place); + } + } + } + } + let mut visitor = Visitor { + tcx, + body, + moves: HashMap::new(), + }; + use mir::visit::Visitor as _; + visitor.visit_body(body); + visitor.moves +} + fn def_local<'tcx>(data: &mir::BasicBlockData<'tcx>, statement_index: usize) -> Option { struct Visitor { local: Option, diff --git a/src/refine/env.rs b/src/refine/env.rs index d9c3dfbc..8fceb659 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1083,6 +1083,22 @@ impl Path { fn tuple_proj(self, idx: usize) -> Self { Path::TupleProj(Box::new(self), idx) } + + /// Structural equality over the place-rooted variants. `PlaceTy` carries an + /// opaque type rather than a place identity, so it never matches; this is + /// only used to compare a drop-walk path against moved-out places, which are + /// always rooted at a `Local`. + fn same_place(&self, other: &Path) -> bool { + match (self, other) { + (Path::Local(a), Path::Local(b)) => a == b, + (Path::Deref(a), Path::Deref(b)) => a.same_place(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 Env @@ -1106,7 +1122,15 @@ where self.path_type(&place.into()) } - fn dropping_assumption(&mut self, path: &Path) -> Assumption { + fn dropping_assumption(&mut self, path: &Path, moved: &[Path]) -> Assumption { + // A sub-place that was moved out of this local earlier has had its + // ownership (and the obligation to resolve any `&mut` prophecy it owns) + // transferred to the move destination. Dropping it here would resolve + // that prophecy a second time, contradicting the resolution performed at + // the destination, so skip the whole moved-out subtree. + if moved.iter().any(|m| m.same_place(path)) { + return Assumption::default(); + } let ty = self.path_type(path); if ty.ty.is_mut() { let mut builder = PlaceTypeBuilder::default(); @@ -1114,10 +1138,10 @@ where 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(), moved) } 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), moved)) .collect() } else if let Some(ety) = ty.ty.as_enum() { let enum_def = self.enum_defs.enum_def(&ety.symbol); @@ -1170,7 +1194,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)), moved); // dropping assumption should not generate any existential assert!(assumption_existentials.is_empty()); formula.push_conj(assumption_body); @@ -1186,7 +1210,14 @@ where } pub fn drop_local(&mut self, local: Local) { - let assumption = self.dropping_assumption(&Path::Local(local)); + self.drop_local_with_moved(local, &[]); + } + + /// Drop `local`, skipping any sub-places listed in `moved_places` whose + /// ownership was transferred away by an earlier partial move. + pub fn drop_local_with_moved(&mut self, local: Local, moved_places: &[Place<'_>]) { + let moved: Vec = moved_places.iter().map(|p| Path::from(*p)).collect(); + let assumption = self.dropping_assumption(&Path::Local(local), &moved); if !assumption.is_top() { self.assume(assumption); } diff --git a/tests/ui/fail/partial_move_drop.rs b/tests/ui/fail/partial_move_drop.rs new file mode 100644 index 00000000..6b24945f --- /dev/null +++ b/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 +} diff --git a/tests/ui/fail/partial_move_field_call.rs b/tests/ui/fail/partial_move_field_call.rs new file mode 100644 index 00000000..fedb5e0b --- /dev/null +++ b/tests/ui/fail/partial_move_field_call.rs @@ -0,0 +1,22 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off + +// Regression test for #122: a `&mut`-bearing field moved out of an aggregate +// into a call must not be re-dropped when the parent is dropped wholesale. +// `w.0` (an owned `(&mut i32,)`) is moved into `bump`; dropping `w` afterwards +// used to resolve the moved-out `&mut` prophecy a second time, so this false +// assertion was wrongly accepted. +fn bump(p: (&mut i64,)) { + *p.0 += 1; +} + +fn apply(w: ((&mut i64,),)) { + bump(w.0); // moves owned field `(&mut i64,)` out of `w` into the call +} + +fn main() { + let mut x = 1_i64; + let w = ((&mut x,),); + apply(w); + assert!(x == 999); // false at runtime: x == 2 +} diff --git a/tests/ui/pass/partial_move_drop.rs b/tests/ui/pass/partial_move_drop.rs new file mode 100644 index 00000000..23c080fa --- /dev/null +++ b/tests/ui/pass/partial_move_drop.rs @@ -0,0 +1,13 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// Companion to the #121 regression test: the moved-out `&mut a` prophecy is +// still resolved exactly once (through `b`), so the true post-condition holds. +// This guards against over-suppressing the drop. +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 == 2); +} diff --git a/tests/ui/pass/partial_move_field_call.rs b/tests/ui/pass/partial_move_field_call.rs new file mode 100644 index 00000000..0ba87b09 --- /dev/null +++ b/tests/ui/pass/partial_move_field_call.rs @@ -0,0 +1,19 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off + +// Companion to the #122 regression test: the moved-out `&mut` prophecy is +// resolved exactly once (inside `bump`), so the true post-condition holds. +fn bump(p: (&mut i64,)) { + *p.0 += 1; +} + +fn apply(w: ((&mut i64,),)) { + bump(w.0); // moves owned field `(&mut i64,)` out of `w` into the call +} + +fn main() { + let mut x = 1_i64; + let w = ((&mut x,),); + apply(w); + assert!(x == 2); +}