@@ -1513,6 +1513,91 @@ def _sub(source: str | None) -> list[Finding]:
15131513 f"got { [(x .component , x .code ) for x in unk ]} " )
15141514 except OwnIRError as e :
15151515 fails .append (f"D5.2: a call to an unknown callee must not crash (OWN040), got { e !r} " )
1516+ # Tier B (D5.3 / P1a): a curated BCL *factory* (`File.OpenRead` &c.) returns an owned
1517+ # IDisposable even with no first-party body, so a leaked `var s = File.OpenRead(p)` is
1518+ # OWN001 AT the factory call (invisible before this table) — the producer half of the
1519+ # boundary contract. Contrast the unknown-callee case just above, which makes no claim.
1520+ def _bcl (body : list ) -> list :
1521+ return check_facts ({"module" : "M" , "functions" : [
1522+ {"name" : "Svc.Do" , "file" : "Bcl.cs" , "body" : body }]})
1523+ checks += 1
1524+ bleak = [(x .code , x .line , x .kind ) for x in _bcl (
1525+ [{"op" : "call" , "callee" : "File.OpenRead" , "args" : ["p" ], "result" : "s" , "line" : 5 }])]
1526+ if bleak != [("OWN001" , 5 , "disposable" )]:
1527+ fails .append (f"Tier B: a leaked BCL factory result must be OWN001@5 disposable, "
1528+ f"got { bleak } " )
1529+ checks += 1
1530+ if _bcl ([{"op" : "call" , "callee" : "File.OpenRead" , "args" : ["p" ], "result" : "s" , "line" : 5 },
1531+ {"op" : "release" , "var" : "s" , "line" : 6 }]):
1532+ fails .append ("Tier B: a disposed BCL factory result must be clean (silent)" )
1533+ checks += 1
1534+ buar = [(x .code , x .line ) for x in _bcl (
1535+ [{"op" : "call" , "callee" : "File.OpenRead" , "args" : ["p" ], "result" : "s" , "line" : 5 },
1536+ {"op" : "release" , "var" : "s" , "line" : 6 },
1537+ {"op" : "use" , "var" : "s" , "line" : 7 }])]
1538+ if buar != [("OWN002" , 5 )]:
1539+ fails .append (f"Tier B: using a BCL factory result after dispose must be OWN002@5, "
1540+ f"got { buar } " )
1541+ checks += 1
1542+ # a namespace-qualified callee resolves on its last two segments (`Type.Method`).
1543+ nsq = [(x .code , x .line ) for x in _bcl (
1544+ [{"op" : "call" , "callee" : "System.IO.File.Create" , "args" : ["p" ],
1545+ "result" : "s" , "line" : 9 }])]
1546+ if nsq != [("OWN001" , 9 )]:
1547+ fails .append (f"Tier B: a namespace-qualified BCL factory must resolve, got { nsq } " )
1548+ checks += 1
1549+ # a non-disposable BCL method (`File.ReadAllText` -> string) is NOT a factory — no false
1550+ # acquire of its result, stays silent (precision-first: the table is owned-returns only).
1551+ if _bcl ([{"op" : "call" , "callee" : "File.ReadAllText" , "args" : ["p" ],
1552+ "result" : "t" , "line" : 3 }]):
1553+ fails .append ("Tier B: a non-disposable BCL method must not be treated as a factory" )
1554+ checks += 1
1555+ # PRECISION (Codex): a same-named factory in ANOTHER namespace is NOT System.IO.File, so
1556+ # the match must not be a loose suffix — only bare `File.X` and `System.IO.File.X` count.
1557+ # A `MyCompany.File.OpenRead` returning a plain value must NOT fabricate a false OWN001.
1558+ if _bcl ([{"op" : "call" , "callee" : "MyCompany.File.OpenRead" , "args" : ["p" ],
1559+ "result" : "s" , "line" : 5 }]):
1560+ fails .append ("Tier B precision: a non-System.IO `*.File.OpenRead` must NOT match" )
1561+ checks += 1
1562+ # a `global::`-qualified System.IO.File factory IS the BCL identity (the qualifier is
1563+ # stripped); a `global::`-qualified non-System.IO look-alike still must NOT match.
1564+ gq = [(x .code , x .line ) for x in _bcl ([{"op" : "call" ,
1565+ "callee" : "global::System.IO.File.OpenRead" , "args" : ["p" ],
1566+ "result" : "s" , "line" : 4 }])]
1567+ if gq != [("OWN001" , 4 )]:
1568+ fails .append (f"Tier B: a `global::System.IO.File.*` factory must match, got { gq } " )
1569+ if _bcl ([{"op" : "call" , "callee" : "global::MyCompany.File.OpenRead" , "args" : ["p" ],
1570+ "result" : "s" , "line" : 4 }]):
1571+ fails .append ("Tier B precision: `global::`-qualified non-System.IO must NOT match" )
1572+ checks += 1
1573+ # OVERRIDE (Codex): a first-party summary is authoritative — a first-party `File.OpenRead`
1574+ # that returns its parameter is NOT fresh, so a caller dropping its result is clean; the
1575+ # table must not fabricate ownership for a callee whose body we can see.
1576+ ov_fp = check_facts ({"module" : "M" , "functions" : [
1577+ {"name" : "File.OpenRead" , "file" : "B.cs" , "params" : [{"name" : "x" , "line" : 1 }],
1578+ "body" : [{"op" : "return" , "var" : "x" , "line" : 2 }]},
1579+ {"name" : "Caller" , "file" : "B.cs" , "body" : [
1580+ {"op" : "acquire" , "var" : "a" , "line" : 10 },
1581+ {"op" : "call" , "callee" : "File.OpenRead" , "args" : ["a" ],
1582+ "result" : "r" , "line" : 11 },
1583+ {"op" : "release" , "var" : "a" , "line" : 12 }]}]})
1584+ if ov_fp :
1585+ fails .append (f"Tier B: a first-party summary must override the BCL table, "
1586+ f"got { [(x .component , x .code ) for x in ov_fp ]} " )
1587+ checks += 1
1588+ # RECALL (Codex): a first-party wrapper that returns a BCL factory result is itself fresh,
1589+ # so a caller dropping `Make()` leaks OWN001 — the return skeleton propagates BCL freshness
1590+ # rather than degrading to a `forward` to the external factory (-> unknown -> invisible).
1591+ wrap = [(x .component , x .line , x .code ) for x in check_facts ({"module" : "M" , "functions" : [
1592+ {"name" : "Make" , "file" : "B.cs" , "body" : [
1593+ {"op" : "call" , "callee" : "File.OpenRead" , "args" : ["p" ],
1594+ "result" : "s" , "line" : 2 },
1595+ {"op" : "return" , "var" : "s" , "line" : 3 }]},
1596+ {"name" : "Caller2" , "file" : "B.cs" , "body" : [
1597+ {"op" : "call" , "callee" : "Make" , "args" : [], "result" : "r" , "line" : 10 }]}]})]
1598+ if wrap != [("Caller2" , 10 , "OWN001" )]:
1599+ fails .append (f"Tier B: a wrapper returning a BCL factory result must be fresh "
1600+ f"(caller leak OWN001@10), got { wrap } " )
15161601 # OVERWRITE kills the prior binding (CodeRabbit): `acquire x; x = Unknown(); release x`
15171602 # — the call's result reuses an owned local and the call is dropped (unknown callee),
15181603 # so the ORIGINAL x leaks (its reference is lost), not read as clean. The release after
0 commit comments