You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
fix(borrow): CORE-01 pt2 — return-escape of borrow rooted at callee-owned (Refs #177) (#254)
CORE-01 pt1 (#240) only inspected *block tails* for escape, so a
`return r` where `r = &local` / `r = &by-value-param` slipped through:
`fn esc(x: Int) -> ref Int { let r = &x; return r; }` type-checked OK
while the returned `ref` dangles once the callee frame is gone — a
reachable unsoundness (verified: oracle accepted it pre-fix).
Fix (bounded, mirrors pt1's BorrowOutlivesOwner rationale):
- state.callee_owned_params: sym-ids of params with effective ownership
None (by-value) or Some Own. ref/mut params are caller-owned referents
and stay out (returning a borrow of them is sound).
- returned_borrow: the borrow a returned expr denotes — a direct
&place/&mut place, or a ref binder `r` resolved in the live
state.ref_bindings graph (None for a returned *value*, incl. *r).
- check_return_escape: if that borrow's root is a callee-owned param OR a
function local (block_local_syms) -> BorrowOutlivesOwner. Wired at
ExprReturn(Some e) (graph live during traversal — catches `return r`),
FnExpr tail, and FnBlock direct-`¶m` implicit tail (pt1 covers the
block-local implicit tail).
Verified (oracle): `return &x`/`return r`(r=&x) for by-value param AND
local now ERROR; `fn ok(x: ref Int) -> ref Int { return x; }` still
passes (no over-rejection of the caller-owned case); `*r`/value returns
and local-only borrows still pass; #240 block-escape + move-twice
regressions intact. Full gate 271 -> 274 (+3 hermetic "E2E Borrow Graph"
return-escape tests + 3 fixtures); ALL 20 stdlib AOT green — zero corpus
over-rejection.
Honest scope (bidirectional-evidence finding): CORE-01 pt2's residual
items — NLL/region inference (Polonius), flow-sensitive escape via
`outer = &x`, tighter quantity integration — are *parser-gated*, not
reachable unsoundnesses today: the surface to express them does not parse
(`&mut e`, `-> &T`, `&`-in-literal, bare block-statements). The next move
there is the parser surface, then the analysis. Ledger + in-code comment
truthed. Refs #177 (not Closes — pt2 residual remains, parser-gated).
Co-authored-by: hyperpolymath <hyperpolymath@users.noreply.github.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
0 commit comments