Skip to content

Commit 2b8aa0b

Browse files
fix(borrow): self-assign guard + return-escape coverage for ref-to-ref (Refs #177, follow-up to #395) (#400)
## Summary Two deltas on top of #395's ref-to-ref binding work, surfaced by the audit posted on #395 at the time it merged. **This PR was the original parallel implementation; it has been rewritten as a thin follow-up now that #395 covered the broader scope.** ### 1. Self-assign `r = r` guard Without this guard, `is_reborrow_source` reports true for the ref-binder LHS=RHS case → `pre_release` ends `r`'s borrow and removes the binding → post-rebind calls `ref_source_borrow` which now finds `r` unbound and returns None → net effect is `r` silently stripped from the borrow-graph. Pathological in practice (`r = r` is dead code) but a silent unsoundness rather than a no-op. The guard short-circuits `pre_release` when the RHS's source binder is the LHS binder itself. ### 2. Return-escape via indirection (new test) The strongest proof that `record_ref_binding`'s delegation to `ref_source_borrow` works is `return r2` where `r2 = r1 = &local` — pre-fix this slipped past `returned_borrow`'s `ref_bindings` lookup. The three fixtures landed in #395 (`let_aliases`, `protects_owner`, `assign_aliases`) don't exercise the return-escape code path, which is historically the most-leaked surface for this class of bug. New fixture `test/e2e/fixtures/ref_to_ref_return_escape.affine` pins it — expects `BorrowOutlivesOwner`. ## Tests - 331 prior tests + 1 new = **332/332 green** - No changes to `lib/borrow.ml` behaviour for any code path other than the self-assign edge case. ## Coordination - Rebased onto current main (post-#395 + post-#399). Force-pushed. - GPG-signed. - This was originally the parallel implementation of #395. After #395 merged via admin-merge during the deferred-items roundup, this PR was rewritten to contain only the two deltas the audit flagged. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent e73067d commit 2b8aa0b

3 files changed

Lines changed: 59 additions & 1 deletion

File tree

lib/borrow.ml

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1392,10 +1392,29 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
13921392
assignment path so the NLL last-use + return-escape
13931393
analyses see the *current* referent after re-assignment,
13941394
not the stale original. *)
1395+
(* Self-assign `r = r` guard (#177 follow-up to #395): without
1396+
this, [is_reborrow_source] reports true for the ref-binder
1397+
LHS=RHS case, pre_release ends `r`'s borrow and removes the
1398+
binding, then post-rebind calls [ref_source_borrow] which
1399+
now finds `r` unbound and returns None — net effect is `r`
1400+
silently stripped from the borrow-graph. *)
1401+
let rhs_is_self_binder =
1402+
match root_var place with
1403+
| Some binder_sym ->
1404+
let rec peel = function ExprSpan (x, _) -> peel x | x -> x in
1405+
(match peel rhs with
1406+
| ExprVar id ->
1407+
(match lookup_symbol_by_name symbols id.name with
1408+
| Some sym -> sym.Symbol.sym_id = binder_sym
1409+
| None -> false)
1410+
| _ -> false)
1411+
| None -> false
1412+
in
13951413
let pre_release =
13961414
match root_var place with
13971415
| Some binder_sym
1398-
when is_reborrow_source state symbols rhs
1416+
when not rhs_is_self_binder
1417+
&& is_reborrow_source state symbols rhs
13991418
&& List.mem_assoc binder_sym state.ref_bindings ->
14001419
let old_borrow = List.assoc binder_sym state.ref_bindings in
14011420
end_borrow state old_borrow;
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt3 ref-to-ref / #177 (follow-up to #395): the strongest
5+
// proof that the let-graph propagation works is `return r2` where
6+
// `r2 = r1 = &local` — pre-fix this slipped past `returned_borrow`'s
7+
// `ref_bindings` lookup. With the let-graph alias landed by #395
8+
// (`record_ref_binding` delegating to `ref_source_borrow`), `r2`
9+
// inherits `r1`'s borrow on the function-local `x` and the
10+
// return-escape check sees `root_var = x` is block-local.
11+
// Expected: BorrowOutlivesOwner.
12+
13+
module RefToRefReturnEscape;
14+
15+
fn esc_via_indir() -> ref Int {
16+
let x = 5;
17+
let r1 = &x;
18+
let r2 = r1;
19+
return r2;
20+
}

test/test_e2e.ml

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4454,6 +4454,23 @@ let test_ref_to_ref_assign_aliases () =
44544454
the subsequent write to `x` was spuriously \
44554455
rejected: " ^ Borrow.format_borrow_error e)
44564456

4457+
(* CORE-01 pt3 ref-to-ref / #177 follow-up: return-escape via
4458+
indirection. Pre-fix `let r2 = r1` did not propagate `r1`'s
4459+
ref-binding, so `returned_borrow` for `return r2` silently
4460+
returned None — the escape was missed. Post-fix `r2` inherits
4461+
`r1`'s borrow on a function-local, and the escape check fires. *)
4462+
let test_ref_to_ref_return_escape () =
4463+
match borrow_result (fixture "ref_to_ref_return_escape.affine") with
4464+
| Error (Borrow.BorrowOutlivesOwner _) -> ()
4465+
| Error e ->
4466+
Alcotest.fail ("ref-to-ref return-escape: expected \
4467+
BorrowOutlivesOwner on `return r2` where r2 = r1 = \
4468+
&local, got: " ^ Borrow.format_borrow_error e)
4469+
| Ok () ->
4470+
Alcotest.fail "ref-to-ref return-escape regressed: the indirection \
4471+
chain was not detected by `returned_borrow`'s \
4472+
ref_bindings lookup — escape silently accepted"
4473+
44574474
(* CORE-01 pt3 / #177 deferred-items: assignment-clears-move.
44584475
Whole-place write `x = …` after a prior move on `x` revives the
44594476
place; the move-record is dropped after the RHS lands so the
@@ -4510,6 +4527,8 @@ let borrow_tests = [
45104527
`Quick test_ref_to_ref_protects_owner;
45114528
Alcotest.test_case "ref-to-ref assign-path: `r = s` releases + aliases (#177 pt3)"
45124529
`Quick test_ref_to_ref_assign_aliases;
4530+
Alcotest.test_case "ref-to-ref return-escape via indirection (#177 pt3 follow-up)"
4531+
`Quick test_ref_to_ref_return_escape;
45134532
Alcotest.test_case "assignment-clears-move: whole-place write revives moved place (#177)"
45144533
`Quick test_borrow_assign_clears_move;
45154534
]

0 commit comments

Comments
 (0)