From 932ce2be6dc31a719ca60ca90fb9ac8cf3e43ac4 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 08:37:17 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(d5):=20D5.1a=20=E2=80=94=20first-party?= =?UTF-8?q?=20interprocedural=20ownership=20transfer?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wire the D5.0 solver into the OwnIR bridge so cross-callee ownership transfer is checked compositionally, resolving the give-up that left a forwarded param plain (P-005 D5.1, docs/notes/d5-ownership-transfer.md). ownir.py: - _build_skeletons(): derive a Method Ownership Summary skeleton per functions[] entry, mirroring _infer_param_effect's rel/passed/used priority (release -> dispose, forward -> forward edge, used -> borrow). Non-unique names are dropped (overload keys aren't distinguishable yet -> forward to such a name stays unknown -> silent). - to_module(): solve() once up front (degrades to no-MOS on any error, never crashes the bridge); thread the MOS into _lower_fn_params. - _infer_param_effect() gains forward_transfer: a forwarded param now resolves through the callee's summary (must -> consume, no -> borrow, may/unknown -> plain, precision-first). rel/used/explicit paths are unchanged, so no regression on the non-forward cases. The former 'ambiguous pass-through stays plain' test is replaced by D5.1 tests: a transitive (incl. two-hop) consuming forward now makes a later release/use OWN002, a borrow-only forward stays borrow (no over-consume FP on a later release), and a correctly forwarded handoff that used to read as a false OWN001 is now silent (a precision win). Full suite green (ownir 130/130, all 19 corpus cases unchanged). D5.1b (leaveOpen, a per-call-site contract) is the next, additive slice. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/notes/d5-ownership-transfer.md | 20 +++-- ownlang/ownir.py | 133 ++++++++++++++++++++++++---- tests/test_ownir.py | 68 ++++++++++++-- 3 files changed, 189 insertions(+), 32 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index bec081c5..fe5938d3 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -230,11 +230,21 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa SCC fixpoint, serialize to `summaries[]`. No behaviour change — compute, serialize, and **unit-test the lattice in pure Python** (monotonicity, SCC convergence, cap behaviour). First PR; fully local, no SDK. -- **D5.1 — T2/T3 wiring + a `leaveOpen` Tier-B slice.** Lower inferred `must`/`no` to - `consume`/`borrow`, *and* ship the `leaveOpen` contracts at the same time (cleanest, - best-documented adoption cases — far better regression anchors than first-party-only). - First live catches: double-dispose / use-after across a consuming call; borrow-leak. - CI A/B sample. +- **D5.1a — first-party T2/T3 wiring (shipped).** The OwnIR bridge now derives a + skeleton per `functions[]` entry, runs the D5.0 solver once, and feeds the resolved + transfer into `_infer_param_effect`'s **forwarded** branch — the exact give-up it used + to leave plain. A param forwarded to a consuming callee is inferred `consume`, one + forwarded to a borrow-only callee `borrow`; `may`/`unknown` stay plain (precision-first). + No core change (the existing `lower_call` applies the effects), no extractor change for + first-party. Live catches, proven by synthetic OwnIR tests: double-dispose / use-after + across a *transitive* (multi-hop) consuming call (OWN002), and the precision win where a + correct forwarded handoff that used to read as a false OWN001 leak is now silent. +- **D5.1b — `leaveOpen` Tier-B slice (next).** `StreamReader(stream, leaveOpen:…)` &c. is a + *per-call-site* contract — the same ctor consumes or borrows by the bool literal — so it + needs a per-call effect channel on the `call` op plus the extractor reading the literal, + rather than a per-method summary. Small, additive; pairs with a CI A/B sample on the real + extractor output (the end-to-end validation that first-party `call` ops are emitted for + forwarding chains). - **D5.2 — T1.** `fresh`-returning calls become acquire sites → factory leaks. Includes `out`/`ref`-owned (another `fresh` door) before async. - **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh` diff --git a/ownlang/ownir.py b/ownlang/ownir.py index e7e6f8ff..239d2f08 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -99,6 +99,7 @@ from __future__ import annotations import json +from collections import Counter from dataclasses import dataclass from typing import Any @@ -134,6 +135,13 @@ find_weak_captive_dependencies, ) from .diagnostics import TITLES, Severity +from .ownership import ( + MethodSkeleton, + ParamSkeleton, + PathAction, + Transfer, + solve, +) # The OwnIR schema version this core understands. Bump it whenever the fact # vocabulary changes incompatibly; the extractor stamps the same number so a @@ -804,6 +812,14 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] loc = [0] raw_fns = facts.get("functions", []) if isinstance(raw_fns, list): + # D5.1: resolve interprocedural ownership transfer once, up front, so a + # forwarded `consume`/`borrow` param is checked compositionally (the give-up + # case `_infer_param_effect` used to leave plain). Never let summary + # computation crash the bridge — degrade to no-MOS (the old behaviour). + try: + mos: dict[str, Any] = solve(_build_skeletons(raw_fns)) + except Exception: + mos = {} for fn in raw_fns: if not isinstance(fn, dict): continue @@ -819,7 +835,7 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] # uses/releases and call arguments resolve to them), then the flow body. localmap: dict[str, str] = {} fparams = _lower_fn_params(fn, ffile, fname, handles, loc, localmap, - released) + released, mos) fbody = _lower_flow(nodes, ffile, fname, handles, loc, localmap, released) # A body that returns a value gets an owned return type, so the core @@ -926,25 +942,97 @@ def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]: return rel, passed, used -def _infer_param_effect(pname: str, nodes: Any) -> str | None: - """Infer a parameter's ownership CONTRACT from the callee's OWN body — the v1 +def _forward_targets(pname: str, nodes: Any) -> list[tuple[str, int]]: + """Every `(callee, arg_index)` a `call` op hands `pname` to, recursing into + if/while branches. The argument *position* is the callee's parameter index — + what `solve()` resolves against the callee's summary (P-005 D5.1).""" + out: list[tuple[str, int]] = [] + if not isinstance(nodes, list): + return out + for n in nodes: + if not isinstance(n, dict): + continue + op = n.get("op") + if op == "call": + callee = str(n.get("callee", "")) + args = n.get("args", []) + if callee and isinstance(args, list): + for j, a in enumerate(args): + if str(a) == pname: + out.append((callee, j)) + elif op in ("if", "while"): + subs = ([n.get("then"), n.get("else")] if op == "if" else [n.get("body")]) + for sub in subs: + out.extend(_forward_targets(pname, sub)) + return out + + +def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: + """Derive a Method Ownership Summary skeleton per first-party function from its + flow body, for the D5.0 solver (P-005 D5.1). A parameter's path actions mirror + the same priority `_infer_param_effect` uses — a release is a `dispose`, a + forward to another call is a `forward` edge the solver resolves, an + otherwise-used param is a `borrow` — so the solved transfer lines up with the + bridge's local inference on the non-forward cases and only *resolves* the + forwarded one. 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).""" + counts = Counter(str(fn.get("name", "")) for fn in raw_fns if isinstance(fn, dict)) + skels: list[MethodSkeleton] = [] + for fn in raw_fns: + if not isinstance(fn, dict): + continue + key = str(fn.get("name", "")) + if not key or counts[key] != 1: + continue + body = fn.get("body", []) + body = body if isinstance(body, list) else [] + raw_params = fn.get("params", []) + raw_params = raw_params if isinstance(raw_params, list) else [] + params: list[ParamSkeleton] = [] + for i, p in enumerate(raw_params): + if not isinstance(p, dict): + continue + cname = str(p.get("name", "?")) + rel, passed, used = _param_signals(cname, body) + if rel: + paths: tuple[PathAction, ...] = (PathAction("dispose"),) + elif passed: + paths = tuple(PathAction("forward", c, j) + for c, j in _forward_targets(cname, body)) + elif used: + paths = (PathAction("borrow"),) + else: + paths = () + params.append(ParamSkeleton(i, cname, True, paths)) + skels.append(MethodSkeleton(key, tuple(params))) + return skels + + +def _infer_param_effect(pname: str, nodes: Any, + forward_transfer: Transfer | None = None) -> str | None: + """Infer a parameter's ownership CONTRACT from the callee's OWN body — the bounded inter-procedural step that lets first-party C# be checked without - annotating every method. A param the body discharges or lets escape - (release) is CONSUME (ownership taken and discharged); one only read and - retained is a BORROW (the caller keeps ownership, must still release). A param - handed to another call is genuinely ambiguous without that callee's contract, - so we do NOT infer it (it stays plain / awaiting an annotation or a later - transitive pass). We deliberately do NOT treat `return ` as a consume - signal: the bridge does not yet model returned (owned) VALUES, so a returned - param is consume-and-handed-back, not a plain consume. Inference fires only on - the unambiguous signals, so it never - upgrades a borrow to a consume (or vice-versa) on a guess — an explicit - `effect` in the fact always wins over inference.""" + annotating every method. A param the body discharges (release) is CONSUME + (ownership taken and discharged); one only read and retained is a BORROW (the + caller keeps ownership, must still release). A param handed to another call + used to be ambiguous and stay plain; **P-005 D5.1** resolves it through the + call graph: `forward_transfer` is the solved transfer of that param (must → + CONSUME, no → BORROW, may/unknown → stay plain, precision-first). We + deliberately do NOT treat `return ` as a consume signal: the bridge + does not yet model returned (owned) VALUES, so a returned param is + consume-and-handed-back, not a plain consume. Inference never upgrades a + borrow to a consume (or vice-versa) on a guess — an explicit `effect` in the + fact always wins over inference.""" rel, passed, used = _param_signals(pname, nodes) if rel: return "consume" if passed: - return None + if forward_transfer == Transfer.MUST: + return "consume" + if forward_transfer == Transfer.NO: + return "borrow" + return None # may / unknown / unresolved -> plain (precision-first) if used: return "borrow" return None @@ -953,7 +1041,8 @@ def _infer_param_effect(pname: str, nodes: Any) -> str | None: def _lower_fn_params(fn: dict[str, Any], ffile: str, fname: str, handles: dict[str, dict[str, Any]], loc: list[int], localmap: dict[str, str], - released_vars: set[str]) -> list[Param]: + released_vars: set[str], + mos: dict[str, Any] | None = None) -> list[Param]: """Lower a function's declared ownership parameters into core Params. Each gets a globally-unique synthetic symbol (`parg_`) so a finding maps back to its C# location; `localmap` resolves later references (and call arguments) by @@ -965,13 +1054,21 @@ def _lower_fn_params(fn: dict[str, Any], ffile: str, fname: str, raw = fn.get("params", []) if not isinstance(raw, list): return out - for p in raw: + summ = mos.get(fname) if mos is not None else None + for i, p in enumerate(raw): if not isinstance(p, dict): continue cname = str(p.get("name", "?")) eff = p.get("effect") if not isinstance(eff, str): - eff = _infer_param_effect(cname, fn.get("body", [])) # contract inference + # D5.1: when the contract is inferred, resolve a *forwarded* param's + # transfer through the call graph (the solved MOS for this method). + ftrans = None + if summ is not None: + ps = next((q for q in summ.params if q.index == i), None) + if ps is not None: + ftrans = ps.transfer + eff = _infer_param_effect(cname, fn.get("body", []), ftrans) tref = _PARAM_EFFECT_TYPE.get(eff) if isinstance(eff, str) else None if tref is None: tref = TypeRef("int", False, False) # a plain (non-owned) parameter diff --git a/tests/test_ownir.py b/tests/test_ownir.py index fe8f3b83..784e5745 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1146,24 +1146,74 @@ def _sub(source: str | None) -> list[Finding]: if rf: fails.append(f"a value-bearing return should be a clean escape (no crash, no " f"false leak), got {[(x.component, x.code) for x in rf]}") - # regression (CodeRabbit review): a param ONLY forwarded to another call is - # ambiguous without that callee's contract, so it is NOT inferred (stays plain) - # -- the v1 boundary. The forwarding fn and its caller stay silent (no false - # positive, no crash); transitive inference is the follow-up that resolves it. - checks += 1 - amb = check_facts({"module": "M", "functions": [ + # --- P-005 D5.1: TRANSITIVE ownership transfer. A param ONLY forwarded to + # another call used to stay plain (the v1 give-up); the interprocedural + # summary solver (ownlang/ownership.py) now resolves it through the callee's + # contract. `forward(s)` hands s to `sink(consume)`, so forward's own param + # is inferred CONSUME — the give-up that `_infer_param_effect` left plain. + _FWD = [ {"name": "forward", "file": "F.cs", "params": [{"name": "s", "line": 1}], "body": [{"op": "call", "callee": "sink", "args": ["s"], "line": 2}]}, {"name": "sink", "file": "F.cs", "params": [{"name": "x", "effect": "consume", "line": 5}], "body": [{"op": "release", "var": "x", "line": 6}]}, + ] + # a caller that releases s AFTER forwarding double-discharges it: the obligation + # already moved to `sink` through `forward`, so the later release is OWN002. + checks += 1 + d51 = check_facts({"module": "M", "functions": _FWD + [ {"name": "caller", "file": "F.cs", "body": [{"op": "acquire", "var": "s", "line": 10}, {"op": "call", "callee": "forward", "args": ["s"], "line": 11}, {"op": "release", "var": "s", "line": 12}]}]}) - if amb: - fails.append(f"an ambiguous pass-through param must not be inferred, crash, " - f"or false-positive, got {[(x.component, x.code) for x in amb]}") + if [(x.component, x.line, x.code) for x in d51] != [("caller", 10, "OWN002")]: + fails.append("D5.1 transitive consume: releasing after a forwarded handoff " + f"must be OWN002@10 (anchored at the acquire), got {[(x.component, x.line, x.code) for x in d51]}") + # the correct handoff (forward and let go) is SILENT — and this is a precision + # WIN: before D5.1 forward's param was plain, so the caller's acquired-but-never- + # released s read as a false OWN001 leak; now the obligation provably moved. + checks += 1 + ok51 = check_facts({"module": "M", "functions": _FWD + [ + {"name": "caller_ok", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 20}, + {"op": "call", "callee": "forward", "args": ["s"], "line": 21}]}]}) + if ok51: + fails.append("a correctly forwarded handoff must be silent (obligation moved " + f"to sink), got {[(x.component, x.code) for x in ok51]}") + # two hops: outer -> mid -> sink(consume). The chain resolves within the depth + # cap, so a caller using s after forwarding to `outer` is use-after-handoff. + checks += 1 + twohop = check_facts({"module": "M", "functions": [ + {"name": "outer", "file": "F.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "mid", "args": ["s"], "line": 2}]}, + {"name": "mid", "file": "F.cs", "params": [{"name": "s", "line": 5}], + "body": [{"op": "call", "callee": "sink2", "args": ["s"], "line": 6}]}, + {"name": "sink2", "file": "F.cs", + "params": [{"name": "x", "effect": "consume", "line": 9}], + "body": [{"op": "release", "var": "x", "line": 10}]}, + {"name": "user", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 15}, + {"op": "call", "callee": "outer", "args": ["s"], "line": 16}, + {"op": "use", "var": "s", "line": 17}]}]}) + if [(x.component, x.line, x.code) for x in twohop] != [("user", 15, "OWN002")]: + fails.append("D5.1 two-hop transitive consume should be OWN002@user:15 (anchored at the acquire), got " + f"{[(x.component, x.line, x.code) for x in twohop]}") + # a param forwarded to a BORROW-only callee resolves to borrow (not consume): + # the caller keeps ownership, so forwarding then RELEASING is clean — proving we + # never over-consume a forwarded borrow (which would false-positive the release). + checks += 1 + bok = check_facts({"module": "M", "functions": [ + {"name": "peek_fwd", "file": "F.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "peek2", "args": ["s"], "line": 2}]}, + {"name": "peek2", "file": "F.cs", "params": [{"name": "x", "line": 5}], + "body": [{"op": "use", "var": "x", "line": 6}]}, + {"name": "keep_ok", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "peek_fwd", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]}) + if bok: + fails.append("forwarding to a borrow-only callee then releasing must be clean " + f"(no over-consume), got {[(x.component, x.code) for x in bok]}") # 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 6f3a89757f5584f4232dfb28274e9c3fbac6e5cd Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 08:39:48 +0000 Subject: [PATCH 2/3] style(d5): fix ruff E501/RUF005 in the D5.1 tests Lint-only: wrap two long assertion messages (extract the got-list into a var) and use [*_FWD, ...] unpacking instead of _FWD + [...]. No behaviour change; ownir 130/130. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- tests/test_ownir.py | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 784e5745..b0e73bee 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1161,19 +1161,20 @@ def _sub(source: str | None) -> list[Finding]: # a caller that releases s AFTER forwarding double-discharges it: the obligation # already moved to `sink` through `forward`, so the later release is OWN002. checks += 1 - d51 = check_facts({"module": "M", "functions": _FWD + [ + d51 = check_facts({"module": "M", "functions": [*_FWD, {"name": "caller", "file": "F.cs", "body": [{"op": "acquire", "var": "s", "line": 10}, {"op": "call", "callee": "forward", "args": ["s"], "line": 11}, {"op": "release", "var": "s", "line": 12}]}]}) - if [(x.component, x.line, x.code) for x in d51] != [("caller", 10, "OWN002")]: - fails.append("D5.1 transitive consume: releasing after a forwarded handoff " - f"must be OWN002@10 (anchored at the acquire), got {[(x.component, x.line, x.code) for x in d51]}") + got51 = [(x.component, x.line, x.code) for x in d51] + if got51 != [("caller", 10, "OWN002")]: + fails.append("D5.1 transitive consume: release after handoff must be " + f"OWN002@10 (anchored at acquire), got {got51}") # the correct handoff (forward and let go) is SILENT — and this is a precision # WIN: before D5.1 forward's param was plain, so the caller's acquired-but-never- # released s read as a false OWN001 leak; now the obligation provably moved. checks += 1 - ok51 = check_facts({"module": "M", "functions": _FWD + [ + ok51 = check_facts({"module": "M", "functions": [*_FWD, {"name": "caller_ok", "file": "F.cs", "body": [{"op": "acquire", "var": "s", "line": 20}, {"op": "call", "callee": "forward", "args": ["s"], "line": 21}]}]}) @@ -1195,9 +1196,10 @@ def _sub(source: str | None) -> list[Finding]: "body": [{"op": "acquire", "var": "s", "line": 15}, {"op": "call", "callee": "outer", "args": ["s"], "line": 16}, {"op": "use", "var": "s", "line": 17}]}]}) - if [(x.component, x.line, x.code) for x in twohop] != [("user", 15, "OWN002")]: - fails.append("D5.1 two-hop transitive consume should be OWN002@user:15 (anchored at the acquire), got " - f"{[(x.component, x.line, x.code) for x in twohop]}") + got2h = [(x.component, x.line, x.code) for x in twohop] + if got2h != [("user", 15, "OWN002")]: + fails.append("D5.1 two-hop transitive consume should be " + f"OWN002@user:15 (anchored at acquire), got {got2h}") # a param forwarded to a BORROW-only callee resolves to borrow (not consume): # the caller keeps ownership, so forwarding then RELEASING is clean — proving we # never over-consume a forwarded borrow (which would false-positive the release). From 5b3fa8a49c7db4cf8fa4570ba362eccb26e67920 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 09:04:35 +0000 Subject: [PATCH 3/3] fix(d5): honor explicit effects + don't flatten conditional forwards (Codex + CodeRabbit) Two precision bugs in the D5.1 skeleton derivation, both flagged in review: - Explicit param effects were ignored: _build_skeletons derived transfer only from body signals, so a contract-only (no release in body) resolved as , and a forwarder became -> false OWN001 instead of the handoff. Explicit effects now seed the skeleton (consume->dispose, borrow->borrow, other->non-owning), matching the documented override semantics. - Conditional/looped forwards were flattened to : a param forwarded only inside an if/while recorded just the forward edge, so solve() returned must (not may), upgrading callers to consume and fabricating OWN002/OWN001. A forward is now resolved only when it is a single, unconditional, straight-line handoff; any conditional / looped / multi-target forward also emits a non-transfer path so the lattice yields may/no (caller stays plain) -- precision-first, never a false must. (_forward_targets gains a recurse flag to tell top-level from nested forwards.) Two regression tests added (explicit-effect seed resolves a forwarder; conditional forward stays silent for a caller that releases after). ownir 132/132, full suite green. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- ownlang/ownir.py | 63 +++++++++++++++++++++++++++++++++------------ tests/test_ownir.py | 38 +++++++++++++++++++++++++++ 2 files changed, 85 insertions(+), 16 deletions(-) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 239d2f08..4fccd361 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -942,10 +942,13 @@ def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]: return rel, passed, used -def _forward_targets(pname: str, nodes: Any) -> list[tuple[str, int]]: - """Every `(callee, arg_index)` a `call` op hands `pname` to, recursing into - if/while branches. The argument *position* is the callee's parameter index — - what `solve()` resolves against the callee's summary (P-005 D5.1).""" +def _forward_targets(pname: str, nodes: Any, + recurse: bool = True) -> list[tuple[str, int]]: + """Every `(callee, arg_index)` a `call` op hands `pname` to. The argument + *position* is the callee's parameter index — what `solve()` resolves against + the callee's summary (P-005 D5.1). With `recurse=False`, only top-level + (straight-line) calls are counted, so a conditional/looped forward can be told + apart from an unconditional one.""" out: list[tuple[str, int]] = [] if not isinstance(nodes, list): return out @@ -960,7 +963,7 @@ def _forward_targets(pname: str, nodes: Any) -> list[tuple[str, int]]: for j, a in enumerate(args): if str(a) == pname: out.append((callee, j)) - elif op in ("if", "while"): + elif op in ("if", "while") and recurse: subs = ([n.get("then"), n.get("else")] if op == "if" else [n.get("body")]) for sub in subs: out.extend(_forward_targets(pname, sub)) @@ -974,9 +977,22 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: forward to another call is a `forward` edge the solver resolves, an otherwise-used param is a `borrow` — so the solved transfer lines up with the bridge's local inference on the non-forward cases and only *resolves* the - forwarded one. 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).""" + forwarded one. + + Two precision rules keep `solve()` from ever inferring a false `must` (which + would upgrade a caller to `consume` and fabricate OWN002/OWN001): + - an **explicit** `effect` seeds the skeleton (it is a documented override — + `consume`→`dispose`, `borrow`/`borrow_mut`→`borrow`, anything else owns + nothing), so a contract-only callee resolves correctly even with no body; + - a forward is resolved only when it is a **single, unconditional, + straight-line** handoff. A conditional / looped / multi-target forward also + emits a non-transfer (`borrow`) path, so the lattice yields `may`/`no` + (→ the caller stays plain), never a flattened `must`. Per-path structure is + not modelled here — D5.1 deliberately under-claims rather than guess. + + 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).""" counts = Counter(str(fn.get("name", "")) for fn in raw_fns if isinstance(fn, dict)) skels: list[MethodSkeleton] = [] for fn in raw_fns: @@ -994,16 +1010,31 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: if not isinstance(p, dict): continue cname = str(p.get("name", "?")) - rel, passed, used = _param_signals(cname, body) - if rel: - paths: tuple[PathAction, ...] = (PathAction("dispose"),) - elif passed: - paths = tuple(PathAction("forward", c, j) - for c, j in _forward_targets(cname, body)) - elif used: + eff = p.get("effect") + paths: tuple[PathAction, ...] + if eff == "consume": + paths = (PathAction("dispose"),) # explicit override + elif eff in ("borrow", "borrow_mut"): paths = (PathAction("borrow"),) + elif isinstance(eff, str): + paths = () # explicit non-owning else: - paths = () + rel, passed, used = _param_signals(cname, body) + if rel: + paths = (PathAction("dispose"),) + elif passed: + allt = _forward_targets(cname, body) + top = _forward_targets(cname, body, recurse=False) + paths = tuple(PathAction("forward", c, j) for c, j in allt) + if not (len(allt) == 1 and len(top) == 1): + # not a single unconditional handoff: a no-transfer path + # exists (other branch / zero-trip loop / sibling call), so + # the join is `may`/`no`, never a false `must`. + paths = (*paths, PathAction("borrow")) + elif used: + paths = (PathAction("borrow"),) + else: + paths = () params.append(ParamSkeleton(i, cname, True, paths)) skels.append(MethodSkeleton(key, tuple(params))) return skels diff --git a/tests/test_ownir.py b/tests/test_ownir.py index b0e73bee..68a592b2 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1216,6 +1216,44 @@ def _sub(source: str | None) -> list[Finding]: if bok: fails.append("forwarding to a borrow-only callee then releasing must be clean " f"(no over-consume), got {[(x.component, x.code) for x in bok]}") + # (Codex P2) an EXPLICIT effect seeds the skeleton even with no body evidence: a + # contract-only `sink_c(x consume)` resolves `must`, so the forwarder `fwd_c` is + # consume and a caller using s after the handoff is OWN002. (sink_c itself leaks + # OWN001 — an undischarged consume obligation — which is the expected existing + # behaviour, included here so the assertion is exact.) + checks += 1 + expl = check_facts({"module": "M", "functions": [ + {"name": "fwd_c", "file": "F.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "sink_c", "args": ["s"], "line": 2}]}, + {"name": "sink_c", "file": "F.cs", + "params": [{"name": "x", "effect": "consume", "line": 5}], "body": []}, + {"name": "use_c", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "fwd_c", "args": ["s"], "line": 11}, + {"op": "use", "var": "s", "line": 12}]}]}) + gotx = sorted((x.component, x.code) for x in expl) + if gotx != [("sink_c", "OWN001"), ("use_c", "OWN002")]: + fails.append(f"D5.1 explicit-effect seed should resolve through a " + f"forwarder (use_c OWN002), got {gotx}") + # (Codex P2 / CodeRabbit) a CONDITIONAL forward must resolve to `may`, not `must`: + # `maybe(s){ if(c) sink(s); }` consumes s on only one path, so a caller that uses s + # after `maybe(s)` must stay SILENT (no false OWN002 on the non-forward path). + checks += 1 + cond = check_facts({"module": "M", "functions": [ + {"name": "maybe", "file": "F.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "if", "then": [ + {"op": "call", "callee": "sink", "args": ["s"], "line": 3}], "else": [], + "line": 2}]}, + {"name": "sink", "file": "F.cs", + "params": [{"name": "x", "effect": "consume", "line": 6}], + "body": [{"op": "release", "var": "x", "line": 7}]}, + {"name": "user_c", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "maybe", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]}) + if cond: + gotc = [(x.component, x.code) for x in cond] + fails.append(f"D5.1 conditional forward must be `may`: caller stays silent, got {gotc}") # 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