diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 7a7939ea..b8999982 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -150,17 +150,35 @@ policy — see §5. ## 4. The fixpoint (the interprocedural pass) -- Build a call graph over first-party methods. -- A method's summary depends on the summaries of methods it forwards a param to / returns - the result of. Compute **bottom-up** with a worklist; iterate SCCs (recursion / - mutual recursion) to a fixpoint on the small lattice. +> **Implemented** in `ownlang/ownership.py` (`solve` / `solve_with_log`). This is the +> shipped algorithm; an earlier slice used a depth-capped recursive descent, which the +> SCC condensation below replaced (it removed both the exponential the cap was guarding +> against *and* the cap-induced false `unknown`s on deep chains). + +- Build a call graph over first-party methods (an edge `M → C` for every callee `C` whose + summary `M`'s summary reads: a forwarded param, or a forwarded return). +- **Condense into SCCs** (iterative Tarjan, emitted bottom-up = reverse-topological) and + process components in that order. The summary is **context-insensitive** — one MOS per + method, independent of caller or depth — so a callee is resolved **once** and reused + (the summary *is* the memoization; only same-SCC callees are still mid-iteration). +- **Param transfers**: within a component, seed each `(method, param)` at the lattice + **bottom** (⊥, "no evidence yet") and iterate the transfer equations to their **least + fixpoint** on the small lattice; a residual ⊥ finalizes as `no`. Seeding at ⊥ (not a + spurious `no`) is what makes recursion *exact*: a method that disposes on its base case + and recurses otherwise resolves to `must` (every *terminating* path disposes), and + mutual recursion grounded by a dispose carries that `must` across the whole SCC, while + recursion that never disposes settles at `no`. +- **Returns**: a single forward target per return ⇒ an **iterative** (not recursive), + memoized, cycle-safe chase along forward-return edges (a return-forward cycle → `unknown`). + Iterative so a deep but acyclic wrapper chain cannot overflow the stack. - **Lattice monotonicity is biased toward precision** (§5): uncertainty resolves toward - "caller does not own". -- **Cap the work.** Default interprocedural chain depth **3** (matching CA2000's - `max_interprocedural_method_call_chain` default); configurable. On cap, emit `unknown` - (→ silent) and **log the cap** — no silent truncation (project discipline). -- The domain is intentionally tiny (4 transfer values × 1 escape bit × 4 return values), - so a bottom-up summary pass stays practical even on large graphs. + "caller does not own". The **only** `unknown` the log surfaces is an extern + (unsummarized) callee boundary — `solve_with_log` returns those, sorted; other + `unknown`s (return-forward cycle, un-remappable `aliasOf`, missing/unrecognised shape) + are intrinsic precision-safe degradations, deterministic from the input, not logged. +- **No depth cap.** The condensation bounds the work (each method resolved once; the + domain is tiny — 4 transfer values × 1 escape bit × 4 return values), so the pass stays + linear on large graphs without truncating deep chains. --- @@ -228,8 +246,8 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa - **D5.0 — infra.** MOS dataclass (two-axis), first-party call graph, bottom-up 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. + and **unit-test the lattice in pure Python** (monotonicity, SCC convergence, deep-chain + termination, extern-boundary logging). First PR; fully local, no SDK. - **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 @@ -301,7 +319,8 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa method returning an owned `IDisposable` — emits a `call callee=… result=r` op (the core mints the acquire only when it proves the callee `fresh`, so a non-fresh call is never falsely owned). `IsFirstPartyDisposableFactory` gates on a source-declared, non-void, disposable, non-dispose- - optional return; overloads (non-unique names) resolve to `unknown` and stay silent. Validated + optional return; same-name overloads are merged into one conservative summary (§10 q2) — + classified `fresh` only when **every** overload returns fresh, else silent. Validated end-to-end by `FactoryLeakSample.cs` in CI: a dropped factory result leaks **interprocedurally** (OWN001 at the call site — beyond the flat detectors), while the disposed caller and the factory itself stay silent. **Remaining T1 door:** `out`/`ref`-owned parameters (another `fresh` source) @@ -444,7 +463,8 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa *release operation*, not the *transfer shape*. - Summaries are may/must per the lattice, biased to precision — not a proof of disposal on *every* path beyond what `--flow-locals` already does. -- Cap the fixpoint; log caps. +- No depth cap: the SCC condensation bounds the work (§4); the only logged residual is an + extern-boundary forward (`solve_with_log`). --- @@ -452,8 +472,15 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa 1. ~~`aliasOf` in the core: shared resource id vs a synthetic discharge edge.~~ **Resolved → §11 (the obligation-identity model): Variant B, a shared RID / alias-set.** -2. Signature-key canonicalisation across overloads / generics / partial classes (the - `method` key must be stable and collision-free). +2. ~~Signature-key canonicalisation across overloads / generics / partial classes (the + `method` key must be stable and collision-free).~~ **Partially addressed:** the call + node names its callee `{Type}.{Method}` with no parameter signature, so a true + signature key is not reconstructable core-side. Instead, same-name overloads are + **merged into one conservative summary** (`_merge_skeletons` in `ownir.py`): a join at + (name, parameter-index) granularity — `must` only when every overload consumes that + index, `fresh` only when all agree — never a fabricated `must`/`fresh`. **Residual:** + argument-type / per-arity disambiguation would need call-site type info the fact stream + does not carry (arity is available but not yet modelled). 3. Whether `escape-without-transfer` ever deserves its own advisory (e.g. "stored in a non-owning field — who owns this?") or stays silent. (Start silent.) diff --git a/ownlang/ownership.py b/ownlang/ownership.py index 1908ae04..0bb3bbb3 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -110,7 +110,10 @@ class ReturnSkeleton: @dataclass(frozen=True) class MethodSkeleton: - key: str # canonical signature key (stable, collision-free — open question 2) + key: str # method identity the call graph resolves on. NOT a full signature key: the + # extractor names a callee `{Type}.{Method}` with no parameter signature, so + # same-name overloads share a key and are merged conservatively before solving + # (`_merge_skeletons` in ownir.py — note's open question 2, partially addressed). params: tuple[ParamSkeleton, ...] = () ret: ReturnSkeleton = field(default_factory=ReturnSkeleton) file: str = "?" diff --git a/ownlang/ownir.py b/ownlang/ownir.py index d9bf1781..5d99b4b1 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -870,13 +870,21 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] mos: dict[str, Any] = solve(_build_skeletons(raw_fns)) except Exception: mos = {} - # every first-party method name (including overloaded ones dropped from `mos`): the - # Tier B BCL table must never fire for a callee we compiled from source — Tier A is - # authoritative even with no usable summary (CodeRabbit). Threaded into the freshness - # checks so direct calls agree with the wrapper-return path in `_infer_return_skeleton`. - first_party = frozenset( - _canonical_callee_name(str(fn.get("name", ""))) for fn in raw_fns - if isinstance(fn, dict) and fn.get("name")) + # every first-party method name: the Tier B BCL table must never fire for a callee we + # compiled from source — Tier A is authoritative even with no usable summary + # (CodeRabbit). Threaded into the freshness checks so direct calls agree with the + # wrapper-return path in `_infer_return_skeleton`. + fp_names = [str(fn.get("name", "")) for fn in raw_fns + if isinstance(fn, dict) and fn.get("name")] + first_party = frozenset(_canonical_callee_name(n) for n in fp_names) + # Names defined more than once are OVERLOADS. Their merged MOS summary is conservative, + # but the core's call-signature table keeps only ONE same-name FnDecl (last-wins), so a + # DIRECT `Call` to an overloaded name would mis-apply one overload's effects. Route those + # args through the merged contract instead (see the `call` handler in `_lower_flow`). + # Keyed on the CANONICAL name (like `first_party`), so a `global::`-qualified direct call + # to an overloaded method still matches (CodeRabbit). + overloaded = frozenset( + n for n, c in Counter(_canonical_callee_name(x) for x in fp_names).items() if c > 1) for fn in raw_fns: if not isinstance(fn, dict): continue @@ -910,7 +918,7 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] hoisted_lets.append(Let(hh, Acquire("Disposable", [], hline), hline)) fbody = [*hoisted_lets, *_lower_flow(nodes, ffile, fname, handles, loc, localmap, - released, mos, set(hoist), first_party)] + released, mos, set(hoist), first_party, overloaded)] # 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 @@ -1146,6 +1154,11 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str], # full exclusivity through `lower_call`. Kept in sync with `_OWNERSHIP_SINK_EXTERNS`. _SINK_PATH_ACTION = {"$consume": "dispose", "$borrow": "borrow"} +# A merged-overload transfer → the sink-extern channel that applies it at a DIRECT call +# site (so an overloaded name uses its conservative MOS contract, not the core's last-wins +# signature). `may`/`unknown` map to nothing (plain) — precision-first, never a guess. +_CHANNEL_FOR_TRANSFER = {Transfer.MUST: "$consume", Transfer.NO: "$borrow"} + # Tier B (P-005 D5.3 / P1a contracts): a curated table of well-known BCL *factories* whose # return the caller OWNS — the producer half of the boundary contract (the consume/borrow @@ -1296,6 +1309,49 @@ def _forward_path_action(callee: str, arg: int) -> PathAction: return PathAction("forward", callee, arg) +def _merge_returns(rets: list[ReturnSkeleton]) -> ReturnSkeleton: + """The conservative return of a set of same-name overloads. Only a kind ALL + overloads agree on survives (so a call to the name returns it regardless of which + overload bound); a `forward`, an `aliasOf` (whose index is overload-specific), or + any disagreement degrades to a no-op `unknown` return — never a fabricated `fresh` + (which would mint a phantom acquire at the caller).""" + kinds = {r.kind for r in rets} + if kinds == {"fresh"}: + return ReturnSkeleton("fresh") + if kinds == {"none"}: + return ReturnSkeleton("none") + if kinds == {"aliased"}: + return ReturnSkeleton("aliased") + return ReturnSkeleton("unknown") # mixed / forward / aliasOf -> fails closed + + +def _merge_skeletons(group: list[MethodSkeleton]) -> MethodSkeleton: + """Collapse same-name overloads into ONE conservative summary. The extractor + names a call's callee `{Type}.{Method}` with no parameter signature (note's open + question 2), so a forward to an overloaded name cannot pick an overload. Rather + than drop them all (every such forward then stays `unknown`), join them on the + lattice at (name, parameter-index) granularity: a parameter transfers `must` only + when EVERY overload carrying that index consumes it, and an overload that merely + keeps an index contributes a `borrow` path so the join can never fabricate a + `must`. Disambiguating by argument type would need call-site type info the fact + stream does not carry; arity is available but not modelled here (the join is + already precision-safe, just coarser than a per-arity split would be).""" + if len(group) == 1: + return group[0] + by_index: dict[int, list[PathAction]] = {} + names: dict[int, str] = {} + for sk in group: + for p in sk.params: + # an overload that does nothing with this index KEEPS it (= `no`); record + # that as a borrow path so it joins in rather than vanishing from concat. + by_index.setdefault(p.index, []).extend(p.paths or (PathAction("borrow"),)) + names.setdefault(p.index, p.name) + params = tuple( + ParamSkeleton(i, names[i], True, tuple(by_index[i])) for i in sorted(by_index) + ) + return MethodSkeleton(group[0].key, params, _merge_returns([sk.ret for sk in group])) + + 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 @@ -1320,21 +1376,23 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: 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).""" + Same-name overloads are MERGED into one conservative summary (`_merge_skeletons`) + rather than dropped: the call node names its callee without a parameter signature + (note's open question 2), so a forward to an overloaded name cannot pick an + overload, but a lattice join over the overloads still resolves it precision-safely + (and lets a uniformly-`fresh` overloaded factory be seen as fresh).""" counts = Counter(str(fn.get("name", "")) for fn in raw_fns if isinstance(fn, dict)) - # every first-party method name (even overloaded/dropped ones): the BCL fresh-factory - # table must NOT apply to a call whose target we compile from source — Tier A (the + # every first-party method name (even overloaded ones): the BCL fresh-factory table + # must NOT apply to a call whose target we compile from source — Tier A (the # first-party summary) authoritatively overrides Tier B (the curated BCL table) even # when the source method happens to share a BCL factory's name (Codex P2). first_party = frozenset(_canonical_callee_name(k) for k in counts if k) - skels: list[MethodSkeleton] = [] + by_key: dict[str, 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: + if not key: continue body = fn.get("body", []) body = body if isinstance(body, list) else [] @@ -1373,8 +1431,10 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: params.append(ParamSkeleton(i, cname, True, paths)) pnames = {str(p.get("name", "")) for p in raw_params if isinstance(p, dict)} ret = _infer_return_skeleton(body, pnames, first_party) - skels.append(MethodSkeleton(key, tuple(params), ret)) - return skels + by_key.setdefault(key, []).append(MethodSkeleton(key, tuple(params), ret)) + # one skeleton per name: solve() keys by name (a forward names its callee with no + # signature), so same-name overloads are joined into a single conservative summary. + return [_merge_skeletons(group) for group in by_key.values()] def _infer_param_effect(pname: str, nodes: Any, @@ -1592,7 +1652,8 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, released_vars: set[str], mos: dict[str, Any] | None = None, hoisted: set[str] | None = None, - first_party: frozenset[str] = frozenset()) -> list[Stmt]: + first_party: frozenset[str] = frozenset(), + overloaded: frozenset[str] = frozenset()) -> 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 @@ -1684,16 +1745,16 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, en = n.get("else", []) then_b = _lower_flow(tn if isinstance(tn, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party) + first_party, overloaded) else_b = _lower_flow(en if isinstance(en, list) else [], ffile, fname, handles, loc, localmap, released_vars, mos, hoisted, - first_party) + first_party, overloaded) 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, hoisted, - first_party) + first_party, overloaded) body.append(While("?", body_b, line)) elif op == "call": # A call to a CONTRACTED callee (a function/extern whose signature the @@ -1705,14 +1766,35 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, # `localmap`; an uncontracted call is simply not emitted by the # extractor (it is an escape, surfaced separately). callee = str(n.get("callee", "")) + identity = _canonical_callee_name(callee) raw_args = n.get("args", []) summ = mos.get(callee) if (mos is not None and callee) else None + # The merged summary, resolving a `global::`-qualified call to its bare key (like + # `_callee_returns_fresh`). Used only by the overload channel below; the direct-`Call` + # path stays on the raw `summ` so it never names a callee absent from the core + # signature table (which would raise OWN040). + merged = summ if summ is not None else ( + mos.get(identity) if (mos is not None and identity != callee) else None) + if identity in overloaded and merged is not None and isinstance(raw_args, list): + # OVERLOADED name: do NOT emit a `Call` resolved against the core's last-wins + # signature table (it stores one same-name FnDecl, so it would mis-apply one + # overload's effect — a false OWN002 when overloads disagree). Apply the MERGED + # MOS contract per argument through the `$consume`/`$borrow` channel instead, + # exactly as a FORWARD to this name resolves (`must`→consume, `no`→borrow, + # `may`/`unknown`→plain). The channel emits sink externs (never the callee name), + # so a qualified callee is safe here. (Codex P2 / CodeRabbit.) + for j, a in enumerate(raw_args): + ps = next((q for q in merged.params if q.index == j), None) + channel = _CHANNEL_FOR_TRANSFER.get(ps.transfer) if ps else None + if channel is not None: + body.append(Call(channel, + [VarRef(localmap.get(str(a), str(a)), line)], line)) # Only emit the `Call` when the callee is RESOLVABLE — a first-party function # with a summary, or a fixed ownership-sink extern. A real extraction surfaces # calls to callees we did not lower as functions (BCL / extension methods like # `GetRequiredService`); those have no signature, so `lower_call` would raise # OWN040. Drop them (no effect, no claim) — precision-safe, never a crash. - if (summ is not None or callee in _SINK_EXTERN_NAMES) \ + elif (summ is not None or callee in _SINK_EXTERN_NAMES) \ and callee and isinstance(raw_args, list): arg_refs: list[Expr] = [VarRef(localmap.get(str(a), str(a)), line) for a in raw_args] diff --git a/tests/test_ownir.py b/tests/test_ownir.py index fb0a85bd..bcb800d0 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1341,6 +1341,128 @@ def _sub(source: str | None) -> list[Finding]: 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}") + # (§10 q2) same-name OVERLOADS are merged, not dropped: when EVERY overload of a + # name consumes the forwarded arg, a forward to that name resolves to `must`, so a + # caller using the local after the handoff is OWN002. Before the merge the name was + # dropped → the forward stayed unknown → this leak was silently missed. + checks += 1 + ovc = check_facts({"module": "M", "functions": [ + {"name": "C.M", "file": "F.cs", "params": [{"name": "a", "line": 1}], + "body": [{"op": "release", "var": "a", "line": 2}]}, + {"name": "C.M", "file": "F.cs", "params": [{"name": "b", "line": 5}], + "body": [{"op": "release", "var": "b", "line": 6}]}, + {"name": "ov_fwd", "file": "F.cs", "params": [{"name": "s", "line": 10}], + "body": [{"op": "call", "callee": "C.M", "args": ["s"], "line": 11}]}, + {"name": "ov_use", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 20}, + {"op": "call", "callee": "ov_fwd", "args": ["s"], "line": 21}, + {"op": "use", "var": "s", "line": 22}]}]}) + gotov = sorted((x.component, x.code) for x in ovc) + if gotov != [("ov_use", "OWN002")]: + fails.append("§10 q2 agreeing overloads should resolve the forward to consume " + f"(ov_use OWN002), got {gotov}") + # (§10 q2) when overloads DISAGREE (one consumes, one only borrows) the merge joins + # to `may`, so the forward stays plain and a caller that releases the local itself is + # clean — the conservative join never fabricates a `must` from an ambiguous name. + checks += 1 + ovd = check_facts({"module": "M", "functions": [ + {"name": "C.N", "file": "F.cs", "params": [{"name": "a", "line": 1}], + "body": [{"op": "release", "var": "a", "line": 2}]}, + {"name": "C.N", "file": "F.cs", "params": [{"name": "b", "line": 5}], + "body": [{"op": "use", "var": "b", "line": 6}]}, + {"name": "ovn_fwd", "file": "F.cs", "params": [{"name": "s", "line": 10}], + "body": [{"op": "call", "callee": "C.N", "args": ["s"], "line": 11}]}, + {"name": "ovn_use", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 20}, + {"op": "call", "callee": "ovn_fwd", "args": ["s"], "line": 21}, + {"op": "release", "var": "s", "line": 22}]}]}) + if ovd: + gotn = [(x.component, x.code) for x in ovd] + fails.append("§10 q2 disagreeing overloads must join to `may` (caller stays " + f"silent), got {gotn}") + # (Codex P2) a DIRECT call to disagreeing overloads must NOT mis-apply the last same-name + # signature: the merged contract is `may`, so `acquire s; C.N(s); release s` stays silent. + # (Before the fix the core's last-wins signature consumed s → a false OWN002.) + checks += 1 + ovdir = check_facts({"module": "M", "functions": [ + {"name": "C.N", "file": "F.cs", "params": [{"name": "b", "line": 1}], + "body": [{"op": "use", "var": "b", "line": 2}]}, # borrow + {"name": "C.N", "file": "F.cs", "params": [{"name": "a", "line": 5}], + "body": [{"op": "release", "var": "a", "line": 6}]}, # consume (defined last) + {"name": "dN", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "C.N", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]}) + if ovdir: + fails.append("§10 q2 direct call to disagreeing overloads must stay silent (merged " + f"may), got {[(x.component, x.code) for x in ovdir]}") + # the same DIRECT path DOES apply consume when every overload agrees: both consume, so + # `acquire s; C.M(s); use s` is use-after-consume OWN002 (the channel carries the merged + # `must`, not a dropped effect). + checks += 1 + ovdir2 = check_facts({"module": "M", "functions": [ + {"name": "C.M", "file": "F.cs", "params": [{"name": "a", "line": 1}], + "body": [{"op": "release", "var": "a", "line": 2}]}, + {"name": "C.M", "file": "F.cs", "params": [{"name": "b", "line": 5}], + "body": [{"op": "release", "var": "b", "line": 6}]}, + {"name": "dM", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "C.M", "args": ["s"], "line": 11}, + {"op": "use", "var": "s", "line": 12}]}]}) + gotdm = sorted((x.component, x.code) for x in ovdir2) + if gotdm != [("dM", "OWN002")]: + fails.append("§10 q2 direct call to agreeing-consume overloads should apply consume " + f"(dM OWN002), got {gotdm}") + # (_merge_returns) overloaded FACTORY: every overload returns fresh, so a dropped result + # leaks interprocedurally (OWN001 at the call) — the merge restores the `fresh` resolution + # that dropping the overloaded name used to lose. + checks += 1 + ovret = check_facts({"module": "M", "functions": [ + {"name": "C.F", "file": "F.cs", + "body": [{"op": "acquire", "var": "r", "line": 1}, + {"op": "return", "var": "r", "line": 2}]}, + {"name": "C.F", "file": "F.cs", "params": [{"name": "p", "line": 4}], + "body": [{"op": "acquire", "var": "r", "line": 5}, + {"op": "return", "var": "r", "line": 6}]}, + {"name": "fdrop", "file": "F.cs", + "body": [{"op": "call", "callee": "C.F", "args": [], "result": "x", "line": 10}]}]}) + gotfr = sorted((x.component, x.code) for x in ovret) + if gotfr != [("fdrop", "OWN001")]: + fails.append("§10 q2 agreeing fresh overloaded factory: dropped result must leak " + f"(fdrop OWN001), got {gotfr}") + # when overloads DISAGREE on the return (one fresh, one not), the merge degrades to a + # non-fresh return, so a dropped result makes NO claim (precision-first: a real leak via + # the fresh overload is a tolerated miss, never a fabricated acquire). + checks += 1 + ovret2 = check_facts({"module": "M", "functions": [ + {"name": "C.G", "file": "F.cs", + "body": [{"op": "acquire", "var": "r", "line": 1}, + {"op": "return", "var": "r", "line": 2}]}, # fresh + {"name": "C.G", "file": "F.cs", "params": [{"name": "p", "line": 4}], + "body": [{"op": "use", "var": "p", "line": 5}]}, # no owned return + {"name": "gdrop", "file": "F.cs", + "body": [{"op": "call", "callee": "C.G", "args": [], "result": "x", "line": 10}]}]}) + if ovret2: + fails.append("§10 q2 disagreeing-return overloads must make no fresh claim (silent), " + f"got {[(x.component, x.code) for x in ovret2]}") + # (CodeRabbit) the overload channel matches on the CANONICAL name, so a `global::`-qualified + # direct call to an overloaded method still applies the merged contract: both overloads + # consume, so `global::C.M(s); release s` is release-after-consume OWN002 (raw-key matching + # would have dropped the handoff and silently missed the double-discharge). + checks += 1 + ovq = check_facts({"module": "M", "functions": [ + {"name": "C.M", "file": "F.cs", "params": [{"name": "a", "line": 1}], + "body": [{"op": "release", "var": "a", "line": 2}]}, + {"name": "C.M", "file": "F.cs", "params": [{"name": "b", "line": 5}], + "body": [{"op": "release", "var": "b", "line": 6}]}, + {"name": "dQ", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "global::C.M", "args": ["s"], "line": 11}, + {"op": "release", "var": "s", "line": 12}]}]}) + gotq = sorted((x.component, x.code) for x in ovq) + if gotq != [("dQ", "OWN002")]: + fails.append("§10 q2 qualified (global::) call to agreeing-consume overloads should " + f"apply the merged consume (dQ OWN002), got {gotq}") # --- P-005 D5.1b: the per-call-site ownership-contract channel. The extractor # routes a call's per-argument ownership through fixed sink externs # ($consume / $borrow / $borrow_mut) the bridge pre-declares, so an effect