From fcebbdd27ac6b77638288b0d01e3c703dff65ce2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 10:15:57 +0000 Subject: [PATCH 1/9] =?UTF-8?q?ownir:=20harden=20the=20C#=E2=86=92core=20s?= =?UTF-8?q?eam=20before=20expanding=20the=20extractor?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three structural fixes to the OwnIR bridge so adding patterns (timers, IDisposable fields, region/escape facts) is additive rather than a rewrite: - Map verdicts back to C# by Diagnostic.subject (a structured name#line identity), not by regex-scraping the human message. Generic `acquire` now stamps `sym.origin` like buffers already did, so OWN001 on a subscription carries its handle. Changing a message no longer silently drops a finding. - Fail loudly instead of silently dropping: any error the core reports on the lowered facts that the bridge cannot attribute to a known handle now raises OwnIRError with an actionable message — a swallowed leak is the worst outcome for a leak checker. - Version the fact contract (`ownir_version`/OWNIR_VERSION). The extractor stamps it and the core rejects a mismatch at load with a clear message, rather than mis-reading a drifted vocabulary. Malformed JSON and bad facts now surface as one-line CLI errors, not tracebacks. Also split __main__.check_module out of _collect as the AST-level entry to the one checker, so the next pattern can build a Module directly instead of re-serialising to .own text and re-parsing it. --- docs/proposals/P-001-csharp-extractor.md | 11 ++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 4 +- ownlang/__main__.py | 43 ++++++--- ownlang/cfg.py | 5 + ownlang/ownir.py | 94 ++++++++++++++++--- tests/fixtures/ownir/sample.facts.json | 1 + tests/test_ownir.py | 38 +++++++- 7 files changed, 162 insertions(+), 34 deletions(-) diff --git a/docs/proposals/P-001-csharp-extractor.md b/docs/proposals/P-001-csharp-extractor.md index b7cd1792..da58ec5b 100644 --- a/docs/proposals/P-001-csharp-extractor.md +++ b/docs/proposals/P-001-csharp-extractor.md @@ -84,7 +84,14 @@ CI-validated C# artifact (like the golden). Land **one pattern** first ## Open questions -1. **Seam:** confirm `C# extractor → OwnIR → Python core` (vs all-in-C#). +1. ~~**Seam:** confirm `C# extractor → OwnIR → Python core` (vs all-in-C#).~~ + **Resolved:** extractor → versioned OwnIR JSON → Python core. The core also + exposes an AST-level entry (`__main__.check_module`) so the next pattern can + build a module directly instead of round-tripping through `.own` text. 2. **v0 scope:** one pattern first, or the four-rule set in one go. -3. **OwnIR serialization:** JSON schema vs emitting `.own` directly. +3. ~~**OwnIR serialization:** JSON schema vs emitting `.own` directly.~~ + **Resolved:** JSON, stamped with `ownir_version` (`OWNIR_VERSION`, currently + 0). A mismatched extractor/core pair fails loudly at load instead of being + silently mis-read; the bridge maps verdicts back to C# by the diagnostic's + structured `subject`, not by scraping the human message. 4. Heuristic vs annotation for "this class is a lifetime-bound component". diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 3d70b221..21ee0762 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -74,7 +74,9 @@ static int LineOf(SyntaxNode node) => } } -var facts = new { module = "Extracted", components }; +// ownir_version stamps the fact-schema vocabulary; the Python core rejects a +// mismatch loudly (ownlang/ownir.py OWNIR_VERSION) rather than mis-reading facts. +var facts = new { ownir_version = 0, module = "Extracted", components }; var json = JsonSerializer.Serialize(facts, new JsonSerializerOptions { WriteIndented = true }); if (outPath is null) Console.WriteLine(json); diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 5dd8a7c9..382ba69d 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -29,25 +29,33 @@ from .report import build_report, render_report -def _collect(src: str) -> tuple[list[Diagnostic], object | None]: - try: - mod = parse(src) - except (ParseError, LexError) as e: - line = getattr(e, "line", 0) - return [Diagnostic("OWN020", str(e).split(": ", 1)[-1], line)], None - rnames = {r.name for r in mod.resources} - sigs = collect_signatures(mod) - pols = collect_policies(mod) - kinds = collect_kinds(mod) +def check_module(mod: object) -> list[Diagnostic]: + """Run the full ownership pipeline over an already-parsed module and return + its diagnostics. This is the AST-level entry to the *one* checker: callers + that already hold a `Module` (the OwnIR bridge lowers facts straight to one) + use this instead of re-serialising to source text and re-parsing it.""" + rnames = {r.name for r in mod.resources} # type: ignore[attr-defined] + sigs = collect_signatures(mod) # type: ignore[arg-type] + pols = collect_policies(mod) # type: ignore[arg-type] + kinds = collect_kinds(mod) # type: ignore[arg-type] diags: list[Diagnostic] = list(validate_policies(pols)) - diags.extend(check_lifetimes(mod)) - for fn in mod.functions: + diags.extend(check_lifetimes(mod)) # type: ignore[arg-type] + for fn in mod.functions: # type: ignore[attr-defined] cfg, d1 = build_cfg(fn, rnames, sigs, pols, kinds) d2 = analyze(cfg) diags.extend(d1) diags.extend(d2) diags.sort(key=lambda d: (d.line, d.code)) - return diags, mod + return diags + + +def _collect(src: str) -> tuple[list[Diagnostic], object | None]: + try: + mod = parse(src) + except (ParseError, LexError) as e: + line = getattr(e, "line", 0) + return [Diagnostic("OWN020", str(e).split(": ", 1)[-1], line)], None + return check_module(mod), mod def cmd_check(path: str) -> int: @@ -176,8 +184,13 @@ def _read(path: str) -> str: def cmd_ownir(path: str) -> int: """Check OwnIR facts (extracted from real C# by the Roslyn frontend) through the same core, surfacing findings at their C# locations (P-001).""" - from .ownir import check_facts, load - findings = check_facts(load(path)) + from .ownir import OwnIRError, check_facts, load + try: + findings = check_facts(load(path)) + except OwnIRError as e: + # bad facts / a drifted contract: a clear one-liner, not a traceback. + print(f"{path}: error: {e}", file=sys.stderr) + return 2 for f in findings: print(f.render()) if not findings: diff --git a/ownlang/cfg.py b/ownlang/cfg.py index cd7c0ec1..e072e6d7 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -350,6 +350,11 @@ def lower_let(self, st: A.Let, cur: Block) -> Block: sym = self.declare(st.name, Kind.OWNED, st.line) sym.type_name = rhs.resource sym.resource_kind = self.resource_kinds.get(rhs.resource) + # a stable identity (name#line) so a diagnostic about this resource + # can be attributed structurally — by Diagnostic.subject — instead of + # by scraping the name out of the human message. The OwnIR bridge keys + # its C#-location map off exactly this (see ownir.check_facts). + sym.origin = f"{st.name}#{rhs.line}" cur.instrs.append(Acquire(sym, rhs.resource, st.line)) return cur if isinstance(rhs, A.BufferIntent): diff --git a/ownlang/ownir.py b/ownlang/ownir.py index e3ef5446..14c86af3 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -9,6 +9,7 @@ OwnIR v0 schema (JSON):: { + "ownir_version": 0, "module": "WpfApp", "components": [ { @@ -37,7 +38,19 @@ from dataclasses import dataclass from typing import Any -from .diagnostics import _SUBJECT_RE, Severity +from .diagnostics import Severity + +# The OwnIR schema version this core understands. Bump it whenever the fact +# vocabulary changes incompatibly; the extractor stamps the same number so a +# mismatched extractor/core pair fails loudly (see load()) instead of silently +# mis-reading facts. +OWNIR_VERSION = 0 + + +class OwnIRError(ValueError): + """A malformed or unmappable OwnIR fact set. Carries a human message; the + driver turns it into a clear one-line error rather than a traceback.""" + _PRELUDE = ( 'resource Subscription {\n' @@ -67,16 +80,32 @@ def load(path: str) -> dict[str, Any]: """Load and shape-check an OwnIR facts file (it is external input — a malformed file should fail with a clear error, not a deep traceback).""" with open(path, encoding="utf-8") as f: - result: Any = json.load(f) + try: + result: Any = json.load(f) + except json.JSONDecodeError as e: + raise OwnIRError(f"{path} is not valid JSON: {e}") from e if not isinstance(result, dict): - raise ValueError("OwnIR root must be a JSON object") + raise OwnIRError("OwnIR root must be a JSON object") + # version gate first: a vocabulary mismatch makes every later shape-check + # meaningless, so reject it up front with an actionable message. An absent + # field is treated as the current version (the only producers that omit it + # predate versioning, i.e. are v0 by definition). + ver = result.get("ownir_version", OWNIR_VERSION) + if not isinstance(ver, int) or isinstance(ver, bool): + raise OwnIRError(f"OwnIR 'ownir_version' must be an integer, got {ver!r}") + if ver != OWNIR_VERSION: + raise OwnIRError( + f"OwnIR facts are schema v{ver}, but this core understands " + f"v{OWNIR_VERSION}. Build the Roslyn extractor and the Python core " + f"from the same commit — the OwnIR fact vocabulary changed between " + f"the version that produced this file and the one reading it.") comps = result.get("components", []) if not isinstance(comps, list) or not all(isinstance(c, dict) for c in comps): - raise ValueError("OwnIR 'components' must be a JSON array of objects") + raise OwnIRError("OwnIR 'components' must be a JSON array of objects") for c in comps: subs = c.get("subscriptions", []) if not isinstance(subs, list) or not all(isinstance(s, dict) for s in subs): - raise ValueError("each component's 'subscriptions' must be objects") + raise OwnIRError("each component's 'subscriptions' must be objects") return result @@ -92,18 +121,18 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: gid = 0 components = facts.get("components", []) if not isinstance(components, list): - raise ValueError("OwnIR 'components' must be a JSON array") + raise OwnIRError("OwnIR 'components' must be a JSON array") for comp in components: if not isinstance(comp, dict): - raise ValueError("each OwnIR component must be a JSON object") + raise OwnIRError("each OwnIR component must be a JSON object") cname = comp.get("name", f"Component{gid}") lines.append(f"fn {cname}() {{") subscriptions = comp.get("subscriptions", []) if not isinstance(subscriptions, list): - raise ValueError("component 'subscriptions' must be a JSON array") + raise OwnIRError("component 'subscriptions' must be a JSON array") for sub in subscriptions: if not isinstance(sub, dict): - raise ValueError("each subscription must be a JSON object") + raise OwnIRError("each subscription must be a JSON object") handle = f"sub_{gid}" gid += 1 handles[handle] = {**sub, "component": cname, @@ -116,22 +145,57 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: return "\n".join(lines), handles +def _handle_of(diag: object) -> str | None: + """The synthetic handle (`sub_N`) a diagnostic is about, recovered from its + structured `subject` (`name#line`) — NOT by scraping the human message. Each + acquire stamps `subject` in cfg.lower_let; None means the diagnostic carries + no subject identity at all.""" + subject = getattr(diag, "subject", None) + if not subject: + return None + return subject.split("#", 1)[0] + + 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).""" - # imported here to avoid a module-level cycle (ownir is a leaf consumer) + back to their original C# locations (v0: the `event += without -=` leak). + + The fact->handle->diagnostic round-trip is fully ours: every error the core + reports on the lowered module MUST attribute to a known subscription handle. + If one does not, the lowering has drifted from the core (or the core grew a + diagnostic the bridge has not been taught to map) — we raise rather than + silently dropping a real finding, since a swallowed leak is the worst + outcome for a leak checker.""" + # imported here to avoid a module-level cycle (ownir is a leaf consumer). + # v0 lowers to `.own` text and goes through _collect (parse + the one + # checker). The next pattern (timers / region facts with no surface syntax) + # builds a Module and calls __main__.check_module directly instead — the + # seam is already split so that switch is additive, not a rewrite. from .__main__ import _collect src, handles = to_own(facts) - diags, _ = _collect(src) + diags, mod = _collect(src) + if mod is None: + # the only source here is our own generator, so a parse failure is an + # internal bug in to_own, not bad user input — surface it loudly. + msg = diags[0].message if diags else "unknown parse error" + raise OwnIRError( + f"internal: the lowered OwnIR module did not parse ({msg}). " + f"This is a bug in the fact lowering, not in the facts.") + findings: list[Finding] = [] for d in diags: if d.severity != Severity.ERROR: continue - m = _SUBJECT_RE.search(d.message) - sub = handles.get(m.group(1)) if m else None + sub = handles.get(_handle_of(d) or "") if sub is None: - continue + raise OwnIRError( + f"internal: the core reported [{d.code}] on the lowered facts " + f"that the bridge cannot map back to a C# subscription " + f"(subject={getattr(d, 'subject', None)!r}, " + f"message={d.message!r}). The OwnIR lowering has drifted from " + f"the core; teach the bridge this diagnostic rather than " + f"dropping the finding.") findings.append(Finding( file=sub["file"], line=int(sub.get("line", 0)), code=d.code, component=sub["component"], event=sub.get("event", "?"), diff --git a/tests/fixtures/ownir/sample.facts.json b/tests/fixtures/ownir/sample.facts.json index c92a4d69..baced1c5 100644 --- a/tests/fixtures/ownir/sample.facts.json +++ b/tests/fixtures/ownir/sample.facts.json @@ -1,4 +1,5 @@ { + "ownir_version": 0, "module": "WpfApp", "components": [ { diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 0893577f..8b9d9de1 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -23,13 +23,31 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang.ownir import check_facts, to_own +import tempfile + +from ownlang.ownir import OWNIR_VERSION, OwnIRError, check_facts, load, to_own from ownlang.parser import parse _FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "sample.facts.json") +def _write_facts(obj: dict) -> str: + """Write a facts dict to a temp file and return its path (load() needs one).""" + fd, path = tempfile.mkstemp(suffix=".facts.json") + with os.fdopen(fd, "w", encoding="utf-8") as f: + json.dump(obj, f) + return path + + +def _load_raises(obj: dict) -> bool: + try: + load(_write_facts(obj)) + except OwnIRError: + return True + return False + + def run() -> int: """Pin the OwnIR bridge on the canonical leak/ok facts; return 0/1.""" fails: list[str] = [] @@ -73,6 +91,24 @@ def run() -> int: if check_facts({"module": "Empty", "components": []}): fails.append("empty facts produced findings") + # the fixture carries the current schema version (the contract is stamped). + checks += 1 + if facts.get("ownir_version") != OWNIR_VERSION: + fails.append("fixture is missing the current ownir_version stamp") + + # a future/foreign schema version must fail loudly at load, not be misread. + checks += 1 + bad = {"ownir_version": OWNIR_VERSION + 1, "module": "Future", "components": []} + if not _load_raises(bad): + fails.append("mismatched ownir_version did not raise OwnIRError") + + # an omitted version is accepted as the current one (legacy v0 producers). + checks += 1 + try: + load(_write_facts({"module": "Legacy", "components": []})) + except OwnIRError as e: + fails.append(f"versionless facts wrongly rejected: {e}") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From 903eb4055c5c2bdad23c2a8292a388fe5dce93cd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 13:49:22 +0000 Subject: [PATCH 2/9] docs: capture the project-direction brainstorm as a roadmap + proposals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A long design discussion covered far more ground than the current spec/ proposals reflect, and such threads evaporate. Systematise it so every idea raised is on the record for consideration (drafts, not commitments). - docs/ROADMAP.md — the strategy hub: the one-sentence pitch, design philosophy (one checker; bug-driven expansion; narrow intraprocedural C# frontend), P0–P3 priorities, the five milestones, the "what static analysis can/can't catch" reality matrix, why not a full Rust-style borrow checker, and an honesty note on the (proxy, not measured) error statistics. - P-004 WPF/UI lifetime leak profile (extends P-001: timers, IDisposable subscription fields, ignored Subscribe, escape→OWN014). - P-005 IDisposable ownership profile (local/field not disposed, double dispose, use-after-dispose, transfer). - P-006 DI lifetime / captive dependency (DI001–003; WeakReference is not the fix; IServiceScopeFactory remedy). - P-007 ArrayPool/Span borrow-view profile (POOL001–005; replay corpus). - P-008 Effects & resources (declared use !Db/Log/Clock, capabilities, layer policies; Wybe/Plasma/Mercury/Clean background). - P-009 No-GC / allocation-free regions (OwnNoGc policy; OWN-GC001–007). - P-010 Richer type disciplines (branded/refinement/units/typestate now; dependent/GADT/HKT/row/existential/modal deferred). - P-011 Editor tooling & syntax highlighting (TextMate → CLI JSON → LSP → semantic tokens → tree-sitter). - P-012 Real-world bug corpus & GitHub/Roslyn mining pipeline. - proposals/README.md index updated; all link back to ROADMAP. Docs only — no code or behaviour change. --- docs/ROADMAP.md | 157 +++++++++++++++++ docs/proposals/P-004-wpf-lifetime-profile.md | 88 ++++++++++ docs/proposals/P-005-idisposable-ownership.md | 85 +++++++++ docs/proposals/P-006-di-lifetimes.md | 84 +++++++++ docs/proposals/P-007-arraypool-span.md | 88 ++++++++++ docs/proposals/P-008-effects-and-resources.md | 163 ++++++++++++++++++ docs/proposals/P-009-nogc-regions.md | 142 +++++++++++++++ docs/proposals/P-010-type-disciplines.md | 157 +++++++++++++++++ docs/proposals/P-011-editor-tooling.md | 124 +++++++++++++ docs/proposals/P-012-bug-corpus-mining.md | 137 +++++++++++++++ docs/proposals/README.md | 14 ++ 11 files changed, 1239 insertions(+) create mode 100644 docs/ROADMAP.md create mode 100644 docs/proposals/P-004-wpf-lifetime-profile.md create mode 100644 docs/proposals/P-005-idisposable-ownership.md create mode 100644 docs/proposals/P-006-di-lifetimes.md create mode 100644 docs/proposals/P-007-arraypool-span.md create mode 100644 docs/proposals/P-008-effects-and-resources.md create mode 100644 docs/proposals/P-009-nogc-regions.md create mode 100644 docs/proposals/P-010-type-disciplines.md create mode 100644 docs/proposals/P-011-editor-tooling.md create mode 100644 docs/proposals/P-012-bug-corpus-mining.md diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md new file mode 100644 index 00000000..750d44b9 --- /dev/null +++ b/docs/ROADMAP.md @@ -0,0 +1,157 @@ +# Own.NET — roadmap & idea backlog + +The strategy hub. `spec/` is normative (what is true today, pinned by tests); +`docs/proposals/` are exploratory designs; **this file** is the map over them: +priorities, milestones, the framing, the design philosophy, and — most importantly +— a place where every idea raised in design discussion is *written down so it does +not evaporate*. An idea here is "on the record for consideration", not a +commitment. When an idea earns a design, it becomes a `P-NNN` proposal; when a +proposal ships, its behaviour moves into `spec/`. + +## The framing (the one-sentence pitch) + +The first public pitch is **not** "we're building a borrow checker for C#". It is: + +> **Own.NET finds lifetime/resource bugs that C# cannot express:** WPF/event +> leaks, missing `Dispose`, DI lifetime mismatch, and pooled-buffer misuse. + +That is concrete, painful, and shippable without a five-year R&D detour. The +borrow checker is the *first combat module*, not the whole universe. The +long-term identity the backlog is aiming at: + +> **An external static-contract layer for C#/.NET** that adds ownership, +> typestate, effects, capabilities, and domain-specific types **without +> rewriting the codebase.** + +## Design philosophy (the load-bearing constraints) + +- **One checker.** The Python core in `ownlang/` is the single source of truth. + Every frontend (the `.own` DSL, the Roslyn C# extractor of P-001, anything + later) *produces or consumes OwnIR facts* in the spec's vocabulary. A second + checker would drift — the project's own meta-irony. +- **Bug-driven expansion.** Do not support a C#/.NET feature because the platform + has it. Support it because a *real bug* needs it. "We supported 40% of the + language and found zero bugs" is the failure mode we are avoiding. + - Concretely: prove Own.NET finds **one** real memory/resource bug in real C#, + then widen the frontend to fit exactly the next real bug. +- **Narrow C# frontend, intraprocedural first.** The frontend's job is not to + "understand C#" (SemanticModel hides async, generics, LINQ, closures, pattern + matching, overload resolution, nullable flow, source generators…). Its job is + to extract *facts*: acquire / borrow / use / release / escape / control-flow. +- **Refuse the soul-eating version.** Every proposal's Non-goals section is the + most important one. Boredom keeps projects alive. + +### What the C# frontend deliberately does NOT touch yet + +`async`/`await`, full generics, LINQ, closures/lambdas, interprocedural analysis, +virtual dispatch, whole-program analysis, source generators, `unsafe` pointer +arithmetic, the XAML/binding engine. Not "never" — just not *before* the tool has +found its first real bug. An `async` method in v0 is honestly skipped (or flagged +"unsupported"), because honestly skipping beats confidently lying; the market for +confident-but-wrong tooling is already saturated. + +## Priorities + +Targets are ranked by four criteria: (1) the pain is frequent or expensive, +(2) it is at least partly catchable *statically*, (3) it maps cleanly onto +ownership/lifetime/effects, (4) an MVP needs no PhD in Roslyn. + +| Tier | Targets | Proposal | +|------|---------|----------| +| **P0** | WPF/event/timer/subscription leaks; `IDisposable` ownership (leaks, fields, use-after-dispose); DI lifetime mismatch (captive dependency) | [P-004](proposals/P-004-wpf-lifetime-profile.md), [P-005](proposals/P-005-idisposable-ownership.md), [P-006](proposals/P-006-di-lifetimes.md) | +| **P1** | ArrayPool/Span ownership-view bugs; hidden effects / architecture rules | [P-007](proposals/P-007-arraypool-span.md), [P-008](proposals/P-008-effects-and-resources.md) | +| **P2** | async resource lifecycle; `ValueTask` affine usage; typestate/protocols | [P-008](proposals/P-008-effects-and-resources.md), [P-010](proposals/P-010-type-disciplines.md) | +| **P3** | LOH fragmentation; static-collection memory bloat; cross-thread `ObjectDisposedException` | — (runtime-bound; see detectability matrix) | + +**The five concrete diagnostics to build first** (balanced across real pain, +architectural strictness, and the borrow-checker showcase): + +1. `WPF001` — event/subscription `+=` without `-=` (the WPF spike; P-001 v0 ✅) +2. `WPF002` — `DispatcherTimer` started/subscribed without stop/unsubscribe +3. `BOR/OWN` — `IDisposable` field not disposed by its owner +4. `DI001` — singleton captures a scoped dependency +5. `POOL` — `Span`/view used after `ArrayPool.Return` + +### Milestones + +1. **WPF leak spike** — find 1–3 real subscription/timer leaks in real code (P-004). +2. **Resource core** — generalise WPF subscriptions + `IDisposable` into one + acquire/release/owner/release-region model (P-004 ∪ P-005), so WPF is a + *profile*, not a one-off. +3. **DI lifetimes** — registration + constructor graph; captive dependency (P-006). +4. **Pool/Span** — `Rent`/`Return`, borrowed views, return-invalidates-views, + known-bug replay corpus (P-007). The borrow checker on stage at full height. +5. **Effects** — `pure` / `use !Db` / `use !Log` / `use Clock`, layer policies + (P-008). The architectural X-ray — landed *after* the leak checkers prove value. + +## What static analysis can and cannot catch (the reality matrix) + +A checker scope must respect this. The corpus (P-012) tags every case by which +bucket it falls in, so we never promise a runtime-only bug to a static checker. + +| Bug class | Static (Roslyn) | Why | +|-----------|-----------------|-----| +| Captive dependency (singleton→scoped) | ✅ deterministic | visible in the type/registration graph | +| Missing `Dispose` (local / field) | ✅ deterministic | a missing call is structurally visible | +| `ArrayPool.Rent` without `Return` (one method) | ✅ deterministic | both calls in one CFG | +| Simple use-after-dispose (one method) | ✅ deterministic | `x.Dispose(); x.Use();` is visible | +| `event +=` without `-=` | ⚠️ heuristic | depends on object lifetime → warn only in long-lived owners; false positives | +| Ownership transfer through a callee | ⚠️ heuristic | `ProcessStream(s)` may dispose internally | +| Cross-thread `ObjectDisposedException` | ❌ impossible | a happens-before race, not a structure | +| LOH fragmentation | ❌ impossible | depends on runtime data volume / GC timing | +| Static-collection memory bloat | ❌ impossible | depends on business data, not code shape | +| Unmanaged cyclic refs / `AllocHGlobal` freed on all paths | ❌ ~impossible | needs whole-program flow we don't have | + +Static analysis is the first line of defence (it stops the dumb bugs early); real +production leaks still need profilers (dotMemory, PerfView) and dump analysis. +Say so honestly in any talk/README. + +## Why not a full Rust-style borrow checker for C# + +Worth stating because people ask. It is not (mainly) reimplementable wholesale, +for three structural reasons: + +1. **GC philosophy conflict.** C# was designed so the programmer need not think + about memory. A full ownership/lifetime regime would make the GC redundant — + and turn everyday C# into a fight with the checker (lifetimes on nearly every + variable). Own.NET instead checks *narrow regions and explicit resources*, + leaving the GC to do the rest. +2. **`IDisposable` is a pattern, not a language rule.** To the C# compiler, + `.Dispose()` is just a method; the object is still valid afterwards. Making + `Dispose()` "kill" a variable at the type level would change the language + semantics and break billions of lines. Own.NET supplies that *typestate* + externally instead (P-005, P-010). +3. **Dynamism.** Objects live on the heap, reachable from many places; DI + containers and reflection build dependency graphs the compiler cannot trace. + Ownership analysis is happiest where the dependency tree is clear, which is why + the frontend stays narrow and fact-based. + +Note the platform is already moving this way — `Span`, `Memory`, `ref +struct` are "Rust strictness, C# ergonomics", compiler-checked escape rules. +Own.NET is complementary: the contracts the compiler still cannot express. + +## A note on "top .NET errors" statistics + +There is no good *public* dataset of real .NET production crashes — it lives in +private dashboards. Any prioritisation numbers in these proposals are **proxy / +hypothesis estimates**, drawn from analyzer rules, exception docs, DI guidance and +issue-tracker keyword frequency — *not* measured statistics. The job of the +mining pipeline (P-012) is to *replace* those guesses with real counts from our +own scan. Label them as estimates wherever they appear. + +## Proposal index (every track on the record) + +| # | Track | Tier | Status | +|---|-------|------|--------| +| [P-001](proposals/P-001-csharp-extractor.md) | C# → OwnIR extractor (WPF leak spike) | P0 | in progress (v0 built) | +| [P-002](proposals/P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | horizon | draft | +| [P-003](proposals/P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | horizon | draft | +| [P-004](proposals/P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | P0 | draft | +| [P-005](proposals/P-005-idisposable-ownership.md) | `IDisposable` ownership profile | P0 | draft | +| [P-006](proposals/P-006-di-lifetimes.md) | DI lifetime / captive dependency | P0 | draft | +| [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | draft | +| [P-008](proposals/P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | P1/P2 | draft | +| [P-009](proposals/P-009-nogc-regions.md) | No-GC / allocation-free regions | horizon | draft | +| [P-010](proposals/P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | P2/horizon | draft | +| [P-011](proposals/P-011-editor-tooling.md) | Editor tooling & syntax highlighting | side-track | draft | +| [P-012](proposals/P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | enabling | draft | diff --git a/docs/proposals/P-004-wpf-lifetime-profile.md b/docs/proposals/P-004-wpf-lifetime-profile.md new file mode 100644 index 00000000..6f5dc899 --- /dev/null +++ b/docs/proposals/P-004-wpf-lifetime-profile.md @@ -0,0 +1,88 @@ +# P-004 — WPF / UI lifetime leak profile + +- **Status:** draft (P0 — the user's real pain; extends P-001 v0) +- **Depends on:** [P-001](P-001-csharp-extractor.md) (the extractor + OwnIR seam), + `spec/OwnCore.md`, `spec/Lifetimes.md` (OWN001 leak, OWN014 region escape). + See [`docs/ROADMAP.md`](../ROADMAP.md) for where this sits (Milestones 1–2). + +## Motivation + +The most emotionally useful result Own.NET can produce is not "our DSL correctly +rejected release-after-move" — it is **"Own.NET found a potential memory leak in +*our real* WPF code"**. Desktop XAML apps leak the same way over and over: a +short-lived View/ViewModel subscribes to a long-lived source and is never +collected. The platform's analyzers mostly stay silent here. + +P-001 v0 already lands the first pattern (`event += without -=`) end-to-end. This +proposal is the rest of the WPF *profile*: the small set of C# patterns that +actually kill memory, expressed as ordinary resource facts so they reuse the one +core, not a bespoke "WPF engine". + +## Scope (the four-rule profile) + +Recognised in classes that look like lifetime-bound components (heuristic: name +ends `ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements +`INotifyPropertyChanged`): + +| Rule | Pattern | Core verdict | +|------|---------|--------------| +| **WPF001** | `source.Event += handler` with no matching `-=` in `Dispose`/`OnClosed`/`Unloaded` | `OWN001` (leak) ✅ v0 | +| **WPF002** | `DispatcherTimer`/`Timer` started (`Tick +=` / `Start()`) with no `Stop()` + detach | `OWN001` | +| **WPF003** | an `IDisposable` subscription field never disposed by the owner | `OWN001` (see P-005) | +| **WPF004** | `Subscribe(...)` whose `IDisposable` result is ignored | `OWN001` | +| **WPF005** | strong capture by a longer-lived source (the ViewModel `escapes` to App) | `OWN014` | + +Modelled as resource facts (no new magic — the resource is just named +`Subscription`): + +```text +event += -> acquire(Subscription, loc) +event -= -> release(Subscription, loc) +token.Dispose() -> release(Subscription, loc) +owner(this, Subscription) +escapes(this, App) -> a strong capture by a longer-lived source (feeds OWN014) +Dispose/OnClosed/Unloaded -> a permitted release region +``` + +The corpus already pins three of these against real core codes: +`corpus/wpf/zombie-viewmodel` (OWN001), `viewmodel-escapes-to-app` (OWN014), +`handler-use-after-dispose` (OWN002). WPF004/WPF005 are the increments that emit +the `Subscribe`-result and `escapes(...)`/lifetime facts the extractor does not +emit yet. + +## Non-goals + +XAML analysis, the binding engine, the visual tree, routed events, dependency +properties, `WeakEventManager` inference, Rx beyond `IDisposable`, and every +event-aggregator library in existence. That road ends in a +2400-line PR where +codegen double-returns an `ArrayPool`, only now with `DispatcherObject`. A +`[OwnIgnore("source lifetime is shorter")]` attribute is the escape hatch. + +## Sketch + +The seam is already built (P-001): Roslyn extractor → versioned OwnIR JSON → +core → diagnostic at the C# line. This profile = (a) more `acquire`/`release` +pattern matchers in the extractor (timer start/stop, ignored `Subscribe` result, +disposable subscription field), and (b) emitting the `owner`/`escapes` lifetime +facts so OWN014 fires for WPF005. + +```text +*.cs --[extractor: += / Tick+Start / Subscribe / field / escapes]--> facts.json + --[core]--> OWN001 (leak) / OWN014 (escape) @ C# line +``` + +Land **one pattern per increment** (WPF002 next, then WPF003/004, then WPF005), +each with `bad_*.cs` / `ok_*.cs` fixtures, exactly as v0 did. WPF003 overlaps the +general `IDisposable`-field rule in [P-005](P-005-idisposable-ownership.md); build +it once in the resource core and let WPF consume it as a profile. + +## Open questions + +1. Heuristic vs annotation for "this class is a lifetime-bound component" + (name/base/interface heuristic for v0; `[OwnComponent]` opt-in later). +2. Where does the release region end — accept `Dispose`/`OnClosed`/`Unloaded`/ + `Unloaded` only, or any method named `Dispose*`? (Conservative set first.) +3. WPF005 needs a lifetime ordering (`Window < App`); is the App-capture fact + inferred (publisher outlives subscriber) or annotated? (Start annotated.) +4. `WeakEventManager` / weak subscription as an *accepted* release — recognise it + as "not a leak" to cut false positives, without modelling its internals. diff --git a/docs/proposals/P-005-idisposable-ownership.md b/docs/proposals/P-005-idisposable-ownership.md new file mode 100644 index 00000000..8aa32bd9 --- /dev/null +++ b/docs/proposals/P-005-idisposable-ownership.md @@ -0,0 +1,85 @@ +# P-005 — `IDisposable` ownership profile + +- **Status:** draft (P0 — the most down-to-earth resource module) +- **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release, + OWN003 double-release), [P-001](P-001-csharp-extractor.md) (the C# seam). + Shares the resource core with [P-004](P-004-wpf-lifetime-profile.md). + See [`docs/ROADMAP.md`](../ROADMAP.md) (Milestone 2). + +## Motivation + +`IDisposable` is the single most common resource discipline in .NET, and the one +C# expresses worst: to the compiler, `.Dispose()` is just a method and the object +is still "valid" afterwards. So the bugs are everywhere and the language shrugs: +a stream not disposed on an exception path, a disposable field the owner forgets, +a write after `Dispose()`. These are exactly OwnLang's `acquire → must release on +all paths`, `use-after-release`, `double-release` — already proven on `.own`. +This profile points that core at real C#. + +## Scope + +The five concrete findings, all intraprocedural (or single-class) to start: + +| Finding | Pattern | Core verdict | +|---------|---------|--------------| +| **D1** local not disposed | `new FileStream(...)` (or any `IDisposable`) not disposed on every path | `OWN001` | +| **D2** owned field not disposed | an `IDisposable` field whose owner's `Dispose()` does not cascade to it | `OWN001` | +| **D3** double dispose | `Dispose()` reachable twice | `OWN003` | +| **D4** use after dispose | `x.Dispose(); x.Write(...)` (same method/CFG) | `OWN002` | +| **D5** transfer unknown | a disposable handed to a callee whose ownership effect is unknown | (heuristic) | + +Resource mapping (the vocabulary is already the core's): + +```text +new IDisposable() / Open(...) -> acquire(Disposable, loc) +Dispose() / using-scope end -> release(Disposable, loc) +using (x) { ... } -> acquire + guaranteed release +an IDisposable field -> owned by the containing object +the owner's Dispose() body -> the release region for owned fields +``` + +`using` declarations are the easy, sound case (guaranteed release); the value is +in the paths *without* `using`. D4 (use-after-dispose) is the part the reality +matrix marks **deterministic** — `x.Dispose(); x.Use();` in one CFG is plainly +visible, contrary to the myth that "`ObjectDisposedException` can't be caught +statically" (the *cross-thread race* can't; the local sequence can). + +## Non-goals + +- **Cross-thread / async disposal races** (thread A disposes while thread B + reads) — a happens-before problem, not a structural one; out of scope (P3). +- Full interprocedural ownership transfer (D5) in v0 — model it as a *heuristic + warning* plus an explicit transfer contract (`[OwnTransfers]` / an extern + signature), rather than tracing every callee. Bug-driven later. +- Finalizers / `SafeHandle` internals / the full Dispose-pattern boilerplate + audit (CA1063 territory) — we care about the leak, not the ceremony. + +## Sketch + +This *is* the resource core; WPF subscriptions (P-004) are a profile of it where +the resource is named `Subscription`. The extractor emits `acquire`/`release` +facts for `new`/`Dispose`/`using`/fields; the core runs its existing flow- +sensitive lattice (the same one that already produces OWN001/002/003 on `.own`). + +```text +*.cs --[extractor: new / using / Dispose / field-cascade]--> facts.json + --[core: flow lattice]--> OWN001 / OWN002 / OWN003 @ C# line +``` + +D2 (owned field) needs an object-level "owner releases its fields in `Dispose`" +fact — the same `owner(this, R)` + release-region machinery P-004 needs for +WPF003, so build it once. D5 stays a warning until a real bug forces a transfer +model. + +## Open questions + +1. Field ownership: does *every* `IDisposable` field imply the class must + implement `IDisposable` and cascade, or only fields the class itself created + (vs injected/borrowed)? (Injected ≈ borrowed, not owned — start there to cut + false positives.) +2. What counts as a release region for D2 — `Dispose()` only, or also + `DisposeAsync()` / `Close()`? (Conservative set first; async is P2.) +3. How to express ownership transfer at the call boundary (D5) without + interprocedural analysis — extern signatures / `[OwnTransfers("arg0")]`? +4. Should `using`-covered locals be reported at all (they are sound) or stay + silent to keep noise down? (Silent.) diff --git a/docs/proposals/P-006-di-lifetimes.md b/docs/proposals/P-006-di-lifetimes.md new file mode 100644 index 00000000..c10f1bf3 --- /dev/null +++ b/docs/proposals/P-006-di-lifetimes.md @@ -0,0 +1,84 @@ +# P-006 — DI lifetime / captive dependency profile + +- **Status:** draft (P0 — clean lifetime model, little R&D, sells to ASP.NET) +- **Depends on:** `spec/Lifetimes.md` (the region-ordering model behind OWN014), + [P-001](P-001-csharp-extractor.md) (the C# seam). See + [`docs/ROADMAP.md`](../ROADMAP.md) (Milestone 3). + +## Motivation + +The captive dependency is one of the most common — and most quietly damaging — +.NET DI bugs: a `Singleton` takes a `Scoped` (or transient `IDisposable`) +dependency in its constructor, and that shorter-lived service is effectively +promoted to live as long as the app — an open DB connection held for the process +lifetime, request-specific state shared across requests, leaks. Microsoft calls +it a misconfiguration; it is **exactly** OwnLang's lifetime ordering, just spelled +in DI terms: + +```text +Transient ≲ Scoped < Singleton (Request < App) +forbid: store Scoped into Singleton (a longer-lived owner retains a shorter-lived value) +``` + +This is almost a free win: the lifetime machinery behind OWN014 (a value escaping +to a longer-lived region) already models it. + +## Scope + +- **DI001 (error):** a singleton service captures a scoped dependency (directly, + or transitively through the constructor graph). +- **DI002 (warning):** a singleton captures a scoped dependency **weakly** + (`WeakReference`). A weak reference fixes *retention* leaks, not a + *lifetime contract* violation — the scoped service is still invalid outside its + scope and may be disposed mid-use. Message: *"`WeakReference` does not make a + scoped service safe to use outside its scope; resolve it inside a fresh scope + via `IServiceScopeFactory`, or make the consumer scoped."* +- **DI003 (warning):** a transient `IDisposable` resolved from the **root** + provider — never disposed until the app exits (a slow leak). + +Suggested fix attached to DI001/DI002: inject `IServiceScopeFactory`, and per +operation `using var scope = factory.CreateScope();` then resolve the scoped +dependency inside the scope (the standard `BackgroundService`/singleton remedy). + +## Non-goals + +- A general aliasing/escape analysis of arbitrary object graphs — this is the + *registration + constructor* graph only. +- Resolving the hard dynamic cases: factory registrations, `IServiceProvider. + GetRequiredService` inside a lambda, open generics, conditional registration, + reflection scanning, Scrutor, config-driven wiring. These defeat a static + graph; report only the *conventional* `IServiceCollection` shape and stay + silent (not wrong) on the rest. (The brainstorm's "100% static" claim is + optimistic — conventional registrations are reliably catchable; dynamic ones + are not.) +- DI001 is **not** "solved by `WeakReference`" — see DI002; the right fix is a + scope boundary or a lifetime redesign, not a weaker reference. + +## Sketch + +Two facts feed the existing lifetime checker: a **registration graph** (service → +lifetime, from `AddSingleton`/`AddScoped`/`AddTransient`) and a **constructor +dependency graph** (service → its ctor parameter types, from Roslyn). The core +then checks the same region ordering it already uses for OWN014: a longer-lived +region (Singleton) must not retain a value from a shorter-lived region (Scoped). + +```text +Startup.cs / Program.cs --[extractor: registrations + ctor graph]--> facts.json + --[core: region ordering (OWN014 family)]--> DI001/DI002/DI003 @ registration site +``` + +Could be its own `Own.DI` profile sharing the lifetime core. Factory and +reflection registrations are recognised as "unknown lifetime" edges and excluded +rather than guessed. + +## Open questions + +1. Where to anchor the diagnostic — the registration line, the consuming + constructor, or both? (Both, with the capture path shown, like OWN014's + "expected: Window — actual: App — path: …".) +2. How far to chase transitive captures through the constructor graph before the + dynamic cases make it unreliable? (Bounded depth; stop at unknown edges.) +3. Is `IServiceScopeFactory` usage inside a singleton recognised as the *fix* + (so we stay silent), as it should be? +4. Treat transient-`IDisposable`-from-root (DI003) as warning or error? (Warning + — it is a slow leak, not always a bug.) diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md new file mode 100644 index 00000000..9f5dd568 --- /dev/null +++ b/docs/proposals/P-007-arraypool-span.md @@ -0,0 +1,88 @@ +# P-007 — ArrayPool / Span borrow-view profile + +- **Status:** draft (P1 — the borrow checker's flagship showcase) +- **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release, + OWN003 double-release, OWN008 release-while-borrowed), the buffer/borrow model + in `spec/`, [P-001](P-001-csharp-extractor.md). See + [`docs/ROADMAP.md`](../ROADMAP.md) (Milestone 4). + +## Motivation + +Pooled-buffer misuse is not the most *frequent* .NET bug, but it is the most +*on-message* one: an owned rented buffer, borrowed views (`Span`/`Memory`) over +it, and a `Return` that invalidates every view. That is precisely +owner/borrow/release — and ordinary analyzers rarely explain it in those terms. +It is the case that shows what Own.NET is *for*: + +```csharp +var arr = ArrayPool.Shared.Rent(n); // acquire: arr owns the pooled buffer +var span = arr.AsSpan(0, n); // borrow: span is a view of arr +ArrayPool.Shared.Return(arr); // release: invalidates dependent views +Use(span); // ❌ use-after-return (POOL002) +``` + +The corpus already pins two real cases (`corpus/real-world/arraypool-double-return`, +`arraypool-use-after-return`), so this profile has ground truth on day one. + +## Scope + +| Finding | Pattern | Core verdict | +|---------|---------|--------------| +| **POOL001** rented not returned | `Rent(...)` with no `Return` on some path (incl. early `return`/`throw`) | `OWN001` | +| **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` | +| **POOL003** double return | `Return` reachable twice for the same buffer | `OWN003` | +| **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` | +| **POOL005** clear/copy past length | write/clear beyond the logical length of the rented region | (buffer-policy check) | + +Resource mapping: + +```text +ArrayPool.Shared.Rent(n) -> acquire(PooledBuffer, loc) // arr owns it +arr.AsSpan(...) / new Span(arr) -> borrow(view, from = arr) // dependent view +ArrayPool.Shared.Return(arr) -> release(arr) // all views of arr now invalid +MemoryPool.Shared.Rent(...) -> acquire (same shape, IMemoryOwner) +``` + +The "Return invalidates all borrowed views" rule is the heart of it — the same +release-while-borrowed / use-after-release reasoning the core already runs, lifted +to the pool API. Generics are needed only *narrowly*: recognise the specific +symbols `System.Buffers.ArrayPool.Rent/Return`, `MemoryPool.Shared.Rent`, +`System.Span`, `System.Memory` — not "understand generics". + +## Non-goals + +- Whole-program / interprocedural escape of a `Span` (a view passed through many + callees). v0 is intraprocedural; a view crossing a call boundary with unknown + ownership is a heuristic warning (see P-005 D5). +- `stackalloc` escape is already the buffer model's job (OWN015–017); this + profile is about *pooled* ownership and its views, not re-deriving stack escape. +- Modelling pool internals (bucketing, array clearing semantics) — POOL005 is a + logical-length check, not a pool simulation. + +## Sketch + +The extractor emits `acquire`/`borrow`/`release` facts for the pool/span symbols; +the core runs its existing loan + ownership lattice (the one that already yields +OWN002/OWN008 on `.own`). Nothing new in the checker — a new *frontend mapping* +plus the known-bug replay corpus. + +```text +*.cs --[extractor: Rent / AsSpan / Return symbols]--> facts.json + --[core: ownership + loans]--> POOL001..004 @ C# line +``` + +**Replay targets** (P-012): `dotnet/runtime` use-after-return, Nethermind +ArrayPool leaks/double-return, AiDotNet.Tensors pooled-buffer leak/over-clear. +Catching a real one of these is the milestone-4 success condition. + +## Open questions + +1. View provenance: track `arr.AsSpan()` → view-of-`arr` precisely, or + conservatively treat any `Span` derived from a rented array as a loan of it? + (Conservative first.) +2. `Return(arr, clearArray: true)` vs sensitive buffers — does POOL005 tie into + the existing sensitive-buffer/clear-on-release check (OWN024)? +3. How much of POOL004 (view escape) overlaps the existing OWN004/OWN015 escape + rules — reuse, don't duplicate. +4. `IMemoryOwner` / `MemoryPool` `Dispose`-based release vs `ArrayPool`'s + explicit `Return` — one model with two release spellings? diff --git a/docs/proposals/P-008-effects-and-resources.md b/docs/proposals/P-008-effects-and-resources.md new file mode 100644 index 00000000..e519ed88 --- /dev/null +++ b/docs/proposals/P-008-effects-and-resources.md @@ -0,0 +1,163 @@ +# P-008 — Effects & Resources (`Own.Effects` / `Own.Resources`) + +- **Status:** draft (horizon — not a near-term commitment) +- **Depends on:** `spec/OwnCore.md` (the ownership/resource core and its fact + vocabulary), `spec/Lifetimes.md`; relates to P-006 (DI lifetime / captive + dependency — layer policies) and P-010 (richer type disciplines — where the + `resource`/capability types would actually live). See `docs/ROADMAP.md` for + where this sits in the strategy. + +## Motivation + +Ownership answers *who owns a value*. It says nothing about *what a function +reaches for*: the DB, the clock, the log, the network, a pooled buffer. In C# +those are ambient globals dressed up with tidy namespaces — `ArrayPool.Shared`, +`DateTime.Now`, `Console.WriteLine`, a captured `DbContext` — and a method +signature lies about all of them. A `CalculateTax(doc)` that quietly hits the +database has the same type as one that doesn't. + +The honest-interface thesis we already apply to ownership extends cleanly: make +a function's **external effects part of its interface**, checkable by the one +core, *without* threading `world0 → world1 → world2` by hand. That last clause is +the whole point — explicit effects are good, manual world-threading is +bookkeeping, not programming. + +## Scope + +Declared effects in OwnLang signatures, visible but not hand-threaded: + +```text +resource Db; resource Log; resource Clock; resource ArrayPool; + +fn CalculateTax(doc: Declaration) -> Money pure; +fn LoadRates() -> Rates use DbRead, Clock; +fn SaveDeclaration(doc: Declaration) use !DbWrite, !Log; +fn Hash(data: Bytes) -> Hash use !ArrayPool; +``` + +Direction markers (borrowed from Wybe): no prefix = read/input only; `!` = +read+write/mutate. `use Log` reads, `use !Log` writes; `use Db` reads, +`use !Db` writes. + +A resource may also carry an acquire/release protocol — capability *and* +ownership in one declaration, so the signature says "uses and mutates the pool" +instead of the pool being a global dumping ground: + +```text +resource ArrayPool { + acquire Rent(size: int) -> owned Buffer; + release Return(buf: owned Buffer); +} +``` + +What the core catches (effects flow up callees to callers like loans do): + +1. **Hidden effects** — a `pure` function that does IO/DB/Log/Clock/Pool. +2. **Unprovided resource** — calling `use !Db` where `Db` isn't permitted. +3. **Wrong direction** — allowed `use Db` (read) but performs a write. +4. **Unpaired protocol** — `Rent` without `Return`, `BeginTransaction` without + `Commit`/`Rollback` (this is just ownership of the capability handle). +5. **Architecture violations** — Domain `use !HttpClient`; Validation `use !Db`; + UI `use !FileSystem`. + +Diagnostics: + +```text +EFF001 undeclared effect (e.g. DbRead) +EFF002 pure method uses Clock/Network/Db/Log/Pool +EFF003 forbidden effect in layer Domain +EFF004 mutable resource used without ! permission +``` + +## Non-goals + +The most important section. We are **not** building: + +- a full algebraic-effects / effect-handlers calculus; +- a monad-transformer replacement (no `ReaderT Config (StateT Log IO)` killer); +- a model of *all* of .NET's effect surface at once. + +Start from an **API → effect spec table** and a handful of effects — Db +read/write, Log, Clock, Network, FileSystem, Pool — and grow it bug- and +architecture-driven. This lands **after** the concrete leak/DI checkers (P-004… +P-007) have proven value, so Own.NET ships an effect checker because real code +needed one, not a philosophical purity analyzer in search of a bug. + +## Sketch + +Effects are computed exactly like loans: a function's effect set is the union of +its own primitive effects and its callees', checked against its declaration. No +new engine — the core already does upward dataflow. + +```text +*.cs --[Roslyn extractor]--> facts.ownir.json --[Python core]--> EFF001..EFF004 + | ^ + +-- api→effect spec ------+ (DateTime.Now ⇒ Clock, Console.WriteLine ⇒ !Console) +``` + +The Roslyn extractor (P-001's seam) carries no effect knowledge of its own; it +reads a spec table the same way the core reads `spec/`: + +```yaml +resources: + ArrayPoolByte: + acquire: { symbol: System.Buffers.ArrayPool.Rent, effect: "!Pool", returns: owned Buffer } + release: { symbol: System.Buffers.ArrayPool.Return, consumes: arg0 } + Clock: { read: { symbol: System.DateTime.Now, effect: "Clock" } } + Console: { write: { symbol: System.Console.WriteLine, effect: "!Console" } } +``` + +So given `var now = DateTime.Now; Console.WriteLine(now);` inside a method +declared `[OwnPure]`, the core reports *"Foo uses undeclared resources: Clock, +!Console."* C# surface mirrors the DSL: + +```csharp +[OwnPure] // EFF002 if it touches the world +[OwnUses("DbRead")] // read-only +[OwnUses("!Log")] // mutating +``` + +Strictness ramps for legacy — warn-only → strict per folder → per namespace → +strict for new code only — so a brownfield solution can adopt it incrementally +instead of drowning in EFF001 on day one. Per-layer policies (Domain forbids +`!Db`, `!Http`; UI forbids `!FileSystem`) reuse P-006's layer machinery. + +## Background — why resources, not monads + +A quick survey of how pure languages let the dirty world in, and why we copy the +last one: + +- **Haskell monads** (`IO a`): effect wrapped in a type, sequenced via `bind`/ + `do`. Honest, but `IO` is one giant box — it says "touches the world", not + *which part*. +- **Clean uniqueness typing** (`*File -> *File`): explicit and unique; the + compiler proves a single reference. Orthogonal to *what* effect it is. +- **Mercury** modes/determinism + unique modes (`io::di, io::uo`): world-state + threaded explicitly — the bookkeeping we want to avoid. +- **Wybe resources**: named, declared, scoped, **directional** implicit + parameters (`def foo() use !io`). Interface integrity = no hidden effects, and + no hand-threading. **Plasma** adopts these, arguing resources compose more + directly than monad-transformer towers. + +The thesis we act on: *don't hide effects, make them part of the interface, but +without hand-threading `world0/world1/world2`.* A resource is a global that had +to pass passport control — the dependency is visible in the signature. +Resources and ownership/uniqueness are **orthogonal and compose**: in Wybe `io` +is both a resource and unique, which is exactly the seam where this proposal +meets the existing core. + +## Open questions + +1. Where do `resource` declarations live — a new `spec/Effects.md` vocabulary, + or folded into P-010's type discipline? (Leaning: P-010 owns the types, + `spec/Effects.md` owns the catalogue + diagnostics.) +2. Effect *polymorphism*: how does a higher-order `Map(f)` propagate `f`'s + effects without inventing effect variables we swore off? (Probably: it just + unions them, no row-polymorphism.) +3. Granularity of `Db` — one resource, or `DbRead`/`DbWrite` as the `!` already + implies? The samples above mix both; pick one before shipping. +4. Does `pure` mean *no resources* or *no `!` resources*? (A read-only `Clock` + user is not referentially transparent — so `pure` should mean no resources + at all, and `LoadRates` is `use DbRead, Clock`, never `pure`.) +5. Ordering vs P-004…P-007: this is explicitly downstream of the concrete leak + checkers. Confirm it stays a horizon item until at least one of them ships. diff --git a/docs/proposals/P-009-nogc-regions.md b/docs/proposals/P-009-nogc-regions.md new file mode 100644 index 00000000..5cac0130 --- /dev/null +++ b/docs/proposals/P-009-nogc-regions.md @@ -0,0 +1,142 @@ +# P-009 — Verified allocation-free ("no-GC") regions (`Own.NoGc`) + +- **Status:** draft (horizon) +- **Depends on:** buffer storage policies (`spec/BufferPolicies.md`, the + `policy P { ... }` block and OWN015–017 escape rules); the ownership core + (`spec/OwnCore.md`); and **P-007** (ArrayPool/Span borrow-view), which supplies + the `Span`-over-owned-storage view this region lives inside. Strategy hub: + [`docs/ROADMAP.md`](../ROADMAP.md), `Own.Performance` track. + +## Motivation + +In audio, game loops, low-latency/trading, serializers, packet processing, +crypto, and WPF hot render/update paths, a hidden managed allocation in the hot +path is real harm: it invites a GC pause exactly when you cannot afford one. The +ask people *say* is "C# without a GC." We cannot deliver that, and pretending +otherwise would be the boil-the-ocean version this project exists to refuse. + +Honest framing: managed objects live on the managed heap and the runtime must +know when to free them — you cannot turn that off for managed C#. Even Native AOT +is not "C# without GC": it removes the JIT and ships a self-contained AOT binary, +but it still ships runtime libraries, still has a GC, bans dynamic loading / +`Reflection.Emit`, and needs trimming. So the deliverable is **not** a runtime +change. It is a **static checker for allocation-free regions**, plus explicit +stack / scratch / native / pool memory with ownership — which is squarely +Own.NET territory. Without the ownership checker, "C# without GC" is just "C with +expensive syntax and new ways to shoot your foot." + +## Scope + +A region (method or block) marked `nogc` is statically verified to perform **no +managed-heap allocation**. The GC still exists app-wide; the region is a verified +island. A ladder of ambition, from most realistic to most aspirational: + +1. **Allocation-free hot path** (the MVP, most useful): GC exists app-wide; one + method/region provably does not allocate. This is the whole prize for audio, + game loops, serializers, packet/image processing, crypto, WPF render. +2. **`NoGCRegion` runtime guard:** pair the static region with + `GC.TryStartNoGCRegion(totalSize)` / `GC.EndNoGCRegion()`. Best-effort, + non-nestable, needs a pre-reserved budget — and **not** a substitute for the + static checker: a body full of `string.Format`/LINQ/closures under + `TryStartNoGCRegion` is just an allocation circus with a budget. +3. **Manual unmanaged memory:** `NativeMemory.Alloc`/`Free`, `Span` over the + pointer — this immediately needs the ownership checker (Alloc = acquire, + Free = release, Span = borrowed view; Free-while-Span-live, use-after-Free, + double-Free, leak). Reuses `native` buffer machinery directly. +4. **An OwnLang `nogc` subset that lowers to `unsafe` C#:** + `fn hash(input: Span) -> u64 nogc { let scratch = Buffer.stack(256); ... }` + → `Span scratch = stackalloc byte[256];`. + +## Non-goals + +- **"Real C# without a GC."** Impossible for managed C#; not attempted. We verify + *regions*, we do not remove the collector. +- **A runtime GC switch / a custom no-GC runtime / forking Native AOT.** Out. +- **Whole-program allocation analysis.** Regions are opt-in and local. Unknown + callees are rejected, not chased. +- **Replacing the runtime guard.** `TryStartNoGCRegion` is a complementary + runtime belt; this proposal is the static suspenders. + +## Sketch + +Reuse note: OwnLang's existing buffer policies (stack/scratch/pool/native + +escape rules OWN015–017) are already ~80% of the machinery. This is largely a new +*policy* (`nogc`/`noheap`) layered on `spec/BufferPolicies.md`'s `policy` block, +plus an **allocation-source detector** on the C# side — not a new analysis. + +DSL surface — a storage/effect policy: + +```text +policy RealtimeAudio { + nogc; noheap; noexceptions; noasync; + allow stack; allow scratch; + forbid pooled unless declared; // use !Pool + forbid native unless owned; // owned wrapper, OWN015–017 apply +} + +fn Render(input: Span, output: Span) policy RealtimeAudio use !Scratch { + let tmp = Buffer.stack(512); + borrow_mut tmp as t { Mix(input, t); Copy(t, output); } +} +``` + +C# surface (the MVP entry point): `[OwnNoGc]` or `[OwnPolicy("RealtimeAudio")]` +on a method; the Roslyn extractor (P-001) flags allocation sources as OwnIR +facts, the Python core renders the verdict at the C# line. + +**Forbidden inside a `nogc` region** → the body allocates: `new` of a class; +`new string` / string interpolation; boxing; lambda/closure with capture; LINQ; +`async` / iterator (`yield`); `ToArray`/`ToList`; delegate allocation; +`params object[]`; exceptions as control flow; hidden allocations from known APIs. + +**Allowed:** `stackalloc`, `Span`, `ref struct`, unmanaged/native memory via an +owned wrapper, and `ArrayPool` **only** when declared `use !Pool`. + +```text +[OwnNoGc] method --[Roslyn alloc-source detector]--> alloc facts (OwnIR) + | + whitelist spec (nogc contracts) --+ + v + Python core --> OWN-GCnnn at C# line +``` + +The practical knob is a **whitelist of known-nogc APIs**, e.g. +`System.MathF.Sin(float): nogc:true`, `System.Span.CopyTo: nogc:true`, +`System.Linq.Enumerable.Select: nogc:false (iterator/delegate allocations likely)`. +An unknown call has **no nogc contract** → rejected by default, with the +allocation reason reported (OWN-GC004), so silence never reads as safety. + +Diagnostics (`OWN-GC` family): + +```text +OWN-GC001 managed allocation in nogc region +OWN-GC002 boxing +OWN-GC003 closure / delegate allocation +OWN-GC004 call to method without a nogc contract +OWN-GC005 async / iterator not allowed in nogc region +OWN-GC006 heap escape from a stack/native buffer (relates to OWN015–017) +OWN-GC007 exception allocation (exception used as control flow) +``` + +**First real target:** a CLAP audio plugin's render/process callback must be +allocation-free — GC pauses and hidden allocations are audible harm. The +project's own audio/CLAP direction stacks with this cleanly, so the MVP lands on +a callback that genuinely needs it rather than a toy. + +**MVP, concretely:** `[OwnNoGc]` method attribute; detect the obvious allocation +sources; allow `stackalloc`/`Span`; reject unknown calls by default; support a +whitelist spec; report the allocation reason. Then wire the CLAP render callback +as the first verified region. + +## Open questions + +1. Granularity: method-level `[OwnNoGc]` only, or also a `nogc { ... }` block + inside an otherwise-allocating method? +2. Whitelist provenance: hand-curated spec, harvested from BCL signatures, or a + community-maintained file? Where does the source-of-truth live in `spec/`? +3. Do we pair the static region with `TryStartNoGCRegion` codegen (level 2), or + keep the runtime guard strictly opt-in and orthogonal? +4. `Own.NoGc` reads as a marketing name; is `noheap`/`noalloc` the more honest + policy keyword, given we are forbidding *allocation*, not the collector? +5. How much of the `native`-escape story (OWN015–017) needs hardening before + level 3 is more than a checker-accepts / codegen-rejects PoC? diff --git a/docs/proposals/P-010-type-disciplines.md b/docs/proposals/P-010-type-disciplines.md new file mode 100644 index 00000000..9e880aeb --- /dev/null +++ b/docs/proposals/P-010-type-disciplines.md @@ -0,0 +1,157 @@ +# P-010 — Richer type disciplines (`Own.Types`) + +- **Status:** draft (horizon) +- **Depends on:** `spec/OwnCore.md` (the ownership/affine core and its fact + vocabulary), `spec/Lifetimes.md`; relates to P-006 (capability/lifetime — where + branded `resource`/capability types are held), P-008 (effects — the `use !Db` + half of a signature), and P-005 (IDisposable typestate — the first concrete + protocol). See `docs/ROADMAP.md` for where this sits in the strategy. + +## Motivation + +The guiding heuristic: types aren't only about the *shape* of data +(`string`/`int`/`User`). They can encode validity, access rights, state, +dimension, order of operations, effects, protocol, ownership, even proofs. If a +bug arises because *"this value was in the wrong state / not validated / used in +the wrong place / called in the wrong order"*, it is a candidate for a smarter +type — one that makes the bad program unrepresentable instead of merely +unit-tested. + +C# gives you the shape dimension and almost nothing else. The two dimensions it +lacks are exactly the interesting ones: **what a value MEANS** (`ProductId` is +not `DeclarationId`, even though both are `string`) and **what STATE it is in** +(a `Report` that is `Draft` cannot be exported). The usual C# coping mechanism — +make everything `string` / `int` / `Guid` / `Dictionary` — is not +flexibility. It is homeless JSON pretending to be architecture. + +`Own.Types` adds those two dimensions as an **external static-contract layer** +over existing C#: an analyzer / source generator / `.own` spec that checks the +discipline, without rewriting the code into a new language. This is the move that +turns Own.NET from "a borrow checker for C#" into "an external static contract +layer for C#/.NET that adds ownership, typestate, effects, capabilities, and +domain types" — while the DSL stays a spec/model/contract language and pointedly +refuses to become a second C# people write business logic in. + +## Scope + +The four most-applied disciplines, in priority order. Each has a `.own` +declaration and a checked C# imitation; none requires a runtime. + +1. **Branded / opaque types.** Distinguish `ProductId`, `DeclarationId`, `Email` + though all are `string` underneath, so `GetProduct(declarationId)` is a + diagnostic, not a 2 a.m. incident. DSL: `brand ProductId : string;`. C#: + `[OwnBrand("ProductId")]` on a `readonly record struct` plus a smart + constructor; the analyzer enforces that the wrapped value only enters through + it. (Mechanically these are phantom types — see the catalog.) + +2. **Refinement types** — "int, but valid": + `refinement Port : int where value >= 1 && value <= 65535;`, + `refinement NonEmptyString : string where !String.IsNullOrWhiteSpace(value);`, + `Age = int where 0 <= value <= 130`, `Percentage = number where 0..100`. This + replaces the scattered `if (age < 0) throw` rituals with one declared + predicate. The C# imitation today is value objects + smart constructors; we + make it **declarative and analyzer-checked** so the predicate lives in one + place and the type system, not code review, enforces the boundary. + +3. **Units of measure**, à la F# `[]`: `unit kg; unit usd; unit kzt;` so + `metres + seconds` and `usd + kg` are compile errors. For money, currency, + tax rates, and physical quantities — the domains where a silent unit mix-up + is a financial bug, not a rounding one. + +4. **Typestate / protocols.** Encode object state in the type so methods can only + be called in a valid order: + + ```text + protocol Report { + state Draft; state Validated; state Built; + validate: Draft -> Validated; + build: Validated -> Built; + export: Built -> File use !Log; + } + ``` + + Examples: `Connection`, `Transaction`, + `Json` (you cannot save unvalidated JSON). This composes + directly with the ownership/affine core: a transition can **consume self**, so + `commit: Started -> Committed` consuming `tx` makes a subsequent `rollback(tx)` + reject — rollback-after-commit is not a runtime guard, it is a use-after-move. + Typestate is also the generalization that subsumes **session types** (typed + message-ordering protocols) as the special case where the object is a channel. + +The combined picture — domain types, refinements, resources, protocol state, and +effects in one signature set: + +```text +brand ProductId : string; +refinement NonEmptyString : string where !String.IsNullOrWhiteSpace(value); +resource Db; resource ArrayPool; + +protocol Report { + state Draft; state Validated; state Built; + validate: Draft -> Validated; + build: Validated -> Built; + export: Built -> File use !Log; +} + +fn CalculateTotal(order: Order) -> Money pure; +fn LoadOrder(id: ProductId) -> Order use Db; +fn RenderReport(report: Report) -> File use !ArrayPool, !Log; +``` + +## Non-goals + +Refuse the boil-the-ocean version. The first move is explicitly **not** dependent +types, GADTs, or higher-kinded types — that way lies a tower of type-level +arithmetic (башня type-level арифметики) where you wanted to write a function and +end up proving 2 + 2 = 4. The DSL must not become a new general-purpose language; +it stays a spec/model/contract layer. No new runtime, no rewriting the codebase — +brands and refinements lower to plain structs and smart constructors, and the +discipline is enforced by analyzer, not by a parallel type checker that drifts +from the core (the project's standing meta-irony). `[OwnIgnore("reason")]` remains +the escape hatch. + +## Deferred catalog + +Surveyed and explicitly **not** first — recorded so the ideas aren't lost: + +- **Dependent types** (`Vector` — length in the type; + `dot: Vector -> Vector -> float`). Maximum strictness, + maximum cognitive cost. Idris / Agda / Coq / Lean / F*. Not a contract layer; a + proof obligation. +- **GADTs** (typed AST: `Expr` / `Expr`, + `Add: Expr -> Expr -> Expr`). Only if a typed AST / DSL / + query-builder need appears — relevant to the Snipper / Reactor / AST-transform + ideas, not before. +- **Phantom types** — already in scope, as the underlying mechanism behind brands. +- **Higher-kinded types** (abstract over `F<_>`: Functor / Monad). Do not touch: + assembling a spaceship out of `IEnumerable`, `Task`, and pain. +- **Row types** ("an object with at least these fields"), **existential types** + ("there is some hidden `T`" — plugin/handler systems, heterogeneous + collections), **intersection `A & B`** / **union `A | B`** types, and + **gradual typing** (strict + dynamic mixed; the risk is `any` spreading until + the type system is a decorative quality sticker). +- **Modal types** (`Html`, `Sql`, + `sanitize: Html -> Html`) and **indexed types** + (`Buffer`, `Password`, pipeline + stages) — both for trust zones, escaping, and lifecycle. These overlap heavily + with branded + typestate, so they may fall out for free once those two land. + +Priority, most-applied → academic tail: **branded/opaque · units of measure · +typestate · refinement · effect types (P-008) · session types · phantom**, then +**dependent / GADT / HKT** as the cognitively expensive end. + +## Open questions + +1. **Surface:** analyzer-only (annotate C# in place) vs `.own` spec + source + generator vs both. Brands and refinements want a generator (smart + constructors); typestate wants the analyzer + the affine core. +2. **Where do brands live** relative to P-006 capabilities — is a capability just + a branded, non-`Copy` resource token, or its own kind? +3. **Refinement strength:** syntactic predicate enforced at the constructor + boundary (cheap, sound-by-construction) vs flow-checked refinement (needs the + verification backend, P-002). v0 should be the former. +4. **Typestate ↔ ownership seam:** confirm transitions express consume-self + through the *existing* affine facts, so `commit` then `rollback` is reported as + use-after-move by the one core — no second mechanism. +5. Do **modal/indexed** types ever need their own surface, or are they always + reducible to brand + typestate in practice? diff --git a/docs/proposals/P-011-editor-tooling.md b/docs/proposals/P-011-editor-tooling.md new file mode 100644 index 00000000..79619283 --- /dev/null +++ b/docs/proposals/P-011-editor-tooling.md @@ -0,0 +1,124 @@ +# P-011 — Editor tooling & syntax highlighting + +- **Status:** draft +- **Depends on:** the CLI `check` command (`python -m ownlang check`); + `ownlang/diagnostics.py` (the OWN### code/severity vocabulary); the lexer and + parser (`ownlang/lexer.py`, `spec/Grammar.md`) as the *only* canonical grammar. + Complements **P-003** (lifetime visualization): P-003 draws lifetimes/loans as a + graph/timeline; P-011 makes `.own` a first-class *editor* language — coloring, + diagnostics squiggles, hover. Strategy hub: [`docs/ROADMAP.md`](../ROADMAP.md). + +## Motivation + +A `.own` file today opens in any editor as undifferentiated grey text: `fn`, +`move`, `release`, the diagnostic codes, the buffer modes — all the same color as +a comma. The checker is genuinely good; the *experience of writing the input to +it* is "Notepad after a head injury". The cheapest possible win in developer +goodwill is coloring keywords. The next-cheapest is drawing the diagnostics the +CLI already produces as red squiggles under the offending span, instead of making +the author re-run `check` in a terminal and count lines by hand. + +This proposal is deliberately staged cheapest-first, so each layer ships value +before the next is begun. The expensive layers (a language server, a second +grammar) are explicitly *not* the starting point. + +## Scope + +A 3-layer plan (plus two optional later layers), in strict cost order: + +- **Layer 1 — VS Code TextMate grammar.** A `vscode-ownlang/` extension that + registers the `ownlang` language id for `.own` and colors keywords, types, + buffer modes, comments, strings, numbers, and diagnostic codes. One evening. +- **Layer 2 — CLI diagnostics in the editor.** The extension shells out to + `python -m ownlang check file.own --json`, parses the result, draws squiggles. + Requires a `--json` output mode on the CLI. A crutch — but a useful one. +- **Layer 3 — LSP + semantic highlighting.** A minimal language server: diagnostics, + hover, go-to-def, document outline, and the headline feature — **semantic tokens** + that color resource *state* (owned / moved / released), not just words. +- **Layer 4 — tree-sitter** (only on cross-editor demand): `tree-sitter-ownlang` + for Neovim/Helix/Zed/Emacs/GitHub. + +Ideal ordering, stated plainly: +**v0** TextMate grammar → **v1** CLI `--json` diagnostics in VS Code → +**v2** LSP diagnostics + hover → **v3** semantic tokens (owned/borrowed/moved/ +released) → **v4** tree-sitter → **v5** visual lifetime graph (= **P-003**). + +## Non-goals + +- **JetBrains-grade IntelliJ-for-`.own` in v0.** Refactorings, full completion, + rename-across-files: no. We are trying to color `fn`, not clone Rider. +- **Writing a three-week language server before `.own` even has colored keywords.** + The LSP is Layer 3 for a reason. If keywords aren't colored, the LSP is premature. +- **A second canonical grammar.** TextMate and tree-sitter are presentation-only + approximations; the Python lexer/parser stays the single source of truth. +- A debugger, a formatter, or a build-system integration. Out of scope here. + +## Sketch + +**Layer 1 (TextMate).** `vscode-ownlang/` contains `package.json` (contributes the +`ownlang` language, `.own` extension, the grammar), `language-configuration.json` +(line `//` comments, brackets, autoclose/surrounding pairs — note: the grammar has +**no block comments**, so don't invent `/* */`), and +`syntaxes/ownlang.tmLanguage.json` (scopeName `source.ownlang`). A regex grammar +covering: + +- **keywords:** `module resource acquire release extern fn let move borrow + borrow_mut consume as use if else return mut policy lifetime subscribe` and the + emit templates `emit_type emit_acquire emit_release emit_borrow`; +- **buffer modes:** `Buffer.(stack|scratch|pooled|native|inline)`; +- **types / built-ins:** identifiers in type position (`int`, `Span<...>`, + `Buffer`, resource names) — TextMate can only approximate this; +- **rejected keywords** (`while for loop async await yield spawn`) colored as + "invalid" so the OWN020 refusal is visible before `check` runs; +- comments (`//`), strings (with `\n \t \" \\` escapes), integer literals; +- **diagnostic codes:** `OWN[0-9]{3}` (the real namespace — see + `ownlang/diagnostics.py`; there is exactly one code prefix today). + +Verify every list above against `ownlang/lexer.py` / `spec/Grammar.md` at build +time — the keyword set is small and authoritative, and this proposal will drift. + +**Layer 2 (`--json` diagnostics).** Add a `--json` mode to `check` emitting an +array of `{code, severity, message, file, line, column, endLine, endColumn}`. +The extension runs it on save, parses, draws squiggles colored by `severity` +(ERROR / WARNING per `Severity`). Honest framing: this is editor UX without +writing a language server — diagnostics in the gutter while we still haven't built +Layer 3. + +**Layer 3 (LSP + semantic tokens).** TextMate colors *words*; it cannot know that +after `let b = move a;` the symbol `a` is moved-out. Semantic tokens can color the +resource *state* over its lifetime — the signature feature, a Rust borrow +visualizer but inline and for OwnLang: + +```text +let a = Buffer.pooled(n); // a: owned (green) +let b = move a; // a: moved (orange/grey), b: owned (green) +release b; // b: released (grey) +use b; // red squiggle (OWN002) +``` + +Proposed legend: **owned = green, borrowed = blue, borrow_mut = purple, +moved = orange, released = grey, error = red**; plus token kinds for *lifetime +name*, *policy name*, *diagnostic code*, and *acquire function*. The state facts +are not recomputed in the server — they are the same CFG/state facts P-003 +consumes. This is exactly where P-011 and P-003 meet: semantic tokens are the +in-line cousin of P-003's graph/timeline. + +**Layer 4 (tree-sitter).** `tree-sitter-ownlang` (`grammar.js`, +`queries/{highlights,locals,folds}.scm`) for the non-VS-Code world. Faster and +more accurate than regex, cross-editor, GitHub-renderable. But it is a *second* +grammar duplicating a Python parser that already exists. Do **not** start here: +it's premature duplication until cross-editor demand is real. + +## Open questions + +1. **One grammar or many?** The Python lexer/parser is canonical; TextMate and + tree-sitter necessarily duplicate it and will drift. Generate them from a shared + token spec, or accept manual sync with a CI test that lexes a sample both ways? +2. **Where does `--json` live?** A first-class core CLI mode (stable, tested, + reusable by P-003 and P-001), or a thin adapter outside the core so the CLI's + human output stays the only blessed surface? +3. **How are semantic-token states fed to the server?** Reuse the CFG/state facts + the checker already computes (as P-003 does) rather than re-deriving ownership + in the language server — one analysis, two presentations. +4. Bundle a Python runtime / pin a version for the LSP, or assume `python -m + ownlang` is on the user's PATH? (Affects how painful Layer 2/3 install is.) diff --git a/docs/proposals/P-012-bug-corpus-mining.md b/docs/proposals/P-012-bug-corpus-mining.md new file mode 100644 index 00000000..31c73c47 --- /dev/null +++ b/docs/proposals/P-012-bug-corpus-mining.md @@ -0,0 +1,137 @@ +# P-012 — Real-world bug corpus & mining pipeline + +- **Status:** draft +- **Depends on:** P-001 (C# → OwnIR extractor — the scanner that does stage 2); + the existing `corpus/` layout (`before.cs`, `after.cs`, + `expected-diagnostics.txt`, `notes.md`/`source.md`). + +## Motivation + +The whole frontend runs on **bug-driven expansion**: prove Own.NET catches ONE +real bug, then grow exactly to fit the next one. That principle is only as good +as the question *"which bug next?"* — and today that question is answered by +vibes. We pick WPF event leaks and ArrayPool double-returns because they *feel* +common and static-friendly, not because we counted. + +We would love to count against a public "top of all .NET production errors" +dataset. It does not exist. That data lives in private dashboards — Sentry, App +Insights, Raygun, Datadog, New Relic — and nobody publishes the aggregate. So +the honest move is to build **proxy signals** and our **own measured corpus** +instead of guessing, and to feed the resulting numbers into `docs/ROADMAP.md`, +where the prioritization and the "what static analysis can / can't catch" matrix +live. This proposal is the data source for that matrix, not a competitor to it. + +**Proxy signals** (legitimate as *signals*, not statistics): + +- Microsoft analyzer rules — CA2000 (disposable not disposed before scope loss, + including exceptional paths), CA2012 (`ValueTask` consumed twice). These encode + what Microsoft thought worth shipping a rule for. +- Resource-leak research — e.g. RLC# on CodeQL reporting resource leaks across + OSS projects and Azure microservices. +- Official exception docs flagging `NullReferenceException` and + `ObjectDisposedException` as *developer* errors. +- DI lifetime guidance — transient `IDisposable` resolved from the root container + leaks; singleton capturing scoped = captive dependency; async factory via + `.Result` deadlocks. + +These tell us *what to look for*. They do not tell us *how often it actually +occurs in real repos*. The pipeline below measures that. + +## Scope + +A **boringly practical, offline research pipeline** in four stages whose output +is a curated corpus plus a *calibrated* priority list. The corpus mirrors the +existing `corpus/` layout so today's three WPF cases and two real-world cases are +already the first members. + +1. **GitHub mining.** Search merged PRs / issues across the .NET ecosystem + (dotnet/runtime, aspnetcore, EF Core, Nethermind, …) for fix-shaped keywords: + `"fix memory leak" .NET`, `ObjectDisposedException`, `"IDisposable" "leak"`, + `"event handler leak"`, `"DispatcherTimer leak"`, `"ArrayPool" "Return"`, + `"captive dependency"`, `"Cannot consume scoped service from singleton"`. + Each promising PR gives a real `before`/`after` pair for free. +2. **Roslyn scan.** Run the **P-001 extractor** over 50–100 popular repos and + count hits per 1k LOC for: `event += without -=`; `IDisposable` fields with no + `Dispose`; `ArrayPool.Rent` without `Return`; `Return` before the last + `AsSpan` use; singleton-captures-scoped from the registration graph. +3. **Runtime telemetry — on our OWN code only.** Exception-type histogram, top + stack traces, memory-dump leak cases, WPF ViewModel retention paths. No + scraping anyone else's telemetry; this is the one signal that is real + measurement rather than proxy, and it is small because it is only ours. +4. **Corpus.** For every confirmed bug store `before.cs`, `after.cs`, + `expected-diagnostics.txt`, and `source.md` (link + a one-paragraph story), + tagged with a **detectability** label (below). + +The payoff is one defensible sentence we *intend to be able to write* — e.g. +"Of 100 projects: 47 suspicious `IDisposable` leaks, 31 event subscriptions with +no unsubscribe, 12 DI lifetime mismatches, 8 ArrayPool suspicious paths, 5 +use-after-dispose candidates." That is the **output we plan to produce**, not a +current measurement. + +## Non-goals + +- No live real-time scan of 100 repos wired in as a CI gate — it is + resource-bound and would make every build hostage to GitHub rate limits. +- No claim of authoritative .NET error statistics. We are explicit that we don't + have them and are building proxies *because* we don't. +- No scraping of private telemetry (Sentry/App Insights/etc.). +- This is an **offline research tool**. Its product is the corpus and a + calibrated priority list — not a user-facing feature. + +## Sketch + +```text +GitHub PRs/issues --[keyword mine]--\ +50–100 repos --[P-001 scan]-----> candidates --[triage + reduce]--> corpus/// +our telemetry --[histogram]-----/ {before.cs, after.cs, + expected-diagnostics.txt, + source.md, detectability tag} + counts -----------------------> docs/ROADMAP.md priority matrix +``` + +**Priority table — PROXY / hypothesis, NOT measured.** Every cell below is an +estimate to be *replaced* by stage-2 counts. Do not cite these as facts. + +| Pattern | Prevalence (proxy) | Note | +| --- | --- | --- | +| `event += without -=` | **Very High** | old WPF/WinForms repos ~3–4× more than Blazor/MAUI | +| `IDisposable` field, no `Dispose` | **High** | broad across services and UI | +| captive dependency (singleton→scoped) | **proxy ~15%** of large ASP.NET Core projects have ≥1 | visible in registration graph | +| `ObjectDisposedException` | **extreme** mention-count (SO/issues) | but largely a timing/race bug — see detectability | +| `ArrayPool.Rent` without `Return` | **Low/Medium** | but ~20–30% in high-load parsing/serialization libs | +| `Return` before last `AsSpan` use | **Very Low** | low-level code only | + +**Detectability — tag every case (full matrix lives in `docs/ROADMAP.md`):** + +- *Deterministic / static-friendly:* captive dependency (in the type/registration + graph); missing `Dispose`; `ArrayPool` Rent/Return within one method; simple + use-after-dispose in one CFG. +- *Heuristic / false-positive-prone:* `event += without -=` (depends on object + lifetime — only warn for long-lived objects); ownership transfer through a + callee (`ProcessStream(s)` may dispose internally). +- *Impossible statically:* `ObjectDisposedException` from a cross-thread race; + LOH fragmentation (runtime data volume); static-collection bloat (business + data); unmanaged cyclic refs / `Marshal.AllocHGlobal` freed on all paths. + +The tag exists so we never promise a runtime-only bug to a static checker. A +corpus entry tagged *impossible* is a documented limit, not a backlog item. + +**Replay corpus targets (concrete stage-3 "replay a known bug" goals):** +dotnet/runtime use-after-return; Nethermind ArrayPool leaks / double-return; +AiDotNet.Tensors pooled-buffer leak / over-clear. Reproduce each, reduce it into +`corpus/`, and confirm the checker's verdict matches the real fix. + +## Open questions + +1. Repo selection for stage 2 — top-N by stars, or weight toward the high-load + serialization/parsing libs where ArrayPool misuse actually concentrates? +2. Triage gate — what false-positive rate makes a stage-2 hit corpus-worthy vs + noise to discard? (The heuristic patterns will be loud.) +3. `source.md` vs the existing `notes.md` — unify on one filename, or let + `notes.md` (hand-reduced) and `source.md` (mined, with provenance link) + coexist as a signal of origin? +4. How much of stage 1 can the `mcp__github__search_*` tooling do reproducibly + vs a one-off scripted scrape we don't keep wired in? +5. Re-scan cadence — is the priority list a one-time calibration, or do we + re-measure when the extractor gains a pattern (so coverage and prevalence + stay honest together)? diff --git a/docs/proposals/README.md b/docs/proposals/README.md index 94fcde3c..5f7fb70b 100644 --- a/docs/proposals/README.md +++ b/docs/proposals/README.md @@ -25,6 +25,20 @@ proposal is marked `done` with a pointer. | [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | in progress (v0 built) | | [P-002](P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | draft | | [P-003](P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | draft | +| [P-004](P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | draft | +| [P-005](P-005-idisposable-ownership.md) | `IDisposable` ownership profile | draft | +| [P-006](P-006-di-lifetimes.md) | DI lifetime / captive dependency | draft | +| [P-007](P-007-arraypool-span.md) | ArrayPool / Span borrow-view | draft | +| [P-008](P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | draft | +| [P-009](P-009-nogc-regions.md) | No-GC / allocation-free regions | draft | +| [P-010](P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | draft | +| [P-011](P-011-editor-tooling.md) | Editor tooling & syntax highlighting | draft | +| [P-012](P-012-bug-corpus-mining.md) | Real-world bug corpus & mining | draft | + +> For priorities, milestones, the framing, and the design philosophy across all +> of these, see the strategy hub: [`docs/ROADMAP.md`](../ROADMAP.md). P-004 … P-012 +> capture ideas raised in design discussion — they are *on the record for +> consideration*, drafts, not commitments. ## The long-term arc (one paragraph) From 148f053b5af67be45d3452a8736bc6814cece2b4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 14:17:44 +0000 Subject: [PATCH 3/9] =?UTF-8?q?ownir:=20WPF002=20=E2=80=94=20DispatcherTim?= =?UTF-8?q?er/Timer=20leak=20(P-004)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A Tick/Elapsed handler on a started timer is a Timer resource: the running timer strong-refs the handler's owner, so an undetached one leaks it (OWN001, tagged [resource: timer]). Released by a matching `-=` OR a `Stop()` on the same receiver (e.g. `_timer.Stop()` in Dispose). - ownir.py: optional `resource` field per subscription ("subscription" default | "timer"); a Timer resource in the prelude (kind "timer"); timer-specific finding message + kind tag. The field is additive, so it does NOT bump ownir_version — an older core just reads every entry as a subscription. - Roslyn extractor: classify `Tick`/`Elapsed` handlers as timers; a timer is released by `-=` or a `Stop()` on the same receiver; emit `resource`. - Sample TimerViewModel.cs (leaking timer + Stop()-in-Dispose clean one) and a hand-written timer.facts.json fixture; test_ownir pins the timer leak, the [resource: timer] tag, and silence on the stopped timer. - wpf-extractor CI job runs the timer sample and asserts the timer leak + [resource: timer] tag, and that the stopped timer stays silent. - Docs: P-004/P-001/ROADMAP mark WPF002 built. Python bridge verified locally (11/11 ownir checks); the extractor is CI-validated (dotnet is CI-only). --- .github/workflows/ci.yml | 12 +++- docs/ROADMAP.md | 2 +- docs/proposals/P-001-csharp-extractor.md | 3 +- docs/proposals/P-004-wpf-lifetime-profile.md | 11 +-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 36 ++++++++-- frontend/roslyn/samples/TimerViewModel.cs | 39 +++++++++++ ownlang/ownir.py | 68 ++++++++++++++----- tests/fixtures/ownir/timer.facts.json | 20 ++++++ tests/test_ownir.py | 26 +++++++ 9 files changed, 189 insertions(+), 28 deletions(-) create mode 100644 frontend/roslyn/samples/TimerViewModel.cs create mode 100644 tests/fixtures/ownir/timer.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4c0fc8aa..25922c9b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -109,6 +109,7 @@ jobs: dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \ frontend/roslyn/samples/CustomerViewModel.cs \ frontend/roslyn/samples/OrdersViewModel.cs \ + frontend/roslyn/samples/TimerViewModel.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" - name: Check facts through the core @@ -122,5 +123,14 @@ jobs: if echo "$out" | grep -q "OrdersViewModel.cs"; then echo "FAIL: disposed subscription wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 at the C# location" + # WPF002: the started, never-stopped timer leaks with a [resource: timer] + # tag; the timer stopped in Dispose stays silent. + echo "$out" | grep -q "TimerViewModel.cs" \ + || { echo "FAIL: expected the TimerViewModel timer leak"; exit 1; } + echo "$out" | grep -q "resource: timer" \ + || { echo "FAIL: expected a [resource: timer] tag"; exit 1; } + if echo "$out" | grep -q "CleanTimerViewModel"; then + echo "FAIL: stopped timer wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer) at the C# location" diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 750d44b9..0bdf9b86 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -67,7 +67,7 @@ ownership/lifetime/effects, (4) an MVP needs no PhD in Roslyn. architectural strictness, and the borrow-checker showcase): 1. `WPF001` — event/subscription `+=` without `-=` (the WPF spike; P-001 v0 ✅) -2. `WPF002` — `DispatcherTimer` started/subscribed without stop/unsubscribe +2. `WPF002` — `DispatcherTimer`/`Timer` `Tick`/`Elapsed` without stop/detach ✅ 3. `BOR/OWN` — `IDisposable` field not disposed by its owner 4. `DI001` — singleton captures a scoped dependency 5. `POOL` — `Span`/view used after `ArrayPool.Return` diff --git a/docs/proposals/P-001-csharp-extractor.md b/docs/proposals/P-001-csharp-extractor.md index da58ec5b..cb7fe855 100644 --- a/docs/proposals/P-001-csharp-extractor.md +++ b/docs/proposals/P-001-csharp-extractor.md @@ -18,7 +18,8 @@ seam: - **CI** (`wpf-extractor` job): real `.cs` → extractor → facts → core → leak at its C# line; the disposed sample stays silent. -Next: timers, `IDisposable` fields, and feeding region facts to OWN014. +Next: `IDisposable` fields, and feeding region facts to OWN014 (timers built — +the WPF002 increment, see [P-004](P-004-wpf-lifetime-profile.md)). ## Motivation diff --git a/docs/proposals/P-004-wpf-lifetime-profile.md b/docs/proposals/P-004-wpf-lifetime-profile.md index 6f5dc899..a9e296c3 100644 --- a/docs/proposals/P-004-wpf-lifetime-profile.md +++ b/docs/proposals/P-004-wpf-lifetime-profile.md @@ -1,6 +1,7 @@ # P-004 — WPF / UI lifetime leak profile -- **Status:** draft (P0 — the user's real pain; extends P-001 v0) +- **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer) built**; + WPF003–005 next - **Depends on:** [P-001](P-001-csharp-extractor.md) (the extractor + OwnIR seam), `spec/OwnCore.md`, `spec/Lifetimes.md` (OWN001 leak, OWN014 region escape). See [`docs/ROADMAP.md`](../ROADMAP.md) for where this sits (Milestones 1–2). @@ -27,7 +28,7 @@ ends `ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements | Rule | Pattern | Core verdict | |------|---------|--------------| | **WPF001** | `source.Event += handler` with no matching `-=` in `Dispose`/`OnClosed`/`Unloaded` | `OWN001` (leak) ✅ v0 | -| **WPF002** | `DispatcherTimer`/`Timer` started (`Tick +=` / `Start()`) with no `Stop()` + detach | `OWN001` | +| **WPF002** | `DispatcherTimer`/`Timer` `Tick`/`Elapsed` handler with no `-=` and no `Stop()` | `OWN001` `[resource: timer]` ✅ | | **WPF003** | an `IDisposable` subscription field never disposed by the owner | `OWN001` (see P-005) | | **WPF004** | `Subscribe(...)` whose `IDisposable` result is ignored | `OWN001` | | **WPF005** | strong capture by a longer-lived source (the ViewModel `escapes` to App) | `OWN014` | @@ -71,8 +72,10 @@ facts so OWN014 fires for WPF005. --[core]--> OWN001 (leak) / OWN014 (escape) @ C# line ``` -Land **one pattern per increment** (WPF002 next, then WPF003/004, then WPF005), -each with `bad_*.cs` / `ok_*.cs` fixtures, exactly as v0 did. WPF003 overlaps the +Land **one pattern per increment** (WPF002 built — a `Tick`/`Elapsed` handler is +a `Timer` resource, released by `-=` or a `Stop()` on the same receiver; next +WPF003/004, then WPF005), each with `bad`/`ok` samples, exactly as v0 did. +WPF003 overlaps the general `IDisposable`-field rule in [P-005](P-005-idisposable-ownership.md); build it once in the resource core and let WPF consume it as a profile. diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 21ee0762..d2c779c3 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -5,10 +5,12 @@ // spec's vocabulary. The Python core (`python -m ownlang ownir facts.json`) then // produces the verdict (OWN001 leak) at the C# location. // -// v0 heuristic (documented in docs/proposals/P-001): a subscription is -// `target += handler` where the right side is a method group (identifier or -// member access), not e.g. `count += 1`. It is "released" if a matching -// `target -= handler` (same text on both sides) exists anywhere in the class. +// Heuristic (docs/proposals/P-001, P-004): a subscription is `target += handler` +// where the right side is a method group (identifier or member access), not e.g. +// `count += 1`. It is "released" if a matching `target -= handler` (same text on +// both sides) exists in the class. A `Tick`/`Elapsed` handler is additionally +// tagged resource=timer (WPF002) and counts as released if the timer's receiver +// also has a `.Stop()` call (e.g. `_timer.Stop()` in Dispose). // // Usage: ownsharp-extract [more.cs ...] [-o facts.json] @@ -37,6 +39,18 @@ static bool IsHandler(ExpressionSyntax rhs) => static int LineOf(SyntaxNode node) => node.GetLocation().GetLineSpan().StartLinePosition.Line + 1; +// The receiver of `target.Member` ("_timer" for `_timer.Tick`), or null when the +// left side is a bare identifier (`Changed += h`). +static string? Receiver(ExpressionSyntax expr) => + expr is MemberAccessExpressionSyntax m ? m.Expression.ToString() : null; + +// A timer subscription is a `Tick`/`Elapsed` handler — DispatcherTimer and the +// WinForms timer expose `Tick`, System.Timers.Timer exposes `Elapsed`. A running +// timer strong-refs the handler's owner, so an undetached one leaks it. +static bool IsTimerEvent(ExpressionSyntax left) => + left is MemberAccessExpressionSyntax m + && (m.Name.Identifier.Text == "Tick" || m.Name.Identifier.Text == "Elapsed"); + var components = new List(); foreach (var path in inputs) @@ -55,17 +69,29 @@ static int LineOf(SyntaxNode node) => if (a.IsKind(SyntaxKind.SubtractAssignmentExpression) && IsHandler(a.Right)) unsub.Add($"{a.Left}|{a.Right}"); + // every receiver with a `.Stop()` call: a timer detached this way counts + // as released even without an explicit `Tick -=` (e.g. Stop() in Dispose). + var stopped = new HashSet(); + foreach (var inv in cls.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Stop") + stopped.Add(m.Expression.ToString()); + var subs = new List(); foreach (var a in assigns) { if (!a.IsKind(SyntaxKind.AddAssignmentExpression) || !IsHandler(a.Right)) continue; + var isTimer = IsTimerEvent(a.Left); + var released = unsub.Contains($"{a.Left}|{a.Right}") + || (isTimer && Receiver(a.Left) is { } recv && stopped.Contains(recv)); subs.Add(new { @event = a.Left.ToString(), handler = a.Right.ToString(), line = LineOf(a.Left), - released = unsub.Contains($"{a.Left}|{a.Right}"), + released, + resource = isTimer ? "timer" : "subscription", }); } diff --git a/frontend/roslyn/samples/TimerViewModel.cs b/frontend/roslyn/samples/TimerViewModel.cs new file mode 100644 index 00000000..fa559766 --- /dev/null +++ b/frontend/roslyn/samples/TimerViewModel.cs @@ -0,0 +1,39 @@ +using System; +using System.Windows.Threading; + +namespace WpfApp; + +// A DispatcherTimer whose Tick handler is never detached and the timer is never +// stopped: the running timer keeps this view-model alive. The core reports +// OWN001 [resource: timer] at the `+=` line. +public sealed class TimerViewModel +{ + private readonly DispatcherTimer _timer = new(); + + public TimerViewModel() + { + _timer.Tick += OnTick; // acquire (timer) — never stopped/detached => leak + _timer.Start(); + } + + private void OnTick(object? sender, EventArgs e) { } +} + +// The same timer, stopped on teardown — released, so the core stays silent. +public sealed class CleanTimerViewModel : IDisposable +{ + private readonly DispatcherTimer _timer = new(); + + public CleanTimerViewModel() + { + _timer.Tick += OnTick; + _timer.Start(); + } + + private void OnTick(object? sender, EventArgs e) { } + + public void Dispose() + { + _timer.Stop(); // release via Stop() + } +} diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 14c86af3..98b4386d 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -6,7 +6,7 @@ checker, and maps the verdict back to the original C# location. The core stays a single checker — we do not reimplement it in C# (a second checker would drift). -OwnIR v0 schema (JSON):: +OwnIR schema (JSON):: { "ownir_version": 0, @@ -17,19 +17,24 @@ "file": "CustomerViewModel.cs", "subscriptions": [ {"event": "bus.CustomerChanged", "handler": "OnCustomerChanged", - "line": 12, "released": false} + "line": 12, "released": false}, + {"event": "_timer.Tick", "handler": "OnTick", "line": 18, + "released": false, "resource": "timer"} ] } ] } -A subscription is modelled as an owned `Subscription` resource: `event +=` is an -`acquire`, a matching `-=` / Dispose is a `release`. An unreleased subscription -is therefore the core's OWN001 (owned-but-not-released), carrying the -`[resource: subscription token]` kind tag — surfaced at the C# `line`. +Each entry in `subscriptions` is an owned resource: `event +=` / `Tick +=` is an +`acquire`, a matching `-=` / `Dispose` / timer `Stop()` is a `release`. The +optional `resource` field picks the kind — "subscription" (default; tag +`[resource: subscription token]`) or "timer" (a started `DispatcherTimer`/`Timer` +whose `Tick`/`Elapsed` handler is never detached; tag `[resource: timer]`). An +unreleased entry is the core's OWN001 (owned-but-not-released) at the C# `line`. -v0 covers exactly the `event += without -=` pattern (released == false -> leak). -Timers, IDisposable fields and region escape are later (see docs/proposals/P-001). +The `resource` field is additive and optional, so it does NOT bump +`ownir_version`: an older core just reads every entry as a subscription. +IDisposable fields and region escape are later (see docs/proposals/P-004). """ from __future__ import annotations @@ -58,8 +63,22 @@ class OwnIRError(ValueError): ' release Dispose\n' ' kind "subscription token"\n' '}\n' + 'resource Timer {\n' + ' acquire Start\n' + ' release Stop\n' + ' kind "timer"\n' + '}\n' ) +# OwnIR resource kinds the bridge knows how to lower: (own resource type to +# acquire, human kind tag the finding carries). `event +=` is a Subscription; a +# `Tick`/`Elapsed` handler on a started timer is a Timer (the running timer +# strong-refs the handler's owner). Unknown values fall back to Subscription. +_RESOURCES = { + "subscription": ("Subscription", "subscription token"), + "timer": ("Timer", "timer"), +} + @dataclass(frozen=True) class Finding: @@ -70,10 +89,11 @@ class Finding: event: str handler: str message: str + kind: str = "subscription token" def render(self) -> str: return (f"{self.file}:{self.line}: error: [{self.code}] " - f"{self.message} [resource: subscription token]") + f"{self.message} [resource: {self.kind}]") def load(path: str) -> dict[str, Any]: @@ -106,6 +126,11 @@ def load(path: str) -> dict[str, Any]: subs = c.get("subscriptions", []) if not isinstance(subs, list) or not all(isinstance(s, dict) for s in subs): raise OwnIRError("each component's 'subscriptions' must be objects") + for s in subs: + r = s.get("resource", "subscription") + if not isinstance(r, str): + raise OwnIRError( + f"subscription 'resource' must be a string, got {r!r}") return result @@ -137,7 +162,9 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: gid += 1 handles[handle] = {**sub, "component": cname, "file": comp.get("file", "?")} - lines.append(f" let {handle} = acquire Subscription();") + rtype, _ = _RESOURCES.get(sub.get("resource", "subscription"), + _RESOURCES["subscription"]) + lines.append(f" let {handle} = acquire {rtype}();") if sub.get("released"): lines.append(f" release {handle};") lines.append("}") @@ -196,13 +223,22 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: f"message={d.message!r}). The OwnIR lowering has drifted from " f"the core; teach the bridge this diagnostic rather than " f"dropping the finding.") + event = sub.get("event", "?") + handler = sub.get("handler", "?") + component = sub["component"] + rkind = sub.get("resource", "subscription") + _, kind = _RESOURCES.get(rkind, _RESOURCES["subscription"]) + if rkind == "timer": + message = (f"timer '{event}' (handler '{handler}') is started but " + f"never stopped or detached — the running timer keeps " + f"'{component}' alive (leak)") + else: + message = (f"event '{event}' is subscribed (handler '{handler}') " + f"but never unsubscribed — the source keeps " + f"'{component}' alive (leak)") findings.append(Finding( file=sub["file"], line=int(sub.get("line", 0)), code=d.code, - component=sub["component"], event=sub.get("event", "?"), - handler=sub.get("handler", "?"), - message=(f"event '{sub.get('event', '?')}' is subscribed " - f"(handler '{sub.get('handler', '?')}') but never " - f"unsubscribed — the source keeps " - f"'{sub['component']}' alive (leak)"))) + component=component, event=event, handler=handler, + message=message, kind=kind)) findings.sort(key=lambda f: (f.file, f.line, f.code)) return findings diff --git a/tests/fixtures/ownir/timer.facts.json b/tests/fixtures/ownir/timer.facts.json new file mode 100644 index 00000000..370d5672 --- /dev/null +++ b/tests/fixtures/ownir/timer.facts.json @@ -0,0 +1,20 @@ +{ + "ownir_version": 0, + "module": "WpfTimers", + "components": [ + { + "name": "TimerViewModel", + "file": "TimerViewModel.cs", + "subscriptions": [ + {"event": "_timer.Tick", "handler": "OnTick", "line": 15, "released": false, "resource": "timer"} + ] + }, + { + "name": "CleanTimerViewModel", + "file": "TimerViewModel.cs", + "subscriptions": [ + {"event": "_timer.Tick", "handler": "OnTick", "line": 29, "released": true, "resource": "timer"} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 8b9d9de1..2dc3c7d3 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -30,6 +30,8 @@ _FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "sample.facts.json") +_TIMER_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", + "timer.facts.json") def _write_facts(obj: dict) -> str: @@ -109,6 +111,30 @@ def run() -> int: except OwnIRError as e: fails.append(f"versionless facts wrongly rejected: {e}") + # --- WPF002 timer profile: a started timer never stopped/detached leaks, + # a stopped one stays silent, and the finding is tagged [resource: timer]. + with open(_TIMER_FIXTURE, encoding="utf-8") as f: + tfacts = json.load(f) + tfindings = check_facts(tfacts) + checks += 1 + leaks = [x for x in tfindings if x.component == "TimerViewModel"] + if len(tfindings) != 1 or not leaks: + fails.append(f"expected 1 timer finding (TimerViewModel), got " + f"{[(x.component, x.code) for x in tfindings]}") + else: + t0 = leaks[0] + checks += 1 + if (t0.file, t0.line, t0.code) != ("TimerViewModel.cs", 15, "OWN001"): + fails.append(f"wrong timer location/code: {t0.file}:{t0.line} {t0.code}") + if "timer" not in t0.message or "stopped" not in t0.message: + fails.append(f"timer message missing timer/stopped: {t0.message!r}") + if "[resource: timer]" not in t0.render(): + fails.append(f"timer finding missing kind tag: {t0.render()!r}") + # a stopped timer (released) must NOT be reported. + checks += 1 + if any(x.component == "CleanTimerViewModel" for x in tfindings): + fails.append("stopped timer was wrongly reported") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From 3efc926ef867063b189aa8690b7b588ad22b15b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 14:46:28 +0000 Subject: [PATCH 4/9] =?UTF-8?q?ownir:=20WPF003=20=E2=80=94=20IDisposable?= =?UTF-8?q?=20field=20never=20disposed=20(P-004=20/=20P-005=20D2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An IDisposable field the class constructs (`new`) but never disposes leaks it (OWN001, tagged [resource: disposable field]). "Owned, not injected" = the field is assigned a `new` in this class; "released" = a `.Dispose()` call exists somewhere in the class. - ownir.py: new "disposable" resource kind (Disposable resource, kind "disposable field"); optional `type` names the field's declared type in the message. Additive — no ownir_version bump. Docstring now describes `subscriptions` as the (historically named) owned-resource list with a `resource` discriminator. - Roslyn extractor: detect disposable fields by a curated type heuristic (syntax-only — no semantic model), gated on the class `new`ing the field so injected/borrowed disposables are not flagged; released iff disposed. - Sample DisposableFieldViewModel.cs (leaking CTS + one disposed in Dispose) and a disposable.facts.json fixture; test_ownir pins the leak, the type in the message, the [resource: disposable field] tag, and silence on the disposed one. CI asserts the same on the real extractor output. - Docs: P-004/P-005/ROADMAP mark WPF003 built. Python bridge verified locally (14/14); extractor CI-validated. --- .github/workflows/ci.yml | 13 +++- docs/ROADMAP.md | 2 +- docs/proposals/P-004-wpf-lifetime-profile.md | 6 +- docs/proposals/P-005-idisposable-ownership.md | 4 +- frontend/roslyn/OwnSharp.Extractor/Program.cs | 61 +++++++++++++++++++ .../samples/DisposableFieldViewModel.cs | 32 ++++++++++ ownlang/ownir.py | 44 +++++++++---- tests/fixtures/ownir/disposable.facts.json | 20 ++++++ tests/test_ownir.py | 28 +++++++++ 9 files changed, 193 insertions(+), 17 deletions(-) create mode 100644 frontend/roslyn/samples/DisposableFieldViewModel.cs create mode 100644 tests/fixtures/ownir/disposable.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 25922c9b..eb279b41 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -110,6 +110,7 @@ jobs: frontend/roslyn/samples/CustomerViewModel.cs \ frontend/roslyn/samples/OrdersViewModel.cs \ frontend/roslyn/samples/TimerViewModel.cs \ + frontend/roslyn/samples/DisposableFieldViewModel.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" - name: Check facts through the core @@ -132,5 +133,15 @@ jobs: if echo "$out" | grep -q "CleanTimerViewModel"; then echo "FAIL: stopped timer wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 (subscription + timer) at the C# location" + # WPF003: the IDisposable field the class new's but never disposes leaks + # with a [resource: disposable field] tag; the one disposed in Dispose + # stays silent. + echo "$out" | grep -q "DisposableFieldViewModel.cs" \ + || { echo "FAIL: expected the ReportViewModel field leak"; exit 1; } + echo "$out" | grep -q "resource: disposable field" \ + || { echo "FAIL: expected a [resource: disposable field] tag"; exit 1; } + if echo "$out" | grep -q "CleanReportViewModel"; then + echo "FAIL: disposed field wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer + field) at the C# location" diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 0bdf9b86..c7388e66 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -68,7 +68,7 @@ architectural strictness, and the borrow-checker showcase): 1. `WPF001` — event/subscription `+=` without `-=` (the WPF spike; P-001 v0 ✅) 2. `WPF002` — `DispatcherTimer`/`Timer` `Tick`/`Elapsed` without stop/detach ✅ -3. `BOR/OWN` — `IDisposable` field not disposed by its owner +3. `OWN001` — `IDisposable` field the class `new`s but never disposes ✅ 4. `DI001` — singleton captures a scoped dependency 5. `POOL` — `Span`/view used after `ArrayPool.Return` diff --git a/docs/proposals/P-004-wpf-lifetime-profile.md b/docs/proposals/P-004-wpf-lifetime-profile.md index a9e296c3..06e2034c 100644 --- a/docs/proposals/P-004-wpf-lifetime-profile.md +++ b/docs/proposals/P-004-wpf-lifetime-profile.md @@ -1,7 +1,7 @@ # P-004 — WPF / UI lifetime leak profile -- **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer) built**; - WPF003–005 next +- **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer)** + **WPF003 + (IDisposable field) built**; WPF004–005 next - **Depends on:** [P-001](P-001-csharp-extractor.md) (the extractor + OwnIR seam), `spec/OwnCore.md`, `spec/Lifetimes.md` (OWN001 leak, OWN014 region escape). See [`docs/ROADMAP.md`](../ROADMAP.md) for where this sits (Milestones 1–2). @@ -29,7 +29,7 @@ ends `ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements |------|---------|--------------| | **WPF001** | `source.Event += handler` with no matching `-=` in `Dispose`/`OnClosed`/`Unloaded` | `OWN001` (leak) ✅ v0 | | **WPF002** | `DispatcherTimer`/`Timer` `Tick`/`Elapsed` handler with no `-=` and no `Stop()` | `OWN001` `[resource: timer]` ✅ | -| **WPF003** | an `IDisposable` subscription field never disposed by the owner | `OWN001` (see P-005) | +| **WPF003** | an `IDisposable` field the class `new`s but never disposes | `OWN001` `[resource: disposable field]` ✅ (core of P-005) | | **WPF004** | `Subscribe(...)` whose `IDisposable` result is ignored | `OWN001` | | **WPF005** | strong capture by a longer-lived source (the ViewModel `escapes` to App) | `OWN014` | diff --git a/docs/proposals/P-005-idisposable-ownership.md b/docs/proposals/P-005-idisposable-ownership.md index 8aa32bd9..de3000c5 100644 --- a/docs/proposals/P-005-idisposable-ownership.md +++ b/docs/proposals/P-005-idisposable-ownership.md @@ -1,6 +1,8 @@ # P-005 — `IDisposable` ownership profile -- **Status:** draft (P0 — the most down-to-earth resource module) +- **Status:** draft (P0 — the most down-to-earth resource module). D2 (owned + field never disposed) has a first cut shipped via WPF003 + ([P-004](P-004-wpf-lifetime-profile.md)); D1/D3/D4/D5 here generalise it. - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release, OWN003 double-release), [P-001](P-001-csharp-extractor.md) (the C# seam). Shares the resource core with [P-004](P-004-wpf-lifetime-profile.md). diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index d2c779c3..8f96f99a 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -51,6 +51,24 @@ static bool IsTimerEvent(ExpressionSyntax left) => left is MemberAccessExpressionSyntax m && (m.Name.Identifier.Text == "Tick" || m.Name.Identifier.Text == "Elapsed"); +// The field name an expression refers to: "_f" for `_f` or `this._f`, else null. +static string? FieldName(ExpressionSyntax expr) => expr switch +{ + IdentifierNameSyntax id => id.Identifier.Text, + MemberAccessExpressionSyntax m => m.Name.Identifier.Text, + _ => null, +}; + +// A field type treated as owned-disposable (syntax-only heuristic — no semantic +// model): a curated set plus a few suffixes. Gated on the class `new`ing the +// field (see below), so injected/borrowed disposables are not flagged. +static bool IsDisposableType(string t) => + t is "IDisposable" or "IAsyncDisposable" or "DispatcherTimer" or "Timer" + or "CancellationTokenSource" or "HttpClient" or "SerialPort" + or "SqlConnection" + || t.EndsWith("Stream") || t.EndsWith("Reader") || t.EndsWith("Writer") + || t.EndsWith("Timer") || t.EndsWith("Subscription"); + var components = new List(); foreach (var path in inputs) @@ -95,6 +113,49 @@ left is MemberAccessExpressionSyntax m }); } + // WPF003: an IDisposable field the class constructs (`new`) but never + // disposes. Owned (not injected) = assigned a `new` in this class; + // released = a `.Dispose()` call somewhere in the class. + var constructed = new HashSet(); + foreach (var fd in cls.Members.OfType()) + foreach (var v in fd.Declaration.Variables) + if (v.Initializer?.Value is ObjectCreationExpressionSyntax + or ImplicitObjectCreationExpressionSyntax) + constructed.Add(v.Identifier.Text); + foreach (var a in assigns) + if (a.IsKind(SyntaxKind.SimpleAssignmentExpression) + && a.Right is ObjectCreationExpressionSyntax + or ImplicitObjectCreationExpressionSyntax + && FieldName(a.Left) is { } fn) + constructed.Add(fn); + + var disposed = new HashSet(); + foreach (var inv in cls.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Dispose" + && FieldName(m.Expression) is { } df) + disposed.Add(df); + + foreach (var fd in cls.Members.OfType()) + { + var tname = fd.Declaration.Type.ToString(); + if (!IsDisposableType(tname)) + continue; + foreach (var v in fd.Declaration.Variables) + { + if (!constructed.Contains(v.Identifier.Text)) + continue; + subs.Add(new + { + @event = v.Identifier.Text, + line = LineOf(v), + released = disposed.Contains(v.Identifier.Text), + resource = "disposable", + type = tname, + }); + } + } + if (subs.Count > 0) components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs }); } diff --git a/frontend/roslyn/samples/DisposableFieldViewModel.cs b/frontend/roslyn/samples/DisposableFieldViewModel.cs new file mode 100644 index 00000000..f7948501 --- /dev/null +++ b/frontend/roslyn/samples/DisposableFieldViewModel.cs @@ -0,0 +1,32 @@ +using System; +using System.Threading; + +namespace WpfApp; + +// A CancellationTokenSource the view-model creates but never disposes: the owner +// leaks it. The core reports OWN001 [resource: disposable field] at the field. +public sealed class ReportViewModel +{ + private readonly CancellationTokenSource _cts = new(); + + public void Refresh() + { + _cts.Cancel(); // used, but never disposed => leak + } +} + +// The same field, disposed on teardown — released, so the core stays silent. +public sealed class CleanReportViewModel : IDisposable +{ + private readonly CancellationTokenSource _cts = new(); + + public void Refresh() + { + _cts.Cancel(); + } + + public void Dispose() + { + _cts.Dispose(); // release + } +} diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 98b4386d..7c2f79a4 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -25,16 +25,22 @@ ] } -Each entry in `subscriptions` is an owned resource: `event +=` / `Tick +=` is an -`acquire`, a matching `-=` / `Dispose` / timer `Stop()` is a `release`. The -optional `resource` field picks the kind — "subscription" (default; tag -`[resource: subscription token]`) or "timer" (a started `DispatcherTimer`/`Timer` -whose `Tick`/`Elapsed` handler is never detached; tag `[resource: timer]`). An -unreleased entry is the core's OWN001 (owned-but-not-released) at the C# `line`. - -The `resource` field is additive and optional, so it does NOT bump -`ownir_version`: an older core just reads every entry as a subscription. -IDisposable fields and region escape are later (see docs/proposals/P-004). +Each entry in `subscriptions` (historically named — it is really the list of +owned-resource records) is an owned resource, discriminated by an optional +`resource` field: + + - "subscription" (default): `event +=` acquires, a matching `-=` releases; + tag `[resource: subscription token]`. + - "timer": a started `DispatcherTimer`/`Timer` whose `Tick`/`Elapsed` handler + is never `-=`'d or `Stop()`ped; tag `[resource: timer]`. + - "disposable": an `IDisposable` field the class `new`s and never `Dispose()`s + (optional `type` names the field's declared type); tag + `[resource: disposable field]`. + +An unreleased entry is the core's OWN001 (owned-but-not-released) at the C# +`line`. The `resource`/`type` fields are additive and optional, so they do NOT +bump `ownir_version`: an older core just reads every entry as a subscription. +Region escape (OWN014) is later (see docs/proposals/P-004). """ from __future__ import annotations @@ -68,15 +74,22 @@ class OwnIRError(ValueError): ' release Stop\n' ' kind "timer"\n' '}\n' + 'resource Disposable {\n' + ' acquire New\n' + ' release Dispose\n' + ' kind "disposable field"\n' + '}\n' ) # OwnIR resource kinds the bridge knows how to lower: (own resource type to # acquire, human kind tag the finding carries). `event +=` is a Subscription; a # `Tick`/`Elapsed` handler on a started timer is a Timer (the running timer -# strong-refs the handler's owner). Unknown values fall back to Subscription. +# strong-refs the handler's owner); an `IDisposable` field the class `new`s is a +# Disposable it owns. Unknown values fall back to Subscription. _RESOURCES = { "subscription": ("Subscription", "subscription token"), "timer": ("Timer", "timer"), + "disposable": ("Disposable", "disposable field"), } @@ -131,6 +144,10 @@ def load(path: str) -> dict[str, Any]: if not isinstance(r, str): raise OwnIRError( f"subscription 'resource' must be a string, got {r!r}") + t = s.get("type") + if t is not None and not isinstance(t, str): + raise OwnIRError( + f"subscription 'type' must be a string, got {t!r}") return result @@ -232,6 +249,11 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: message = (f"timer '{event}' (handler '{handler}') is started but " f"never stopped or detached — the running timer keeps " f"'{component}' alive (leak)") + elif rkind == "disposable": + typ = sub.get("type") + of_type = f" (type '{typ}')" if typ else "" + message = (f"IDisposable field '{event}'{of_type} is never " + f"disposed — its owner '{component}' leaks it (leak)") else: message = (f"event '{event}' is subscribed (handler '{handler}') " f"but never unsubscribed — the source keeps " diff --git a/tests/fixtures/ownir/disposable.facts.json b/tests/fixtures/ownir/disposable.facts.json new file mode 100644 index 00000000..646e7a2b --- /dev/null +++ b/tests/fixtures/ownir/disposable.facts.json @@ -0,0 +1,20 @@ +{ + "ownir_version": 0, + "module": "WpfDisposables", + "components": [ + { + "name": "ReportViewModel", + "file": "DisposableFieldViewModel.cs", + "subscriptions": [ + {"event": "_cts", "line": 11, "released": false, "resource": "disposable", "type": "CancellationTokenSource"} + ] + }, + { + "name": "CleanReportViewModel", + "file": "DisposableFieldViewModel.cs", + "subscriptions": [ + {"event": "_cts", "line": 25, "released": true, "resource": "disposable", "type": "CancellationTokenSource"} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 2dc3c7d3..61d41dac 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -32,6 +32,8 @@ "sample.facts.json") _TIMER_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "timer.facts.json") +_DISPOSABLE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "disposable.facts.json") def _write_facts(obj: dict) -> str: @@ -135,6 +137,32 @@ def run() -> int: if any(x.component == "CleanTimerViewModel" for x in tfindings): fails.append("stopped timer was wrongly reported") + # --- WPF003 IDisposable field: a field the class new's and never disposes + # leaks; one disposed in Dispose() stays silent; tag [resource: disposable field]. + with open(_DISPOSABLE_FIXTURE, encoding="utf-8") as f: + dfacts = json.load(f) + dfindings = check_facts(dfacts) + checks += 1 + dleaks = [x for x in dfindings if x.component == "ReportViewModel"] + if len(dfindings) != 1 or not dleaks: + fails.append(f"expected 1 disposable finding (ReportViewModel), got " + f"{[(x.component, x.code) for x in dfindings]}") + else: + d0 = dleaks[0] + checks += 1 + if (d0.file, d0.line, d0.code) != ("DisposableFieldViewModel.cs", 11, "OWN001"): + fails.append(f"wrong field location/code: {d0.file}:{d0.line} {d0.code}") + if "IDisposable field" not in d0.message or "_cts" not in d0.message: + fails.append(f"disposable message missing field: {d0.message!r}") + if "CancellationTokenSource" not in d0.message: + fails.append(f"disposable message missing type: {d0.message!r}") + if "[resource: disposable field]" not in d0.render(): + fails.append(f"disposable finding missing kind tag: {d0.render()!r}") + # a field disposed in Dispose() (released) must NOT be reported. + checks += 1 + if any(x.component == "CleanReportViewModel" for x in dfindings): + fails.append("disposed field was wrongly reported") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From a21599d61673c2640e8f189d7a69f9e332ebe0a7 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 14:49:23 +0000 Subject: [PATCH 5/9] =?UTF-8?q?ownir:=20WPF004=20=E2=80=94=20ignored=20Sub?= =?UTF-8?q?scribe()=20result=20(P-004)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A `X.Subscribe(...)` whose IDisposable result is ignored (the call stands as a bare statement, not assigned/returned/added) drops the subscription token, so it is never disposed and leaks (OWN001, tagged [resource: subscription token]). - ownir.py: new "subscribe" resource kind (maps to the Subscription resource / subscription-token tag, with its own "result ignored" message). Additive — no ownir_version bump. - Roslyn extractor: flag member-access `x.Subscribe(...)` calls whose parent is an ExpressionStatement (result discarded); member-access only, to avoid bare void `Subscribe(...)` helpers. A captured-and-disposed token is not flagged. - Sample MessengerViewModel.cs (ignored Subscribe + captured/disposed clean one) and a subscribe.facts.json fixture; test_ownir pins the leak, the "ignored" message, and the [resource: subscription token] tag. CI asserts the same on the real extractor output. - Docs: P-004 marks WPF004 built. Python bridge verified locally (16/16); extractor CI-validated. --- .github/workflows/ci.yml | 12 ++++++- docs/proposals/P-004-wpf-lifetime-profile.md | 12 ++++--- frontend/roslyn/OwnSharp.Extractor/Program.cs | 16 +++++++++ frontend/roslyn/samples/MessengerViewModel.cs | 36 +++++++++++++++++++ ownlang/ownir.py | 8 +++++ tests/fixtures/ownir/subscribe.facts.json | 13 +++++++ tests/test_ownir.py | 21 +++++++++++ 7 files changed, 112 insertions(+), 6 deletions(-) create mode 100644 frontend/roslyn/samples/MessengerViewModel.cs create mode 100644 tests/fixtures/ownir/subscribe.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eb279b41..e1f2df7c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -111,6 +111,7 @@ jobs: frontend/roslyn/samples/OrdersViewModel.cs \ frontend/roslyn/samples/TimerViewModel.cs \ frontend/roslyn/samples/DisposableFieldViewModel.cs \ + frontend/roslyn/samples/MessengerViewModel.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" - name: Check facts through the core @@ -143,5 +144,14 @@ jobs: if echo "$out" | grep -q "CleanReportViewModel"; then echo "FAIL: disposed field wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 (subscription + timer + field) at the C# location" + # WPF004: an ignored `X.Subscribe(...)` result leaks; the captured+ + # disposed one stays silent. "ignored" is unique to the WPF004 message. + echo "$out" | grep -q "MessengerViewModel.cs" \ + || { echo "FAIL: expected the InboxViewModel ignored-Subscribe leak"; exit 1; } + echo "$out" | grep -q "is ignored" \ + || { echo "FAIL: expected the ignored-Subscribe message"; exit 1; } + if echo "$out" | grep -q "CleanInboxViewModel"; then + echo "FAIL: captured+disposed subscription wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe) at the C# location" diff --git a/docs/proposals/P-004-wpf-lifetime-profile.md b/docs/proposals/P-004-wpf-lifetime-profile.md index 06e2034c..407024b6 100644 --- a/docs/proposals/P-004-wpf-lifetime-profile.md +++ b/docs/proposals/P-004-wpf-lifetime-profile.md @@ -1,7 +1,8 @@ # P-004 — WPF / UI lifetime leak profile - **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer)** + **WPF003 - (IDisposable field) built**; WPF004–005 next + (IDisposable field)** + **WPF004 (ignored Subscribe) built**; WPF005 (escape) + next - **Depends on:** [P-001](P-001-csharp-extractor.md) (the extractor + OwnIR seam), `spec/OwnCore.md`, `spec/Lifetimes.md` (OWN001 leak, OWN014 region escape). See [`docs/ROADMAP.md`](../ROADMAP.md) for where this sits (Milestones 1–2). @@ -30,7 +31,7 @@ ends `ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements | **WPF001** | `source.Event += handler` with no matching `-=` in `Dispose`/`OnClosed`/`Unloaded` | `OWN001` (leak) ✅ v0 | | **WPF002** | `DispatcherTimer`/`Timer` `Tick`/`Elapsed` handler with no `-=` and no `Stop()` | `OWN001` `[resource: timer]` ✅ | | **WPF003** | an `IDisposable` field the class `new`s but never disposes | `OWN001` `[resource: disposable field]` ✅ (core of P-005) | -| **WPF004** | `Subscribe(...)` whose `IDisposable` result is ignored | `OWN001` | +| **WPF004** | `X.Subscribe(...)` whose `IDisposable` result is ignored (bare statement) | `OWN001` `[resource: subscription token]` ✅ | | **WPF005** | strong capture by a longer-lived source (the ViewModel `escapes` to App) | `OWN014` | Modelled as resource facts (no new magic — the resource is just named @@ -72,9 +73,10 @@ facts so OWN014 fires for WPF005. --[core]--> OWN001 (leak) / OWN014 (escape) @ C# line ``` -Land **one pattern per increment** (WPF002 built — a `Tick`/`Elapsed` handler is -a `Timer` resource, released by `-=` or a `Stop()` on the same receiver; next -WPF003/004, then WPF005), each with `bad`/`ok` samples, exactly as v0 did. +Land **one pattern per increment** (WPF002/003/004 built — a `Tick`/`Elapsed` +handler is a `Timer`; a `new`'d-and-undisposed `IDisposable` field is a +`Disposable`; an ignored `X.Subscribe(...)` is a dropped subscription token; +WPF005 escape next), each with `bad`/`ok` samples, exactly as v0 did. WPF003 overlaps the general `IDisposable`-field rule in [P-005](P-005-idisposable-ownership.md); build it once in the resource core and let WPF consume it as a profile. diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 8f96f99a..b3220cf3 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -156,6 +156,22 @@ or ImplicitObjectCreationExpressionSyntax } } + // WPF004: a `X.Subscribe(...)` whose IDisposable result is ignored — the + // call stands as a bare statement (not assigned/returned/added), so the + // token is dropped and never disposed. Member-access only (`x.Subscribe`), + // to avoid flagging bare void `Subscribe(...)` helpers. + foreach (var inv in cls.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Subscribe" + && inv.Parent is ExpressionStatementSyntax) + subs.Add(new + { + @event = m.ToString(), + line = LineOf(inv), + released = false, + resource = "subscribe", + }); + if (subs.Count > 0) components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs }); } diff --git a/frontend/roslyn/samples/MessengerViewModel.cs b/frontend/roslyn/samples/MessengerViewModel.cs new file mode 100644 index 00000000..d7d17688 --- /dev/null +++ b/frontend/roslyn/samples/MessengerViewModel.cs @@ -0,0 +1,36 @@ +using System; + +namespace WpfApp; + +// The result of Subscribe(...) is an IDisposable token; here it is ignored, so +// the subscription is never disposed and leaks. The core reports OWN001 +// [resource: subscription token] at the call. +public sealed class InboxViewModel +{ + public InboxViewModel(IMessenger messenger) + { + messenger.Subscribe(OnMessage); // result ignored => leak + } + + private void OnMessage(object msg) { } +} + +// The token is captured in a field and disposed on teardown — not flagged. +public sealed class CleanInboxViewModel : IDisposable +{ + private readonly IDisposable _sub; + + public CleanInboxViewModel(IMessenger messenger) + { + _sub = messenger.Subscribe(OnMessage); + } + + private void OnMessage(object msg) { } + + public void Dispose() => _sub.Dispose(); +} + +public interface IMessenger +{ + IDisposable Subscribe(Action handler); +} diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 7c2f79a4..0645d7f3 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -36,6 +36,9 @@ - "disposable": an `IDisposable` field the class `new`s and never `Dispose()`s (optional `type` names the field's declared type); tag `[resource: disposable field]`. + - "subscribe": a `X.Subscribe(...)` whose `IDisposable` result is ignored (a + bare statement, not captured/disposed) — always a leak; tag + `[resource: subscription token]`. An unreleased entry is the core's OWN001 (owned-but-not-released) at the C# `line`. The `resource`/`type` fields are additive and optional, so they do NOT @@ -88,6 +91,7 @@ class OwnIRError(ValueError): # Disposable it owns. Unknown values fall back to Subscription. _RESOURCES = { "subscription": ("Subscription", "subscription token"), + "subscribe": ("Subscription", "subscription token"), "timer": ("Timer", "timer"), "disposable": ("Disposable", "disposable field"), } @@ -254,6 +258,10 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: of_type = f" (type '{typ}')" if typ else "" message = (f"IDisposable field '{event}'{of_type} is never " f"disposed — its owner '{component}' leaks it (leak)") + elif rkind == "subscribe": + message = (f"the result of '{event}' is ignored — the IDisposable " + f"subscription is never disposed, leaking " + f"'{component}' (leak)") else: message = (f"event '{event}' is subscribed (handler '{handler}') " f"but never unsubscribed — the source keeps " diff --git a/tests/fixtures/ownir/subscribe.facts.json b/tests/fixtures/ownir/subscribe.facts.json new file mode 100644 index 00000000..f43e72b1 --- /dev/null +++ b/tests/fixtures/ownir/subscribe.facts.json @@ -0,0 +1,13 @@ +{ + "ownir_version": 0, + "module": "WpfMessenger", + "components": [ + { + "name": "InboxViewModel", + "file": "MessengerViewModel.cs", + "subscriptions": [ + {"event": "_messenger.Subscribe", "line": 12, "released": false, "resource": "subscribe"} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 61d41dac..4aa0a53c 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -34,6 +34,8 @@ "timer.facts.json") _DISPOSABLE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "disposable.facts.json") +_SUBSCRIBE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "subscribe.facts.json") def _write_facts(obj: dict) -> str: @@ -163,6 +165,25 @@ def run() -> int: if any(x.component == "CleanReportViewModel" for x in dfindings): fails.append("disposed field was wrongly reported") + # --- WPF004 ignored Subscribe(): the dropped IDisposable token always leaks, + # carrying the [resource: subscription token] tag. + with open(_SUBSCRIBE_FIXTURE, encoding="utf-8") as f: + sfacts = json.load(f) + sfindings = check_facts(sfacts) + checks += 1 + if len(sfindings) != 1: + fails.append(f"expected 1 subscribe finding, got " + f"{[(x.component, x.code) for x in sfindings]}") + else: + s0 = sfindings[0] + checks += 1 + if (s0.file, s0.line, s0.code) != ("MessengerViewModel.cs", 12, "OWN001"): + fails.append(f"wrong subscribe location/code: {s0.file}:{s0.line} {s0.code}") + if "ignored" not in s0.message or "Subscribe" not in s0.message: + fails.append(f"subscribe message missing ignored/Subscribe: {s0.message!r}") + if "[resource: subscription token]" not in s0.render(): + fails.append(f"subscribe finding missing kind tag: {s0.render()!r}") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From 4e276f04967417a82f328a26a0204feedc60d21f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 15:00:59 +0000 Subject: [PATCH 6/9] =?UTF-8?q?ownir:=20POOL001=20=E2=80=94=20ArrayPool=20?= =?UTF-8?q?buffer=20rented=20but=20never=20returned=20(P-007)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An ArrayPool/MemoryPool buffer Rent'ed but never Return'ed leaks (pool exhaustion / GC pressure) — OWN001, tagged [resource: pooled buffer]. The first finding of the flagship borrow-view profile, in the same flat acquire/release model as the WPF resources. - ownir.py: new "pool" resource kind (PooledBuffer resource, kind "pooled buffer", Rent/Return verbs). Additive — no ownir_version bump. - Roslyn extractor: detect `.Rent(...)` assigned to a variable/field (receiver text contains "pool"); released iff a `Return(buf)` with that identifier exists. Matched PER MEMBER so a `buf` returned in one method does not mask a same-named leak in another. - Sample PooledBufferSample.cs (leaky Rent + rent/return-in-finally clean one) and a pool.facts.json fixture; test_ownir pins the leak, the rented/returned message, and the [resource: pooled buffer] tag. CI asserts the leaky buffer is reported and the returned one is silent. - Docs: P-007/ROADMAP mark POOL001 built. Python bridge verified locally (18/18); extractor CI-validated. --- .github/workflows/ci.yml | 10 ++++- docs/ROADMAP.md | 3 +- docs/proposals/P-007-arraypool-span.md | 5 ++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 41 +++++++++++++++++++ frontend/roslyn/samples/PooledBufferSample.cs | 23 +++++++++++ ownlang/ownir.py | 14 ++++++- tests/fixtures/ownir/pool.facts.json | 14 +++++++ tests/test_ownir.py | 21 ++++++++++ 8 files changed, 126 insertions(+), 5 deletions(-) create mode 100644 frontend/roslyn/samples/PooledBufferSample.cs create mode 100644 tests/fixtures/ownir/pool.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e1f2df7c..2a0c96b6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -112,6 +112,7 @@ jobs: frontend/roslyn/samples/TimerViewModel.cs \ frontend/roslyn/samples/DisposableFieldViewModel.cs \ frontend/roslyn/samples/MessengerViewModel.cs \ + frontend/roslyn/samples/PooledBufferSample.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" - name: Check facts through the core @@ -153,5 +154,12 @@ jobs: if echo "$out" | grep -q "CleanInboxViewModel"; then echo "FAIL: captured+disposed subscription wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe) at the C# location" + # POOL001: a Rent'd-but-never-Return'd buffer leaks; the rent+return + # (finally) one stays silent. + echo "$out" | grep -q "pooled buffer 'leaky'" \ + || { echo "FAIL: expected the rented-not-returned buffer leak"; exit 1; } + if echo "$out" | grep -q "pooled buffer 'ok'"; then + echo "FAIL: returned buffer wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool) at the C# location" diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index c7388e66..db1e1096 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -70,7 +70,8 @@ architectural strictness, and the borrow-checker showcase): 2. `WPF002` — `DispatcherTimer`/`Timer` `Tick`/`Elapsed` without stop/detach ✅ 3. `OWN001` — `IDisposable` field the class `new`s but never disposes ✅ 4. `DI001` — singleton captures a scoped dependency -5. `POOL` — `Span`/view used after `ArrayPool.Return` +5. `POOL001` — `ArrayPool` buffer `Rent`ed but never `Return`ed ✅ + (`POOL002` `Span`/view used after `Return` next) ### Milestones diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 9f5dd568..8987e682 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -1,6 +1,7 @@ # P-007 — ArrayPool / Span borrow-view profile -- **Status:** draft (P1 — the borrow checker's flagship showcase) +- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; + POOL002–005 (views, escape, double-return) next - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release, OWN003 double-release, OWN008 release-while-borrowed), the buffer/borrow model in `spec/`, [P-001](P-001-csharp-extractor.md). See @@ -28,7 +29,7 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu | Finding | Pattern | Core verdict | |---------|---------|--------------| -| **POOL001** rented not returned | `Rent(...)` with no `Return` on some path (incl. early `return`/`throw`) | `OWN001` | +| **POOL001** rented not returned | `Rent(...)` with no matching `Return(buf)` in the same member | `OWN001` `[resource: pooled buffer]` ✅ | | **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` | | **POOL003** double return | `Return` reachable twice for the same buffer | `OWN003` | | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` | diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index b3220cf3..fbc8ff03 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -172,6 +172,47 @@ or ImplicitObjectCreationExpressionSyntax resource = "subscribe", }); + // POOL001: an ArrayPool/MemoryPool buffer `Rent`ed but never `Return`ed, + // matched per member so a `buf` returned in one method does not mask a + // leak of a same-named `buf` in another. + foreach (var member in cls.Members) + { + var rented = new List<(string Name, int Line)>(); + foreach (var inv in member.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Rent" + && (m.Expression.ToString().Contains("Pool") + || m.Expression.ToString().Contains("pool"))) + { + string? name = inv.Parent switch + { + EqualsValueClauseSyntax { Parent: VariableDeclaratorSyntax vd } + => vd.Identifier.Text, + AssignmentExpressionSyntax asg => FieldName(asg.Left), + _ => null, + }; + if (name != null) + rented.Add((name, LineOf(inv))); + } + if (rented.Count == 0) + continue; + var returned = new HashSet(); + foreach (var inv in member.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Return" + && inv.ArgumentList.Arguments.Count > 0 + && inv.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax id) + returned.Add(id.Identifier.Text); + foreach (var (name, line) in rented) + subs.Add(new + { + @event = name, + line, + released = returned.Contains(name), + resource = "pool", + }); + } + if (subs.Count > 0) components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs }); } diff --git a/frontend/roslyn/samples/PooledBufferSample.cs b/frontend/roslyn/samples/PooledBufferSample.cs new file mode 100644 index 00000000..76592f6a --- /dev/null +++ b/frontend/roslyn/samples/PooledBufferSample.cs @@ -0,0 +1,23 @@ +using System; +using System.Buffers; + +namespace PoolApp; + +public static class Hasher +{ + // Rents a pooled buffer and never returns it: pool leak / GC pressure. The + // core reports OWN001 [resource: pooled buffer] at the Rent. + public static int LeakyHash(int n) + { + var leaky = ArrayPool.Shared.Rent(n); + return leaky.Length; // never Return(leaky) => leak + } + + // Rents and returns in a finally — not flagged. + public static int CleanHash(int n) + { + var ok = ArrayPool.Shared.Rent(n); + try { return ok.Length; } + finally { ArrayPool.Shared.Return(ok); } + } +} diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 0645d7f3..9f9851c4 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -39,6 +39,8 @@ - "subscribe": a `X.Subscribe(...)` whose `IDisposable` result is ignored (a bare statement, not captured/disposed) — always a leak; tag `[resource: subscription token]`. + - "pool": an `ArrayPool`/`MemoryPool` buffer `Rent`ed but never `Return`ed; + tag `[resource: pooled buffer]`. An unreleased entry is the core's OWN001 (owned-but-not-released) at the C# `line`. The `resource`/`type` fields are additive and optional, so they do NOT @@ -82,18 +84,25 @@ class OwnIRError(ValueError): ' release Dispose\n' ' kind "disposable field"\n' '}\n' + 'resource PooledBuffer {\n' + ' acquire Rent\n' + ' release Return\n' + ' kind "pooled buffer"\n' + '}\n' ) # OwnIR resource kinds the bridge knows how to lower: (own resource type to # acquire, human kind tag the finding carries). `event +=` is a Subscription; a # `Tick`/`Elapsed` handler on a started timer is a Timer (the running timer # strong-refs the handler's owner); an `IDisposable` field the class `new`s is a -# Disposable it owns. Unknown values fall back to Subscription. +# Disposable it owns; an `ArrayPool`/`MemoryPool` `Rent` is a PooledBuffer that +# must be `Return`ed. Unknown values fall back to Subscription. _RESOURCES = { "subscription": ("Subscription", "subscription token"), "subscribe": ("Subscription", "subscription token"), "timer": ("Timer", "timer"), "disposable": ("Disposable", "disposable field"), + "pool": ("PooledBuffer", "pooled buffer"), } @@ -262,6 +271,9 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: message = (f"the result of '{event}' is ignored — the IDisposable " f"subscription is never disposed, leaking " f"'{component}' (leak)") + elif rkind == "pool": + message = (f"pooled buffer '{event}' is rented but never returned " + f"to the pool (leak)") else: message = (f"event '{event}' is subscribed (handler '{handler}') " f"but never unsubscribed — the source keeps " diff --git a/tests/fixtures/ownir/pool.facts.json b/tests/fixtures/ownir/pool.facts.json new file mode 100644 index 00000000..d46b58b4 --- /dev/null +++ b/tests/fixtures/ownir/pool.facts.json @@ -0,0 +1,14 @@ +{ + "ownir_version": 0, + "module": "PoolApp", + "components": [ + { + "name": "Hasher", + "file": "PooledBufferSample.cs", + "subscriptions": [ + {"event": "leaky", "line": 9, "released": false, "resource": "pool"}, + {"event": "ok", "line": 16, "released": true, "resource": "pool"} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 4aa0a53c..6f46aa7b 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -36,6 +36,8 @@ "ownir", "disposable.facts.json") _SUBSCRIBE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "subscribe.facts.json") +_POOL_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "pool.facts.json") def _write_facts(obj: dict) -> str: @@ -184,6 +186,25 @@ def run() -> int: if "[resource: subscription token]" not in s0.render(): fails.append(f"subscribe finding missing kind tag: {s0.render()!r}") + # --- POOL001 ArrayPool: a buffer rented but never returned leaks; a returned + # one stays silent; tag [resource: pooled buffer]. + with open(_POOL_FIXTURE, encoding="utf-8") as f: + pfacts = json.load(f) + pfindings = check_facts(pfacts) + checks += 1 + if len(pfindings) != 1 or pfindings[0].event != "leaky": + fails.append(f"expected 1 pool finding (leaky), got " + f"{[(x.event, x.code) for x in pfindings]}") + else: + p0 = pfindings[0] + checks += 1 + if (p0.file, p0.line, p0.code) != ("PooledBufferSample.cs", 9, "OWN001"): + fails.append(f"wrong pool location/code: {p0.file}:{p0.line} {p0.code}") + if "rented" not in p0.message or "returned" not in p0.message: + fails.append(f"pool message missing rented/returned: {p0.message!r}") + if "[resource: pooled buffer]" not in p0.render(): + fails.append(f"pool finding missing kind tag: {p0.render()!r}") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From e7637a3c0e721671ebb1c4bd3fb000ef24a31637 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 15:11:52 +0000 Subject: [PATCH 7/9] =?UTF-8?q?ownir:=20D1=20=E2=80=94=20local=20IDisposab?= =?UTF-8?q?le=20never=20disposed=20(P-005)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A local the method `new`s of an IDisposable type, never disposed and not guarded by `using` (and not returned/passed/assigned out), leaks — OWN001, tagged [resource: disposable]. The local analog of WPF003's owned fields; the canonical CA2000 leak. - ownir.py: new "local-disposable" resource kind (Disposable resource, tag "disposable", with its own message). Additive — no ownir_version bump. - Roslyn extractor: per-member detection of `new`'d IDisposable locals; released iff disposed; conservatively excludes `using`-guarded locals and ones whose ownership may leave the scope (returned / passed as an argument / assigned out — transfer is ambiguous syntactically, P-005 D5). - Sample LocalDisposableSample.cs (leaky local + a `using` one + a returned/ transferred one) and a local_disposable.facts.json fixture; test_ownir pins the leak, the type in the message, and the [resource: disposable] tag. CI asserts the leaky local is reported and the using/returned ones are silent. - Docs: P-005 marks D1 built (and D2 via WPF003). Python bridge verified locally (20/20); extractor CI-validated. --- .github/workflows/ci.yml | 10 +++- docs/proposals/P-005-idisposable-ownership.md | 10 ++-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 54 +++++++++++++++++++ .../roslyn/samples/LocalDisposableSample.cs | 31 +++++++++++ ownlang/ownir.py | 9 ++++ .../ownir/local_disposable.facts.json | 14 +++++ tests/test_ownir.py | 21 ++++++++ 7 files changed, 143 insertions(+), 6 deletions(-) create mode 100644 frontend/roslyn/samples/LocalDisposableSample.cs create mode 100644 tests/fixtures/ownir/local_disposable.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2a0c96b6..60cf817d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -113,6 +113,7 @@ jobs: frontend/roslyn/samples/DisposableFieldViewModel.cs \ frontend/roslyn/samples/MessengerViewModel.cs \ frontend/roslyn/samples/PooledBufferSample.cs \ + frontend/roslyn/samples/LocalDisposableSample.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" - name: Check facts through the core @@ -161,5 +162,12 @@ jobs: if echo "$out" | grep -q "pooled buffer 'ok'"; then echo "FAIL: returned buffer wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool) at the C# location" + # P-005 D1: a `new`'d local IDisposable never disposed leaks; a `using` + # one and a returned (transferred) one stay silent. + echo "$out" | grep -q "local IDisposable 'leaky'" \ + || { echo "FAIL: expected the undisposed-local leak"; exit 1; } + if echo "$out" | grep -qE "'guarded'|'moved'"; then + echo "FAIL: using/returned local wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) at the C# location" diff --git a/docs/proposals/P-005-idisposable-ownership.md b/docs/proposals/P-005-idisposable-ownership.md index de3000c5..8cda6c98 100644 --- a/docs/proposals/P-005-idisposable-ownership.md +++ b/docs/proposals/P-005-idisposable-ownership.md @@ -1,8 +1,8 @@ # P-005 — `IDisposable` ownership profile -- **Status:** draft (P0 — the most down-to-earth resource module). D2 (owned - field never disposed) has a first cut shipped via WPF003 - ([P-004](P-004-wpf-lifetime-profile.md)); D1/D3/D4/D5 here generalise it. +- **Status:** in progress (P0 — the most down-to-earth resource module). **D1 + (local never disposed)** built, plus **D2 (owned field never disposed)** via + WPF003 ([P-004](P-004-wpf-lifetime-profile.md)); D3/D4/D5 next. - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release, OWN003 double-release), [P-001](P-001-csharp-extractor.md) (the C# seam). Shares the resource core with [P-004](P-004-wpf-lifetime-profile.md). @@ -24,8 +24,8 @@ The five concrete findings, all intraprocedural (or single-class) to start: | Finding | Pattern | Core verdict | |---------|---------|--------------| -| **D1** local not disposed | `new FileStream(...)` (or any `IDisposable`) not disposed on every path | `OWN001` | -| **D2** owned field not disposed | an `IDisposable` field whose owner's `Dispose()` does not cascade to it | `OWN001` | +| **D1** local not disposed | a `new`'d `IDisposable` local, no `using`, not disposed/returned/passed out | `OWN001` `[resource: disposable]` ✅ | +| **D2** owned field not disposed | an `IDisposable` field whose owner's `Dispose()` does not cascade to it | `OWN001` ✅ (WPF003) | | **D3** double dispose | `Dispose()` reachable twice | `OWN003` | | **D4** use after dispose | `x.Dispose(); x.Write(...)` (same method/CFG) | `OWN002` | | **D5** transfer unknown | a disposable handed to a callee whose ownership effect is unknown | (heuristic) | diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index fbc8ff03..4afe91e4 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -213,6 +213,60 @@ or ImplicitObjectCreationExpressionSyntax }); } + // D1 (P-005): a local IDisposable the method `new`s but never disposes, + // not guarded by `using`, and not handed out (returned / passed as an + // argument / assigned out) — ownership transfer is ambiguous syntactically + // (P-005 D5), so those are conservatively excluded. Per member. + foreach (var member in cls.Members) + { + var usingGuarded = new HashSet(); + foreach (var u in member.DescendantNodes().OfType()) + if (u.Declaration is { } ud) + foreach (var v in ud.Variables) + usingGuarded.Add(v.Identifier.Text); + + var escaped = new HashSet(); + foreach (var id in member.DescendantNodes().OfType()) + if (id.Parent is ReturnStatementSyntax or ArgumentSyntax + || (id.Parent is AssignmentExpressionSyntax asg && asg.Right == id)) + escaped.Add(id.Identifier.Text); + + var disposedLocal = new HashSet(); + foreach (var inv in member.DescendantNodes().OfType()) + if (inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "Dispose" + && FieldName(m.Expression) is { } dn) + disposedLocal.Add(dn); + + foreach (var ld in member.DescendantNodes().OfType()) + { + if (ld.UsingKeyword != default) + continue; // `using var x = ...` is safe + foreach (var v in ld.Declaration.Variables) + { + var name = v.Identifier.Text; + if (usingGuarded.Contains(name) || escaped.Contains(name)) + continue; + string? ctype = v.Initializer?.Value switch + { + ObjectCreationExpressionSyntax oc => oc.Type.ToString(), + ImplicitObjectCreationExpressionSyntax => ld.Declaration.Type.ToString(), + _ => null, + }; + if (ctype is null || !IsDisposableType(ctype)) + continue; + subs.Add(new + { + @event = name, + line = LineOf(v), + released = disposedLocal.Contains(name), + resource = "local-disposable", + type = ctype, + }); + } + } + } + if (subs.Count > 0) components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs }); } diff --git a/frontend/roslyn/samples/LocalDisposableSample.cs b/frontend/roslyn/samples/LocalDisposableSample.cs new file mode 100644 index 00000000..a1c7d3cd --- /dev/null +++ b/frontend/roslyn/samples/LocalDisposableSample.cs @@ -0,0 +1,31 @@ +using System; +using System.IO; + +namespace Streams; + +public static class Loader +{ + // A MemoryStream created but never disposed and not in a `using`: leak. The + // core reports OWN001 [resource: disposable] at the declaration. + public static long Leaky() + { + var leaky = new MemoryStream(); + leaky.WriteByte(1); + return leaky.Length; // never disposed => leak + } + + // `using` guarantees disposal — not flagged. + public static long Guarded() + { + using var guarded = new MemoryStream(); + guarded.WriteByte(1); + return guarded.Length; + } + + // Ownership transferred to the caller (returned) — not flagged. + public static Stream Transfer() + { + var moved = new MemoryStream(); + return moved; + } +} diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 9f9851c4..7c441018 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -39,6 +39,9 @@ - "subscribe": a `X.Subscribe(...)` whose `IDisposable` result is ignored (a bare statement, not captured/disposed) — always a leak; tag `[resource: subscription token]`. + - "local-disposable": a local the method `new`s of an `IDisposable` type, + never disposed and not guarded by `using` (and not returned/passed out); + tag `[resource: disposable]`. - "pool": an `ArrayPool`/`MemoryPool` buffer `Rent`ed but never `Return`ed; tag `[resource: pooled buffer]`. @@ -102,6 +105,7 @@ class OwnIRError(ValueError): "subscribe": ("Subscription", "subscription token"), "timer": ("Timer", "timer"), "disposable": ("Disposable", "disposable field"), + "local-disposable": ("Disposable", "disposable"), "pool": ("PooledBuffer", "pooled buffer"), } @@ -267,6 +271,11 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: of_type = f" (type '{typ}')" if typ else "" message = (f"IDisposable field '{event}'{of_type} is never " f"disposed — its owner '{component}' leaks it (leak)") + elif rkind == "local-disposable": + typ = sub.get("type") + of_type = f" (type '{typ}')" if typ else "" + message = (f"local IDisposable '{event}'{of_type} is created but " + f"never disposed (leak)") elif rkind == "subscribe": message = (f"the result of '{event}' is ignored — the IDisposable " f"subscription is never disposed, leaking " diff --git a/tests/fixtures/ownir/local_disposable.facts.json b/tests/fixtures/ownir/local_disposable.facts.json new file mode 100644 index 00000000..50b34a46 --- /dev/null +++ b/tests/fixtures/ownir/local_disposable.facts.json @@ -0,0 +1,14 @@ +{ + "ownir_version": 0, + "module": "Streams", + "components": [ + { + "name": "Loader", + "file": "LocalDisposableSample.cs", + "subscriptions": [ + {"event": "leaky", "line": 10, "released": false, "resource": "local-disposable", "type": "MemoryStream"}, + {"event": "disposed", "line": 18, "released": true, "resource": "local-disposable", "type": "MemoryStream"} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 6f46aa7b..75fbc27e 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -38,6 +38,8 @@ "ownir", "subscribe.facts.json") _POOL_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "pool.facts.json") +_LOCAL_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "local_disposable.facts.json") def _write_facts(obj: dict) -> str: @@ -205,6 +207,25 @@ def run() -> int: if "[resource: pooled buffer]" not in p0.render(): fails.append(f"pool finding missing kind tag: {p0.render()!r}") + # --- P-005 D1 local IDisposable: a `new`'d local never disposed leaks; an + # explicitly disposed one stays silent; tag [resource: disposable]. + with open(_LOCAL_FIXTURE, encoding="utf-8") as f: + lfacts = json.load(f) + lfindings = check_facts(lfacts) + checks += 1 + if len(lfindings) != 1 or lfindings[0].event != "leaky": + fails.append(f"expected 1 local-disposable finding (leaky), got " + f"{[(x.event, x.code) for x in lfindings]}") + else: + l0 = lfindings[0] + checks += 1 + if (l0.file, l0.line, l0.code) != ("LocalDisposableSample.cs", 10, "OWN001"): + fails.append(f"wrong local location/code: {l0.file}:{l0.line} {l0.code}") + if "local IDisposable" not in l0.message or "MemoryStream" not in l0.message: + fails.append(f"local message missing text/type: {l0.message!r}") + if "[resource: disposable]" not in l0.render(): + fails.append(f"local finding missing kind tag: {l0.render()!r}") + for f in fails: print(f"OWNIR FAIL: {f}") print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") From c71125683d12bcd5c31a13042c469496a7333f1d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 15:27:44 +0000 Subject: [PATCH 8/9] =?UTF-8?q?ownir:=20address=20PR=20#9=20review=20(Code?= =?UTF-8?q?Rabbit)=20=E2=80=94=20fix=20CI=20lint=20+=20extractor=20edge=20?= =?UTF-8?q?cases?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verified each of the 7 review threads against the code; all valid, all minimal: - mypy --strict (the actual red CI): _handle_of returned Any from getattr; narrow with isinstance(subject, str) before .split(). Confirmed clean with `mypy` + `ruff check .`. - extractor: ArrayPool Return detection now uses FieldName() so `pool.Return(this._buf)` matches the rented `this._buf` (was a false-positive leak for qualified fields). - extractor: disposal detection (both owned-field and local) now matches `DisposeAsync()` as well as `Dispose()` — IsDisposableType already accepts IAsyncDisposable, so an awaited DisposeAsync was a false positive. - CI: local-disposable check now also asserts the source file and the exact `[resource: disposable]` tag (parity with the other resource checks; the trailing `]` avoids matching `disposable field`). - P-008: add EFF005 for the unpaired-protocol case the prose already lists. - fixtures/tests: realign the hand-written disposable/local fixture line anchors to the actual sample declarations (10/21 and 12) so the fixtures faithfully mirror the samples. Tests 20/20; mypy + ruff clean locally. --- .github/workflows/ci.yml | 4 ++++ docs/proposals/P-008-effects-and-resources.md | 1 + frontend/roslyn/OwnSharp.Extractor/Program.cs | 8 ++++---- ownlang/ownir.py | 2 +- tests/fixtures/ownir/disposable.facts.json | 4 ++-- tests/fixtures/ownir/local_disposable.facts.json | 2 +- tests/test_ownir.py | 4 ++-- 7 files changed, 15 insertions(+), 10 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 60cf817d..53db3d8d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -166,6 +166,10 @@ jobs: # one and a returned (transferred) one stay silent. echo "$out" | grep -q "local IDisposable 'leaky'" \ || { echo "FAIL: expected the undisposed-local leak"; exit 1; } + echo "$out" | grep -q "LocalDisposableSample.cs" \ + || { echo "FAIL: expected LocalDisposableSample.cs in the local-disposable finding"; exit 1; } + echo "$out" | grep -q "resource: disposable]" \ + || { echo "FAIL: expected a [resource: disposable] tag"; exit 1; } if echo "$out" | grep -qE "'guarded'|'moved'"; then echo "FAIL: using/returned local wrongly reported"; exit 1 fi diff --git a/docs/proposals/P-008-effects-and-resources.md b/docs/proposals/P-008-effects-and-resources.md index e519ed88..07b5bfd4 100644 --- a/docs/proposals/P-008-effects-and-resources.md +++ b/docs/proposals/P-008-effects-and-resources.md @@ -67,6 +67,7 @@ EFF001 undeclared effect (e.g. DbRead) EFF002 pure method uses Clock/Network/Db/Log/Pool EFF003 forbidden effect in layer Domain EFF004 mutable resource used without ! permission +EFF005 unpaired resource protocol (Rent without Return, BeginTransaction without Commit/Rollback) ``` ## Non-goals diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 4afe91e4..36c7eda8 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -132,7 +132,7 @@ or ImplicitObjectCreationExpressionSyntax var disposed = new HashSet(); foreach (var inv in cls.DescendantNodes().OfType()) if (inv.Expression is MemberAccessExpressionSyntax m - && m.Name.Identifier.Text == "Dispose" + && m.Name.Identifier.Text is "Dispose" or "DisposeAsync" && FieldName(m.Expression) is { } df) disposed.Add(df); @@ -201,8 +201,8 @@ or ImplicitObjectCreationExpressionSyntax if (inv.Expression is MemberAccessExpressionSyntax m && m.Name.Identifier.Text == "Return" && inv.ArgumentList.Arguments.Count > 0 - && inv.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax id) - returned.Add(id.Identifier.Text); + && FieldName(inv.ArgumentList.Arguments[0].Expression) is { } rn) + returned.Add(rn); foreach (var (name, line) in rented) subs.Add(new { @@ -234,7 +234,7 @@ or ImplicitObjectCreationExpressionSyntax var disposedLocal = new HashSet(); foreach (var inv in member.DescendantNodes().OfType()) if (inv.Expression is MemberAccessExpressionSyntax m - && m.Name.Identifier.Text == "Dispose" + && m.Name.Identifier.Text is "Dispose" or "DisposeAsync" && FieldName(m.Expression) is { } dn) disposedLocal.Add(dn); diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 7c441018..b2468ceb 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -212,7 +212,7 @@ def _handle_of(diag: object) -> str | None: acquire stamps `subject` in cfg.lower_let; None means the diagnostic carries no subject identity at all.""" subject = getattr(diag, "subject", None) - if not subject: + if not isinstance(subject, str) or not subject: return None return subject.split("#", 1)[0] diff --git a/tests/fixtures/ownir/disposable.facts.json b/tests/fixtures/ownir/disposable.facts.json index 646e7a2b..e8cbbd1f 100644 --- a/tests/fixtures/ownir/disposable.facts.json +++ b/tests/fixtures/ownir/disposable.facts.json @@ -6,14 +6,14 @@ "name": "ReportViewModel", "file": "DisposableFieldViewModel.cs", "subscriptions": [ - {"event": "_cts", "line": 11, "released": false, "resource": "disposable", "type": "CancellationTokenSource"} + {"event": "_cts", "line": 10, "released": false, "resource": "disposable", "type": "CancellationTokenSource"} ] }, { "name": "CleanReportViewModel", "file": "DisposableFieldViewModel.cs", "subscriptions": [ - {"event": "_cts", "line": 25, "released": true, "resource": "disposable", "type": "CancellationTokenSource"} + {"event": "_cts", "line": 21, "released": true, "resource": "disposable", "type": "CancellationTokenSource"} ] } ] diff --git a/tests/fixtures/ownir/local_disposable.facts.json b/tests/fixtures/ownir/local_disposable.facts.json index 50b34a46..de628c69 100644 --- a/tests/fixtures/ownir/local_disposable.facts.json +++ b/tests/fixtures/ownir/local_disposable.facts.json @@ -6,7 +6,7 @@ "name": "Loader", "file": "LocalDisposableSample.cs", "subscriptions": [ - {"event": "leaky", "line": 10, "released": false, "resource": "local-disposable", "type": "MemoryStream"}, + {"event": "leaky", "line": 12, "released": false, "resource": "local-disposable", "type": "MemoryStream"}, {"event": "disposed", "line": 18, "released": true, "resource": "local-disposable", "type": "MemoryStream"} ] } diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 75fbc27e..6ef25089 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -156,7 +156,7 @@ def run() -> int: else: d0 = dleaks[0] checks += 1 - if (d0.file, d0.line, d0.code) != ("DisposableFieldViewModel.cs", 11, "OWN001"): + if (d0.file, d0.line, d0.code) != ("DisposableFieldViewModel.cs", 10, "OWN001"): fails.append(f"wrong field location/code: {d0.file}:{d0.line} {d0.code}") if "IDisposable field" not in d0.message or "_cts" not in d0.message: fails.append(f"disposable message missing field: {d0.message!r}") @@ -219,7 +219,7 @@ def run() -> int: else: l0 = lfindings[0] checks += 1 - if (l0.file, l0.line, l0.code) != ("LocalDisposableSample.cs", 10, "OWN001"): + if (l0.file, l0.line, l0.code) != ("LocalDisposableSample.cs", 12, "OWN001"): fails.append(f"wrong local location/code: {l0.file}:{l0.line} {l0.code}") if "local IDisposable" not in l0.message or "MemoryStream" not in l0.message: fails.append(f"local message missing text/type: {l0.message!r}") From a4a9029fe61172d22d7f5db55b874210124500c6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 15:35:05 +0000 Subject: [PATCH 9/9] extractor: don't flag timer fields as disposable (fixes wpf-extractor CI) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The C# leak-extractor CI job has been red since WPF003 landed: IsDisposableType matched `*Timer` (and `DispatcherTimer`/`Timer`), so a DispatcherTimer field was reported as a "disposable field" needing Dispose(). DispatcherTimer is not even IDisposable, and a timer's release is Stop()/detach (the WPF002 pattern) — so this double-reported every timer and false-positived CleanTimerViewModel (a correctly Stop()'d timer), breaking the "stopped timer not reported" assertion. Fix: exclude timer types from the disposable-field/local heuristic; timers are owned by the WPF002 timer pattern. Caught only in CI (dotnet is CI-only) — the local Python bridge suite cannot exercise the extractor heuristic. --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 36c7eda8..eca27c30 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -59,15 +59,17 @@ left is MemberAccessExpressionSyntax m _ => null, }; -// A field type treated as owned-disposable (syntax-only heuristic — no semantic -// model): a curated set plus a few suffixes. Gated on the class `new`ing the -// field (see below), so injected/borrowed disposables are not flagged. +// A field/local type treated as owned-disposable (syntax-only heuristic — no +// semantic model): a curated set plus a few suffixes. Gated on the class `new`ing +// the value, so injected/borrowed disposables are not flagged. Timer types are +// deliberately excluded: a `Tick`/`Elapsed` timer is the WPF002 pattern's job +// (released by Stop()/detach), and DispatcherTimer is not even IDisposable, so +// matching `*Timer` here would double-report and false-positive a stopped timer. static bool IsDisposableType(string t) => - t is "IDisposable" or "IAsyncDisposable" or "DispatcherTimer" or "Timer" - or "CancellationTokenSource" or "HttpClient" or "SerialPort" - or "SqlConnection" + t is "IDisposable" or "IAsyncDisposable" or "CancellationTokenSource" + or "HttpClient" or "SerialPort" or "SqlConnection" || t.EndsWith("Stream") || t.EndsWith("Reader") || t.EndsWith("Writer") - || t.EndsWith("Timer") || t.EndsWith("Subscription"); + || t.EndsWith("Subscription"); var components = new List();