From 4f0b068f5d1fa18813211f6c1720ac7031be53fd Mon Sep 17 00:00:00 2001 From: PhysShell Date: Tue, 14 Jul 2026 23:15:04 +0500 Subject: [PATCH] corpus(wpf): a `-=` that exists is not a `-=` that runs (#278) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A regression guard for the release-reachability soundness gap: the subscription is to a STATIC publisher, a matching `-=` does exist in the class — so the extractor's "any matching `-=` in the class releases it" model falls silent — but it never runs. It sits behind a bool parameter every caller passes as `true`, in a method that is not a teardown, and that a whole subsystem never calls at all. before.cs is RED today: it is a real leak and own-check says nothing. That is the point of the case. after.cs must stay silent (the release is unconditional and in Dispose), so the fix cannot trade the false negative for a false positive. The .own reduction shows the core already handles this correctly — it reports OWN001 "not released before return (leaks on at least one path)" and points at the guarded branch. The bug is upstream, in the extractor's release-matching. Reduced from SectorTS GTD.cs:5192/:5259 and proven on the heap with a ClrMD root walk: 66.3% of the heap still reachable from the GC roots after 31 documents, held via [PinnedHandle] -> static KernelProperty -> GBProperty -> PropertyChangedEventHandler -> GTD. Detaching after each document makes the process memory-flat (peak RSS 2.71 GB -> 0.61 GB, byte-identical output), which confirms the diagnosis. Prior art: corpus/wpf/subscription-explicit-delegate-release/notes.md:28-41 already records the model as not flow-sensitive, but scoped it to a rebinding setter and deferred it. This case shows the surface is wider and gives it a real instance. CI: recall floor is unaffected (--min-recall is an absolute floor of caught cases, and this one is not caught yet); after.cs adds no false positive. The cfg/diag parity fixtures are regenerated because the corpus grew; tests/run_tests.py and cargo test are both green. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01PjQnE1FDucd6vBVQbFswiE --- corpus/wpf/unsubscribe-behind-a-flag/after.cs | 60 +++++++++++++++ .../wpf/unsubscribe-behind-a-flag/before.cs | 62 +++++++++++++++ corpus/wpf/unsubscribe-behind-a-flag/case.own | 26 +++++++ .../expected-diagnostics.txt | 1 + corpus/wpf/unsubscribe-behind-a-flag/notes.md | 77 +++++++++++++++++++ tests/fixtures/cfg_parity.json | 6 ++ tests/fixtures/diag_parity.json | 10 +++ 7 files changed, 242 insertions(+) create mode 100644 corpus/wpf/unsubscribe-behind-a-flag/after.cs create mode 100644 corpus/wpf/unsubscribe-behind-a-flag/before.cs create mode 100644 corpus/wpf/unsubscribe-behind-a-flag/case.own create mode 100644 corpus/wpf/unsubscribe-behind-a-flag/expected-diagnostics.txt create mode 100644 corpus/wpf/unsubscribe-behind-a-flag/notes.md diff --git a/corpus/wpf/unsubscribe-behind-a-flag/after.cs b/corpus/wpf/unsubscribe-behind-a-flag/after.cs new file mode 100644 index 00000000..8266bb65 --- /dev/null +++ b/corpus/wpf/unsubscribe-behind-a-flag/after.cs @@ -0,0 +1,60 @@ +// FIXED. The release is unconditional and in a teardown. +// +// Two things changed, and both matter: +// +// 1. the `-=` moved into `Dispose()` — a teardown context, which is what P-001/P-004 require; +// 2. the flag no longer guards it. `UnregisterChildren` still exists for the callers that only +// wanted the child rows detached, but it can no longer be mistaken for a full teardown, and +// it cannot silently skip the static detach. +// +// own-check MUST treat this as released (silent). The point of the pair is that `before.cs` and +// `after.cs` differ ONLY in whether the release is provably reached — the `+=` and the `-=` name +// the same (receiver, handler) pair in both files. A model that keys on the mere existence of a +// matching `-=` cannot tell these two apart, which is exactly the soundness gap this case pins. +using System; +using System.ComponentModel; + +public static class AppSettings +{ + public static readonly NotifyingOptions Options = new NotifyingOptions(); +} + +public class NotifyingOptions : INotifyPropertyChanged +{ + public event PropertyChangedEventHandler PropertyChanged; +} + +public sealed class Document : IDisposable +{ + public Document() + { + AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged); + } + + public void Dispose() + { + // Unconditional, in a teardown. This is the one the subscription is paired with. + AppSettings.Options.PropertyChanged -= OnOptionsChanged; + UnregisterChildren(); + } + + // Narrowed and honestly named: it detaches the child rows, and nothing else. It can no longer + // be handed a flag that quietly turns it into a no-op for the static subscription. + public void UnregisterChildren() + { + // ... detach the child rows only ... + } + + private void OnOptionsChanged(object sender, PropertyChangedEventArgs e) { /* ... */ } +} + +public sealed class ImportService +{ + public void Import() + { + using (var doc = new Document()) + { + // ... map / import ... + } // Dispose() detaches it from the static publisher + } +} diff --git a/corpus/wpf/unsubscribe-behind-a-flag/before.cs b/corpus/wpf/unsubscribe-behind-a-flag/before.cs new file mode 100644 index 00000000..93aabe2f --- /dev/null +++ b/corpus/wpf/unsubscribe-behind-a-flag/before.cs @@ -0,0 +1,62 @@ +// BUGGY. A `-=` that exists is not a `-=` that runs. +// +// The document subscribes to a STATIC event in its constructor. A matching `-=` does exist — +// so own-check's release model ("any matching `-=` in the class releases it") falls silent — +// but it is unreachable in practice on two independent counts: +// +// 1. it lives in `UnregisterEventHandlers`, which is not a teardown (`Dispose`/`OnClosed`/ +// `Unloaded`); P-001 and P-004 both specify the release must be *in* a teardown, and the +// extractor is looser than its own spec; +// 2. even when that method IS called, the `-=` sits behind `if (!unregOnlyChildren)`, and the +// calling code passes `true`. +// +// The publisher is static, so the handler pins the whole document graph for the life of the +// process. Reduced from SectorTS `BrokerDataClasses/GTD.cs:5192` (subscribe) / `:5259` +// (the flag-guarded release); heap-proven — 66% of the heap still reachable from the GC roots +// after 31 documents, retention path +// [PinnedHandle] -> static KernelProperty -> GBProperty -> PropertyChangedEventHandler -> GTD. +using System.ComponentModel; + +// The app-lifetime settings object. Static => lives for the whole process. +public static class AppSettings +{ + public static readonly NotifyingOptions Options = new NotifyingOptions(); +} + +public class NotifyingOptions : INotifyPropertyChanged +{ + public event PropertyChangedEventHandler PropertyChanged; +} + +public sealed class Document +{ + public Document() + { + // Subscribed to a STATIC publisher. Nothing detaches this unless somebody calls + // UnregisterEventHandlers(false) — and nobody does. -> OWN001 + AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged); + } + + // NOT a teardown, and the release is guarded away by the parameter every caller passes. + public void UnregisterEventHandlers(bool unregOnlyChildren = false) + { + if (!unregOnlyChildren) + { + AppSettings.Options.PropertyChanged -= OnOptionsChanged; // the `-=` that never runs + } + + // ... detach the child rows only ... + } + + private void OnOptionsChanged(object sender, PropertyChangedEventArgs e) { /* ... */ } +} + +public sealed class ImportService +{ + public Document Import() + { + var doc = new Document(); + doc.UnregisterEventHandlers(true); // true => the static `-=` above is skipped + return doc; + } +} diff --git a/corpus/wpf/unsubscribe-behind-a-flag/case.own b/corpus/wpf/unsubscribe-behind-a-flag/case.own new file mode 100644 index 00000000..32e5d30c --- /dev/null +++ b/corpus/wpf/unsubscribe-behind-a-flag/case.own @@ -0,0 +1,26 @@ +// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC +// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that +// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`; +// one whole subsystem (DocCloud) never calls it at all. +// +// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`. +// The flag is modelled as the branch that returns before the release — the path that skips cleanup — +// so the core flags the un-released subscription as OWN001. +// +// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is +// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching, +// which emits `released: true` from the mere *existence* of a matching `-=` in the class +// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278. +module Corpus +resource Subscription { + acquire Subscribe + release Dispose + kind "subscription token" +} +fn Document(options: int, unregOnlyChildren: int) { + let sub = acquire Subscription(options); // ctor: `+=` on the process-wide static publisher + if (unregOnlyChildren) { + return; // caller passed `true` -> the static `-=` is skipped + } + release sub; // the `-=` only a caller passing `false` ever reaches +} diff --git a/corpus/wpf/unsubscribe-behind-a-flag/expected-diagnostics.txt b/corpus/wpf/unsubscribe-behind-a-flag/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/unsubscribe-behind-a-flag/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/unsubscribe-behind-a-flag/notes.md b/corpus/wpf/unsubscribe-behind-a-flag/notes.md new file mode 100644 index 00000000..e7d88d00 --- /dev/null +++ b/corpus/wpf/unsubscribe-behind-a-flag/notes.md @@ -0,0 +1,77 @@ +# Unsubscribe behind a flag, in a method nobody calls (release-reachability FN) + +> **This case is RED today.** `before.cs` is a real, heap-proven leak and own-check is **silent** on it. +> It is a regression guard for #278, not a passing test. It goes green when release-matching stops +> concluding "released" from the mere *existence* of a `-=`. + +**Pattern.** A document subscribes to a **static** publisher in its constructor. A matching `-=` does +exist in the class — so the current model pairs them and says nothing — but it never runs: + +```csharp +public Document() +{ + AppSettings.Options.PropertyChanged += new PropertyChangedEventHandler(OnOptionsChanged); // static publisher +} + +public void UnregisterEventHandlers(bool unregOnlyChildren = false) // NOT a teardown +{ + if (!unregOnlyChildren) // callers pass true + AppSettings.Options.PropertyChanged -= OnOptionsChanged; // the `-=` that never runs +} +``` + +Three independent reasons the release is unreachable, any one of which is enough: + +1. `UnregisterEventHandlers` is **not a teardown** — not `Dispose`, `OnClosed` or `Unloaded`. + `docs/proposals/P-001-csharp-extractor.md:51` and `P-004-wpf-lifetime-profile.md:33` both specify the + release must be *in* one of those. The extractor is looser than its own spec + (`OwnSharp.Extractor/Program.cs:13`: *"released by a matching `-=` **in the class**"*). +2. The `-=` sits behind a **parameter guard**, and the calling code passes `true`. +3. Whole subsystems **never call the method at all**. + +**Why it matters.** The publisher is static, so the handler pins the subscriber for the life of the +process — the strongest leak tier P-004 defines, and the one the analyzer is supposed to call a *provable* +leak rather than a possible one. + +**Provenance.** Reduced from SectorTS `BrokerDataClasses/GTD.cs:5192` (subscribe to the static +`AppData.Properties.GBProperty`) and `:5259` (`UnregisterEventHandlers(bool UnregOnlyGoodys)`). +`Service/GTDService.cs` passes `true` at five sites; `BrokerDataClasses/DocCloud/**` — including eight +AutoMapper `.ConstructUsing(x => new GTD(null, null))` profiles that build a document per mapping — +never calls it at all. + +Proven at runtime with a ClrMD root walk, after **31 documents**: + +``` +on the heap : 1 685 951 objects 223 MB +REACHABLE from roots : 1 569 072 objects 148 MB +>>> 66.3% of the heap is genuinely RETAINED + +[PinnedHandle] System.Object[] + KernelProperty <- AppData.Properties (static) + GBProperty + PropertyChangedEventHandler + System.Object[] <- the delegate's invocation list + PropertyChangedEventHandler + GTD <- the whole document graph +``` + +Detaching after each document (`UnregisterEventHandlers(false)`) makes the process memory-flat — +peak RSS 2.71 GB → 0.61 GB on the same 389 documents, **byte-identical output** — which confirms the +diagnosis rather than merely being consistent with it. + +**Relation to the known gap.** `corpus/wpf/subscription-explicit-delegate-release/notes.md:28-41` +already records that the release model is not flow-sensitive ("*it treats any matching `-=` in the class +as releasing the subscription … that soundness gap is pre-existing*", Codex P2 on #163). That note scoped +the gap to a **rebinding setter** and deferred it. This case shows the surface is much wider — a +parameter guard, a non-teardown method, and an uncalled method are all ordinary code — and gives the gap +its first real, heap-proven instance. + +**Regression guard.** `scripts/benchmark.py` runs the real C# through the extractor + core: + +* `before.cs` must be **caught** (OWN001) — it is a genuine leak. *Currently it is not: this is the bug.* +* `after.cs` must be **silent** — the release is unconditional and in `Dispose`. It must stay silent + after the fix, or the fix has simply traded a false negative for a false positive. + +The pair differs **only** in whether the release is provably reached; the `+=` and the `-=` name the same +`(receiver, handler)` in both. That is deliberate: a model that keys on the existence of a matching `-=` +cannot tell these two files apart. diff --git a/tests/fixtures/cfg_parity.json b/tests/fixtures/cfg_parity.json index 2b07d228..0d322c6f 100644 --- a/tests/fixtures/cfg_parity.json +++ b/tests/fixtures/cfg_parity.json @@ -241,6 +241,12 @@ "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"GraphicsConfigurationDialog\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 20,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"systemEvents\",\n \"origin\": \"systemEvents#20\",\n \"resource_kind\": null,\n \"type_name\": \"SystemEvents\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", "diags": [] }, + { + "name": "corpus/wpf/unsubscribe-behind-a-flag/case.own", + "source": "// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC\n// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that\n// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`;\n// one whole subsystem (DocCloud) never calls it at all.\n//\n// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`.\n// The flag is modelled as the branch that returns before the release — the path that skips cleanup —\n// so the core flags the un-released subscription as OWN001.\n//\n// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is\n// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching,\n// which emits `released: true` from the mere *existence* of a matching `-=` in the class\n// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278.\nmodule Corpus\nresource Subscription {\n acquire Subscribe\n release Dispose\n kind \"subscription token\"\n}\nfn Document(options: int, unregOnlyChildren: int) {\n let sub = acquire Subscription(options); // ctor: `+=` on the process-wide static publisher\n if (unregOnlyChildren) {\n return; // caller passed `true` -> the static `-=` is skipped\n }\n release sub; // the `-=` only a caller passing `false` ever reaches\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 21,\n \"op\": \"acquire\",\n \"resource\": \"Subscription\",\n \"sym\": 2\n }\n ],\n \"label\": \"entry\",\n \"succ\": [\n 1,\n 2\n ]\n },\n {\n \"id\": 1,\n \"instrs\": [\n {\n \"line\": 23,\n \"op\": \"return\",\n \"sym\": null\n }\n ],\n \"label\": \"then\",\n \"succ\": []\n },\n {\n \"id\": 2,\n \"instrs\": [],\n \"label\": \"else\",\n \"succ\": [\n 3\n ]\n },\n {\n \"id\": 3,\n \"instrs\": [\n {\n \"line\": 25,\n \"op\": \"release\",\n \"sym\": 2\n }\n ],\n \"label\": \"merge\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"Document\",\n \"params\": [\n 0,\n 1\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 20,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"options\",\n \"origin\": \"options#20\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 20,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"unregOnlyChildren\",\n \"origin\": \"unregOnlyChildren#20\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 21,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"sub\",\n \"origin\": \"sub#21\",\n \"resource_kind\": \"subscription token\",\n \"type_name\": \"Subscription\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, { "name": "corpus/wpf/viewmodel-escapes-to-app/case.own", "source": "module WpfRegionEscape\n\n// Lifetime regions: a Window-lived ViewModel must not outlive its window, and\n// the App-lived event bus outlives everything.\nlifetime App;\nlifetime Window < App;\nlifetime ViewModel < Window;\n\n// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived\n// bus. Because App strictly outlives ViewModel, the subscription promotes the\n// VM to App lifetime -> it can never die while the app runs => OWN014. This is\n// the region-escape theorem: the *ordering* is what makes it a leak (subscribing\n// to a same/shorter-lived source would be fine).\nfn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {\n subscribe self to bus;\n}\n", diff --git a/tests/fixtures/diag_parity.json b/tests/fixtures/diag_parity.json index 01fc954c..faf40c9d 100644 --- a/tests/fixtures/diag_parity.json +++ b/tests/fixtures/diag_parity.json @@ -405,6 +405,16 @@ ] ] }, + { + "name": "corpus/wpf/unsubscribe-behind-a-flag/case.own", + "source": "// OwnLang model of SectorTS `BrokerDataClasses/GTD.cs` — a document that subscribes to a STATIC\n// publisher in its constructor (`:5192`) and whose `-=` lives behind a parameter, in a method that\n// is not a teardown (`UnregisterEventHandlers(bool UnregOnlyGoodys)`, `:5259`). Callers pass `true`;\n// one whole subsystem (DocCloud) never calls it at all.\n//\n// `acquire` == `AppSettings.Options.PropertyChanged += h`, `release` == the matching `-=`.\n// The flag is modelled as the branch that returns before the release — the path that skips cleanup —\n// so the core flags the un-released subscription as OWN001.\n//\n// NOTE what this reduction proves: **the core already gets this right.** Give it a release that is\n// not reached on every path and it says so. The bug is upstream, in the extractor's release-matching,\n// which emits `released: true` from the mere *existence* of a matching `-=` in the class\n// (`OwnSharp.Extractor/Program.cs:13`) and never asks whether it runs. See notes.md and #278.\nmodule Corpus\nresource Subscription {\n acquire Subscribe\n release Dispose\n kind \"subscription token\"\n}\nfn Document(options: int, unregOnlyChildren: int) {\n let sub = acquire Subscription(options); // ctor: `+=` on the process-wide static publisher\n if (unregOnlyChildren) {\n return; // caller passed `true` -> the static `-=` is skipped\n }\n release sub; // the `-=` only a caller passing `false` ever reaches\n}\n", + "diags": [ + [ + 23, + "OWN001" + ] + ] + }, { "name": "corpus/wpf/viewmodel-escapes-to-app/case.own", "source": "module WpfRegionEscape\n\n// Lifetime regions: a Window-lived ViewModel must not outlive its window, and\n// the App-lived event bus outlives everything.\nlifetime App;\nlifetime Window < App;\nlifetime ViewModel < Window;\n\n// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived\n// bus. Because App strictly outlives ViewModel, the subscription promotes the\n// VM to App lifetime -> it can never die while the app runs => OWN014. This is\n// the region-escape theorem: the *ordering* is what makes it a leak (subscribing\n// to a same/shorter-lived source would be fine).\nfn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel {\n subscribe self to bus;\n}\n",