Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 25 additions & 2 deletions docs/notes/d5-ownership-transfer.md
Original file line number Diff line number Diff line change
Expand Up @@ -333,8 +333,31 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa
cumulative), and the early-return guard shape (`guard` — stays a loud OWN030 raise rather than a
false positive). (Bridge branch-scope fix: Codex P2 on #116; loop exclusion Codex P1, hoist
safety predicate + pool-kind preservation CodeRabbit on #120.)
- **D5.3 — Tier B breadth.** The rest of the documented BCL ownership table + `fresh`
factories.
- **D5.3 — Tier B breadth.**
- **Producer side — `fresh` factories (shipped, first slice).** A curated
`_BCL_FRESH_FACTORIES` table in the OwnIR bridge (`ownir.py`) marks well-known BCL
factories whose return the caller owns (`File.OpenRead/OpenText/OpenWrite/Open/Create/
CreateText/AppendText`). A `call` to one binds a `fresh` result via the SAME `_callee_
returns_fresh` path the first-party T1 inference uses (now the single source of truth for
the leak pre-scan, branch-hoist safety, and lowering), so a leaked `var s =
File.OpenRead(p)` surfaces as OWN001 *at the factory call* — invisible before (no body to
infer from; see `corpus-benchmark.md`). Matched conservatively (Codex): ONLY the bare
`File.Method` or the fully-qualified `System.IO.File.Method` — a same-named factory in
another namespace (`MyCompany.File.OpenRead`) is **not** a match, so we never fabricate
ownership for a look-alike. A **first-party summary overrides** the table (`_callee_
returns_fresh` trusts a known body over Tier B), and a first-party **wrapper** that
returns a factory result (`Make(){ return File.OpenRead(p) }`) is itself `fresh`, so a
dropped `Make()` leaks too (the return skeleton propagates BCL freshness instead of
forwarding to the external, unsummarizable callee). Pure factories only — overload-
ambiguous *wrappers* that adopt an arg (`new StreamReader(stream)`) are excluded (sink/T4).
Tests in `test_ownir.py` (leak / disposed-clean / use-after-dispose / namespace-qualified /
non-System.IO look-alike rejected / first-party override / wrapper-fresh recall / a
non-disposable `File.ReadAllText` making no claim).
- **Sink side — `leaveOpen` breadth (remaining, extractor-side).** The documented
consume/borrow table (`StreamReader`/`StreamWriter`/`CryptoStream`/… by the `leaveOpen`
bool literal) rides the existing `$consume`/`$borrow` channel (D5.1b); its breadth is a
C#-extractor table (the bool literal is a per-call-site fact the extractor sees), so it is
CI/C#-only, not a pure-Python slice.
- **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit
cadence** so the core change is de-risked: **(step 0)** a *no-op identity refactor* —
move resource state from per-binding to per-RID with a 1:1 binding↔RID mapping, behaviour
Expand Down
57 changes: 52 additions & 5 deletions ownlang/ownir.py
Original file line number Diff line number Diff line change
Expand Up @@ -1041,6 +1041,12 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton:
(v,) = tuple(returned)
callee = call_results.get(v)
if callee and v not in param_names and v not in acquired:
if _is_bcl_fresh_factory(callee):
# a thin wrapper returning a BCL factory's result is itself `fresh` — the
# caller owns it (Codex). Without this the return is a `forward` to an
# external (bodyless) callee, which the solver degrades to `unknown`, so a
# dropped `Make()` whose body is `return File.OpenRead(p)` leaks invisibly.
return ReturnSkeleton("fresh")
return ReturnSkeleton("forward", callee=callee)
return ReturnSkeleton() # not provably owned -> no claim

Expand Down Expand Up @@ -1095,6 +1101,49 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton:
_SINK_PATH_ACTION = {"$consume": "dispose", "$borrow": "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
# *sink* half rides the `$consume`/`$borrow` channel above). These are pure factories: the
# result is a fresh owned `IDisposable` and the arguments are not resources, so a leaked
# `var s = File.OpenRead(p)` now surfaces as an OWN001 leak AT the factory call — it was
# invisible before (no body to infer `fresh` from; see docs/notes/corpus-benchmark.md).
# Overload-ambiguous *wrappers* that ADOPT an argument (e.g. `new StreamReader(stream)`) are
# deliberately excluded — that is the sink / T4 case, not a pure factory. Keyed by
# `Type.Method`; a callee matches on its last two dotted segments so a namespace-qualified
# `System.IO.File.OpenRead` resolves the same.
_BCL_FRESH_FACTORIES = frozenset({
"File.OpenRead", "File.OpenText", "File.OpenWrite",
"File.Open", "File.Create", "File.CreateText", "File.AppendText",
})
# the fully-qualified `System.IO.File.*` identities — accepted alongside the bare forms.
_BCL_FRESH_FQNS = frozenset("System.IO." + e for e in _BCL_FRESH_FACTORIES)


def _is_bcl_fresh_factory(callee: str) -> bool:
"""True if `callee` names a curated BCL factory whose return the caller owns. Accepts
ONLY the bare `Type.Method` (`File.OpenRead`) or the fully-qualified `System.IO.File.*`
identity (with an optional `global::` qualifier) — a same-named type in another namespace
(`MyCompany.File.OpenRead`) is NOT a match. Precision-first: we never fabricate ownership
for a non-BCL look-alike (Codex / CodeRabbit)."""
if not callee:
return False
name = callee.removeprefix("global::")
return name in _BCL_FRESH_FACTORIES or name in _BCL_FRESH_FQNS


def _callee_returns_fresh(callee: str, mos: dict[str, Any] | None) -> bool:
"""Whether a `call` to `callee` yields a fresh owned result the caller must release.
A first-party summary is AUTHORITATIVE — if one exists we trust its `returns`, so a
same-named first-party `File.OpenRead` (Tier A) overrides the BCL table (Tier B) and is
never given a fabricated `fresh` (Codex). Only a callee we have no body for falls back to
the curated BCL factory table. The single source of truth shared by the leak pre-scan,
the branch-hoist safety walk, and the flow lowering, so all three agree."""
summ = mos.get(callee) if (mos is not None and callee) else None
if summ is not None:
return getattr(summ, "returns", None) == "fresh"
return _is_bcl_fresh_factory(callee)


def _param_signals(pname: str, nodes: Any) -> tuple[bool, bool, bool]:
"""Scan a flow body for how parameter `pname` is treated, returning
(released, handed-to-a-call, used). Recurses into if/while branches so a
Expand Down Expand Up @@ -1327,8 +1376,7 @@ def acquires(n: dict[str, Any]) -> bool:
if n.get("op") == "acquire" and str(n.get("var", "")) == name:
return True
if n.get("op") == "call" and str(n.get("result", "")) == name:
summ = mos.get(str(n.get("callee", ""))) if mos is not None else None
return summ is not None and getattr(summ, "returns", None) == "fresh"
return _callee_returns_fresh(str(n.get("callee", "")), mos)
return False

def analyze(seq: Any, acquired: bool) -> tuple[bool, bool]:
Expand Down Expand Up @@ -1396,8 +1444,7 @@ def fresh_result(n: dict[str, Any]) -> str | None:
callee, res = n.get("callee"), n.get("result")
if not (isinstance(res, str) and res and isinstance(callee, str) and callee):
return None
summ = mos.get(callee) if mos is not None else None
return res if (summ is not None and getattr(summ, "returns", None) == "fresh") else None
return res if _callee_returns_fresh(callee, mos) else None

def note_ref(name: str, depth: int) -> None:
if name not in ref_depth or depth < ref_depth[name]:
Expand Down Expand Up @@ -1561,7 +1608,7 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str,
if isinstance(result, str) and result and result not in hoisted:
localmap.pop(result, None)
if (isinstance(result, str) and result and result not in hoisted
and summ is not None and getattr(summ, "returns", None) == "fresh"):
and _callee_returns_fresh(callee, mos)):
handle = f"loc_{loc[0]}"
loc[0] += 1
localmap[result] = handle
Expand Down
85 changes: 85 additions & 0 deletions tests/test_ownir.py
Original file line number Diff line number Diff line change
Expand Up @@ -1513,6 +1513,91 @@ def _sub(source: str | None) -> list[Finding]:
f"got {[(x.component, x.code) for x in unk]}")
except OwnIRError as e:
fails.append(f"D5.2: a call to an unknown callee must not crash (OWN040), got {e!r}")
# Tier B (D5.3 / P1a): a curated BCL *factory* (`File.OpenRead` &c.) returns an owned
# IDisposable even with no first-party body, so a leaked `var s = File.OpenRead(p)` is
# OWN001 AT the factory call (invisible before this table) — the producer half of the
# boundary contract. Contrast the unknown-callee case just above, which makes no claim.
def _bcl(body: list) -> list:
return check_facts({"module": "M", "functions": [
{"name": "Svc.Do", "file": "Bcl.cs", "body": body}]})
checks += 1
bleak = [(x.code, x.line, x.kind) for x in _bcl(
[{"op": "call", "callee": "File.OpenRead", "args": ["p"], "result": "s", "line": 5}])]
if bleak != [("OWN001", 5, "disposable")]:
fails.append(f"Tier B: a leaked BCL factory result must be OWN001@5 disposable, "
f"got {bleak}")
checks += 1
if _bcl([{"op": "call", "callee": "File.OpenRead", "args": ["p"], "result": "s", "line": 5},
{"op": "release", "var": "s", "line": 6}]):
fails.append("Tier B: a disposed BCL factory result must be clean (silent)")
checks += 1
buar = [(x.code, x.line) for x in _bcl(
[{"op": "call", "callee": "File.OpenRead", "args": ["p"], "result": "s", "line": 5},
{"op": "release", "var": "s", "line": 6},
{"op": "use", "var": "s", "line": 7}])]
if buar != [("OWN002", 5)]:
fails.append(f"Tier B: using a BCL factory result after dispose must be OWN002@5, "
f"got {buar}")
checks += 1
# a namespace-qualified callee resolves on its last two segments (`Type.Method`).
nsq = [(x.code, x.line) for x in _bcl(
[{"op": "call", "callee": "System.IO.File.Create", "args": ["p"],
"result": "s", "line": 9}])]
if nsq != [("OWN001", 9)]:
fails.append(f"Tier B: a namespace-qualified BCL factory must resolve, got {nsq}")
checks += 1
# a non-disposable BCL method (`File.ReadAllText` -> string) is NOT a factory — no false
# acquire of its result, stays silent (precision-first: the table is owned-returns only).
if _bcl([{"op": "call", "callee": "File.ReadAllText", "args": ["p"],
"result": "t", "line": 3}]):
fails.append("Tier B: a non-disposable BCL method must not be treated as a factory")
checks += 1
# PRECISION (Codex): a same-named factory in ANOTHER namespace is NOT System.IO.File, so
# the match must not be a loose suffix — only bare `File.X` and `System.IO.File.X` count.
# A `MyCompany.File.OpenRead` returning a plain value must NOT fabricate a false OWN001.
if _bcl([{"op": "call", "callee": "MyCompany.File.OpenRead", "args": ["p"],
"result": "s", "line": 5}]):
fails.append("Tier B precision: a non-System.IO `*.File.OpenRead` must NOT match")
checks += 1
# a `global::`-qualified System.IO.File factory IS the BCL identity (the qualifier is
# stripped); a `global::`-qualified non-System.IO look-alike still must NOT match.
gq = [(x.code, x.line) for x in _bcl([{"op": "call",
"callee": "global::System.IO.File.OpenRead", "args": ["p"],
"result": "s", "line": 4}])]
if gq != [("OWN001", 4)]:
fails.append(f"Tier B: a `global::System.IO.File.*` factory must match, got {gq}")
if _bcl([{"op": "call", "callee": "global::MyCompany.File.OpenRead", "args": ["p"],
"result": "s", "line": 4}]):
fails.append("Tier B precision: `global::`-qualified non-System.IO must NOT match")
checks += 1
# OVERRIDE (Codex): a first-party summary is authoritative — a first-party `File.OpenRead`
# that returns its parameter is NOT fresh, so a caller dropping its result is clean; the
# table must not fabricate ownership for a callee whose body we can see.
ov_fp = check_facts({"module": "M", "functions": [
{"name": "File.OpenRead", "file": "B.cs", "params": [{"name": "x", "line": 1}],
"body": [{"op": "return", "var": "x", "line": 2}]},
{"name": "Caller", "file": "B.cs", "body": [
{"op": "acquire", "var": "a", "line": 10},
{"op": "call", "callee": "File.OpenRead", "args": ["a"],
"result": "r", "line": 11},
{"op": "release", "var": "a", "line": 12}]}]})
if ov_fp:
fails.append(f"Tier B: a first-party summary must override the BCL table, "
f"got {[(x.component, x.code) for x in ov_fp]}")
checks += 1
# RECALL (Codex): a first-party wrapper that returns a BCL factory result is itself fresh,
# so a caller dropping `Make()` leaks OWN001 — the return skeleton propagates BCL freshness
# rather than degrading to a `forward` to the external factory (-> unknown -> invisible).
wrap = [(x.component, x.line, x.code) for x in check_facts({"module": "M", "functions": [
{"name": "Make", "file": "B.cs", "body": [
{"op": "call", "callee": "File.OpenRead", "args": ["p"],
"result": "s", "line": 2},
{"op": "return", "var": "s", "line": 3}]},
{"name": "Caller2", "file": "B.cs", "body": [
{"op": "call", "callee": "Make", "args": [], "result": "r", "line": 10}]}]})]
if wrap != [("Caller2", 10, "OWN001")]:
fails.append(f"Tier B: a wrapper returning a BCL factory result must be fresh "
f"(caller leak OWN001@10), got {wrap}")
# OVERWRITE kills the prior binding (CodeRabbit): `acquire x; x = Unknown(); release x`
# — the call's result reuses an owned local and the call is dropped (unknown callee),
# so the ORIGINAL x leaks (its reference is lost), not read as clean. The release after
Expand Down
Loading