From 8bb8633ca8a2790b5c4bf8d6575d8057def135e3 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 15:35:27 +0000 Subject: [PATCH 1/4] fix(bridge): hoist cross-branch locals to outer scope so post-merge release is clean A local acquired inside both if-branches (or via a fresh factory call) and released after the merge used to crash: the bridge emitted each synthetic Let inside its branch block, so the post-merge reference was out-of-scope and the core raised OWN030 -> OwnIRError. _hoisted_branch_locals now finds locals acquired at depth>=1 whose shallowest reference is at depth 0 (the function top, always reached), and to_module declares each once at the outer scope, skipping the in-branch acquire. A balanced cross-branch release is now CLEAN; an un-released one still leaks OWN001 (precision-safe: both the unconditional acquire and the depth-0 reference run on every path). Covers plain acquire and fresh call-result forms. We do NOT soft-skip OWN030 -- the strict map-or-raise invariant stays intact. A nested reference (released at depth>=1 in an enclosing block) is left as a narrower limitation -- function-top is not the common-dominator scope there, so hoisting would leak on the sibling path; locked by the nested_branch xfail test for a common-dominator follow-up. Tests: branch_merge (clean), branch_leak (OWN001), branch_factory (clean), nested_branch (still raises, locked). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 35 ++++---- ownlang/ownir.py | 125 +++++++++++++++++++++++++--- tests/test_ownir.py | 81 ++++++++++++++---- 3 files changed, 198 insertions(+), 43 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 24451c6f..80c6706e 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -291,20 +291,27 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa and the param-return precision guard. **Remaining T1 door:** `out`/`ref`-owned parameters (another `fresh` source) — extractor-side recognition of an out-assignment as a fresh acquire — rides into a later slice before async. -- **Bridge branch-scope limitation (pre-existing, tracked separately — NOT a D5 deliverable).** - The OwnIR→core bridge uses a *flat* `localmap`, but emits each synthetic `Let` *inside* the - branch block it occurs in. So a local `acquire`d in **both** branches of an `if` and released - **after** the merge (`if c: r=acquire() else: r=acquire(); release r`) lowers to a post-merge - `release` of an out-of-scope handle → the core reports **OWN030 (undefined name)**, which - `check_facts` strictly refuses to map and raises `OwnIRError`. This predates D5 and reproduces - with a **plain `acquire`** (no fresh/factory path) — D5.2's call-result acquire merely adds one - more way to reach it. The fix belongs in the bridge, in its own slice: make `acquire` lowering - **branch-aware** — hoist / declare the synthetic handle at the common merge scope so a balanced - cross-branch release is accepted as CLEAN. We deliberately do **not** soft-skip OWN030 (it - would mask genuine lowering drift; the strict map-or-raise invariant is load-bearing). Locked - by an xfail-style regression in `tests/test_ownir.py` (`branch_merge`) that asserts the current - raise and flips to a clean-balanced-release assertion once the bridge fix lands. (Codex P2 on - #116.) +- **Bridge branch-scope fix (shipped — separate from the D5 transfer ladder).** The OwnIR→core + bridge uses a *flat* `localmap` but emitted each synthetic `Let` *inside* the branch block it + occurred in, so a local `acquire`d in **both** branches of an `if` and released **after** the + merge (`if c: r=acquire() else: r=acquire(); release r`) lowered to a post-merge `release` of + an out-of-scope handle → the core reported **OWN030 (undefined name)** and `check_facts` raised + `OwnIRError`. It predated D5 (reproduced with a **plain `acquire`**, no fresh/factory path); + D5.2's call-result acquire only added another way to reach it. Fixed by making `acquire` + lowering **branch-aware**: `_hoisted_branch_locals` finds locals acquired at depth ≥ 1 whose + shallowest reference is at **depth 0** (the function top, always reached), and `to_module` + declares each **once at the function's outer scope** (a single `Let`), skipping the in-branch + acquire. A balanced cross-branch release is now CLEAN; an un-released one still leaks **OWN001** + (hoisting a conditional acquire to unconditional is precision-safe *because* the depth-0 + reference also runs on every path — never a fabricated use/double-release). Covers both the + plain `acquire` and the `fresh` call-result form. We deliberately did **not** soft-skip OWN030 + (it would mask genuine lowering drift; the strict map-or-raise invariant is load-bearing). + Tests: `branch_merge` (clean), `branch_leak` (OWN001), `branch_factory` (clean). **Narrower + remaining limitation:** when the reference is itself at depth ≥ 1 (acquired at depth 2 inside a + nested `if`, released at depth 1 in the enclosing block), function-top is not the + common-dominator scope, so the hoist deliberately does not fire and the OWN030 raise persists — + the correct fix is to hoist to the common-dominator block, tracked for a follow-up and locked + by the `nested_branch` xfail test. (Codex P2 on #116.) - **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh` factories. - **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 2848e177..4b7aacc9 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -840,8 +840,24 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] localmap: dict[str, str] = {} fparams = _lower_fn_params(fn, ffile, fname, handles, loc, localmap, released, mos) - fbody = _lower_flow(nodes, ffile, fname, handles, loc, localmap, - released, mos) + # Cross-branch locals (acquired inside an `if`/`while` branch but referenced + # after the merge) must be declared once at the function's outer scope, or + # the core rejects the post-merge reference as OWN030 (the bridge branch- + # scope fix). Pre-declare them here, then skip their in-branch acquire. + hoist = _hoisted_branch_locals(nodes, mos) + hoisted_lets: list[Stmt] = [] + for hname in sorted(hoist): + hh = f"loc_{loc[0]}" + loc[0] += 1 + hline = hoist[hname] + localmap[hname] = hh + handles[hh] = {"file": ffile, "line": hline, "event": hname, + "component": fname, "resource": "flow-local", + "ever_released": hname in released, "pool": False} + hoisted_lets.append(Let(hh, Acquire("Disposable", [], hline), hline)) + fbody = [*hoisted_lets, + *_lower_flow(nodes, ffile, fname, handles, loc, localmap, + released, mos, set(hoist))] # A body that returns a value gets an owned return type, so the core # models `return s` as a valid ESCAPE (the value is discharged to the # caller) instead of a void-return mismatch that would leave `s` looking @@ -1279,11 +1295,85 @@ def _lower_fn_params(fn: dict[str, Any], ffile: str, fname: str, return out +def _hoisted_branch_locals(nodes: Any, mos: dict[str, Any] | None) -> dict[str, int]: + """Locals acquired INSIDE an `if`/`while` branch but referenced after the merge. + + The core resolver is strictly lexical: an `if` pushes a scope per branch and pops + it at the merge, so a `Let` emitted inside a branch is out of scope afterwards. + The bridge's flat `localmap`, however, lets a later `release`/`use` resolve to + that branch-scoped handle — which the core then rejects as OWN030 (undefined + name), and `check_facts` raises. C# allows this shape (`IDisposable r; if (c) r = + new X(); else r = new Y(); r.Dispose();`) because the *declaration* lives in the + outer scope. So such a local must be declared once at the function's outer scope. + + A name is hoisted iff it is **acquired** (a plain `acquire`, or a `fresh`-returning + call `result`) at depth ≥ 1 and its shallowest **reference** (use/release/return/ + call-arg) is at **depth 0** — the function's top level, which is always reached. We + declare it once at the outer scope (always executed), so a balanced cross-branch + release reads as clean and an un-released hoisted acquire still leaks (OWN001) — the + hoist is precision-safe because both the (now unconditional) acquire and the depth-0 + reference run on every path. We deliberately do NOT hoist when the reference is at + depth ≥ 1 (e.g. acquired at depth 2, released at depth 1 inside a nested block): + function-top is not the common-dominator scope there, so an unconditional top-level + acquire would leak on the sibling path — a *false* OWN001. That nested variant + (correct fix = hoist to the common-dominator block) remains a narrower limitation; + the common method-level pattern (a local declared at method scope, assigned in a + branch, disposed at method level) is depth-0 and fully covered. The returned line is + the first branch-acquire site, so a finding anchors near the acquire. (Bridge + branch-scope fix; Codex P2 on #116.)""" + acq_depth: dict[str, int] = {} # name -> shallowest acquire depth + acq_line: dict[str, int] = {} # name -> first-seen acquire line + ref_depth: dict[str, int] = {} # name -> shallowest non-acquire reference depth + + def fresh_result(n: dict[str, Any]) -> str | None: + callee, res = n.get("callee"), n.get("result") + if not (isinstance(res, str) and res and isinstance(callee, str) and callee): + return None + summ = mos.get(callee) if mos is not None else None + return res if (summ is not None and getattr(summ, "returns", None) == "fresh") else None + + def note_ref(name: str, depth: int) -> None: + if name not in ref_depth or depth < ref_depth[name]: + ref_depth[name] = depth + + def walk(ns: Any, depth: int) -> None: + if not isinstance(ns, list): + return + for n in ns: + if not isinstance(n, dict): + continue + op = n.get("op") + line = _as_int(n.get("line", 0)) + acq = (str(n.get("var", "?")) if op == "acquire" + else fresh_result(n) if op == "call" else None) + if acq is not None: + if acq not in acq_depth or depth < acq_depth[acq]: + acq_depth[acq] = depth + acq_line.setdefault(acq, line) + if op in ("use", "release", "overspan", "return"): + v = n.get("var") + if isinstance(v, str): + note_ref(v, depth) + elif op == "call": + for a in (n.get("args") or []): + note_ref(str(a), depth) + if op == "if": + walk(n.get("then"), depth + 1) + walk(n.get("else"), depth + 1) + elif op == "while": + walk(n.get("body"), depth + 1) + + walk(nodes, 0) + return {name: acq_line[name] for name, d in acq_depth.items() + if d >= 1 and ref_depth.get(name, -1) == 0} + + def _lower_flow(nodes: list[Any], ffile: str, fname: str, handles: dict[str, dict[str, Any]], loc: list[int], localmap: dict[str, str], released_vars: set[str], - mos: dict[str, Any] | None = None) -> list[Stmt]: + mos: dict[str, Any] | None = None, + hoisted: set[str] | None = None) -> list[Stmt]: """Lower one OwnIR flow body (B0b/B2) into core statements. acquire/use/release/ return reference a C# local by name (`var`); `if` carries `then`/`else` sub-bodies; `while` carries a `body` (a back-edge — the core's worklist fixpoint @@ -1294,7 +1384,14 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, P-005 D5.2 (T1): a `call` op that binds a `result` local, whose callee's solved summary (`mos`) returns `fresh`, is **also** lowered as an `acquire` of that local — the call site is a factory, so the result is a newly-owned obligation and - the existing leak / double-release / use-after-release checks apply to it.""" + the existing leak / double-release / use-after-release checks apply to it. + + `hoisted` names (see `_hoisted_branch_locals`) are declared once at the function's + outer scope by the caller, so an in-branch acquire of such a name is SKIPPED here + (the hoisted `Let` already declared+acquired it) — this keeps a cross-branch local + in scope after the merge instead of emitting a branch-scoped `Let` the core would + reject as OWN030.""" + hoisted = hoisted or set() body: list[Stmt] = [] for n in nodes: if not isinstance(n, dict): @@ -1302,9 +1399,13 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, op = n.get("op") line = _as_int(n.get("line", 0)) if op == "acquire": + name = str(n.get("var", "?")) + if name in hoisted: + # declared+acquired once at the outer scope (cross-branch local) — the + # hoisted `Let` stands in for this in-branch acquire; emit nothing. + continue handle = f"loc_{loc[0]}" loc[0] += 1 - name = str(n.get("var", "?")) localmap[name] = handle handles[handle] = {"file": ffile, "line": line, "event": name, "component": fname, "resource": "flow-local", @@ -1335,15 +1436,15 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, elif op == "if": tn = n.get("then", []) en = n.get("else", []) - then_b = _lower_flow(tn if isinstance(tn, list) else [], - ffile, fname, handles, loc, localmap, released_vars, mos) - else_b = _lower_flow(en if isinstance(en, list) else [], - ffile, fname, handles, loc, localmap, released_vars, mos) + then_b = _lower_flow(tn if isinstance(tn, list) else [], ffile, fname, + handles, loc, localmap, released_vars, mos, hoisted) + else_b = _lower_flow(en if isinstance(en, list) else [], ffile, fname, + handles, loc, localmap, released_vars, mos, hoisted) body.append(If("?", then_b, else_b, line)) elif op == "while": bn = n.get("body", []) - body_b = _lower_flow(bn if isinstance(bn, list) else [], - ffile, fname, handles, loc, localmap, released_vars, mos) + body_b = _lower_flow(bn if isinstance(bn, list) else [], ffile, fname, + handles, loc, localmap, released_vars, mos, hoisted) body.append(While("?", body_b, line)) elif op == "call": # A call to a CONTRACTED callee (a function/extern whose signature the @@ -1367,7 +1468,7 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # claim, so the result is never falsely owned (precision-first). result = n.get("result") summ = mos.get(callee) if (mos is not None and callee) else None - if (isinstance(result, str) and result + if (isinstance(result, str) and result and result not in hoisted and summ is not None and getattr(summ, "returns", None) == "fresh"): handle = f"loc_{loc[0]}" loc[0] += 1 diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 00431a26..8a6a7d39 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1462,30 +1462,77 @@ def _sub(source: str | None) -> list[Finding]: if gotbare: fails.append("D5.2 T1: a method with a non-owned (`return null`) path is not " f"`fresh`, so a caller's dropped result must be silent, got {gotbare}") - # KNOWN BRIDGE LIMITATION (tracked separately — see docs/notes/d5-ownership-transfer.md - # "branch-scope" entry). A local acquired in BOTH branches of an `if` and released - # AFTER the merge currently crashes: the bridge's flat `localmap` emits each synthetic - # `Let` *inside* its branch block, so the post-merge `release` references an out-of-scope - # handle -> the core reports OWN030 (undefined name), which `check_facts` (correctly, - # strictly) refuses to map and raises OwnIRError. This predates D5.2 — it reproduces with - # a PLAIN `acquire` (no factory/fresh path), shown here so the bug is NOT attributed to - # D5.2's call-result acquire. This is an xfail-style LOCK: when the bridge is made branch- - # aware (hoist/declare synthetic handles at the merge scope), this balanced release must - # become CLEAN (no findings) and this assertion flips to `if bm_findings: fail`. - checks += 1 - bm_raised = False + # BRIDGE BRANCH-SCOPE FIX. A local acquired in BOTH branches of an `if` and released + # AFTER the merge used to crash: the bridge emitted each synthetic `Let` *inside* its + # branch block, so the post-merge `release` referenced an out-of-scope handle -> the + # core reported OWN030 (undefined name) and `check_facts` raised OwnIRError. The bridge + # now HOISTS such cross-branch locals to the function's outer scope (declared once, + # in-branch acquires skipped), so a balanced release is CLEAN. `branch_merge` is the + # exact pre-existing repro (a PLAIN `acquire`, no factory path) — must not crash, no + # findings. (Codex P2 on #116.) + checks += 1 try: - check_facts({"module": "M", "functions": [ + bmf = check_facts({"module": "M", "functions": [ {"name": "branch_merge", "file": "T1.cs", "body": [{"op": "if", "line": 1, "then": [{"op": "acquire", "var": "r", "line": 2}], "else": [{"op": "acquire", "var": "r", "line": 3}]}, {"op": "release", "var": "r", "line": 4}]}]}) + if bmf: + fails.append("bridge branch-scope: a cross-branch acquire released after the " + f"merge must be CLEAN, got {[(x.component, x.code) for x in bmf]}") + except OwnIRError as e: + fails.append(f"bridge branch-scope: cross-branch acquire still crashes ({e})") + # the leak is still caught when the cross-branch local is NOT released: hoisting makes + # the acquire unconditional, so an undischarged one is OWN001 (no false-clean). + checks += 1 + bml = check_facts({"module": "M", "functions": [ + {"name": "branch_leak", "file": "T1.cs", + "body": [{"op": "if", "line": 1, + "then": [{"op": "acquire", "var": "r", "line": 2}], + "else": [{"op": "acquire", "var": "r", "line": 3}]}, + {"op": "use", "var": "r", "line": 4}]}]}) + gotbml = [(x.component, x.code) for x in bml] + if gotbml != [("branch_leak", "OWN001")]: + fails.append("bridge branch-scope: a cross-branch acquire that is used but never " + f"released must still leak OWN001, got {gotbml}") + # and the factory-result form (D5.2 acquire inside a branch) is hoisted too: a fresh + # call result assigned in both branches and released after the merge is CLEAN. + checks += 1 + try: + bmfr = check_facts({"module": "M", "functions": [_MAKE, + {"name": "branch_factory", "file": "T1.cs", + "body": [{"op": "if", "line": 1, + "then": [{"op": "call", "callee": "make", "args": [], "result": "r", + "line": 2}], + "else": [{"op": "call", "callee": "make", "args": [], "result": "r", + "line": 3}]}, + {"op": "release", "var": "r", "line": 4}]}]}) + if bmfr: + fails.append("bridge branch-scope: a cross-branch FACTORY result released after " + f"the merge must be CLEAN, got {[(x.component, x.code) for x in bmfr]}") + except OwnIRError as e: + fails.append(f"bridge branch-scope: cross-branch factory result still crashes ({e})") + # NARROWER REMAINING LIMITATION (xfail-style lock). When the reference is itself at + # depth >= 1 (acquired at depth 2 inside a nested `if`, released at depth 1 in the + # enclosing block), function-top is NOT the common-dominator scope, so the depth-0 + # hoist deliberately does not fire — and the original OWN030 -> OwnIRError still + # occurs. The correct fix is to hoist to the common-dominator block; tracked for a + # follow-up. This lock asserts the current raise and flips when that lands. + checks += 1 + nst_raised = False + try: + check_facts({"module": "M", "functions": [ + {"name": "nested_branch", "file": "T1.cs", + "body": [{"op": "if", "line": 1, "else": [], + "then": [{"op": "if", "line": 2, "else": [], + "then": [{"op": "acquire", "var": "r", "line": 3}]}, + {"op": "release", "var": "r", "line": 4}]}]}]}) except OwnIRError: - bm_raised = True - if not bm_raised: - fails.append("branch-acquire-after-merge no longer raises OwnIRError — the bridge " - "branch-scope fix has landed; make this shape CLEAN and flip this lock") + nst_raised = True + if not nst_raised: + fails.append("bridge branch-scope: nested cross-branch acquire no longer raises — the " + "common-dominator hoist has landed; make this CLEAN and flip this lock") # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; # the buffer is still returned, so there is no OWN001 leak. Routes through the From 66eb5135a23175fada657054c70a39d2493e97fb Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 15:41:29 +0000 Subject: [PATCH 2/4] fix(bridge): exclude while-body acquires from the branch-merge hoist (Codex P1) The hoist is sound only for mutually-exclusive if branches: exactly one acquire runs, so a single unconditional one is balanced. A while body is cumulative -- hoisting while { acquire r }; release r to one acquire collapsed 0..N iterations and HID the per-iteration leak (returned no findings). _hoisted_branch_locals now tracks loop-enclosed acquires and excludes them, so a loop-acquired local keeps its pre-existing loud behaviour (OWN030 -> OwnIRError) instead of a silent false- clean. A loop-aware model is a separate follow-up. Test: loop_acq locks the raise (not a false-clean) and flips when that lands. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 7 ++++++- ownlang/ownir.py | 31 ++++++++++++++++++++--------- tests/test_ownir.py | 20 +++++++++++++++++++ 3 files changed, 48 insertions(+), 10 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 80c6706e..e1cfa813 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -311,7 +311,12 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa nested `if`, released at depth 1 in the enclosing block), function-top is not the common-dominator scope, so the hoist deliberately does not fire and the OWN030 raise persists — the correct fix is to hoist to the common-dominator block, tracked for a follow-up and locked - by the `nested_branch` xfail test. (Codex P2 on #116.) + by the `nested_branch` xfail test. **`while` bodies are also excluded:** `if` branches are + mutually exclusive (one acquire runs → unconditional is balanced), but loop iterations are + *cumulative*, so hoisting `while { r = acquire() }; release r` to a single acquire would hide a + per-iteration leak. A loop-acquired local keeps its pre-existing (loud OWN030) behaviour rather + than a silent false-clean; a loop-aware model is a separate follow-up, locked by the `loop_acq` + xfail test. (Codex P2 on #116; loop exclusion Codex P1 on #120.) - **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh` factories. - **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 4b7aacc9..312071c6 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -1319,11 +1319,17 @@ def _hoisted_branch_locals(nodes: Any, mos: dict[str, Any] | None) -> dict[str, (correct fix = hoist to the common-dominator block) remains a narrower limitation; the common method-level pattern (a local declared at method scope, assigned in a branch, disposed at method level) is depth-0 and fully covered. The returned line is - the first branch-acquire site, so a finding anchors near the acquire. (Bridge - branch-scope fix; Codex P2 on #116.)""" + the first branch-acquire site, so a finding anchors near the acquire. + + Acquires inside a `while` body are also excluded: `if` branches are mutually + exclusive (one acquire runs → unconditional is balanced) but loop iterations are + cumulative, so hoisting `while { r = acquire() }; release r` to one acquire would + hide a per-iteration leak. A loop-aware model is a separate follow-up. (Bridge + branch-scope fix; Codex P2 on #116, loop exclusion Codex P1 on #120.)""" acq_depth: dict[str, int] = {} # name -> shallowest acquire depth acq_line: dict[str, int] = {} # name -> first-seen acquire line ref_depth: dict[str, int] = {} # name -> shallowest non-acquire reference depth + loop_acq: set[str] = set() # names acquired anywhere inside a `while` body def fresh_result(n: dict[str, Any]) -> str | None: callee, res = n.get("callee"), n.get("result") @@ -1336,7 +1342,7 @@ def note_ref(name: str, depth: int) -> None: if name not in ref_depth or depth < ref_depth[name]: ref_depth[name] = depth - def walk(ns: Any, depth: int) -> None: + def walk(ns: Any, depth: int, in_loop: bool) -> None: if not isinstance(ns, list): return for n in ns: @@ -1350,6 +1356,8 @@ def walk(ns: Any, depth: int) -> None: if acq not in acq_depth or depth < acq_depth[acq]: acq_depth[acq] = depth acq_line.setdefault(acq, line) + if in_loop: + loop_acq.add(acq) if op in ("use", "release", "overspan", "return"): v = n.get("var") if isinstance(v, str): @@ -1358,14 +1366,19 @@ def walk(ns: Any, depth: int) -> None: for a in (n.get("args") or []): note_ref(str(a), depth) if op == "if": - walk(n.get("then"), depth + 1) - walk(n.get("else"), depth + 1) + walk(n.get("then"), depth + 1, in_loop) + walk(n.get("else"), depth + 1, in_loop) elif op == "while": - walk(n.get("body"), depth + 1) - - walk(nodes, 0) + walk(n.get("body"), depth + 1, True) + + walk(nodes, 0, False) + # Only `if`-branch acquires are hoistable: branches are mutually exclusive, so + # exactly one acquire runs and a single unconditional one is balanced. A `while` + # body is CUMULATIVE — hoisting it would collapse 0..N iterations into one acquire + # and hide a per-iteration leak (Codex P1), so a loop-acquired local is excluded (it + # keeps its pre-existing behaviour; a loop-aware model is a separate follow-up). return {name: acq_line[name] for name, d in acq_depth.items() - if d >= 1 and ref_depth.get(name, -1) == 0} + if d >= 1 and ref_depth.get(name, -1) == 0 and name not in loop_acq} def _lower_flow(nodes: list[Any], ffile: str, fname: str, diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 8a6a7d39..0ff11b2c 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1533,6 +1533,26 @@ def _sub(source: str | None) -> list[Finding]: if not nst_raised: fails.append("bridge branch-scope: nested cross-branch acquire no longer raises — the " "common-dominator hoist has landed; make this CLEAN and flip this lock") + # LOOP EXCLUSION (Codex P1): the hoist is for mutually-exclusive `if` branches only. + # A `while` body is cumulative, so hoisting `while { acquire r }; release r` to one + # acquire would HIDE the per-iteration leak (a false-clean). Loop-acquired locals are + # excluded, so this keeps its pre-existing LOUD behaviour (OWN030 -> OwnIRError) rather + # than silently returning no findings. A loop-aware model is a separate follow-up; this + # lock asserts the raise (NOT a false-clean) and flips when that model lands. + checks += 1 + loop_raised = False + try: + check_facts({"module": "M", "functions": [ + {"name": "loop_acq", "file": "T1.cs", + "body": [{"op": "while", "line": 1, + "body": [{"op": "acquire", "var": "r", "line": 2}]}, + {"op": "release", "var": "r", "line": 3}]}]}) + except OwnIRError: + loop_raised = True + if not loop_raised: + fails.append("bridge branch-scope: a while-body acquire released after the loop must " + "NOT be silently hoisted to clean — it stays loud until a loop-aware model " + "lands; got no raise (false-clean or premature loop hoist)") # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; # the buffer is still returned, so there is no OWN001 leak. Routes through the From 0c3254af8870fdb30da9213513b07e868dfc5dcf Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 15:54:21 +0000 Subject: [PATCH 3/4] fix(bridge): gate the branch hoist with a safety predicate + preserve pool kind (CodeRabbit) Two issues in the branch-scope hoist: 1) (Major) depth-0 reference is not sufficient. Hoisting makes a conditional acquire unconditional, so a branch that early-returns before the release on a path that did not acquire the local leaks the hoisted resource -- a FALSE OWN001 (if c: acquire r else: return; release r). Add _branch_hoist_safe, a definite-assignment walk (an if establishes acquisition only when both arms do, a while body never does, a non-discharging return on a not-yet-acquired path is unsafe); a name is hoisted only when it holds. The guard shape now stays a loud OWN030 raise instead of a fabricated finding. 2) (Minor) hoisted acquires hardcoded pool=False, dropping ArrayPool-rent metadata. Track the acquire kind and preserve it on the hoisted handle, so a branch-hoisted Rent still reports as a pooled buffer. Tests: guard (early-return -> not hoisted, no false finding), one_branch (no early return -> clean), pool_branch (pooled kind preserved). branch_merge / branch_factory / branch_leak unchanged. Full suite green (corpus 19/19), ruff + mypy clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 36 +++++------ ownlang/ownir.py | 98 +++++++++++++++++++++-------- tests/test_ownir.py | 50 +++++++++++++++ 3 files changed, 141 insertions(+), 43 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index e1cfa813..c4aa7f63 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -299,24 +299,24 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa `OwnIRError`. It predated D5 (reproduced with a **plain `acquire`**, no fresh/factory path); D5.2's call-result acquire only added another way to reach it. Fixed by making `acquire` lowering **branch-aware**: `_hoisted_branch_locals` finds locals acquired at depth ≥ 1 whose - shallowest reference is at **depth 0** (the function top, always reached), and `to_module` - declares each **once at the function's outer scope** (a single `Let`), skipping the in-branch - acquire. A balanced cross-branch release is now CLEAN; an un-released one still leaks **OWN001** - (hoisting a conditional acquire to unconditional is precision-safe *because* the depth-0 - reference also runs on every path — never a fabricated use/double-release). Covers both the - plain `acquire` and the `fresh` call-result form. We deliberately did **not** soft-skip OWN030 - (it would mask genuine lowering drift; the strict map-or-raise invariant is load-bearing). - Tests: `branch_merge` (clean), `branch_leak` (OWN001), `branch_factory` (clean). **Narrower - remaining limitation:** when the reference is itself at depth ≥ 1 (acquired at depth 2 inside a - nested `if`, released at depth 1 in the enclosing block), function-top is not the - common-dominator scope, so the hoist deliberately does not fire and the OWN030 raise persists — - the correct fix is to hoist to the common-dominator block, tracked for a follow-up and locked - by the `nested_branch` xfail test. **`while` bodies are also excluded:** `if` branches are - mutually exclusive (one acquire runs → unconditional is balanced), but loop iterations are - *cumulative*, so hoisting `while { r = acquire() }; release r` to a single acquire would hide a - per-iteration leak. A loop-acquired local keeps its pre-existing (loud OWN030) behaviour rather - than a silent false-clean; a loop-aware model is a separate follow-up, locked by the `loop_acq` - xfail test. (Codex P2 on #116; loop exclusion Codex P1 on #120.) + shallowest reference is at **depth 0** (function-top, so function-scope is the common dominator), + and `to_module` declares each **once at the function's outer scope** (a single `Let`), skipping + the in-branch acquire. A balanced cross-branch release is now CLEAN; an un-released one still + leaks **OWN001**. Covers both the plain `acquire` and the `fresh` call-result form, and a hoisted + ArrayPool rent keeps its `pool` kind (so it still reports as a pooled buffer). We deliberately did + **not** soft-skip OWN030 (it would mask genuine lowering drift; the strict map-or-raise invariant + is load-bearing). Because hoisting makes a conditional acquire **unconditional**, it is gated by + `_branch_hoist_safe` — a definite-assignment walk that blocks the hoist when a branch can + early-`return` before the release on a path that did not acquire the local (else the hoisted + resource would leak there — a *false* OWN001, e.g. `if c: acquire r else: return; release r`). + Tests: `branch_merge` / `branch_factory` / `one_branch` (clean), `branch_leak` (OWN001), + `pool_branch` (pooled kind preserved), `guard` (early-return → not hoisted, no fabricated + finding). **Narrower remaining limitations** (each a documented xfail lock, fixed by a later + loop-/dominator-aware model): a reference at depth ≥ 1 inside a nested block (`nested_branch` — + function-top isn't the common dominator), a `while`-body acquire (`loop_acq` — iterations are + cumulative), and the early-return guard shape (`guard` — stays a loud OWN030 raise rather than a + false positive). (Bridge branch-scope fix: Codex P2 on #116; loop exclusion Codex P1, hoist + safety predicate + pool-kind preservation CodeRabbit on #120.) - **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh` factories. - **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 312071c6..bf46fed8 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -849,11 +849,11 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] for hname in sorted(hoist): hh = f"loc_{loc[0]}" loc[0] += 1 - hline = hoist[hname] + hline, hpool = hoist[hname] localmap[hname] = hh handles[hh] = {"file": ffile, "line": hline, "event": hname, "component": fname, "resource": "flow-local", - "ever_released": hname in released, "pool": False} + "ever_released": hname in released, "pool": hpool} hoisted_lets.append(Let(hh, Acquire("Disposable", [], hline), hline)) fbody = [*hoisted_lets, *_lower_flow(nodes, ffile, fname, handles, loc, localmap, @@ -1295,7 +1295,57 @@ def _lower_fn_params(fn: dict[str, Any], ffile: str, fname: str, return out -def _hoisted_branch_locals(nodes: Any, mos: dict[str, Any] | None) -> dict[str, int]: +def _branch_hoist_safe(nodes: Any, name: str, mos: dict[str, Any] | None) -> bool: + """Whether hoisting `name` to an *unconditional* outer-scope acquire is leak-safe. + + Hoisting makes a conditional acquire unconditional, so it is only safe if no path + can EXIT (early `return`) before the post-merge release on a path where the source + did not already acquire `name` — otherwise the hoisted resource leaks on that path, + a *false* OWN001 (e.g. `if c: acquire r else: return; release r`). This is a + definite-assignment walk: an `if` establishes acquisition only when **both** arms + do, a `while` body never does (it may run zero times), and a `return` that does not + itself return `name` (a discharge) on a not-yet-acquired path is unsafe. (CodeRabbit + Major on #120.)""" + def acquires(n: dict[str, Any]) -> bool: + if n.get("op") == "acquire" and str(n.get("var", "")) == name: + return True + if n.get("op") == "call" and str(n.get("result", "")) == name: + summ = mos.get(str(n.get("callee", ""))) if mos is not None else None + return summ is not None and getattr(summ, "returns", None) == "fresh" + return False + + def analyze(seq: Any, acquired: bool) -> tuple[bool, bool]: + # (safe, acquired_after); safe=False => a fabricated-leak exit exists. + if not isinstance(seq, list): + return True, acquired + for n in seq: + if not isinstance(n, dict): + continue + op = n.get("op") + if acquires(n): + acquired = True + elif op == "return": + if not acquired and str(n.get("var", "")) != name: + return False, acquired + elif op == "if": + s1, a1 = analyze(n.get("then"), acquired) + if not s1: + return False, acquired + s2, a2 = analyze(n.get("else"), acquired) + if not s2: + return False, acquired + acquired = acquired or (a1 and a2) + elif op == "while": + s, _ = analyze(n.get("body"), acquired) # 0-trip: no acquisition gained + if not s: + return False, acquired + return True, acquired + + return analyze(nodes, False)[0] + + +def _hoisted_branch_locals(nodes: Any, + mos: dict[str, Any] | None) -> dict[str, tuple[int, bool]]: """Locals acquired INSIDE an `if`/`while` branch but referenced after the merge. The core resolver is strictly lexical: an `if` pushes a scope per branch and pops @@ -1306,28 +1356,22 @@ def _hoisted_branch_locals(nodes: Any, mos: dict[str, Any] | None) -> dict[str, new X(); else r = new Y(); r.Dispose();`) because the *declaration* lives in the outer scope. So such a local must be declared once at the function's outer scope. - A name is hoisted iff it is **acquired** (a plain `acquire`, or a `fresh`-returning - call `result`) at depth ≥ 1 and its shallowest **reference** (use/release/return/ - call-arg) is at **depth 0** — the function's top level, which is always reached. We - declare it once at the outer scope (always executed), so a balanced cross-branch - release reads as clean and an un-released hoisted acquire still leaks (OWN001) — the - hoist is precision-safe because both the (now unconditional) acquire and the depth-0 - reference run on every path. We deliberately do NOT hoist when the reference is at - depth ≥ 1 (e.g. acquired at depth 2, released at depth 1 inside a nested block): - function-top is not the common-dominator scope there, so an unconditional top-level - acquire would leak on the sibling path — a *false* OWN001. That nested variant - (correct fix = hoist to the common-dominator block) remains a narrower limitation; - the common method-level pattern (a local declared at method scope, assigned in a - branch, disposed at method level) is depth-0 and fully covered. The returned line is - the first branch-acquire site, so a finding anchors near the acquire. - - Acquires inside a `while` body are also excluded: `if` branches are mutually - exclusive (one acquire runs → unconditional is balanced) but loop iterations are - cumulative, so hoisting `while { r = acquire() }; release r` to one acquire would - hide a per-iteration leak. A loop-aware model is a separate follow-up. (Bridge - branch-scope fix; Codex P2 on #116, loop exclusion Codex P1 on #120.)""" + A name is hoisted iff (1) it is **acquired** (a plain `acquire`, or a `fresh`- + returning call `result`) at depth ≥ 1; (2) its shallowest **reference** (use/release/ + return/call-arg) is at **depth 0** — the function top, so function-scope is the + common-dominator (a depth ≥ 1 reference, e.g. acquired at depth 2 / released at depth + 1, is *not* dominated by function-top, so hoisting there would leak on a sibling path; + that nested variant stays a narrower limitation); (3) it is not acquired inside a + `while` body (loop iterations are cumulative — hoisting `while { r = acquire() }; + release r` to one acquire would hide a per-iteration leak); and (4) `_branch_hoist_safe` + holds — no path can early-`return` before the release on a path that did not acquire + the local (else the unconditional hoisted acquire fabricates a leak — a *false* + OWN001). The returned `(line, pool)` is the first branch-acquire site and whether it + is an ArrayPool rent (so a hoisted pooled buffer keeps its kind). (Bridge branch-scope + fix; Codex P2 on #116, loop exclusion Codex P1 + safety/pool CodeRabbit on #120.)""" acq_depth: dict[str, int] = {} # name -> shallowest acquire depth acq_line: dict[str, int] = {} # name -> first-seen acquire line + acq_pool: dict[str, bool] = {} # name -> is an ArrayPool rent (any acquire) ref_depth: dict[str, int] = {} # name -> shallowest non-acquire reference depth loop_acq: set[str] = set() # names acquired anywhere inside a `while` body @@ -1356,6 +1400,8 @@ def walk(ns: Any, depth: int, in_loop: bool) -> None: if acq not in acq_depth or depth < acq_depth[acq]: acq_depth[acq] = depth acq_line.setdefault(acq, line) + if op == "acquire" and n.get("kind") == "pool": + acq_pool[acq] = True if in_loop: loop_acq.add(acq) if op in ("use", "release", "overspan", "return"): @@ -1377,8 +1423,10 @@ def walk(ns: Any, depth: int, in_loop: bool) -> None: # body is CUMULATIVE — hoisting it would collapse 0..N iterations into one acquire # and hide a per-iteration leak (Codex P1), so a loop-acquired local is excluded (it # keeps its pre-existing behaviour; a loop-aware model is a separate follow-up). - return {name: acq_line[name] for name, d in acq_depth.items() - if d >= 1 and ref_depth.get(name, -1) == 0 and name not in loop_acq} + return {name: (acq_line[name], acq_pool.get(name, False)) + for name, d in acq_depth.items() + if d >= 1 and ref_depth.get(name, -1) == 0 and name not in loop_acq + and _branch_hoist_safe(nodes, name, mos)} def _lower_flow(nodes: list[Any], ffile: str, fname: str, diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 0ff11b2c..9690d6f6 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1553,6 +1553,56 @@ def _sub(source: str | None) -> list[Finding]: fails.append("bridge branch-scope: a while-body acquire released after the loop must " "NOT be silently hoisted to clean — it stays loud until a loop-aware model " "lands; got no raise (false-clean or premature loop hoist)") + # SAFETY (CodeRabbit Major): the hoist must NOT fire when a branch early-`return`s on a + # path that did not acquire the local — an unconditional hoisted acquire would leak on + # that path, a FALSE OWN001. `guard` (`if c: acquire r else: return; release r`) is + # clean C# (else returns, r never acquired there). `_branch_hoist_safe` blocks the hoist, + # so this stays the pre-existing loud raise — never a fabricated OWN001. + checks += 1 + guard_ok = False + try: + gf = check_facts({"module": "M", "functions": [ + {"name": "guard", "file": "T1.cs", + "body": [{"op": "if", "line": 1, + "then": [{"op": "acquire", "var": "r", "line": 2}], + "else": [{"op": "return", "line": 3}]}, + {"op": "release", "var": "r", "line": 4}]}]}) + guard_ok = not gf # if it lowered, it must NOT fabricate a finding + except OwnIRError: + guard_ok = True # not hoisted -> loud raise, never a false OWN001 + if not guard_ok: + fails.append("bridge branch-scope: an early-return branch must not be hoisted into a " + "fabricated OWN001 (the hoist safety predicate must block it)") + # a one-branch acquire with NO early return IS safe to hoist (else falls through to the + # release; null-safe dispose). It must be CLEAN, not crash. + checks += 1 + try: + ob = check_facts({"module": "M", "functions": [ + {"name": "one_branch", "file": "T1.cs", + "body": [{"op": "if", "line": 1, "else": [], + "then": [{"op": "acquire", "var": "r", "line": 2}]}, + {"op": "release", "var": "r", "line": 3}]}]}) + if ob: + gotob = [(x.component, x.code) for x in ob] + fails.append("bridge branch-scope: a one-branch acquire (no early return) released " + f"after the merge must be CLEAN, got {gotob}") + except OwnIRError as e: + fails.append(f"bridge branch-scope: a safe one-branch acquire must not crash ({e!r})") + # a hoisted ArrayPool rent keeps its `pool` kind: a cross-branch Rent that is never + # released leaks as a POOLED buffer (OWN025-style wording), not a generic disposable. + # (CodeRabbit: the hoist must preserve acquire `kind`.) Asserted via the leak being + # tagged pooled in its structured finding. + checks += 1 + pl = check_facts({"module": "M", "functions": [ + {"name": "pool_branch", "file": "T1.cs", + "body": [{"op": "if", "line": 1, + "then": [{"op": "acquire", "var": "r", "kind": "pool", "line": 2}], + "else": [{"op": "acquire", "var": "r", "kind": "pool", "line": 3}]}, + {"op": "use", "var": "r", "line": 4}]}]}) + pooled = [x for x in pl if getattr(x, "pooled", False) or "pool" in (x.message or "").lower()] + if not pl or not pooled: + fails.append("bridge branch-scope: a hoisted ArrayPool rent that leaks must stay tagged " + f"a pooled buffer (kind preserved), got {[(x.code, x.message) for x in pl]}") # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; # the buffer is still returned, so there is no OWN001 leak. Routes through the From 4cd2a2de0ff66e3c2e8d54b7795ac6933501ef0d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 15:58:08 +0000 Subject: [PATCH 4/4] test(bridge): assert structured Finding.kind in the hoisted-pool regression (CodeRabbit) The pool-preservation test checked a nonexistent 'pooled' attribute or 'pool' in the message wording, which could miss a metadata regression while passing on text. Assert the exact shape instead: [(code, kind)] == [('OWN001', 'pooled buffer')] -- dropping the pool flag lowers the hoisted handle to 'disposable', which this now catches directly. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- tests/test_ownir.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 9690d6f6..16c66deb 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1599,10 +1599,12 @@ def _sub(source: str | None) -> list[Finding]: "then": [{"op": "acquire", "var": "r", "kind": "pool", "line": 2}], "else": [{"op": "acquire", "var": "r", "kind": "pool", "line": 3}]}, {"op": "use", "var": "r", "line": 4}]}]}) - pooled = [x for x in pl if getattr(x, "pooled", False) or "pool" in (x.message or "").lower()] - if not pl or not pooled: + # assert the structured kind, not wording: dropping the pool flag would lower the + # hoisted handle to a generic "disposable" (CodeRabbit). + gotpl = [(x.code, x.kind) for x in pl] + if gotpl != [("OWN001", "pooled buffer")]: fails.append("bridge branch-scope: a hoisted ArrayPool rent that leaks must stay tagged " - f"a pooled buffer (kind preserved), got {[(x.code, x.message) for x in pl]}") + f"kind='pooled buffer' (kind preserved through the hoist), got {gotpl}") # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; # the buffer is still returned, so there is no OWN001 leak. Routes through the