diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index fe5938d3..59542814 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -239,12 +239,45 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa 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.1b — the per-call-site ownership-contract channel (shipped).** `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 rather than a per-method summary. The + bridge now pre-declares three fixed sink externs (`$consume` / `$borrow` / `$borrow_mut`) + in every lowered `Module`; the extractor routes any call's per-argument ownership through + them (`call $consume [x]`), and they resolve via the **same** `collect_signatures` + + `lower_call` path as any contracted call — no new checker, no new flow lowering. The `$` + prefix cannot collide with a real C# member. The solver also reads a forward to a sink as a + *known* transfer (`$consume`→must, `$borrow`→no), so the channel propagates **transitively** + through first-party wrappers, not just at the direct call. `$borrow_mut` is intentionally + excluded from the *transitive* shortcut — the transfer lattice has no shared-vs-exclusive + axis, so a wrapper summary would silently downgrade an exclusive loan to a shared one; the + honest move is to decline that claim (the wrapper param stays plain) while the *direct* + `$borrow_mut` call keeps full exclusivity through `lower_call` (Codex P2). Proven by synthetic + OwnIR tests: + use/double-release after `$consume` (OWN002), a `$borrow`'d-then-never-released local still + leaking (OWN001), a clean borrow-then-release, and transitive propagation through a wrapper. + The remaining piece is **CI/C#-only**: the extractor emitting these sink calls from the bool + literal / annotation (paired with an A/B sample on real extractor output) — Tier-B breadth + rides into D5.3. +- **D5.1c — transitive borrow-kind propagation (deferred).** The D5.0 summary solver is + *transfer*-oriented: its `Transfer` lattice (no/must/may/unknown) has no shared-vs-exclusive + axis, so an explicit `borrow`/`borrow_mut` and a `$borrow_mut` forward both seed the same + summary-side `borrow` bucket. The **core checker already distinguishes them** (`cfg.py` + emits `Effect.BORROW` vs `BORROW_MUT`; `analysis.py` routes them to `_check_shared_borrowable` + vs `_check_mut_borrowable`), so the *direct* `$borrow_mut` call keeps full exclusivity — only + the *transitive* claim through a first-party wrapper is lost. D5.1b takes the precision-safe + decline (a wrapper that only forwards to `$borrow_mut` stays plain — a tolerated false- + negative, never a false shared-borrow assertion). The clean fix is **not** one more `Transfer` + enum value but an **orthogonal borrow-kind axis** (`none | shared | mut`) on the summary, + structured sink semantics (don't normalize `$borrow_mut` away before inference), and the same + brutally-conservative rule the must-consume path uses: infer `borrow_mut` only on a single, + unconditional, straight-line forward to `$borrow_mut`; any mix / fan-out / conditional / loop + → degrade to plain/unknown and stay silent. Deliverables: borrow-kind on the summary, direct + behaviour unchanged, `$borrow_mut` wrapper tests, and mixed-path regressions proving ambiguous + flows degrade to silence (not shared borrow). Prior art: Rust `&`/`&mut`, RustBelt exclusivity, + 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.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh` diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 4fccd361..6a25a48a 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -106,7 +106,10 @@ from .ast_nodes import ( Acquire, Call, + Effect, + EffectParam, Expr, + ExternDecl, FnDecl, If, Let, @@ -848,7 +851,9 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] if _returns_value(nodes) else None) functions.append(FnDecl(fname, fparams, fret, fbody, 0)) return (Module(str(facts.get("module", "Extracted")), - resources=_prelude_resources(), functions=functions, + resources=_prelude_resources(), + externs=list(_OWNERSHIP_SINK_EXTERNS), + functions=functions, lifetimes=list(_CAPTURE_LIFETIMES) if any_capture else []), handles) @@ -913,6 +918,37 @@ def _returns_value(nodes: Any) -> bool: "borrow_mut": TypeRef("Disposable", True, True), # exclusive loan, noescape } +# P-005 D5.1b — the per-call-site ownership-contract channel. The extractor cannot +# always pin a call's ownership effect from a first-party body: a BCL sink (e.g. +# `new StreamReader(s, leaveOpen: false)`) or a `[ConsumesOwnership]`-style +# annotation lives outside our summary set. Rather than grow a bespoke lowering for +# each such case, we pre-declare three fixed sink externs and let the extractor +# route any call's per-argument ownership through them: a `call $consume [x]` takes +# ownership of `x`, `$borrow`/`$borrow_mut` lend it for the call. They resolve via +# the SAME `collect_signatures` + `lower_call` path as any contracted call (so a +# later use of a consumed `x` is OWN002, an un-discharged borrow is still OWN001) — +# no new checker, no new flow lowering. Externs are declaration-only, never leak- +# checked themselves, and the `$` prefix cannot collide with a real C# member name. +_OWNERSHIP_SINK_EXTERNS = ( + ExternDecl("$consume", [EffectParam(Effect.CONSUME, "Disposable", 0)], None, 0), + ExternDecl("$borrow", [EffectParam(Effect.BORROW, "Disposable", 0)], None, 0), + ExternDecl("$borrow_mut", + [EffectParam(Effect.BORROW_MUT, "Disposable", 0)], None, 0), +) + +# A forward to a sink extern is a *known* transfer, so a skeleton can record the +# resolved path action directly — `$consume` is ownership leaving (a must-transfer), +# `$borrow` is a kept loan — rather than a `forward` edge to an unsummarized callee +# (which the solver would degrade to `unknown`, diluting a real `must` to plain). +# `$borrow_mut` is DELIBERATELY ABSENT (Codex P2): the transfer lattice carries no +# shared-vs-exclusive axis, so mapping it to `borrow` would silently downgrade an +# EXCLUSIVE loan to a shared one in the wrapper's contract — asserting something +# weaker than the truth. We decline the transitive claim instead (it falls through +# to a `forward` edge → `unknown` → the wrapper param stays plain, no false shared- +# borrow contract). The DIRECT `call $borrow_mut [x]` channel is unaffected and keeps +# full exclusivity through `lower_call`. Kept in sync with `_OWNERSHIP_SINK_EXTERNS`. +_SINK_PATH_ACTION = {"$consume": "dispose", "$borrow": "borrow"} + def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]: """Scan a flow body for how parameter `pname` is treated, returning @@ -970,6 +1006,17 @@ def _forward_targets(pname: str, nodes: Any, return out +def _forward_path_action(callee: str, arg: int) -> PathAction: + """The skeleton path action for one forward edge. A forward to a fixed + ownership-sink extern (D5.1b) is a *resolved* transfer recorded directly + (`$consume` → `dispose`, `$borrow*` → `borrow`); any other callee is a + `forward` edge the solver resolves against that callee's summary.""" + kind = _SINK_PATH_ACTION.get(callee) + if kind is not None: + return PathAction(kind) + return PathAction("forward", callee, arg) + + 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 @@ -1025,7 +1072,7 @@ def _build_skeletons(raw_fns: list[Any]) -> list[MethodSkeleton]: 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) + paths = tuple(_forward_path_action(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 diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 68a592b2..c4fce693 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1254,6 +1254,95 @@ 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}") + # --- 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 + # the callee's body cannot reveal (a BCL `leaveOpen: false`, an annotation) + # is checked through the SAME lower_call path — no new checker. + # $consume takes ownership: a local acquired then handed to $consume has left, so + # a later USE is OWN002 (anchored at the acquire, like every transitive handoff). + checks += 1 + csink = check_facts({"module": "M", "functions": [ + {"name": "use_after_consume", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 10}, + {"op": "call", "callee": "$consume", "args": ["x"], "line": 11}, + {"op": "use", "var": "x", "line": 12}]}]}) + gotcs = [(x.component, x.line, x.code) for x in csink] + if gotcs != [("use_after_consume", 10, "OWN002")]: + fails.append("D5.1b $consume channel: use after a $consume handoff must be " + f"OWN002@10 (ownership left at the call), got {gotcs}") + # releasing AFTER $consume double-discharges (the obligation already moved out). + checks += 1 + crel = check_facts({"module": "M", "functions": [ + {"name": "release_after_consume", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 20}, + {"op": "call", "callee": "$consume", "args": ["x"], "line": 21}, + {"op": "release", "var": "x", "line": 22}]}]}) + gotcr = [(x.component, x.line, x.code) for x in crel] + if gotcr != [("release_after_consume", 20, "OWN002")]: + fails.append("D5.1b $consume channel: release after a $consume handoff must be " + f"OWN002@20, got {gotcr}") + # $borrow only LENDS for the call: the caller keeps ownership, so a local handed + # to $borrow and never released is still a leak (OWN001) — the channel does NOT + # over-consume a borrow into a (silent) transfer. + checks += 1 + bleak = check_facts({"module": "M", "functions": [ + {"name": "borrow_then_leak", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 30}, + {"op": "call", "callee": "$borrow", "args": ["x"], "line": 31}]}]}) + gotbl = [(x.component, x.line, x.code) for x in bleak] + if gotbl != [("borrow_then_leak", 30, "OWN001")]: + fails.append("D5.1b $borrow channel: a borrowed-then-never-released local must " + f"still leak OWN001@30 (borrow keeps ownership), got {gotbl}") + # and $borrow then releasing is clean — the loan is returned, the owner discharges. + checks += 1 + bclean = check_facts({"module": "M", "functions": [ + {"name": "borrow_then_release", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 40}, + {"op": "call", "callee": "$borrow", "args": ["x"], "line": 41}, + {"op": "release", "var": "x", "line": 42}]}]}) + if bclean: + fails.append("D5.1b $borrow channel: borrow-then-release must be clean, " + f"got {[(x.component, x.code) for x in bclean]}") + # the DIRECT $borrow_mut channel keeps the exclusive loan: like $borrow, it lends + # for the call and the caller keeps ownership, so a never-released local still + # leaks (OWN001) and a released one is clean. (The transitive shortcut for + # $borrow_mut is deliberately declined — the transfer lattice has no shared-vs- + # exclusive axis, so a wrapper would silently downgrade it; see _SINK_PATH_ACTION.) + checks += 1 + bmleak = check_facts({"module": "M", "functions": [ + {"name": "borrow_mut_leak", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 50}, + {"op": "call", "callee": "$borrow_mut", "args": ["x"], "line": 51}]}]}) + gotbm = [(x.component, x.line, x.code) for x in bmleak] + if gotbm != [("borrow_mut_leak", 50, "OWN001")]: + fails.append("D5.1b $borrow_mut channel: a borrowed-then-never-released local " + f"must still leak OWN001@50 (exclusive loan keeps ownership), got {gotbm}") + checks += 1 + bmclean = check_facts({"module": "M", "functions": [ + {"name": "borrow_mut_release", "file": "F.cs", + "body": [{"op": "acquire", "var": "x", "line": 60}, + {"op": "call", "callee": "$borrow_mut", "args": ["x"], "line": 61}, + {"op": "release", "var": "x", "line": 62}]}]}) + if bmclean: + fails.append("D5.1b $borrow_mut channel: borrow_mut-then-release must be clean, " + f"got {[(x.component, x.code) for x in bmclean]}") + # the channel resolves TRANSITIVELY too: a param ONLY forwarded to $consume makes + # the method a must-consumer (the solver reads the sink as a known transfer), so a + # caller using its arg after the handoff is OWN002 — same as forwarding to a + # first-party consumer, but sourced from the per-call channel. + checks += 1 + ctrans = check_facts({"module": "M", "functions": [ + {"name": "wrap_consume", "file": "F.cs", "params": [{"name": "s", "line": 1}], + "body": [{"op": "call", "callee": "$consume", "args": ["s"], "line": 2}]}, + {"name": "caller_t", "file": "F.cs", + "body": [{"op": "acquire", "var": "s", "line": 10}, + {"op": "call", "callee": "wrap_consume", "args": ["s"], "line": 11}, + {"op": "use", "var": "s", "line": 12}]}]}) + gotct = [(x.component, x.line, x.code) for x in ctrans] + 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}") # 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