@@ -1233,8 +1233,41 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
12331233 (* Can't assign while borrowed *)
12341234 Error (MoveWhileBorrowed (place, borrow))
12351235 | None ->
1236- (* Assignment is ok, check the RHS *)
1237- check_expr ctx state symbols rhs
1236+ (* Slice B (CORE-01 pt3 / #177): flow-sensitive escape via
1237+ `outer = &y`. If LHS is a ref-binder symbol that already
1238+ holds a borrow and RHS is a fresh `&y`/`&mut y` reference,
1239+ the assignment *replaces* the held borrow. We pre-release
1240+ the old held borrow before checking the RHS so the same-
1241+ target reborrow case (`r = &mut x` while `r` already holds
1242+ `&mut x`) does not trip [ConflictingBorrow] on the
1243+ about-to-be-replaced exclusive borrow; we then re-bind the
1244+ ref-graph entry to the freshly-created borrow. Mirrors
1245+ [record_ref_binding]'s let-graph contract for the
1246+ assignment path so the NLL last-use + return-escape
1247+ analyses see the *current* referent after re-assignment,
1248+ not the stale original. *)
1249+ let pre_release =
1250+ match root_var place, ref_target symbols rhs with
1251+ | Some binder_sym, Some _
1252+ when List. mem_assoc binder_sym state.ref_bindings ->
1253+ let old_borrow = List. assoc binder_sym state.ref_bindings in
1254+ end_borrow state old_borrow;
1255+ state.ref_bindings < -
1256+ List. filter (fun (s , _ ) -> s <> binder_sym) state.ref_bindings;
1257+ Some binder_sym
1258+ | _ -> None
1259+ in
1260+ let * () = check_expr ctx state symbols rhs in
1261+ (match pre_release, ref_target symbols rhs with
1262+ | Some binder_sym , Some new_target ->
1263+ (match List. find_opt (fun b ->
1264+ places_overlap b.b_place new_target) state.borrows with
1265+ | Some new_b ->
1266+ state.ref_bindings < -
1267+ (binder_sym, new_b) :: state.ref_bindings
1268+ | None -> () )
1269+ | _ -> () );
1270+ Ok ()
12381271 end
12391272 | None ->
12401273 (* LHS is not a place (e.g., function call result), check both sides *)
@@ -1341,11 +1374,26 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
13411374 Outer-block ref-bindings are deliberately preserved — they expire
13421375 only at their own block's exit.
13431376
1344- Still deferred — region-/flow-sensitive remainder:
1345- - Flow-sensitive escape via assignment to an outer mutable
1346- (`outer = &x`): the assignment must update the borrow graph the
1347- way [let r = &x] already does.
1377+ CORE-01 pt3 Slice B (flow-sensitive escape via re-assignment):
1378+ `outer = &y` now updates the borrow graph the way `let outer = &y`
1379+ does. In StmtAssign, when LHS is a ref-binder symbol with a held
1380+ borrow and RHS is a direct `&p`/`&mut p`, the old borrow is
1381+ pre-released (so a same-target reborrow like `r = &mut x` while
1382+ `r` already holds `&mut x` does not trip ConflictingBorrow on the
1383+ about-to-be-replaced exclusive borrow), then after the RHS check
1384+ the (binder -> new_borrow) ref-graph entry is re-bound to the
1385+ freshly-created borrow. NLL last-use + return-escape now see the
1386+ *current* referent after re-assignment, not the stale original.
1387+
1388+ Still deferred:
1389+ - Reborrow through indirection: `r = some_other_ref_var` (RHS not a
1390+ direct `&place`) does not yet copy the other binder's graph
1391+ entry — the ref-binding stays stale. Same limitation as
1392+ [record_ref_binding] for the let-graph path; would require
1393+ symmetric let/assign handling for ref-to-ref binding.
13481394 - Origin/region variables (Polonius surface) + loan-live-at-point
1349- dataflow across CFG joins (Slice C).
1350- - Tighter integration with the quantity checker for captured linears.
1395+ dataflow across CFG joins for `ExprHandle`/`ExprTry`/loops
1396+ (Slice C).
1397+ - Tighter integration with the quantity checker for captured
1398+ linears (Slice D).
13511399*)
0 commit comments