Skip to content

P-015: reachability codeFlows for flow-local + DI-sourced subscription findings #125

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
PhysShell merged 2 commits into from
Jun 26, 2026
Merged

P-015: reachability codeFlows for flow-local + DI-sourced subscription findings #125

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d43f89f
P-015: reachability codeFlows for flow-local + DI-sourced subscriptio…
claude Jun 26, 2026
dcd71a2
P-015: cover the OWN025 pooled-buffer Rent->view flow (CodeRabbit #125)
claude Jun 26, 2026
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
57 changes: 54 additions & 3 deletions ownlang/ownir.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1565,6 +1565,34 @@ def _handle_of(diag: object) -> str | None:
return subject.split("#", 1)[0]


# the violation-site label per flow-local code, for the 2-step "origin -> manifestation"
# reachability slice (P-015): the Rent/acquire site is where the resource came from, the
# diagnostic line is where the obligation is violated.
_FLOW_LOCAL_VIOLATION = {
"OWN002": "used here after it was released/returned",
"OWN003": "released/returned here a second time",
"OWN009": "may be used here after release on some path",
"OWN025": "viewed here at full length, past what it was rented for",
}


def _flow_local_steps(sub: dict[str, Any], code: str, dline: int,
pool: bool) -> tuple[tuple[str, int, str], ...]:
"""A reachability slice for a flow-local finding: the Rent/acquire site (where the
resource came from) -> the site where its obligation is violated (`dline`). Only the
use/return/view codes have a distinct second site; a plain leak (OWN001) is a single
point (the acquire itself) and gets no flow. Empty when a line is unknown or the two
sites coincide (then the primary location already says it all)."""
viol = _FLOW_LOCAL_VIOLATION.get(code)
acq = _as_int(sub.get("line", 0))
if viol is None or acq < 1 or dline < 1 or dline == acq:
return ()
f = str(sub.get("file", "?"))
name = sub.get("event", "?")
origin = f"rented '{name}' here" if pool else f"acquired '{name}' here"
return ((f, acq, origin), (f, dline, viol))


def check_facts(facts: dict[str, Any]) -> list[Finding]:
"""Run the core checker over the lowered facts and return findings mapped
back to their original C# locations (v0: the `event += without -=` leak).
Expand All @@ -1584,6 +1612,12 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]:
mod, handles = to_module(facts)
diags = check_module(mod)

# registration site of each DI service, to anchor a subscription-escape slice's
# source hop: the injected event SOURCE is a registered service (P-006 + P-004), so
# the reachability slice can point at where that longer-lived source was registered.
svc_loc = {str(s.get("name", "")): (str(s.get("file", "?")), _as_int(s.get("line", 0)))
for s in (facts.get("services") or []) if isinstance(s, dict)}

findings: list[Finding] = []
for d in diags:
if d.severity != Severity.ERROR:
Expand Down Expand Up @@ -1630,7 +1664,8 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]:
message=(f"pooled buffer '{name}' is viewed at its full "
f"length, past the logical length it was rented for "
f"(over-read / over-clear)"),
kind="pooled buffer"))
kind="pooled buffer",
flow=_flow_local_steps(sub, d.code, d.line, True)))
continue
# An ArrayPool Rent is released by Return (a "pooled buffer"), not Dispose (a
# "disposable"); the extractor stamps the acquire's kind so the flow path words
Expand Down Expand Up @@ -1669,7 +1704,8 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]:
findings.append(Finding(
file=sub["file"], line=int(sub.get("line", 0)), code=d.code,
component=component, event=name, handler="", message=msg,
kind="pooled buffer" if pool else "disposable"))
kind="pooled buffer" if pool else "disposable",
flow=_flow_local_steps(sub, d.code, d.line, bool(pool))))

@chatgpt-codex-connector chatgpt-codex-connector Bot Jun 26, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Preserve distinct flow-local violation sites

When the same local has multiple violations with the same acquire site, code, and message, this newly added flow is the only field that distinguishes them, but the later de-duplication key does not include flow. For example, acquire s; release s; use s on line 3; use s on line 4 produces two core OWN002 diagnostics, yet check_facts keeps only the first flow and silently drops the second violation site, so SARIF points to only one bad use.

Useful? React with 👍 / 👎.

@PhysShell PhysShell Jun 26, 2026

Copy link
Copy Markdown
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Declining — the premise doesn't reproduce. Two checks:

1. The core emits one OWN002 per local, not two. The loan/permission model reports use-after-release once (at the first offending use), so there is no second finding to drop. Verified on exactly your scenario:

acquire s @3; release s @4; use s @5; use s @6
→ check_facts returns 1 finding:
   OWN002 anchor 3 | "IDisposable local 's' is used after it is disposed"
   flow: (F.cs:3 "acquired 's' here", F.cs:5 "used here after it was released/returned")

The second use @6 was already not separately reported before this PR — that's pre-existing precision-first behaviour, unrelated to flow.

2. There is no flow-blind de-duplication. Neither check_facts nor build_sarif dedupes findings — every diagnostic becomes its own Finding and every Finding its own SARIF result. So even if two identical-except-flow findings did arise, both would be emitted; nothing is silently collapsed.

So no behaviour change is needed here. (Reporting all use-after-release sites for one local would be a deliberate change to the core analysis's one-finding-per-variable policy — out of scope for this slice, and a separate precision/noise tradeoff.)

Generated by Claude Code

continue
if sub.get("di_source_life"):
# OWN014 region escape sourced from the DI graph (P-006 + P-004): the
Expand All @@ -1690,10 +1726,25 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]:
f"subscription promotes '{component}' to the source's "
f"lifetime, so it can never be collected — a captive/region "
f"escape (leak, no release path)")
# reachability slice: the subscribe site -> where the longer-lived source was
# registered (its lifetime is why this escapes). The source hop is present only
# when the registration site is known from the services graph.
sub_ln = _as_int(sub.get("line", 0))
esc_flow: tuple[tuple[str, int, str], ...] = ()
if sub_ln >= 1:
steps = [(str(sub["file"]), sub_ln,
f"'{component}' subscribes '{event}' to '{st}' here")]
sf, sl = svc_loc.get(st, ("?", 0))
if sl >= 1:
steps.append((sf, sl,
f"source '{st}' ({life}) registered here — outlives "
f"'{component}'"))
if len(steps) >= 2:
esc_flow = tuple(steps)
findings.append(Finding(
file=sub["file"], line=int(sub.get("line", 0)), code=d.code,
component=component, event=event, handler=handler,
message=message, kind="subscription token"))
message=message, kind="subscription token", flow=esc_flow))
continue
if rkind == "capture":
# OWN014 region escape (P-004): the lifetime engine proved the event
Expand Down
36 changes: 36 additions & 0 deletions tests/test_ownir.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1098,6 +1098,24 @@ def _sub(source: str | None) -> list[Finding]:
if [(x.code, x.severity) for x in warn] != [("OWN001", "warning")]:
fails.append(f"injected sub without DI info should stay an OWN001 warning, "
f"got {[(x.code, x.severity) for x in warn]}")
# P-015: a DI-sourced subscription escape (OWN014) carries a CROSS-FILE slice — the
# subscribe site -> where the longer-lived source service was registered (its lifetime
# is *why* the subscriber escapes). The source hop comes from the services graph.
checks += 1
esc = check_facts({"ownir_version": 0, "module": "M", "functions": [],
"components": [{"name": "Vm", "file": "VM.cs", "subscriptions": [
{"event": "bus.Tick", "handler": "OnTick", "line": 11, "released": False,
"resource": "subscription", "source": "injected", "source_type": "IBus"}]}],
"services": [
{"name": "IBus", "lifetime": "singleton", "deps": [],
"file": "Startup.cs", "line": 7},
{"name": "Vm", "lifetime": "transient", "deps": ["IBus"],
"file": "Startup.cs", "line": 8}]})
e14 = next((x for x in esc if x.code == "OWN014"), None)
if e14 is None or e14.flow != (
("VM.cs", 11, "'Vm' subscribes 'bus.Tick' to 'IBus' here"),
("Startup.cs", 7, "source 'IBus' (singleton) registered here — outlives 'Vm'")):
fails.append(f"DI-source OWN014 escape flow wrong: {e14.flow if e14 else None!r}")

# --- P-006/2b: COMPOSITIONAL ownership transfer through the bridge. A C#
# method's ownership contract (a `consume`/`borrow` parameter) lowers to a
Expand Down Expand Up @@ -1130,6 +1148,15 @@ def _sub(source: str | None) -> list[Finding]:
and "[resource: disposable]" in run_f[0].render()):
fails.append(f"use-after-handoff should read as use-after-disposal, got "
f"{[x.render() for x in run_f]}")
checks += 1
# P-015: the flow-local finding carries a reachability slice — where the resource was
# acquired -> where it is used after its obligation moved (the precise violation line the
# primary anchor, at the acquire, does not itself show).
if not run_f or run_f[0].flow != (
("Archiver.cs", 24, "acquired 's' here"),
("Archiver.cs", 26, "used here after it was released/returned")):
fails.append(f"flow-local OWN002 reachability flow wrong: "
f"{run_f[0].flow if run_f else None!r}")

# regression (codex review): an undischarged `consume` parameter must MAP to a
# finding AT the parameter, not crash check_facts. Before params carried an
Expand Down Expand Up @@ -1679,6 +1706,15 @@ def _sub(source: str | None) -> list[Finding]:
fails.append(f"an `overspan` fact should raise OWN025 at the view line (12) "
f"tagged a pooled buffer, got "
f"{[(x.code, x.line, x.kind) for x in osp]}")
checks += 1
# P-015: the OWN025 slice runs Rent site -> view site (the primary anchor is the VIEW
# at line 12, but the flow's first hop is the Rent at line 10) — the pooled-buffer
# branch's own flow path, distinct from the OWN002 case above.
if not osp or osp[0].flow != (
("Framer.cs", 10, "rented 'buf' here"),
("Framer.cs", 12, "viewed here at full length, past what it was rented for")):
fails.append(f"OWN025 Rent->view reachability flow wrong: "
f"{osp[0].flow if osp else None!r}")

# --- output surfaces (Уровень 1): the same finding renders for a human, a
# GitHub annotation, and an MSBuild/VS Error List line. The format lives
Expand Down
Loading