Don't drop partially-moved sub-places (fix #121, #122)

src/analyze/basic_block.rs

@@ -145,6 +145,10 @@ pub struct Analyzer<'tcx, 'ctx> {
     local_decls: IndexVec<Local, mir::LocalDecl<'tcx>>,
     // TODO: remove this
     prophecy_vars: HashMap<usize, TempVarIdx>,
+    /// 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<Local, Vec<mir::Place<'tcx>>>,
 }
 
 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
     }
 

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<Local, Vec<mir::Place<'tcx>>> {
+    struct Visitor<'a, 'tcx> {
+        tcx: rustc_middle::ty::TyCtxt<'tcx>,
+        body: &'a Body<'tcx>,
+        moves: HashMap<Local, Vec<mir::Place<'tcx>>>,
+    }
+    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<Local> {
     struct Visitor {
         local: Option<Local>,

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<T> Env<T>
@@ -1106,18 +1122,26 @@ 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();
             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(), 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<Path> = 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);
         }

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
+}

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
+}

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);
+}

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);
+}