diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a10ea86a..2968aa5d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -127,6 +127,7 @@ jobs: frontend/roslyn/samples/SelfOwnedControlParts.cs \ frontend/roslyn/samples/ExternalRefSubscription.cs \ frontend/roslyn/samples/StaticHandlerViewModel.cs \ + frontend/roslyn/samples/StaticEventEscapeViewModel.cs \ frontend/roslyn/samples/SampleTypes.cs \ -o "$RUNNER_TEMP/facts.json" cat "$RUNNER_TEMP/facts.json" @@ -234,7 +235,22 @@ jobs: if echo "$out" | grep -q "StaticHandlerViewModel.cs"; then echo "FAIL: a static-handler subscription was wrongly reported"; exit 1 fi - echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) at the C# location" + # P-004 WPF005 region escape: an INSTANCE handler subscribed to a + # process-lived STATIC event (Calc.GlobalPing) with no `-=` is a region + # escape, NOT a token leak. The extractor lowers the static-source `+=` to + # a `capture` fact and the core's region engine reports OWN014 (the + # view-model is promoted to process lifetime), an error — proving real C# + # static-event subscriptions reach the region core, not only OWN001. + echo "$out" | grep -qE "StaticEventEscapeViewModel\.cs:[0-9]+: error: \[OWN014\]" \ + || { echo "FAIL: expected OWN014 region escape on the static-event instance subscription"; exit 1; } + echo "$out" | grep -q "region escape" \ + || { echo "FAIL: expected the region-escape wording on the static-event capture"; exit 1; } + # the unsubscribed variant (a matching `-=`, released capture) is mitigated + # -> silent. Must NOT be reported. + if echo "$out" | grep -q "CleanStaticEventViewModel"; then + echo "FAIL: an unsubscribed (released) static-event subscription was wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) + OWN014 (static-event region escape) at the C# location" - name: Flow-sensitive local IDisposables (--flow-locals, P-016 B0b/B2) run: | # Path-sensitive flow analysis of local IDisposables — bugs the flat D1 diff --git a/README.md b/README.md index e85faa44..d7295a30 100644 --- a/README.md +++ b/README.md @@ -149,6 +149,14 @@ CustomerViewModel.cs:9: error: [OWN001] event 'bus.CustomerChanged' is subscribe (handler 'OnCustomerChanged') but never unsubscribed — ... (leak) [resource: subscription token] ``` +А `+=` со **статическим** событием (например `SystemEvents.*`) — это уже не +токен-утечка, а *region escape*: экстрактор понижает его в бестокенный +`capture`-факт, и **то же ядро** выдаёт **OWN014** (объект промотится в +process-lifetime; парный `-=` снимает находку) — WPF-escape как профиль общей +region-модели, а не отдельный детектор (P-004 WPF005; сэмпл +`StaticEventEscapeViewModel`). Источник-инъекция (неизвестное время жизни) +остаётся OWN001-warning'ом, пока ownership-моделирование не докажет его время жизни. + Ядро одно (не второй чекер на C#): экстрактор только производит факты. dotnet есть лишь в CI (job `wpf-extractor` гоняет экстрактор на сэмплах сквозняком); Python-мост тестируется локально (`tests/test_ownir.py`) на рукописных фактах. @@ -158,9 +166,12 @@ Python-мост тестируется локально (`tests/test_ownir.py`) `after.cs`/`case.own`/expected), прибитый `tests/test_wpf.py`; региональная теорема — `tests/test_lifetimes.py` (10 кейсов). Полный план модуля (каталог OWN-WPF, границы слайсов, что отложено) — в [`docs/lifetimes.md`](docs/lifetimes.md). -Честно: `case.own` — hand reduction паттерна, не C#, который чекер съел (C#-фронта -нет, это поздний слайс); `self`/`source` — это scope самой функции и её параметры, -без cross-procedural points-to. +Честно: `case.own` — hand reduction паттерна (region-escape со **статическим** +источником экстрактор уже эмитит сам — `+=` → `capture` → OWN014, см. +`StaticEventEscapeViewModel` и `corpus/wpf/systemevents-region-escape`; cross- +procedural points-to и прочие региональные факты — пока hand reduction); +`self`/`source` — это scope самой функции и её параметры, без cross-procedural +points-to. ### Golden-пример: настоящий ArrayPool diff --git a/corpus/wpf/systemevents-region-escape/after.cs b/corpus/wpf/systemevents-region-escape/after.cs new file mode 100644 index 00000000..3062b7e3 --- /dev/null +++ b/corpus/wpf/systemevents-region-escape/after.cs @@ -0,0 +1,27 @@ +// FIXED. The subscription is released when the window is done (on Closed), +// breaking the static source's strong hold so the dialog drops back to its +// intended Window lifetime and is collectable. A disposable-token form works too +// (see corpus/wpf/viewmodel-escapes-to-app/after.cs); either way the region check +// then sees a release path and stays quiet — no promotion, no OWN014. +using System; +using System.Windows; +using Microsoft.Win32; + +public partial class GraphicsConfigurationDialog : Window +{ + public GraphicsConfigurationDialog() + { + InitializeComponent(); + SystemEvents.DisplaySettingsChanged += OnDisplaySettingsChanged; + Closed += OnClosed; + } + + private void OnClosed(object? sender, EventArgs e) + { + // release path -> dialog no longer promoted to Process lifetime + SystemEvents.DisplaySettingsChanged -= OnDisplaySettingsChanged; + Closed -= OnClosed; + } + + private void OnDisplaySettingsChanged(object? sender, EventArgs e) { /* ... */ } +} diff --git a/corpus/wpf/systemevents-region-escape/before.cs b/corpus/wpf/systemevents-region-escape/before.cs new file mode 100644 index 00000000..5a892377 --- /dev/null +++ b/corpus/wpf/systemevents-region-escape/before.cs @@ -0,0 +1,30 @@ +// BUGGY (the canonical SystemEvents leak, hand-reduced into case.own). +// +// A Window-scoped dialog subscribes itself to Microsoft.Win32.SystemEvents — a +// STATIC, process-lifetime event source — with a strong method-group handler and +// keeps no unsubscribe token. The static source is reachable from a +// process-lifetime GC root, and through the strong delegate so is the dialog: the +// dialog is *promoted* to process lifetime. Close the window all you want -- it +// lives until the process exits. The lifetime mismatch (the dialog expected +// Window scope, actually gets Process scope) is the leak. +// +// Seen here through the REGION model (OWN014, region escape); the same bug viewed +// through the token model (OWN001, owned-but-not-released) is in +// corpus/real-world/screentogif-systemevents-leak. Distilled from +// NickeManarin/ScreenToGif (GraphicsConfigurationDialog / Troubleshoot). +using System; +using System.Windows; +using Microsoft.Win32; + +public partial class GraphicsConfigurationDialog : Window +{ + public GraphicsConfigurationDialog() + { + InitializeComponent(); + // strong subscription to a process-lived static event, no token kept + // -> the Window-scoped dialog is promoted to Process lifetime (region escape) + SystemEvents.DisplaySettingsChanged += OnDisplaySettingsChanged; + } + + private void OnDisplaySettingsChanged(object? sender, EventArgs e) { /* ... */ } +} diff --git a/corpus/wpf/systemevents-region-escape/case.own b/corpus/wpf/systemevents-region-escape/case.own new file mode 100644 index 00000000..20a8d452 --- /dev/null +++ b/corpus/wpf/systemevents-region-escape/case.own @@ -0,0 +1,22 @@ +module SystemEventsRegionEscape + +// Lifetime regions. The static `Microsoft.Win32.SystemEvents` class lives for the +// whole process; a WPF window/dialog that subscribes to it is strictly +// shorter-lived. This `<` order is exactly what the C# bridge gives a `capture` +// OwnIR fact whose source is a `static` (process-lived) event — see +// ownlang/ownir.py (`Subscriber < Process`); the corpus uses the WPF-authentic +// name `Window` for the short region. +lifetime Process; // Microsoft.Win32.SystemEvents — a static, process-lived source +lifetime Window < Process; // the dialog/window — strictly shorter-lived + +// The window strongly subscribes itself to the process-lived +// SystemEvents.DisplaySettingsChanged static event and keeps no unsubscribe +// token. Because Process strictly outlives Window, the strong delegate promotes +// the window to process lifetime -> it can never be collected while the app runs +// => OWN014. This is the SAME real bug as +// corpus/real-world/screentogif-systemevents-leak, seen through the REGION model +// (escape) rather than the token model (OWN001) — and the precise shape the +// extractor lowers a static-event `+=` to (the `capture` fact, P-004 WPF005). +fn GraphicsConfigurationDialog(systemEvents: SystemEvents lifetime Process) lifetime Window { + subscribe self to systemEvents; +} diff --git a/corpus/wpf/systemevents-region-escape/expected-diagnostics.txt b/corpus/wpf/systemevents-region-escape/expected-diagnostics.txt new file mode 100644 index 00000000..3fd038d5 --- /dev/null +++ b/corpus/wpf/systemevents-region-escape/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN014 diff --git a/corpus/wpf/systemevents-region-escape/notes.md b/corpus/wpf/systemevents-region-escape/notes.md new file mode 100644 index 00000000..27975a81 --- /dev/null +++ b/corpus/wpf/systemevents-region-escape/notes.md @@ -0,0 +1,53 @@ +# WPF window promoted to process lifetime via a static SystemEvents subscription (region escape) + +**Pattern:** a `Window`-scoped dialog strongly subscribes itself to +`Microsoft.Win32.SystemEvents.DisplaySettingsChanged` — a **static, +process-lifetime** event source — and keeps no unsubscribe token. The static +source holds a strong reference to the handler's owner (the dialog) for the whole +life of the process, so the dialog is *promoted* to process lifetime: it outlives +its window and lives until the process exits. The bug is the **lifetime mismatch** +(the dialog expected `Window`, actually `Process`), not any single missing +`Dispose` call in isolation. This is the SystemEvents leak the .NET docs +explicitly warn about; distilled from `NickeManarin/ScreenToGif` +(`GraphicsConfigurationDialog` / `Troubleshoot`). + +**What the checker says:** the region-escape theorem (slice #2). With the regions +declared (`Window < Process`) and the static source tagged `Process`-lived, the +strong `subscribe self to systemEvents` where the source strictly outlives `self` +trips the generic **OWN014**: + +```text +$ python -m ownlang check corpus/wpf/systemevents-region-escape/case.own +case.own:24:23: error: [OWN014] 'systemEvents' (lifetime 'Process') outlives the + captured object 'GraphicsConfigurationDialog' (lifetime 'Window'); the strong + subscription promotes 'GraphicsConfigurationDialog' to 'Process' and it leaks + (no release path) +``` + +**Two views of one bug — token vs region.** The same SystemEvents leak appears in +the corpus twice, on purpose: + +- `corpus/real-world/screentogif-systemevents-leak` models it through the **token + model** — `event +=` acquires an owned subscription that is never released, so + the core's **OWN001** fires (a static source is a hard error). +- **This case** models it through the **region model** — the source is + process-lived, the subscriber is shorter-lived, and the strong capture promotes + the subscriber to the longer lifetime, so **OWN014** fires. The *ordering* is + what makes it a leak: subscribing to a same- or shorter-lived source produces no + diagnostic (no promotion possible). + +The region view is what the C# bridge produces for a static-event `+=`: a +`capture` OwnIR fact whose `source: "static"` maps to the process-lived region, +lowered to `subscribe self to ` and checked by `ownlang/lifetimes.py` +(pinned end-to-end by `tests/fixtures/ownir/capture.facts.json`). The region view +is also more *precise* than the token view — a subscription to an +equal-or-shorter-lived source is correctly silent, where the flat token model +would warn. + +**Honesty / scope.** `case.own` is a *hand reduction*, not direct C# extractor +output — `self`/`source` are the function's own scope and its annotated +parameters; there is no cross-procedural points-to, and weak-event policy as an +explicit escape hatch is a later slice (see `docs/lifetimes.md`). `before.cs` / +`after.cs` are representative of the leak and its fix, not a verbatim copy of one +PR. The fix breaks the static source's hold (here on `Closed`; a disposable token +works too). diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 1f8a2b65..d9637529 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -103,6 +103,19 @@ architectural strictness, and the borrow-checker showcase): 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. + ◑ *In progress* — the acquire/release half is the live engine (OWN001 across + subscriptions / timers / fields / pools). The **region half is now wired end to + end through the C# extractor**: a static-source `+=` is lowered to a *tokenless* + `capture` OwnIR fact that routes through the lifetime/region engine and surfaces + as **OWN014** (the WPF "escape to App"), so the subscription leak is expressible + through the *general* owner/release-region model — not a bespoke detector. It is + also more *precise* than the token model: a source that does not provably outlive + the subscriber stays silent (no false positive) where the token tier only warns, + and a released `-=` mitigates the capture. Proven by the `capture` fixture, the + `StaticEventEscapeViewModel` sample (CI `wpf-extractor` → OWN014), and the + `corpus/wpf/systemevents-region-escape` reduction (P-004 WPF005 ✅). Remaining: + migrating the *injected*-source subscription tier (today an honest OWN001 + warning) once lifetime modelling can prove or refute those sources. 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. @@ -171,7 +184,7 @@ own scan. Label them as estimates wherever they appear. | [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-004](proposals/P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | P0 | in progress (WPF001–005 built) | | [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 | in progress (DI001 core check built) | | [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | draft | diff --git a/docs/lifetimes.md b/docs/lifetimes.md index d07e2178..4691a2b8 100644 --- a/docs/lifetimes.md +++ b/docs/lifetimes.md @@ -146,9 +146,24 @@ MVP (slice #1) сознательно сводит WPF004/005/002 к уже-ра `subscribe self to X;`), region-escape-анализ → `OWN014`; структурная валидация порядка (`OWN030`/`OWN031`/`OWN036`). Корпус `corpus/wpf/viewmodel-escapes-to-app` + `tests/test_lifetimes.py` (10 кейсов). -- **slice #3 (далеко):** узкий Roslyn-frontend — pattern matcher (`event +=`, - `Subscribe`, `DispatcherTimer`, `IDisposable`-поля) → кормит это же ядро. - Не «ингест всего C#» (это человеко-годы), а распознавание известных паттернов. +- **slice #3 ✅ region-escape конец-в-конец:** узкий Roslyn-frontend — pattern + matcher (`event +=`, `Subscribe`, `DispatcherTimer`, `IDisposable`-поля) → + кормит это же ядро. Не «ингест всего C#» (это человеко-годы), а распознавание + известных паттернов. **Region-escape ветка готова целиком:** экстрактор + понижает `+=` со **статическим** источником (static event / static-receiver) в + бестокенный OwnIR-факт `capture`; мост (`ownir.to_module`) отображает его + `source` в process-lived регион и эмитит `subscribe self to `, а + region-движок (`ownlang/lifetimes.py`) докладывает `OWN014` на C#-строке. + Источник `static` промотит подписчика; источник неизвестного времени жизни + (`injected`) остаётся токен-`subscription` (OWN001, по тиру); `capture` с парным + `-=` (`released`) митигирован → молчит. Пинится `capture`-фикстурой + (`tests/fixtures/ownir/capture.facts.json`) и сэмплом `StaticEventEscapeViewModel` + (CI `wpf-extractor`: OWN014 на instance-handler'е, тишина на отписанном). + Корпус: `corpus/wpf/systemevents-region-escape` (тот же баг, что + `screentogif-systemevents-leak`, но через регион-модель). Так WPF-escape стал + *профилем* общей region-модели (`subscribe self to `), а не one-off — + цель Milestone 2 в ROADMAP. Остальные паттерны (`Subscribe` без токена, + таймеры, поля) экстрактор уже эмитит как OWN001-формы (slice #1). ## 7. Открытые развилки (на согласование) diff --git a/docs/proposals/P-004-wpf-lifetime-profile.md b/docs/proposals/P-004-wpf-lifetime-profile.md index 7a2cb1ee..9a422763 100644 --- a/docs/proposals/P-004-wpf-lifetime-profile.md +++ b/docs/proposals/P-004-wpf-lifetime-profile.md @@ -2,7 +2,9 @@ - **Status:** in progress (P0) — WPF001 (v0) + **WPF002 (timer)** + **WPF003 (IDisposable field)** + **WPF004 (ignored Subscribe)** + **self-owned & static- - handler exemptions (P-014 Tier A) built**; WPF005 (escape) next + handler exemptions (P-014 Tier A) built**; **WPF005 (escape → OWN014) built + end-to-end** — the extractor lowers a static-event `+=` to a `capture` fact that + the region engine reports as OWN014 (a released `-=` mitigates it -> silent) - **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). @@ -32,7 +34,7 @@ ends `ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements | **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** | `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` | +| **WPF005** | strong capture by a longer-lived source (the ViewModel `escapes` to App) | `OWN014` ✅ end-to-end (extractor emits `capture` for a static-event `+=`) | Modelled as resource facts (no new magic — the resource is just named `Subscription`): @@ -63,11 +65,34 @@ Samples: `SelfOwnedViewModel.cs` / `StaticHandlerViewModel.cs` (silent) vs `Context`'s subscription to the *same* event — the deciding factor is the subscriber/handler, not the source. -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. +The corpus pins four of these against real core codes: `corpus/wpf/zombie-viewmodel` +(OWN001), `viewmodel-escapes-to-app` (OWN014), `handler-use-after-dispose` (OWN002), +and **`systemevents-region-escape` (OWN014)** — the SystemEvents leak seen through +the region model, the same bug `corpus/real-world/screentogif-systemevents-leak` +shows through the token model. + +**WPF004 and WPF005 are now built end-to-end.** WPF005's contract splits strictly by +the source's lifetime — the extractor classifies the `+=`, the core decides — and +the three cases do **not** overlap: + +- **static / process-lived source** (a static event, or a static field/property + receiver) → a *tokenless* `capture` fact → the region engine promotes the + subscriber to the longer region → **OWN014** (a hard leak). The engine would stay + silent for an equal-or-shorter-lived source, but the extractor only routes + provably-longer (process-lived) sources into it, so every emitted `capture` + escapes unless released. +- **injected / unknown-lifetime source** → stays a token `subscription` → **OWN001 + at the WARNING tier** — an honest "may outlive this", **not** silent and **not** + OWN014 — until ownership modelling can prove or refute the source's lifetime. +- **a matching `-=` (`released`)**, on either path → mitigated → **silent**. + +So a reader should infer neither that OWN014 applies to every subscription, nor that +an injected subscription is silent: the source kind picks the path. Exercised by the +`capture` fixture (`tests/fixtures/ownir/capture.facts.json`) and the +`StaticEventEscapeViewModel` sample (CI `wpf-extractor`, asserting OWN014 on the +instance handler and silence on the unsubscribed one). This makes the WPF escape a +*profile* of the general region model (`subscribe self to `), not a bespoke +path — the ROADMAP Milestone-2 goal. ## Non-goals @@ -82,19 +107,21 @@ codegen double-returns an `ArrayPool`, only now with `DispatcherObject`. A 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. +disposable subscription field) — built; and (b) emitting the region-escape fact +(a static-source `+=` → a `capture`) so OWN014 fires for WPF005 — built: a +static event/static-receiver subscription is the `capture`, the bridge maps its +`source` to a process-lived region and the engine reports the promotion. ```text *.cs --[extractor: += / Tick+Start / Subscribe / field / escapes]--> facts.json --[core]--> OWN001 (leak) / OWN014 (escape) @ C# line ``` -Land **one pattern per increment** (WPF002/003/004 built — a `Tick`/`Elapsed` +Land **one pattern per increment** (WPF002/003/004/005 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 +`Disposable`; an ignored `X.Subscribe(...)` is a dropped subscription token; a +static-event `+=` is a `capture` → region escape), 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. @@ -102,9 +129,15 @@ it once in the resource core and let WPF consume it as a profile. 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.) +2. Where does the release region end — accept `Dispose`/`OnClosed`/`Unloaded` + only, or any method named `Dispose*`? (Conservative set first.) +3. WPF005 needs a lifetime ordering (`Subscriber < Process`). **Resolved for the + first source class:** the bridge *infers* it from the source kind — a `static`/ + process-lived event is the longest region and strictly outlives any subscriber, + so `subscribe self to ` → OWN014 with no annotation. Other source + classes (an injected source of unknown lifetime → conservatively silent today; a + parent scope) are later increments. A single shared `Subscriber` region suffices + while there is one source region; multiple source regions will want a per-source + ordering (the `< LONGER` form takes one edge per decl). 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/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index faa0fdfb..5bbb4f80 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -835,7 +835,18 @@ or ImplicitObjectCreationExpressionSyntax handler = a.Right.ToString(), line = LineOf(a.Left), released, - resource = isTimer ? "timer" : "subscription", + // A static-source subscription (a process-lived event, or a + // static-field/property receiver) is a region escape, not a + // token leak: route it through the lifetime engine as a + // `capture` -> OWN014 (the WPF "escape to App"). The bridge + // skips a released capture (a `-=` on close), so a correctly + // unsubscribed static subscription stays silent. An injected/ + // unknown source stays a token `subscription` (OWN001, + // severity-tiered); timers are their own kind. (P-004 WPF005; + // see ownlang/ownir.py `capture`.) + resource = isTimer ? "timer" + : source == "static" ? "capture" + : "subscription", source, lambda = !isTimer && IsLambdaHandler(a.Right), }); diff --git a/frontend/roslyn/samples/StaticEventEscapeViewModel.cs b/frontend/roslyn/samples/StaticEventEscapeViewModel.cs new file mode 100644 index 00000000..c3f958de --- /dev/null +++ b/frontend/roslyn/samples/StaticEventEscapeViewModel.cs @@ -0,0 +1,50 @@ +using System; + +// A region escape (P-004 WPF005): an INSTANCE-method handler subscribed to a +// process-lived STATIC event (Calc.GlobalPing) with no matching `-=`. The static +// event pins the handler's owner (this instance) for the whole life of the +// process, so the short-lived view-model is *promoted* to process lifetime and can +// never be collected. The extractor lowers a static-source `+=` to a `capture` +// fact, and the core's region engine reports OWN014 (the lifetime-promotion leak) +// rather than the token-model OWN001. +// +// Contrast StaticHandlerViewModel (same static event, but a STATIC handler -> null +// delegate target -> no instance retained -> silent): the deciding factor is the +// handler, not the source. Calc.GlobalPing is the self-contained analog of +// Microsoft.Win32.SystemEvents.* — a static, process-lifetime event source the +// .NET docs explicitly warn about. +public sealed class StaticEventEscapeViewModel +{ + private int _count; + + public StaticEventEscapeViewModel() + { + // instance handler on a process-lived static event, no `-=` kept + // -> this view-model escapes to process lifetime (OWN014) + Calc.GlobalPing += OnGlobalPing; + } + + private void OnGlobalPing(object? sender, EventArgs e) { _count++; } +} + +// FIXED: the instance subscription is torn down with a matching `-=` (here in +// Dispose, e.g. called on window close), so the static event no longer pins this +// instance -> no escape. The extractor's `capture` fact carries `released: true` +// and the bridge stays silent (a mitigated capture, exactly like a released token +// subscription). Must NOT be reported. +public sealed class CleanStaticEventViewModel : IDisposable +{ + private int _count; + + public CleanStaticEventViewModel() + { + Calc.GlobalPing += OnGlobalPing; + } + + public void Dispose() + { + Calc.GlobalPing -= OnGlobalPing; // release path -> no promotion + } + + private void OnGlobalPing(object? sender, EventArgs e) { _count++; } +} diff --git a/ownlang/lifetimes.py b/ownlang/lifetimes.py index 1df6c719..8c0009d7 100644 --- a/ownlang/lifetimes.py +++ b/ownlang/lifetimes.py @@ -144,5 +144,11 @@ def _check_fn(fn: A.FnDecl, names: set[str], f"'{sub.source}' (lifetime '{src_lt}') outlives the captured " f"object '{fn.name}' (lifetime '{self_lt}'); the strong " f"subscription promotes '{fn.name}' to '{src_lt}' and it leaks " - f"(no release path)", sub.line)) + f"(no release path)", sub.line, + # a stable identity (source#line) of the captured-by source, so a + # consumer can attribute the escape by symbol rather than scraping + # the message — the OwnIR bridge maps OWN014 back to the original + # C# subscription off exactly this (ownir._handle_of). Invisible to + # rendering, which keys its caret off the message. + subject=f"{sub.source}#{sub.line}")) return out diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 4ce7898f..c83e0bdf 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -39,6 +39,19 @@ - "subscribe": a `X.Subscribe(...)` whose `IDisposable` result is ignored (a bare statement, not captured/disposed) — always a leak; tag `[resource: subscription token]`. + - "capture": a *tokenless* strong subscription (`event += handler` with no + token to release) whose event SOURCE provably outlives the subscriber. This + is NOT an acquire/release owned resource — it lowers to the lifetime engine's + `subscribe self to ` (ownlang/lifetimes.py) with the source's region, + so a source that strictly outlives the captured component yields OWN014 (the + region escape — the captured object is promoted to the longer lifetime and + leaks). The source's lifetime class is the entry's `source`: a `static` + (process-lived) event is the longest region. A source of unknown/shorter + lifetime is left conservative (no finding) — the region model is precise where + the token model (`resource: "subscription"`) only warns. A `capture` with a + matching `-=` (`released: true`) is mitigated and stays silent (the source no + longer holds self on close), just as a released token subscription nets to a + balanced acquire/release. 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]`. @@ -52,7 +65,10 @@ 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). +A `capture` entry instead routes through the lifetime/region engine and surfaces +as OWN014 (region escape) when its source provably outlives — see docs/proposals/ +P-004 and docs/lifetimes.md (the C# facts now reach the region core, not only the +`.own` DSL). An optional top-level `services` array carries the DI registration graph for the DI001 captive-dependency check (P-006) — a separate core analysis (ownlang/di.py) @@ -79,12 +95,16 @@ FnDecl, If, Let, + LifetimeDecl, Module, + Param, Release, ResourceDecl, ResourceMember, Return, Stmt, + Subscribe, + TypeRef, Use, While, ) @@ -154,6 +174,29 @@ def _esc_prop(s: str) -> str: "pool": ("PooledBuffer", "pooled buffer"), } +# --- P-004 region escape (the `capture` resource kind) ---------------------- +# A `capture` is a tokenless strong subscription routed NOT through the +# acquire/release ownership model but through the lifetime/region engine +# (ownlang/lifetimes.py): the captured component lives in a short region, its +# event source in a longer one, and `subscribe self to ` promotes the +# component to the longer lifetime -> OWN014. The map below turns the extractor's +# `source` kind into the source's region; only *provably longer* sources are +# mapped, so an unknown/shorter source produces no node and no finding (the region +# model is conservative — no false positive). `_SUBSCRIBER_REGION` is the shorter +# region every captured component lives in, declared strictly inside every mapped +# source region by `_CAPTURE_LIFETIMES` (added to the module once when any capture +# is present). Slice #1 models the one provable case — a process-lived `static` +# event; further source classes (singletons, parent scopes) are a later slice. +_SUBSCRIBER_REGION = "Subscriber" +_CAPTURE_SOURCE_REGIONS = { + "static": "Process", # a static event (e.g. SystemEvents.*) lives for the + # whole process -> strictly longer than any subscriber. +} +_CAPTURE_LIFETIMES = [ + LifetimeDecl("Process", None, 0), + LifetimeDecl(_SUBSCRIBER_REGION, "Process", 0), # Subscriber strictly < Process +] + @dataclass(frozen=True) class Finding: @@ -287,8 +330,9 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: `release` iff the extractor found a matching unsubscribe. Handles are globally unique so a diagnostic naming one maps straight back to its C# location.""" handles: dict[str, dict[str, Any]] = {} - lines = [f"module {facts.get('module', 'Extracted')}", "", _PRELUDE] gid = 0 + any_capture = False + comp_lines: list[str] = [] components = facts.get("components", []) if not isinstance(components, list): raise OwnIRError("OwnIR 'components' must be a JSON array") @@ -296,30 +340,69 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: if not isinstance(comp, dict): 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 OwnIRError("component 'subscriptions' must be a JSON array") + cap_params: list[str] = [] # `: EventSource lifetime ` + cap_handles: list[str] = [] # sources for `subscribe self to ;` + owned_lines: list[str] = [] # `let = acquire ();` (+ release) for sub in subscriptions: if not isinstance(sub, dict): raise OwnIRError("each subscription must be a JSON object") + rkind = sub.get("resource", "subscription") # An "unresolved-subscription" marker is not an owned resource (the # extractor could not bind the LHS to an event). Do not lower it to an # acquire — that would become a phantom OWN001 leak. It is surfaced as # an advisory OWN050 note by _unresolved_findings instead. - if sub.get("resource") == "unresolved-subscription": + if rkind == "unresolved-subscription": + continue + # A `capture` is the tokenless region-escape shape: it does NOT acquire + # a token (no OWN001); it lowers to `subscribe self to ` with + # the source's region, so the lifetime engine reports OWN014 when the + # source provably outlives. An unmapped (unknown/shorter) source stays + # conservative — no node, no finding. Mirrors to_module exactly. + if rkind == "capture": + # a released capture (matching `-=`) is mitigated -> silent; skip + # it, mirroring to_module (and a released token subscription). + src = sub.get("source") + region = _CAPTURE_SOURCE_REGIONS.get(src) \ + if isinstance(src, str) else None + if region is None or sub.get("released"): + continue + handle = f"cap_{gid}" + gid += 1 + handles[handle] = {**sub, "component": cname, + "file": comp.get("file", "?")} + cap_params.append(f"{handle}: EventSource lifetime {region}") + cap_handles.append(handle) + any_capture = True continue handle = f"sub_{gid}" gid += 1 handles[handle] = {**sub, "component": cname, "file": comp.get("file", "?")} - rtype, _ = _RESOURCES.get(sub.get("resource", "subscription"), - _RESOURCES["subscription"]) - lines.append(f" let {handle} = acquire {rtype}();") + rtype, _ = _RESOURCES.get(rkind, _RESOURCES["subscription"]) + owned_lines.append(f" let {handle} = acquire {rtype}();") if sub.get("released"): - lines.append(f" release {handle};") - lines.append("}") - lines.append("") + owned_lines.append(f" release {handle};") + sig = ", ".join(cap_params) + lt = f" lifetime {_SUBSCRIBER_REGION}" if cap_handles else "" + comp_lines.append(f"fn {cname}({sig}){lt} {{") + comp_lines.extend(owned_lines) + for handle in cap_handles: + comp_lines.append(f" subscribe self to {handle};") + comp_lines.append("}") + comp_lines.append("") + # The region order the captures reference — emitted once, only when needed, so + # a capture-free fact set lowers to byte-identical output as before. + lifetime_lines: list[str] = [] + if any_capture: + for d in _CAPTURE_LIFETIMES: + lifetime_lines.append(f"lifetime {d.name};" if d.longer is None + else f"lifetime {d.name} < {d.longer};") + lifetime_lines.append("") + lines = [f"module {facts.get('module', 'Extracted')}", "", _PRELUDE, + *lifetime_lines, *comp_lines] return "\n".join(lines), handles @@ -357,6 +440,7 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] handles: dict[str, dict[str, Any]] = {} functions: list[FnDecl] = [] gid = 0 + any_capture = False components = facts.get("components", []) if not isinstance(components, list): raise OwnIRError("OwnIR 'components' must be a JSON array") @@ -365,27 +449,60 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] raise OwnIRError("each OwnIR component must be a JSON object") cname = comp.get("name", f"Component{gid}") body: list[Stmt] = [] + params: list[Param] = [] # capture sources, carrying their region + fn_lt: str | None = None # the subscriber region, set iff a capture subscriptions = comp.get("subscriptions", []) if not isinstance(subscriptions, list): raise OwnIRError("component 'subscriptions' must be a JSON array") for sub in subscriptions: if not isinstance(sub, dict): raise OwnIRError("each subscription must be a JSON object") + rkind = sub.get("resource", "subscription") # an unresolved-subscription marker is not an owned resource — it is # surfaced as an advisory OWN050 note, never lowered (see to_own). - if sub.get("resource") == "unresolved-subscription": + if rkind == "unresolved-subscription": + continue + # P-004 region escape: a `capture` is a tokenless strong subscription + # whose source provably outlives the subscriber. Lower it to the + # lifetime engine (`subscribe self to ` + the source's region) + # -> OWN014, NOT to an acquire/release token. The source becomes a + # param carrying its (longer) region; the function carries the shorter + # subscriber region. A source of unknown/shorter lifetime stays + # conservative (no node emitted, hence no finding). cfg.lower_stmt + # treats Subscribe as a no-op and a non-resource param as PLAIN, so + # this is inert for the OWN001 ownership pass — only check_lifetimes + # reads it. + if rkind == "capture": + # A `capture` whose subscription IS torn down (a matching `-=`, + # `released: true`) is mitigated: the source no longer holds self + # on close, so there is no escape — skip it (silent), exactly as a + # released token subscription nets to a balanced acquire/release. + src = sub.get("source") + region = _CAPTURE_SOURCE_REGIONS.get(src) \ + if isinstance(src, str) else None + if region is None or sub.get("released"): + continue + handle = f"cap_{gid}" + gid += 1 + handles[handle] = {**sub, "component": cname, + "file": comp.get("file", "?")} + line = _as_int(sub.get("line", 0)) + params.append(Param(handle, TypeRef("EventSource", False, False, 0), + 0, lifetime=region)) + body.append(Subscribe(handle, line)) + fn_lt = _SUBSCRIBER_REGION + any_capture = True continue handle = f"sub_{gid}" gid += 1 handles[handle] = {**sub, "component": cname, "file": comp.get("file", "?")} - rtype, _ = _RESOURCES.get(sub.get("resource", "subscription"), - _RESOURCES["subscription"]) + rtype, _ = _RESOURCES.get(rkind, _RESOURCES["subscription"]) line = _as_int(sub.get("line", 0)) body.append(Let(handle, Acquire(rtype, [], line), line)) if sub.get("released"): body.append(Release(handle, line)) - functions.append(FnDecl(cname, [], None, body, 0)) + functions.append(FnDecl(cname, params, None, body, 0, lifetime=fn_lt)) # P-016 B0b/B2: per-method flow bodies for local IDisposables (acquire / use / # release / if / return over a CFG). The core checks them path-sensitively # (OWN001 not-released-on-all-paths, OWN002 use-after-release, OWN003 double- @@ -408,7 +525,8 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]] fbody = _lower_flow(nodes, ffile, fname, handles, loc, {}, released) functions.append(FnDecl(fname, [], None, fbody, 0)) return (Module(str(facts.get("module", "Extracted")), - resources=_prelude_resources(), functions=functions), + resources=_prelude_resources(), functions=functions, + lifetimes=list(_CAPTURE_LIFETIMES) if any_capture else []), handles) @@ -562,6 +680,27 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: component=component, event=name, handler="", message=msg, kind="disposable")) continue + if rkind == "capture": + # OWN014 region escape (P-004): the lifetime engine proved the event + # SOURCE outlives the subscriber, so the strong (tokenless) subscription + # promotes '{component}' to the source's longer lifetime and it can + # never be collected. This is the `event += handler` fire-and-forget; + # the mitigation — a disposable token released on close — would be a + # `resource: "subscription"` (OWN001), not this. A provable leak, so it + # stays error-tier (severity None). + src = sub.get("source", "?") + origin = ("a static (process-lived) event source" if src == "static" + else f"a longer-lived source ('{src}')") + message = (f"event '{event}' is subscribed (handler '{handler}') to " + f"{origin} that outlives '{component}'; the strong " + f"subscription promotes '{component}' to the source's " + f"lifetime, so it can never be collected — a region escape " + f"(leak, no release path)") + findings.append(Finding( + file=sub["file"], line=int(sub.get("line", 0)), code=d.code, + component=component, event=event, handler=handler, + message=message, kind="subscription token")) + continue _, kind = _RESOURCES.get(rkind, _RESOURCES["subscription"]) # P-004 tiering: only the plain `event += handler` leak (the else branch # below) grades its severity from the source's proven lifetime; every other diff --git a/scripts/oracle_compare.py b/scripts/oracle_compare.py index 7df59496..feae76de 100644 --- a/scripts/oracle_compare.py +++ b/scripts/oracle_compare.py @@ -54,7 +54,8 @@ def _load_titles() -> dict[str, str]: # Which rule of each tool is the comparable "resource leak / not disposed" class. # Only these are diffed three ways; everything else is reported as context. -OWN_LEAK = {"OWN001"} # owned resource not released on a path +OWN_LEAK = {"OWN001", "OWN014"} # not released on a path / promoted to a + # longer-lived region (subscription escape) OWN_USE_AFTER = {"OWN002", "OWN009"} # use after release (definite / maybe) OWN_DOUBLE = {"OWN003"} # double release INFER_LEAK = {"PULSE_RESOURCE_LEAK", "DOTNET_RESOURCE_LEAK", "RESOURCE_LEAK", diff --git a/tests/fixtures/ownir/capture.facts.json b/tests/fixtures/ownir/capture.facts.json new file mode 100644 index 00000000..aba82fba --- /dev/null +++ b/tests/fixtures/ownir/capture.facts.json @@ -0,0 +1,48 @@ +{ + "ownir_version": 0, + "module": "WpfApp", + "components": [ + { + "name": "ThemeViewModel", + "file": "ThemeViewModel.cs", + "subscriptions": [ + { + "event": "SystemEvents.UserPreferenceChanged", + "handler": "OnUserPreferenceChanged", + "line": 18, + "released": false, + "resource": "capture", + "source": "static" + } + ] + }, + { + "name": "OrdersViewModel", + "file": "OrdersViewModel.cs", + "subscriptions": [ + { + "event": "_bus.OrderPlaced", + "handler": "OnOrderPlaced", + "line": 9, + "released": false, + "resource": "capture", + "source": "injected" + } + ] + }, + { + "name": "CleanThemeViewModel", + "file": "CleanThemeViewModel.cs", + "subscriptions": [ + { + "event": "SystemEvents.UserPreferenceChanged", + "handler": "OnUserPreferenceChanged", + "line": 22, + "released": true, + "resource": "capture", + "source": "static" + } + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 4d572647..73e8fb3b 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -64,6 +64,8 @@ "ownir", "di.facts.json") _UNRESOLVED_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "unresolved.facts.json") +_CAPTURE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "capture.facts.json") def _write_facts(obj: dict) -> str: @@ -513,6 +515,60 @@ def _one(source: str, lambda_: bool = False) -> Finding: fails.append(f"expected 1 real OWN001 leak (non-advisory), got " f"{[(x.code, x.advisory) for x in ufindings]}") + # --- P-004 region escape (OWN014): a `capture` (a TOKENLESS strong + # subscription) whose event SOURCE provably outlives the subscriber routes + # through the lifetime/region engine and lands as OWN014 at the C# site — + # proving C# subscription facts reach the region core (docs/lifetimes.md + # slice #3), not only the hand-written `.own` DSL. An injected-source + # capture (unknown lifetime) stays SILENT: the region model is conservative + # where it cannot prove the source outlives — precise where the token model + # (resource:"subscription") only warns. The lowered sketch still parses. + with open(_CAPTURE_FIXTURE, encoding="utf-8") as f: + cfacts = json.load(f) + csrc, _ = to_own(cfacts) + checks += 1 + try: + parse(csrc) + except Exception as e: + fails.append(f"lowered capture facts do not parse: {e}") + # a capture must NOT be lowered to an acquire STATEMENT (`= acquire`, the token + # model -> OWN001); it lowers to `subscribe self to ...` under a lifetime + # region. (The resource PRELUDE legitimately contains the word "acquire" as a + # member keyword, so match the `= acquire` statement form, not bare "acquire".) + checks += 1 + if "= acquire" in csrc or "subscribe self to cap_0" not in csrc \ + or "lifetime Subscriber < Process" not in csrc: + fails.append(f"capture lowered to the wrong shape (want subscribe+lifetime, " + f"no acquire statement): {csrc!r}") + cfindings = check_facts(cfacts) + checks += 1 + if [(x.component, x.line, x.code) for x in cfindings] != \ + [("ThemeViewModel", 18, "OWN014")]: + fails.append(f"expected one OWN014 region escape (ThemeViewModel@18), got " + f"{[(x.component, x.line, x.code) for x in cfindings]}") + else: + c0 = cfindings[0] + checks += 1 + if c0.severity is not None: + fails.append(f"region escape should be error-tier (None), got " + f"{c0.severity!r}") + if "region escape" not in c0.message or \ + "UserPreferenceChanged" not in c0.message: + fails.append(f"region-escape message wrong: {c0.message!r}") + if "[resource: subscription token]" not in c0.render(): + fails.append(f"region-escape finding missing kind tag: {c0.render()!r}") + # the injected-source capture (unknown lifetime) must NOT be reported. + checks += 1 + if any(x.component == "OrdersViewModel" for x in cfindings): + fails.append("injected-source capture (unprovable) was wrongly reported") + # a RELEASED static capture (a matching `-=` on close — the fix shape) is + # mitigated and must stay silent: the region lowering skips a released capture, + # mirroring a released token subscription. This is what keeps the extractor's + # static-source reroute from flagging correctly-unsubscribed code. + checks += 1 + if any(x.component == "CleanThemeViewModel" for x in cfindings): + fails.append("a released (unsubscribed) static capture was wrongly reported") + # --- output surfaces (Уровень 1): the same finding renders for a human, a # GitHub annotation, and an MSBuild/VS Error List line. The format lives # in the core (one checker), so the Action/script stay thin wrappers.