Skip to content

Commit 20e72b8

Browse files
hyperpolymathclaude
andcommitted
fix(borrow): propagate ref-binding through reborrow indirection (Refs #177)
Pre-fix, `let r2 = r1` and `r2 = r1` (where `r1` is itself a ref-binder rather than a fresh `&p`) silently skipped recording `r2`'s ref-graph entry — both `record_ref_binding` and `StmtAssign` resolved the RHS via `ref_target`, which only matches direct `&place`/`&mut place`. Without the binding, the indirection chain `r2 = r1 = &local` slipped past `returned_borrow`'s lookup in `state.ref_bindings`, so `return r2` escaped without erroring. This is the "Reborrow through indirection" item in the deferred-items comment at lib/borrow.ml:1483. Fix is three coupled pieces: 1. `record_ref_binding` delegates to `returned_borrow` (which already handled both `&p` and binder lookup for the return-escape path); `returned_borrow` is moved above `record_ref_binding` to make the dependency satisfiable in OCaml's top-down order. 2. `StmtAssign` pre_release + post-rebind use `returned_borrow` for the same reason. A self-assignment guard (`r = r`) prevents the no-op case from unbinding `r` and leaving it unprotected. 3. `expire_dead_ref_bindings` gates `end_borrow` on a multi-binder liveness check: a borrow whose `b_id` is still referenced by any live entry in `still_live` MUST NOT be ended when the first binder dies. Without this gate, sharing the borrow object across binders creates a soundness hole — the borrow is ended at the first binder's last use, leaving the second binder unprotected and the underlying place silently writable. Four new e2e tests pin the fix: - `borrow_reborrow_indir_ok.affine` — `let r2 = r1; *r1; *r2` (Ok). - `borrow_reborrow_indir_escape.affine` — `return r2` where `r2 = r1 = &local` now correctly errors `BorrowOutlivesOwner`. - `borrow_reborrow_indir_nll_alias.affine` — `r1` dies, `r2` alive; `x = 5` must error `MoveWhileBorrowed` (multi-binder gate). - `borrow_reborrow_indir_assign.affine` — `r2 = r1` rebinds and releases `r2`'s old loan; the later `y = 10` succeeds. 327 prior tests + 4 new = 331/331 green. Slice A/B/C anti-regressions preserved. Comment at lib/borrow.ml:1483 left in place — the indirection item description still applies as historical context for the merged fix. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 1a57163 commit 20e72b8

6 files changed

Lines changed: 214 additions & 48 deletions

lib/borrow.ml

Lines changed: 70 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -494,34 +494,13 @@ and expr_to_place (symbols : Symbol.t) (expr : expr) : place option =
494494
expr_to_place symbols e
495495
| _ -> None
496496

497-
(** Record a borrow-graph edge for [let <pat> = &p] (or [&mut p]).
498-
499-
Call *after* the value expression has been checked, so the borrow it
500-
created is already on [state.borrows]. Binds the let-bound symbol to
501-
that borrow so block-exit validation can detect a reference outliving
502-
a block-local owner. CORE-01 / #177. *)
503-
let record_ref_binding (state : state) (symbols : Symbol.t)
504-
(pat : pattern) (value : expr) : unit =
505-
match pat with
506-
| PatVar id ->
507-
begin match ref_target symbols value with
508-
| Some target ->
509-
begin match
510-
List.find_opt (fun b -> places_overlap b.b_place target) state.borrows,
511-
lookup_symbol_by_name symbols id.name
512-
with
513-
| Some b, Some sym ->
514-
state.ref_bindings <- (sym.Symbol.sym_id, b) :: state.ref_bindings
515-
| _ -> ()
516-
end
517-
| None -> ()
518-
end
519-
| _ -> ()
520-
521-
(** The borrow a *returned* expression denotes, if any: either a direct
522-
[&place] / [&mut place], or a reference binder [r] (from [let r = &p])
523-
looked up in the live borrow-graph. Returning a *value* (incl. [*r]) is
524-
not a borrow and yields [None]. CORE-01 pt2 / #177 (return-escape). *)
497+
(** The borrow a reference-bearing expression denotes, if any: either a
498+
direct [&place] / [&mut place], or a reference binder [r] (from
499+
[let r = &p]) looked up in the live ref-graph. Returning a *value*
500+
(incl. [*r]) is not a borrow and yields [None]. Originally added
501+
for return-escape (CORE-01 pt2 / #177); also the resolver used by
502+
[record_ref_binding] and [StmtAssign] to handle reborrow through
503+
indirection (CORE-01 pt3 / #177 deferred-items). *)
525504
let returned_borrow (state : state) (symbols : Symbol.t)
526505
(e : expr) : borrow option =
527506
let rec peel = function ExprSpan (x, _) -> peel x | x -> x in
@@ -541,6 +520,29 @@ let returned_borrow (state : state) (symbols : Symbol.t)
541520
| None -> None)
542521
| _ -> None)
543522

523+
(** Record a borrow-graph edge for [let <pat> = rhs] where [rhs] is a
524+
reference-bearing expression — either a direct [&p] / [&mut p] or
525+
another ref-binder. Indirection (e.g. [let r2 = r1]) propagates
526+
[r1]'s bound borrow to [r2], so escape + NLL analyses see [r2]
527+
through the same target. CORE-01 / #177 deferred-items.
528+
529+
Call *after* the value expression has been checked, so the borrow
530+
it created (for the direct case) is already on [state.borrows]. *)
531+
let record_ref_binding (state : state) (symbols : Symbol.t)
532+
(pat : pattern) (value : expr) : unit =
533+
match pat with
534+
| PatVar id ->
535+
begin match returned_borrow state symbols value with
536+
| Some b ->
537+
begin match lookup_symbol_by_name symbols id.name with
538+
| Some sym ->
539+
state.ref_bindings <- (sym.Symbol.sym_id, b) :: state.ref_bindings
540+
| None -> ()
541+
end
542+
| None -> ()
543+
end
544+
| _ -> ()
545+
544546
(** Return-escape (CORE-01 pt2 / #177): a [return e] (or fn-tail) whose
545547
value is a reference rooted at a *callee-owned* binding — a function
546548
local or a by-value/[own] parameter — dangles once the callee frame is
@@ -1212,7 +1214,14 @@ and check_block (ctx : context) (state : state) (symbols : Symbol.t) (blk : bloc
12121214
(not (is_outer_binding sym)) && last_use_of sym <= stmt_idx
12131215
) state.ref_bindings
12141216
in
1215-
List.iter (fun (_sym, b) -> end_borrow state b) dying;
1217+
(* A borrow shared by multiple binders (via reborrow-through-
1218+
indirection, #177 deferred-items) must outlive every binder
1219+
that aliases it. Only end the borrow if no live binder still
1220+
references the same [b_id]. *)
1221+
List.iter (fun (_sym, b) ->
1222+
if not (List.exists (fun (_s, b') -> b'.b_id = b.b_id) still_live) then
1223+
end_borrow state b
1224+
) dying;
12161225
state.ref_bindings <- still_live
12171226
in
12181227
let* () =
@@ -1317,37 +1326,50 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
13171326
| None ->
13181327
(* Slice B (CORE-01 pt3 / #177): flow-sensitive escape via
13191328
`outer = &y`. If LHS is a ref-binder symbol that already
1320-
holds a borrow and RHS is a fresh `&y`/`&mut y` reference,
1321-
the assignment *replaces* the held borrow. We pre-release
1329+
holds a borrow and RHS resolves to a borrow (a direct
1330+
`&y`/`&mut y` OR another ref-binder via [returned_borrow]
1331+
— the indirection path of #177 deferred-items), the
1332+
assignment *replaces* the held borrow. We pre-release
13221333
the old held borrow before checking the RHS so the same-
13231334
target reborrow case (`r = &mut x` while `r` already holds
13241335
`&mut x`) does not trip [ConflictingBorrow] on the
13251336
about-to-be-replaced exclusive borrow; we then re-bind the
1326-
ref-graph entry to the freshly-created borrow. Mirrors
1337+
ref-graph entry to the borrow the RHS denotes. Mirrors
13271338
[record_ref_binding]'s let-graph contract for the
13281339
assignment path so the NLL last-use + return-escape
13291340
analyses see the *current* referent after re-assignment,
1330-
not the stale original. *)
1341+
not the stale original. A self-assignment `r = r` is
1342+
treated as a no-op: it preserves [r]'s existing binding
1343+
rather than unbinding-then-failing-to-rebind. *)
13311344
let pre_release =
1332-
match root_var place, ref_target symbols rhs with
1333-
| Some binder_sym, Some _
1345+
match root_var place with
1346+
| Some binder_sym
13341347
when List.mem_assoc binder_sym state.ref_bindings ->
1335-
let old_borrow = List.assoc binder_sym state.ref_bindings in
1336-
end_borrow state old_borrow;
1337-
state.ref_bindings <-
1338-
List.filter (fun (s, _) -> s <> binder_sym) state.ref_bindings;
1339-
Some binder_sym
1348+
let rhs_is_self =
1349+
let rec peel = function ExprSpan (x, _) -> peel x | x -> x in
1350+
match peel rhs with
1351+
| ExprVar id ->
1352+
(match lookup_symbol_by_name symbols id.name with
1353+
| Some sym -> sym.Symbol.sym_id = binder_sym
1354+
| None -> false)
1355+
| _ -> false
1356+
in
1357+
if rhs_is_self then None
1358+
else (match returned_borrow state symbols rhs with
1359+
| Some _ ->
1360+
let old_borrow = List.assoc binder_sym state.ref_bindings in
1361+
end_borrow state old_borrow;
1362+
state.ref_bindings <-
1363+
List.filter (fun (s, _) -> s <> binder_sym) state.ref_bindings;
1364+
Some binder_sym
1365+
| None -> None)
13401366
| _ -> None
13411367
in
13421368
let* () = check_expr ctx state symbols rhs in
1343-
(match pre_release, ref_target symbols rhs with
1344-
| Some binder_sym, Some new_target ->
1345-
(match List.find_opt (fun b ->
1346-
places_overlap b.b_place new_target) state.borrows with
1347-
| Some new_b ->
1348-
state.ref_bindings <-
1349-
(binder_sym, new_b) :: state.ref_bindings
1350-
| None -> ())
1369+
(match pre_release, returned_borrow state symbols rhs with
1370+
| Some binder_sym, Some new_b ->
1371+
state.ref_bindings <-
1372+
(binder_sym, new_b) :: state.ref_bindings
13511373
| _ -> ());
13521374
Ok ()
13531375
end
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt3 / #177 deferred-items: reborrow through indirection,
5+
// assignment leg. Pre-fix, `r2 = r1` (RHS is a ref-binder, not a
6+
// direct `&y`) did not release `r2`'s prior borrow on `y` nor rebind
7+
// `r2` to `r1`'s borrow — so the later `y = 10` would be rejected
8+
// MoveWhileBorrowed because `r2`'s stale borrow on `y` was still
9+
// live. Post-fix, `returned_borrow` resolves `r1` to its bound
10+
// borrow, the pre-release path releases `r2`'s old borrow on `y`,
11+
// and `r2` is rebound to share `r1`'s borrow on `x`. `y = 10` then
12+
// succeeds because nothing borrows `y` anymore. Expected: Ok.
13+
14+
module BorrowReborrowIndirAssign;
15+
16+
fn read_int(x: Int) -> Int = 0;
17+
18+
fn assign_indir_ok() -> Int {
19+
let mut x = 1;
20+
let mut y = 2;
21+
let r1 = &x;
22+
let mut r2 = &y;
23+
r2 = r1;
24+
y = 10;
25+
read_int(*r2) + y
26+
}
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt3 / #177 deferred-items: reborrow through indirection,
5+
// return-escape leg. Pre-fix, `let r2 = r1` did not propagate `r1`'s
6+
// ref-binding, so `returned_borrow` for `return r2` resolved through
7+
// `state.ref_bindings` and silently returned `None` — the escape was
8+
// missed. Post-fix, `r2` inherits `r1`'s borrow on the function-local
9+
// `x`, and the return-escape check sees `root_var = x` is
10+
// block-local and errors. Expected: BorrowOutlivesOwner.
11+
12+
module BorrowReborrowIndirEscape;
13+
14+
fn esc_via_indir() -> ref Int {
15+
let x = 5;
16+
let r1 = &x;
17+
let r2 = r1;
18+
return r2;
19+
}
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt3 / #177 deferred-items: NLL safety for shared borrows.
5+
// When `let r2 = r1` propagates `r1`'s binding to `r2`, the
6+
// underlying borrow on `x` is now aliased by two binders. When `r1`
7+
// dies (last use at `let z = *r1`), `expire_dead_ref_bindings` must
8+
// NOT end the borrow — `r2` is still alive and references the same
9+
// `b_id`. Hence `x = 5` (after `r1`'s death) must still be rejected
10+
// `MoveWhileBorrowed`, protecting the subsequent `*r2` read.
11+
// Expected: Error MoveWhileBorrowed.
12+
13+
module BorrowReborrowIndirNllAlias;
14+
15+
fn nll_aliased() -> Int {
16+
let mut x = 1;
17+
let r1 = &x;
18+
let r2 = r1;
19+
let z = *r1;
20+
x = 5;
21+
*r2 + z
22+
}
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt3 / #177 deferred-items: reborrow through indirection.
5+
// `let r2 = r1` where `r1` is itself a ref-binder must propagate
6+
// `r1`'s bound borrow to `r2` (rather than leaving `r2` unbound).
7+
// Both binders share the same borrow on `x`; dereferencing either
8+
// is sound. Expected: Ok.
9+
10+
module BorrowReborrowIndirOk;
11+
12+
fn read_int(x: Int) -> Int = 0;
13+
14+
fn indir_ok() -> Int {
15+
let x = 1;
16+
let r1 = &x;
17+
let r2 = r1;
18+
read_int(*r1) + read_int(*r2)
19+
}

test/test_e2e.ml

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4415,6 +4415,56 @@ let test_slice_c_body_move_persists () =
44154415
the catch-arm merge — `read_int(y)` after a moved `y` \
44164416
was silently accepted"
44174417

4418+
(* CORE-01 pt3 / #177 deferred-items: reborrow through indirection.
4419+
`let r2 = r1` (RHS is another ref-binder) must propagate `r1`'s
4420+
bound borrow to `r2`; symmetrically for the assignment path
4421+
`r2 = r1`. Aliased borrows must outlive every binder referencing
4422+
them — the multi-binder gate in [expire_dead_ref_bindings].
4423+
Four tests: positive let, negative return-escape, NLL anti-
4424+
regression for the alias-keeps-alive case, and positive assign. *)
4425+
let test_borrow_reborrow_indir_ok () =
4426+
match borrow_result (fixture "borrow_reborrow_indir_ok.affine") with
4427+
| Ok () -> ()
4428+
| Error e ->
4429+
Alcotest.fail ("reborrow-indir (let): `let r2 = r1; *r1; *r2` \
4430+
spuriously rejected — propagation failed or \
4431+
multi-binder gate over-expired: "
4432+
^ Borrow.format_borrow_error e)
4433+
4434+
let test_borrow_reborrow_indir_escape () =
4435+
match borrow_result (fixture "borrow_reborrow_indir_escape.affine") with
4436+
| Error (Borrow.BorrowOutlivesOwner _) -> ()
4437+
| Error e ->
4438+
Alcotest.fail ("reborrow-indir return-escape: expected \
4439+
BorrowOutlivesOwner on `return r2` where r2 = r1 = \
4440+
&local, got: " ^ Borrow.format_borrow_error e)
4441+
| Ok () ->
4442+
Alcotest.fail "reborrow-indir regressed: return-escape was silently \
4443+
accepted — `let r2 = r1` did not propagate the binding \
4444+
so `returned_borrow` missed the escape"
4445+
4446+
let test_borrow_reborrow_indir_nll_alias () =
4447+
match borrow_result (fixture "borrow_reborrow_indir_nll_alias.affine") with
4448+
| Error (Borrow.MoveWhileBorrowed _) -> ()
4449+
| Error e ->
4450+
Alcotest.fail ("reborrow-indir NLL aliasing: expected \
4451+
MoveWhileBorrowed on `x = 5` after r1 dies (r2 still \
4452+
aliases the same borrow), got: "
4453+
^ Borrow.format_borrow_error e)
4454+
| Ok () ->
4455+
Alcotest.fail "reborrow-indir multi-binder gate failed: a shared \
4456+
borrow was ended when its first binder died, leaving \
4457+
the second binder unprotected — `x = 5` slipped through"
4458+
4459+
let test_borrow_reborrow_indir_assign () =
4460+
match borrow_result (fixture "borrow_reborrow_indir_assign.affine") with
4461+
| Ok () -> ()
4462+
| Error e ->
4463+
Alcotest.fail ("reborrow-indir (assign): `r2 = r1` did not release \
4464+
r2's old borrow on y / did not rebind r2 to r1's \
4465+
borrow — `y = 10` spuriously rejected: "
4466+
^ Borrow.format_borrow_error e)
4467+
44184468
let borrow_tests = [
44194469
Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
44204470
`Quick test_borrow_outlives_owner;
@@ -4450,6 +4500,14 @@ let borrow_tests = [
44504500
`Quick test_slice_c_catch_arm_isolation;
44514501
Alcotest.test_case "Slice C anti-regression: body's move persists past try (#177 pt3 Slice C)"
44524502
`Quick test_slice_c_body_move_persists;
4503+
Alcotest.test_case "reborrow-indir: `let r2 = r1; *r1; *r2` is Ok (#177)"
4504+
`Quick test_borrow_reborrow_indir_ok;
4505+
Alcotest.test_case "reborrow-indir: return-escape via r2 = r1 = &local (#177)"
4506+
`Quick test_borrow_reborrow_indir_escape;
4507+
Alcotest.test_case "reborrow-indir NLL alias: shared borrow outlives first binder (#177)"
4508+
`Quick test_borrow_reborrow_indir_nll_alias;
4509+
Alcotest.test_case "reborrow-indir: `r2 = r1` rebinds + releases r2's old borrow (#177)"
4510+
`Quick test_borrow_reborrow_indir_assign;
44534511
]
44544512

44554513
(* ============================================================================

0 commit comments

Comments
 (0)