From 0bf537b3eec451ac0b8f289bf988315c8134585d Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 11:38:11 +0000 Subject: [PATCH 1/5] feat(d5): D5.2 -- T1 fresh-returning factories become acquire sites Infer a method's owned-return kind in _build_skeletons: a body that acquires a local and returns it is fresh (a factory); a single returned local that is the result of a first-party call is a forward-return the solver propagates. Caller- side, a call op that binds a result whose callee summary returns fresh is also lowered to an acquire of that local, so the existing leak / double-release / use-after-release checks apply at the call site -- the factory-leak class, lost before D5.2. Precision-first: a returned parameter is never fresh (that is wrap/alias, T4/D5.4), and a non-fresh/unknown return makes no claim, so a result is never falsely owned. The out/ref-owned door is noted as a later T1 slice. Tests: factory-result leak (OWN001 at the call), disposed-clean, use-after- dispose (OWN002), forward-return propagation, param-return precision guard. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 15 +++- ownlang/ownir.py | 117 +++++++++++++++++++++++++++- tests/test_ownir.py | 68 ++++++++++++++++ 3 files changed, 194 insertions(+), 6 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 59542814..0dcc9778 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -278,8 +278,19 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa Oxide's `shrd|uniq`, Polonius's per-loan invalidation — exclusivity is a distinct semantic axis, not coarser metadata. Tracked here so the deferral is recorded, not buried (Codex P2 / CodeRabbit Major on #113). -- **D5.2 — T1.** `fresh`-returning calls become acquire sites → factory leaks. Includes - `out`/`ref`-owned (another `fresh` door) before async. +- **D5.2 — T1 return-value door (shipped).** A `fresh`-returning call becomes an **acquire + site**. `_build_skeletons` now infers the return kind (`_infer_return_skeleton`): a body that + `acquire`s a local and returns it is `fresh` (a factory), and a single returned local that is + the result of a first-party `call` is a `forward`-return the solver propagates (factory-of- + factory). Caller-side, a `call` op that binds a `result` whose callee summary returns `fresh` + is **also** lowered to an `acquire` of that local, so the existing leak / double-release / + use-after-release checks apply at the call site. Precision-first: a returned **parameter** is + never `fresh` (that is wrap/alias, T4/D5.4), and a non-fresh / unknown return makes no claim — + the result is never falsely owned. Proven by synthetic OwnIR tests: factory-result leak + (OWN001 @ the call), disposed-clean, use-after-dispose (OWN002), forward-return propagation, + 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. - **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 6a25a48a..71b3bc92 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -142,6 +142,7 @@ MethodSkeleton, ParamSkeleton, PathAction, + ReturnSkeleton, Transfer, solve, ) @@ -840,7 +841,7 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] fparams = _lower_fn_params(fn, ffile, fname, handles, loc, localmap, released, mos) fbody = _lower_flow(nodes, ffile, fname, handles, loc, localmap, - released) + released, mos) # 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 @@ -905,6 +906,85 @@ def _returns_value(nodes: Any) -> bool: return False +def _collect_vars(nodes: Any, op_kind: str, field: str) -> set[str]: + """Every string `field` of every `op_kind` op in a flow body (recursing into + if/while). Used to gather the locals a body `acquire`s and the locals it + `return`s, for P-005 D5.2 fresh-return inference.""" + out: set[str] = set() + if not isinstance(nodes, list): + return out + for n in nodes: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == op_kind: + v = n.get(field) + if isinstance(v, str): + out.add(v) + elif op == "if": + out |= _collect_vars(n.get("then"), op_kind, field) + out |= _collect_vars(n.get("else"), op_kind, field) + elif op == "while": + out |= _collect_vars(n.get("body"), op_kind, field) + return out + + +def _call_result_callees(nodes: Any) -> dict[str, str | None]: + """Map each `result` local of a `call` op to the callee that produced it (for + forward-return inference, P-005 D5.2). A local bound by two *different* callees + (e.g. on separate branches) maps to None — ambiguous, so never claimed as a + forward-return (precision-first).""" + out: dict[str, str | None] = {} + if not isinstance(nodes, list): + return out + + def visit(ns: Any) -> None: + if not isinstance(ns, list): + return + for n in ns: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == "call": + res = n.get("result") + callee = n.get("callee") + if isinstance(res, str) and isinstance(callee, str) and callee: + out[res] = None if res in out and out[res] != callee else callee + elif op == "if": + visit(n.get("then")) + visit(n.get("else")) + elif op == "while": + visit(n.get("body")) + + visit(nodes) + return out + + +def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton: + """Infer a method's owned-return kind for the D5.0 solver (P-005 D5.2, T1). + + `fresh` — every `return ` path returns a local the body itself `acquire`d + (a factory: `acquire x; …; return x`). A returned **parameter** is NOT fresh + (that is the wrap/alias case, T4 / D5.4) — claiming fresh there would make a + caller acquire a value it does not own. `forward` — a single returned local that + is the result of a first-party `call` (a factory-of-factory: `var t = Make(); + return t;`); the solver propagates `Make`'s own return kind. Anything else stays + `none` (no claim) — precision-first: we only mark a call an acquire site when we + can prove the result is freshly owned.""" + returned = _collect_vars(nodes, "return", "var") + if not returned: + return ReturnSkeleton() # void / no value return + acquired = _collect_vars(nodes, "acquire", "var") + if all(v in acquired and v not in param_names for v in returned): + return ReturnSkeleton("fresh") + if len(returned) == 1: + (v,) = tuple(returned) + callee = _call_result_callees(nodes).get(v) + if callee and v not in param_names and v not in acquired: + return ReturnSkeleton("forward", callee=callee) + return ReturnSkeleton() # not provably owned -> no claim + + # P-006/2b: a method's ownership CONTRACT is its parameters' effects. Encoding # each effect as the TypeRef `collect_signatures` reads (a resource-typed value => # CONSUME, a borrowed type => BORROW/BORROW_MUT, anything else => PLAIN) lets the @@ -1037,6 +1117,10 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: (→ the caller stays plain), never a flattened `must`. Per-path structure is not modelled here — D5.1 deliberately under-claims rather than guess. + The return kind is inferred too (P-005 D5.2, T1): a body that `acquire`s a local + and returns it is `fresh` (a factory); `_infer_return_skeleton` keeps it + precision-first (a returned parameter is never `fresh`). + Functions whose name is not unique are dropped (overload keys are not yet distinguishable — note's open question 2 — so a forward to such a name stays `unknown` → silent, the precision-safe choice).""" @@ -1083,7 +1167,9 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: else: paths = () params.append(ParamSkeleton(i, cname, True, paths)) - skels.append(MethodSkeleton(key, tuple(params))) + pnames = {str(p.get("name", "")) for p in raw_params if isinstance(p, dict)} + ret = _infer_return_skeleton(body, pnames) + skels.append(MethodSkeleton(key, tuple(params), ret)) return skels @@ -1164,13 +1250,19 @@ def _lower_fn_params(fn: dict[str, Any], ffile: str, fname: str, 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]) -> list[Stmt]: + released_vars: set[str], + mos: dict[str, Any] | 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 checks it, P-016 A1). Each acquire gets a globally-unique handle `loc_` (so a finding maps back to the C# local); `localmap` resolves later references within - the same function and its branches/loops.""" + the same function and its branches/loops. + + 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.""" body: list[Stmt] = [] for n in nodes: if not isinstance(n, dict): @@ -1236,6 +1328,23 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, arg_refs: list[Expr] = [VarRef(localmap.get(str(a), str(a)), line) for a in raw_args] body.append(Call(callee, arg_refs, line)) + # P-005 D5.2 (T1): if the call binds a result and the callee is a known + # `fresh`-returning factory, the result is a newly-owned local — mint an + # acquire for it (the args' effects, if any, were applied by the Call + # above; this models the return). A non-fresh / unknown return makes no + # 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 + and summ is not None and getattr(summ, "returns", None) == "fresh"): + handle = f"loc_{loc[0]}" + loc[0] += 1 + localmap[result] = handle + handles[handle] = {"file": ffile, "line": line, "event": result, + "component": fname, "resource": "flow-local", + "ever_released": result in released_vars, + "pool": False} + body.append(Let(handle, Acquire("Disposable", [], line), line)) return body diff --git a/tests/test_ownir.py b/tests/test_ownir.py index c4fce693..2df01d1a 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1343,6 +1343,74 @@ def _sub(source: str | None) -> list[Finding]: if gotct != [("caller_t", 10, "OWN002")]: fails.append("D5.1b $consume channel must propagate transitively: a param " f"forwarded to $consume makes the method consume, got {gotct}") + # --- P-005 D5.2 (T1): a `fresh`-returning factory call becomes an acquire SITE. + # A method that acquires a local and returns it (`make`) has returnsOwned=fresh; + # a caller binding its result (`var r = make()`) now owns `r`, so the existing + # leak / double-release / use-after checks apply to the call site. This is the + # factory-leak class — silently lost before D5.2. + _MAKE = {"name": "make", "file": "T1.cs", + "body": [{"op": "acquire", "var": "x", "line": 1}, + {"op": "return", "var": "x", "line": 2}]} + # the result is never disposed -> the factory call site leaks (OWN001 @ the call). + checks += 1 + fl = check_facts({"module": "M", "functions": [_MAKE, + {"name": "caller", "file": "T1.cs", + "body": [{"op": "call", "callee": "make", "args": [], "result": "r", + "line": 10}]}]}) + gotfl = [(x.component, x.line, x.code) for x in fl] + if gotfl != [("caller", 10, "OWN001")]: + fails.append("D5.2 T1: a fresh-returning factory whose result is never disposed " + f"must leak OWN001@10 at the call site, got {gotfl}") + # the same result, disposed, is clean (the obligation is discharged). + checks += 1 + fok = check_facts({"module": "M", "functions": [_MAKE, + {"name": "caller_ok", "file": "T1.cs", + "body": [{"op": "call", "callee": "make", "args": [], "result": "r", "line": 10}, + {"op": "release", "var": "r", "line": 11}]}]}) + if fok: + fails.append("D5.2 T1: a factory result that IS disposed must be clean, " + f"got {[(x.component, x.code) for x in fok]}") + # using the factory result after dispose is use-after-release (OWN002 @ the call). + checks += 1 + fuar = check_facts({"module": "M", "functions": [_MAKE, + {"name": "caller_uar", "file": "T1.cs", + "body": [{"op": "call", "callee": "make", "args": [], "result": "r", "line": 10}, + {"op": "release", "var": "r", "line": 11}, + {"op": "use", "var": "r", "line": 12}]}]}) + gotuar = [(x.component, x.line, x.code) for x in fuar] + if gotuar != [("caller_uar", 10, "OWN002")]: + fails.append("D5.2 T1: using a factory result after dispose must be OWN002@10, " + f"got {gotuar}") + # fresh propagates through a forward-return factory-of-factory: `relay` returns the + # result of `make`, so `relay` is fresh too, and a caller leaking it is OWN001. + checks += 1 + ff = check_facts({"module": "M", "functions": [_MAKE, + {"name": "relay", "file": "T1.cs", + "body": [{"op": "call", "callee": "make", "args": [], "result": "t", "line": 1}, + {"op": "return", "var": "t", "line": 2}]}, + {"name": "caller_ff", "file": "T1.cs", + "body": [{"op": "call", "callee": "relay", "args": [], "result": "r", + "line": 10}]}]}) + gotff = [(x.component, x.line, x.code) for x in ff] + if gotff != [("caller_ff", 10, "OWN001")]: + fails.append("D5.2 T1: fresh must propagate through a forward-return factory-of-" + f"factory, so the caller leaks OWN001@10, got {gotff}") + # PRECISION: a method that returns a PARAMETER is NOT fresh (that is the wrap/alias + # case, T4/D5.4). `ident(s){ return s }` must not make the caller acquire `r`, and + # must not consume the arg — so acquire/call/release of `a` stays clean and silent. + checks += 1 + pr = check_facts({"module": "M", "functions": [ + {"name": "ident", "file": "T1.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "return", "var": "s", "line": 2}]}, + {"name": "caller_pr", "file": "T1.cs", + "body": [{"op": "acquire", "var": "a", "line": 10}, + {"op": "call", "callee": "ident", "args": ["a"], "result": "r", + "line": 11}, + {"op": "release", "var": "a", "line": 12}]}]}) + if pr: + gotpr = [(x.component, x.code) for x in pr] + fails.append("D5.2 T1: returning a parameter is not `fresh` (no false acquire of " + f"the result, no consume of the arg), got {gotpr}") # 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 0b456988e5ac9794568dccf38ce004e4da86ae22 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 11:48:55 +0000 Subject: [PATCH 2/5] fix(d5): thread MOS into nested flow lowering so factory leaks in if/while are caught (Codex P2) The recursive _lower_flow calls for if/then/else and while bodies dropped the new mos argument, so a fresh-returning factory call inside control flow ran with mos=None and silently skipped the D5.2 acquire -- a factory leak in a branch/loop went unreported. Pass mos through all three recursive calls. Adds a regression test: a fresh factory call in an if branch whose result is never disposed must leak OWN001 at the call site, like the top-level case. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- ownlang/ownir.py | 6 +++--- tests/test_ownir.py | 14 ++++++++++++++ 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 71b3bc92..f7bc5762 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -1304,14 +1304,14 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, 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) + 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) + ffile, fname, handles, loc, localmap, released_vars, mos) 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) + ffile, fname, handles, loc, localmap, released_vars, mos) body.append(While("?", body_b, line)) elif op == "call": # A call to a CONTRACTED callee (a function/extern whose signature the diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 2df01d1a..6829b9a5 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1411,6 +1411,20 @@ def _sub(source: str | None) -> list[Finding]: gotpr = [(x.component, x.code) for x in pr] fails.append("D5.2 T1: returning a parameter is not `fresh` (no false acquire of " f"the result, no consume of the arg), got {gotpr}") + # the factory acquire must fire inside CONTROL FLOW too: a fresh-returning call in + # an `if` branch whose result is never disposed leaks, exactly like a top-level one. + # (Codex P2: the recursive _lower_flow calls must thread `mos` into nested bodies, + # else the D5.2 acquire is silently skipped in branch/loop bodies.) + checks += 1 + fif = check_facts({"module": "M", "functions": [_MAKE, + {"name": "caller_if", "file": "T1.cs", + "body": [{"op": "if", "line": 9, "then": [ + {"op": "call", "callee": "make", "args": [], "result": "r", "line": 10}], + "else": []}]}]}) + gotfif = [(x.component, x.line, x.code) for x in fif] + if gotfif != [("caller_if", 10, "OWN001")]: + fails.append("D5.2 T1: a fresh factory call inside an `if` branch must also leak " + f"OWN001@10 (mos threaded into nested flow), got {gotfif}") # 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 f85ecea1cdeab22e02ee1d8a5929ca4b93380178 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 11:54:23 +0000 Subject: [PATCH 3/5] fix(d5): don't infer fresh from a mixed-origin return local (CodeRabbit Major) _infer_return_skeleton classified a returned local as fresh whenever it appeared in any acquire, even if the same local is also a call result on another path (if c: x = acquire() else: x = other()). That would make a caller acquire a value it does not own on the non-acquire path, fabricating OWN001/OWN002 there. Require every returned local to be acquired AND not also a call result before claiming fresh; otherwise degrade to no-claim (precision-first). Adds a regression test: a method that acquires x then overwrites it with a non- owned call result and returns it is not fresh, so a caller's dropped result is silent. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- ownlang/ownir.py | 10 ++++++++-- tests/test_ownir.py | 19 +++++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index f7bc5762..f267f99b 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -975,11 +975,17 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton: if not returned: return ReturnSkeleton() # void / no value return acquired = _collect_vars(nodes, "acquire", "var") - if all(v in acquired and v not in param_names for v in returned): + call_results = _call_result_callees(nodes) + # `fresh` only when EVERY returned local is acquired here and *nowhere else*. A local + # that is also a call result on another path is mixed-origin (`if c: x = acquire() + # else: x = other()`) — claiming fresh would make a caller acquire a value it does not + # own on the non-acquire path, fabricating OWN001/OWN002 there. Degrade (CodeRabbit). + if all(v in acquired and v not in param_names and v not in call_results + for v in returned): return ReturnSkeleton("fresh") if len(returned) == 1: (v,) = tuple(returned) - callee = _call_result_callees(nodes).get(v) + callee = call_results.get(v) if callee and v not in param_names and v not in acquired: return ReturnSkeleton("forward", callee=callee) return ReturnSkeleton() # not provably owned -> no claim diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 6829b9a5..ea5be557 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1425,6 +1425,25 @@ def _sub(source: str | None) -> list[Finding]: if gotfif != [("caller_if", 10, "OWN001")]: fails.append("D5.2 T1: a fresh factory call inside an `if` branch must also leak " f"OWN001@10 (mos threaded into nested flow), got {gotfif}") + # PRECISION (CodeRabbit): a returned local that is also a call RESULT is mixed-origin, + # not provably `fresh`. `mixed` acquires x, then overwrites it with `other`'s (non- + # owned) result, and returns it — `returned == acquired == {x}` would wrongly read as + # fresh, so a caller acquiring its dropped result would fabricate OWN001. The result + # must NOT be fresh -> the caller stays silent. + checks += 1 + mxd = check_facts({"module": "M", "functions": [ + {"name": "other", "file": "T1.cs", "body": []}, + {"name": "mixed", "file": "T1.cs", + "body": [{"op": "acquire", "var": "x", "line": 1}, + {"op": "call", "callee": "other", "args": [], "result": "x", "line": 2}, + {"op": "return", "var": "x", "line": 3}]}, + {"name": "caller_mx", "file": "T1.cs", + "body": [{"op": "call", "callee": "mixed", "args": [], "result": "r", + "line": 10}]}]}) + gotmxd = [(x.component, x.code) for x in mxd if x.component == "caller_mx"] + if gotmxd: + fails.append("D5.2 T1: a mixed-origin return (acquired AND a call result) is not " + f"`fresh`, so the caller's dropped result must be silent, got {gotmxd}") # 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 b68c198e23a1ee4f1753af18fa630fa689481c53 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 12:38:07 +0000 Subject: [PATCH 4/5] fix(d5): a non-owned return path blocks the fresh claim (Codex P2) _infer_return_skeleton only collected returns carrying a var, so a method that returns an acquired local on one branch but a bare return (return null / non- owned) on another was still marked fresh -- a caller dropping its result was charged a bogus OWN001 on the null path. Add _has_bare_return: if any return path yields a non-owned value, make no fresh/forward claim (precision-first). Regression test: a method with a return-null branch is not fresh, so a caller's dropped result is silent. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- ownlang/ownir.py | 26 ++++++++++++++++++++++++++ tests/test_ownir.py | 18 ++++++++++++++++++ 2 files changed, 44 insertions(+) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index f267f99b..2848e177 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -929,6 +929,27 @@ def _collect_vars(nodes: Any, op_kind: str, field: str) -> set[str]: return out +def _has_bare_return(nodes: Any) -> bool: + """True if some `return` op carries NO `var` (a bare `return` / `return null` / + a non-local expression) anywhere in the body. Such a path returns a non-owned + value, so the method is not uniformly `fresh` — `_infer_return_skeleton` must not + claim fresh/forward when one exists (P-005 D5.2 precision; Codex).""" + if not isinstance(nodes, list): + return False + for n in nodes: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == "return" and n.get("var") is None: + return True + if op == "if" and (_has_bare_return(n.get("then")) + or _has_bare_return(n.get("else"))): + return True + if op == "while" and _has_bare_return(n.get("body")): + return True + return False + + def _call_result_callees(nodes: Any) -> dict[str, str | None]: """Map each `result` local of a `call` op to the callee that produced it (for forward-return inference, P-005 D5.2). A local bound by two *different* callees @@ -974,6 +995,11 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton: returned = _collect_vars(nodes, "return", "var") if not returned: return ReturnSkeleton() # void / no value return + if _has_bare_return(nodes): + # some normal-return path yields a non-owned value (`return null` / bare + # `return`), so the method is not uniformly fresh — a caller dropping the + # result must not be charged a leak on that path. Make no claim (Codex). + return ReturnSkeleton() acquired = _collect_vars(nodes, "acquire", "var") call_results = _call_result_callees(nodes) # `fresh` only when EVERY returned local is acquired here and *nowhere else*. A local diff --git a/tests/test_ownir.py b/tests/test_ownir.py index ea5be557..18528a54 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1444,6 +1444,24 @@ def _sub(source: str | None) -> list[Finding]: if gotmxd: fails.append("D5.2 T1: a mixed-origin return (acquired AND a call result) is not " f"`fresh`, so the caller's dropped result must be silent, got {gotmxd}") + # PRECISION (Codex): `fresh` requires EVERY return path to be owned. A method that + # returns an acquired local on one branch but a bare `return` (null / non-owned) on + # another is not uniformly fresh — a caller dropping its result must NOT be charged a + # leak on the null path. `maybe_make` must not be fresh -> caller_bare stays silent. + checks += 1 + bare = check_facts({"module": "M", "functions": [ + {"name": "maybe_make", "file": "T1.cs", + "body": [{"op": "if", "line": 1, + "then": [{"op": "acquire", "var": "x", "line": 2}, + {"op": "return", "var": "x", "line": 3}], + "else": [{"op": "return", "line": 4}]}]}, + {"name": "caller_bare", "file": "T1.cs", + "body": [{"op": "call", "callee": "maybe_make", "args": [], "result": "r", + "line": 10}]}]}) + gotbare = [(x.component, x.code) for x in bare if x.component == "caller_bare"] + 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}") # 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 4a879cd16ab8c7dc0bae6bf89b4eca11a6c41af3 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 12:57:57 +0000 Subject: [PATCH 5/5] docs(d5): track branch-scope bridge limitation + lock it with an xfail regression Codex flagged that a local acquired in both if-branches and released after the merge crashes (OWN030 -> OwnIRError). Confirmed pre-existing: it reproduces with a plain acquire, no fresh/factory path, so it is a bridge flat-localmap branch- scope limitation, not a D5.2 regression. Per the decision, land D5.2 as-is and track the bridge fix as its own slice (make acquire lowering branch-aware / hoist synthetic handles to the merge scope) rather than soft-skipping OWN030, which would mask real lowering drift. Records the limitation in the D5 note and adds an xfail-style lock (branch_merge) asserting the current raise, to flip to a clean-balanced-release assertion once the bridge fix lands. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 14 ++++++++++++++ tests/test_ownir.py | 24 ++++++++++++++++++++++++ 2 files changed, 38 insertions(+) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 0dcc9778..24451c6f 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -291,6 +291,20 @@ 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.) - **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/tests/test_ownir.py b/tests/test_ownir.py index 18528a54..00431a26 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1462,6 +1462,30 @@ 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 + try: + 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}]}]}) + 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") # 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