From 6c0b3bb32961803788e3b299a14d7ab59c0426ec Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 13 Aug 2026 17:19:47 +0000 Subject: [PATCH] Bind the structure of the value a mutable borrow prophesies A mutable borrow rebinds the borrowed variable to the borrow's prophecy variable, which stands for the value the place takes once the borrow ends. That variable is opaque: it is bound as a value, not with the `FlowBinding` that `locate_place` and `borrow_var` walk to reach through a reference, a box, a tuple, or an enum. A place whose value has structure therefore lost that structure as soon as it was borrowed. Writing to a `mut` local is elaborated into a borrow of the local's slot, so a straight-line reassignment of a `&mut` local followed by a write through it hit exactly that: the reassignment left the local's content standing for the prophecy, and elaborating the write into a reborrow of `*r` panicked with `borrowing unbound var`. The same reassignment of a tuple local panicked with `deref unbound var` when projecting a field afterwards. Reading through the reassigned local was fine, since reads go through `place_type`, which needs no flow binding. Bind a fresh variable equal to the prophecy through `bind_impl` instead, so that the prophesied value carries the structure of the value it replaces. A value bound without a flow binding keeps standing for the prophecy variable directly, leaving the constraints generated for a borrow of a scalar unchanged. Fixes #176 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_017gbkD8SESxdRSj7taHpFJs --- src/refine/env.rs | 26 ++++++++++++++++++++++++-- tests/ui/fail/reassign_mut_ref.rs | 12 ++++++++++++ tests/ui/pass/reassign_mut_ref.rs | 12 ++++++++++++ 3 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 tests/ui/fail/reassign_mut_ref.rs create mode 100644 tests/ui/pass/reassign_mut_ref.rs diff --git a/src/refine/env.rs b/src/refine/env.rs index f54ca15c..9bb2b6be 100644 --- a/src/refine/env.rs +++ b/src/refine/env.rs @@ -1001,16 +1001,38 @@ where self.var_type(local.into()) } + /// Returns the variable holding the value of `current` after a mutable borrow of it ends, + /// which the borrow's `prophecy` variable stands for. + /// + /// When `current` has a flow binding, the prophesied value is given one as well, so that it + /// can be projected and borrowed through just like the value it replaces. `prophecy` itself + /// is an opaque variable and admits neither, which would leave a reference stored in the + /// prophesied value unusable as the target of a later write. + fn bind_prophesied_value(&mut self, current: TempVarIdx, prophecy: TempVarIdx) -> TempVarIdx { + if self.flow_binding(current.into()).is_none() { + return prophecy; + } + let ty = self.var_type(current.into()).ty; + let refinement = chc::Term::var(rty::RefinedTypeVar::Value) + .equal_to(chc::Term::var(rty::RefinedTypeVar::Free(prophecy.into()))) + .into(); + let var = self.temp_vars.next_index(); + self.bind_impl(var.into(), rty::RefinedType::new(ty, refinement), 0); + var + } + fn borrow_var(&mut self, var: Var, prophecy: TempVarIdx) -> PlaceType { match *self.flow_binding(var).expect("borrowing unbound var") { FlowBinding::Box(x) => { let inner_ty = self.var_type(x.into()); - self.insert_flow_binding(var, FlowBinding::Box(prophecy)); + let current = self.bind_prophesied_value(x, prophecy); + self.insert_flow_binding(var, FlowBinding::Box(current)); inner_ty.mut_with_proph_term(chc::Term::var(prophecy.into())) } FlowBinding::Mut(x1, x2) => { let inner_ty = self.var_type(x1.into()); - self.insert_flow_binding(var, FlowBinding::Mut(prophecy, x2)); + let current = self.bind_prophesied_value(x1, prophecy); + self.insert_flow_binding(var, FlowBinding::Mut(current, x2)); inner_ty.mut_with_proph_term(chc::Term::var(prophecy.into())) } _ => panic!("invalid borrow"), diff --git a/tests/ui/fail/reassign_mut_ref.rs b/tests/ui/fail/reassign_mut_ref.rs new file mode 100644 index 00000000..50637ce3 --- /dev/null +++ b/tests/ui/fail/reassign_mut_ref.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat + +fn main() { + let mut a = 1_i64; + let mut b = 2_i64; + let mut r = &mut a; + *r = 10; + r = &mut b; + *r = 20; + assert!(a == 10); + assert!(b == 21); +} diff --git a/tests/ui/pass/reassign_mut_ref.rs b/tests/ui/pass/reassign_mut_ref.rs new file mode 100644 index 00000000..b7a0671e --- /dev/null +++ b/tests/ui/pass/reassign_mut_ref.rs @@ -0,0 +1,12 @@ +//@check-pass + +fn main() { + let mut a = 1_i64; + let mut b = 2_i64; + let mut r = &mut a; + *r = 10; + r = &mut b; + *r = 20; + assert!(a == 10); + assert!(b == 20); +}