From 76d29aff32b141d646e6691abf1069b627ae3c06 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 18:43:36 +0000 Subject: [PATCH 1/3] P-005 D5.3 / P1a: curated BCL fresh-factory table (producer side of Tier B) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit C+D first slice — the producer half of the boundary contract. A leaked BCL factory result (`var s = File.OpenRead(p)`) was invisible because there is no first-party body to infer `fresh` from; now a curated table makes it owned. - ownir.py: `_BCL_FRESH_FACTORIES` (File.OpenRead/OpenText/OpenWrite/Open/Create/ CreateText/AppendText) + `_is_bcl_fresh_factory` (matches `Type.Method`, so a namespace-qualified callee resolves on its last two segments). New `_callee_returns_fresh` centralises the "does this call yield a fresh owned result?" decision (Tier A first-party summary OR Tier B BCL table) and is now the single source of truth shared by the leak pre-scan, the branch-hoist safety walk, and the flow lowering — so all three agree. - A leaked factory result is OWN001 at the call; disposed is clean; use-after-dispose is OWN002; it composes with the P-015 codeFlows slice (the finding anchors at the factory call). Pure factories only — overload-ambiguous wrappers that adopt an arg (`new StreamReader(stream)`) stay out (sink/T4). - The leaveOpen *sink* breadth rides the existing $consume/$borrow channel and is extractor-side (the bool literal is a per-call-site fact), so it is CI/C#-only; documented as the remaining half in d5-ownership-transfer.md §7. Tests: leak / disposed-clean / use-after-dispose / namespace-qualified / a non-disposable `File.ReadAllText` making no claim. ownir 174/174; ruff + mypy clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KkpSWNx7ARLpQeAs13kkyA --- docs/notes/d5-ownership-transfer.md | 20 +++++++++++-- ownlang/ownir.py | 44 +++++++++++++++++++++++++---- tests/test_ownir.py | 38 +++++++++++++++++++++++++ 3 files changed, 95 insertions(+), 7 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index e3309ed8..7998849f 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -333,8 +333,24 @@ 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`). Keyed by `Type.Method` (matches a namespace- + qualified callee on its last two segments). 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 / a + non-disposable `File.ReadAllText` correctly 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 diff --git a/ownlang/ownir.py b/ownlang/ownir.py index ea4d5509..737cdfb9 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -1095,6 +1095,42 @@ 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", +}) + + +def _is_bcl_fresh_factory(callee: str) -> bool: + """True if `callee` names a curated BCL factory whose return the caller owns. Matches + the bare `Type.Method` or any namespace-qualified form of it (its last two segments).""" + if not callee: + return False + return (callee in _BCL_FRESH_FACTORIES + or ".".join(callee.split(".")[-2:]) in _BCL_FRESH_FACTORIES) + + +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 that returns `fresh` (Tier A) OR a curated BCL factory (Tier B). + The single source of truth shared by the leak pre-scan, the branch-hoist safety walk, + and the flow lowering, so all three agree on what counts as an acquire.""" + if _is_bcl_fresh_factory(callee): + return True + summ = mos.get(callee) if (mos is not None and callee) else None + return summ is not None and getattr(summ, "returns", None) == "fresh" + + 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 @@ -1327,8 +1363,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]: @@ -1396,8 +1431,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]: @@ -1561,7 +1595,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 diff --git a/tests/test_ownir.py b/tests/test_ownir.py index d23ddbed..8a362d1b 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1513,6 +1513,44 @@ 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") # 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 From 52a562e52e361c4862d979ef0126390df37003cf Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 18:50:35 +0000 Subject: [PATCH 2/3] D5.3: tighten BCL factory match + propagate freshness through wrappers (Codex #127) Two Codex P2s on the BCL fresh-factory table: - PRECISION: the match was a loose last-two-segments suffix, so an external `MyCompany.File.OpenRead` returning a plain value would be treated as a BCL factory and fabricate a false OWN001/OWN002. Now matches ONLY the bare `File.Method` or the fully-qualified `System.IO.File.Method` identity. Also flipped `_callee_returns_fresh` so a first-party summary is authoritative and OVERRIDES the table (a callee whose body we can see is never given a fabricated `fresh`). - RECALL: a first-party wrapper `Make(){ return File.OpenRead(p) }` recorded a `forward` to the external factory, which the solver degraded to `unknown`, so a dropped `Make()` leaked invisibly. `_infer_return_skeleton` now classifies such a return as `fresh`, so the caller is charged the leak. Tests: non-System.IO look-alike rejected, first-party override, wrapper-fresh recall. ownir 177/177; ruff + mypy clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KkpSWNx7ARLpQeAs13kkyA --- docs/notes/d5-ownership-transfer.md | 17 ++++++++++---- ownlang/ownir.py | 35 +++++++++++++++++----------- tests/test_ownir.py | 36 +++++++++++++++++++++++++++++ 3 files changed, 70 insertions(+), 18 deletions(-) diff --git a/docs/notes/d5-ownership-transfer.md b/docs/notes/d5-ownership-transfer.md index 7998849f..39b1cbf3 100644 --- a/docs/notes/d5-ownership-transfer.md +++ b/docs/notes/d5-ownership-transfer.md @@ -341,11 +341,18 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa 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`). Keyed by `Type.Method` (matches a namespace- - qualified callee on its last two segments). 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 / a - non-disposable `File.ReadAllText` correctly making no claim). + 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 diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 737cdfb9..839f65cc 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -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 @@ -1109,26 +1115,29 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton: "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. Matches - the bare `Type.Method` or any namespace-qualified form of it (its last two segments).""" - if not callee: - return False - return (callee in _BCL_FRESH_FACTORIES - or ".".join(callee.split(".")[-2:]) in _BCL_FRESH_FACTORIES) + """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 — 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).""" + return bool(callee) and (callee in _BCL_FRESH_FACTORIES or callee 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 that returns `fresh` (Tier A) OR a curated BCL factory (Tier B). - The single source of truth shared by the leak pre-scan, the branch-hoist safety walk, - and the flow lowering, so all three agree on what counts as an acquire.""" - if _is_bcl_fresh_factory(callee): - return True + """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 - return summ is not None and getattr(summ, "returns", None) == "fresh" + 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]: diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 8a362d1b..9e26b523 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1551,6 +1551,42 @@ def _bcl(body: list) -> list: 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 + # 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 From fe74309a66fae7efefc6352cfb7cf7ed99decd13 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 18:51:55 +0000 Subject: [PATCH 3/3] D5.3: normalize a global:: qualifier on the BCL factory match (CodeRabbit #127) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit marked the Tier-B precision concern addressed by 52a562e; this folds in its remaining suggestion — strip an optional `global::` qualifier before the match, so `global::System.IO.File.OpenRead` resolves as the BCL identity while a `global::`-qualified non-System.IO look-alike is still rejected. Tests for both. ownir 177/177; ruff + mypy clean. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01KkpSWNx7ARLpQeAs13kkyA --- ownlang/ownir.py | 10 +++++++--- tests/test_ownir.py | 11 +++++++++++ 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 839f65cc..0b5fe3c5 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -1122,9 +1122,13 @@ def _infer_return_skeleton(nodes: Any, param_names: set[str]) -> ReturnSkeleton: 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 — 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).""" - return bool(callee) and (callee in _BCL_FRESH_FACTORIES or callee in _BCL_FRESH_FQNS) + 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: diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 9e26b523..158746a5 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1559,6 +1559,17 @@ def _bcl(body: list) -> list: "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.