From 8f936f5502cee0565e3320fd5e9235aee5ae8392 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 19 Jul 2026 02:52:16 +0000 Subject: [PATCH 1/3] =?UTF-8?q?test(corpus):=20red=20=E2=80=94=20WPF002=20?= =?UTF-8?q?Stop()=20teardown=20soundness:=207=20timer=20fixtures?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The stopped set credits ANY .Stop() anywhere in the class — existence as proof of execution, the exact false-negative class #278 closed for -=. Reproduced on real C# through the extractor + core (DispatcherTimer stand-in — not IDisposable, so Stop() IS the release and WPF003 stays out of the way): six before.cs are falsely SILENT today (timer fact stamped released: true by a Stop() that nothing proves runs): * timer-stop-nonteardown-release — Stop() only in an arbitrary method * timer-stop-finalizer-release — Stop() only in the finalizer * timer-stop-unwired-lifecycle — Stop() in an unwired Window_Closing * timer-stop-uncalled-helper — Stop() in a helper no teardown calls * timer-stop-uncalled-lambda — Stop() in a stored, never-invoked lambda * timer-stop-param-guarded — Stop() behind a caller-parameter guard Each after.cs is the positive twin (Dispose / platform teardown / wired handler / transitively-called helper / wired lambda / field guard) and is silent both before and after the fix. The seventh case pins what already holds: timer-stop-wrong-receiver — a sibling's Stop() must not release the checked timer (receiver identity; flagged today, stays flagged). case.own reductions extend the wpf suite to 24/24; the P-022 parity fixtures (cfg 83 / diag 84 cases) are regenerated for the new corpus and the frozen-corpus Rust parity test stays green. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01MdYFKUaygHz1T9H1qJ7BqK --- .../wpf/timer-stop-finalizer-release/after.cs | 31 ++++++++ .../timer-stop-finalizer-release/before.cs | 37 ++++++++++ .../wpf/timer-stop-finalizer-release/case.own | 17 +++++ .../expected-diagnostics.txt | 1 + .../wpf/timer-stop-finalizer-release/notes.md | 12 ++++ .../timer-stop-nonteardown-release/after.cs | 32 +++++++++ .../timer-stop-nonteardown-release/before.cs | 38 ++++++++++ .../timer-stop-nonteardown-release/case.own | 18 +++++ .../expected-diagnostics.txt | 1 + .../timer-stop-nonteardown-release/notes.md | 12 ++++ corpus/wpf/timer-stop-param-guarded/after.cs | 40 +++++++++++ corpus/wpf/timer-stop-param-guarded/before.cs | 43 ++++++++++++ corpus/wpf/timer-stop-param-guarded/case.own | 18 +++++ .../expected-diagnostics.txt | 1 + corpus/wpf/timer-stop-param-guarded/notes.md | 12 ++++ .../wpf/timer-stop-uncalled-helper/after.cs | 37 ++++++++++ .../wpf/timer-stop-uncalled-helper/before.cs | 42 +++++++++++ .../wpf/timer-stop-uncalled-helper/case.own | 17 +++++ .../expected-diagnostics.txt | 1 + .../wpf/timer-stop-uncalled-helper/notes.md | 12 ++++ .../wpf/timer-stop-uncalled-lambda/after.cs | 29 ++++++++ .../wpf/timer-stop-uncalled-lambda/before.cs | 33 +++++++++ .../wpf/timer-stop-uncalled-lambda/case.own | 17 +++++ .../expected-diagnostics.txt | 1 + .../wpf/timer-stop-uncalled-lambda/notes.md | 12 ++++ .../wpf/timer-stop-unwired-lifecycle/after.cs | 35 ++++++++++ .../timer-stop-unwired-lifecycle/before.cs | 37 ++++++++++ .../wpf/timer-stop-unwired-lifecycle/case.own | 17 +++++ .../expected-diagnostics.txt | 1 + .../wpf/timer-stop-unwired-lifecycle/notes.md | 12 ++++ corpus/wpf/timer-stop-wrong-receiver/after.cs | 36 ++++++++++ .../wpf/timer-stop-wrong-receiver/before.cs | 39 +++++++++++ corpus/wpf/timer-stop-wrong-receiver/case.own | 19 +++++ .../expected-diagnostics.txt | 1 + corpus/wpf/timer-stop-wrong-receiver/notes.md | 12 ++++ tests/fixtures/cfg_parity.json | 42 +++++++++++ tests/fixtures/diag_parity.json | 70 +++++++++++++++++++ 37 files changed, 835 insertions(+) create mode 100644 corpus/wpf/timer-stop-finalizer-release/after.cs create mode 100644 corpus/wpf/timer-stop-finalizer-release/before.cs create mode 100644 corpus/wpf/timer-stop-finalizer-release/case.own create mode 100644 corpus/wpf/timer-stop-finalizer-release/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-finalizer-release/notes.md create mode 100644 corpus/wpf/timer-stop-nonteardown-release/after.cs create mode 100644 corpus/wpf/timer-stop-nonteardown-release/before.cs create mode 100644 corpus/wpf/timer-stop-nonteardown-release/case.own create mode 100644 corpus/wpf/timer-stop-nonteardown-release/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-nonteardown-release/notes.md create mode 100644 corpus/wpf/timer-stop-param-guarded/after.cs create mode 100644 corpus/wpf/timer-stop-param-guarded/before.cs create mode 100644 corpus/wpf/timer-stop-param-guarded/case.own create mode 100644 corpus/wpf/timer-stop-param-guarded/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-param-guarded/notes.md create mode 100644 corpus/wpf/timer-stop-uncalled-helper/after.cs create mode 100644 corpus/wpf/timer-stop-uncalled-helper/before.cs create mode 100644 corpus/wpf/timer-stop-uncalled-helper/case.own create mode 100644 corpus/wpf/timer-stop-uncalled-helper/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-uncalled-helper/notes.md create mode 100644 corpus/wpf/timer-stop-uncalled-lambda/after.cs create mode 100644 corpus/wpf/timer-stop-uncalled-lambda/before.cs create mode 100644 corpus/wpf/timer-stop-uncalled-lambda/case.own create mode 100644 corpus/wpf/timer-stop-uncalled-lambda/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-uncalled-lambda/notes.md create mode 100644 corpus/wpf/timer-stop-unwired-lifecycle/after.cs create mode 100644 corpus/wpf/timer-stop-unwired-lifecycle/before.cs create mode 100644 corpus/wpf/timer-stop-unwired-lifecycle/case.own create mode 100644 corpus/wpf/timer-stop-unwired-lifecycle/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-unwired-lifecycle/notes.md create mode 100644 corpus/wpf/timer-stop-wrong-receiver/after.cs create mode 100644 corpus/wpf/timer-stop-wrong-receiver/before.cs create mode 100644 corpus/wpf/timer-stop-wrong-receiver/case.own create mode 100644 corpus/wpf/timer-stop-wrong-receiver/expected-diagnostics.txt create mode 100644 corpus/wpf/timer-stop-wrong-receiver/notes.md diff --git a/corpus/wpf/timer-stop-finalizer-release/after.cs b/corpus/wpf/timer-stop-finalizer-release/after.cs new file mode 100644 index 00000000..743a4fab --- /dev/null +++ b/corpus/wpf/timer-stop-finalizer-release/after.cs @@ -0,0 +1,31 @@ +// FIXED. The Stop() moves to a recognised platform teardown method +// (`OnClosed`) — a real teardown root, so the release is proven. +using System; + +public class HeartbeatMonitor +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public HeartbeatMonitor() + { + _timer.Tick += OnBeat; + _timer.Start(); + } + + protected virtual void OnClosed(EventArgs e) + { + _timer.Stop(); + } + + private void OnBeat(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-finalizer-release/before.cs b/corpus/wpf/timer-stop-finalizer-release/before.cs new file mode 100644 index 00000000..973df139 --- /dev/null +++ b/corpus/wpf/timer-stop-finalizer-release/before.cs @@ -0,0 +1,37 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The only `Stop()` sits in the FINALIZER. A finalizer is not a teardown +// proof: it runs only if the object is ever collected — and the running timer +// is exactly what keeps the object reachable, so the finalizer never fires +// for the live leak. Same rule as the `-=`-in-finalizer case (#278). +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class HeartbeatMonitor +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public HeartbeatMonitor() + { + _timer.Tick += OnBeat; + _timer.Start(); + } + + ~HeartbeatMonitor() + { + _timer.Stop(); // never proven to run; the timer pins the object + } + + private void OnBeat(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-finalizer-release/case.own b/corpus/wpf/timer-stop-finalizer-release/case.own new file mode 100644 index 00000000..6be83f3b --- /dev/null +++ b/corpus/wpf/timer-stop-finalizer-release/case.own @@ -0,0 +1,17 @@ +module WpfTimerStopFinalizer + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The only Stop() is in the finalizer, which the running timer itself keeps +// from ever firing. Modelled as the ctor scope alone => OWN001. +fn HeartbeatMonitor(interval: int) { + let t = acquire Timer(interval); + // finalizer Stop() is not a teardown path -> never-stopped timer (before.cs) +} diff --git a/corpus/wpf/timer-stop-finalizer-release/expected-diagnostics.txt b/corpus/wpf/timer-stop-finalizer-release/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-finalizer-release/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-finalizer-release/notes.md b/corpus/wpf/timer-stop-finalizer-release/notes.md new file mode 100644 index 00000000..8014ddbb --- /dev/null +++ b/corpus/wpf/timer-stop-finalizer-release/notes.md @@ -0,0 +1,12 @@ +# timer-stop-finalizer-release + +**Pattern.** Stop() only in the finalizer: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — a finalizer is not a teardown proof — the running timer itself pins the object. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-nonteardown-release/after.cs b/corpus/wpf/timer-stop-nonteardown-release/after.cs new file mode 100644 index 00000000..d8e77d98 --- /dev/null +++ b/corpus/wpf/timer-stop-nonteardown-release/after.cs @@ -0,0 +1,32 @@ +// FIXED. The SAME Stop() — but now it runs in Dispose, a proven teardown +// context, unconditionally. own-check MUST treat the timer as released +// (silent). +using System; + +public sealed class TickerView : IDisposable +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public TickerView() + { + _timer.Tick += OnTick; + _timer.Start(); + } + + public void Dispose() + { + _timer.Stop(); + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-nonteardown-release/before.cs b/corpus/wpf/timer-stop-nonteardown-release/before.cs new file mode 100644 index 00000000..a2b1699f --- /dev/null +++ b/corpus/wpf/timer-stop-nonteardown-release/before.cs @@ -0,0 +1,38 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The ctor wires and starts a timer; the only `Stop()` sits in an arbitrary +// public method (`Pause`) that no lifecycle path is proven to call. The mere +// EXISTENCE of a Stop() is not evidence that it RUNS — the same #278 rule that +// already governs `-=`. The old "any Stop() on the receiver = released" model +// silenced this — the false negative this case pins. +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class TickerView +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public TickerView() + { + _timer.Tick += OnTick; + _timer.Start(); + } + + public void Pause() + { + _timer.Stop(); // arbitrary method: nobody has to call this + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-nonteardown-release/case.own b/corpus/wpf/timer-stop-nonteardown-release/case.own new file mode 100644 index 00000000..06f3168c --- /dev/null +++ b/corpus/wpf/timer-stop-nonteardown-release/case.own @@ -0,0 +1,18 @@ +module WpfTimerStopNonTeardown + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The ctor starts the timer; the only `Stop()` lives in an arbitrary +// non-teardown method nothing is proven to call. Modelled as the ctor scope +// alone: acquired, never released on any teardown path => OWN001. +fn TickerView(interval: int) { + let t = acquire Timer(interval); + // no `release t;` on any teardown path -> never-stopped timer (before.cs) +} diff --git a/corpus/wpf/timer-stop-nonteardown-release/expected-diagnostics.txt b/corpus/wpf/timer-stop-nonteardown-release/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-nonteardown-release/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-nonteardown-release/notes.md b/corpus/wpf/timer-stop-nonteardown-release/notes.md new file mode 100644 index 00000000..8d441f3a --- /dev/null +++ b/corpus/wpf/timer-stop-nonteardown-release/notes.md @@ -0,0 +1,12 @@ +# timer-stop-nonteardown-release + +**Pattern.** Stop() only in an arbitrary public method: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — the release-context rule that already governs `-=` (#278) applied to `Stop()`. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-param-guarded/after.cs b/corpus/wpf/timer-stop-param-guarded/after.cs new file mode 100644 index 00000000..d59b693e --- /dev/null +++ b/corpus/wpf/timer-stop-param-guarded/after.cs @@ -0,0 +1,40 @@ +// FIXED. The SAME teardown path — but the guard is now the class's OWN state +// (a field), not a caller-controlled parameter, so the release is credited +// (field guards are the class's own bookkeeping). +using System; + +public sealed class FeedTicker : IDisposable +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + private bool _running; + + public FeedTicker() + { + _timer.Tick += OnTick; + _timer.Start(); + _running = true; + } + + public void Dispose() + { + Shutdown(); + } + + private void Shutdown() + { + if (_running) + _timer.Stop(); + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-param-guarded/before.cs b/corpus/wpf/timer-stop-param-guarded/before.cs new file mode 100644 index 00000000..012854a1 --- /dev/null +++ b/corpus/wpf/timer-stop-param-guarded/before.cs @@ -0,0 +1,43 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The Stop() DOES sit on a teardown path (Dispose calls Shutdown), but behind +// a guard that depends on a PARAMETER of the enclosing method — the caller +// chooses whether the release runs. Same #278 rule as the parameter-guarded +// `-=`: not proven. +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class FeedTicker : IDisposable +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public FeedTicker() + { + _timer.Tick += OnTick; + _timer.Start(); + } + + public void Dispose() + { + Shutdown(false); + } + + private void Shutdown(bool stopTimer) + { + if (stopTimer) + _timer.Stop(); // caller-controlled: the release may be skipped + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-param-guarded/case.own b/corpus/wpf/timer-stop-param-guarded/case.own new file mode 100644 index 00000000..6f9de3a0 --- /dev/null +++ b/corpus/wpf/timer-stop-param-guarded/case.own @@ -0,0 +1,18 @@ +module WpfTimerStopParamGuarded + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The Stop() sits on a teardown path but behind a caller-controlled +// parameter guard — the caller can skip it. Modelled as the ctor scope +// alone => OWN001. +fn FeedTicker(interval: int) { + let t = acquire Timer(interval); + // a caller-parameter-guarded Stop() is not a proven release (before.cs) +} diff --git a/corpus/wpf/timer-stop-param-guarded/expected-diagnostics.txt b/corpus/wpf/timer-stop-param-guarded/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-param-guarded/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-param-guarded/notes.md b/corpus/wpf/timer-stop-param-guarded/notes.md new file mode 100644 index 00000000..13e6124c --- /dev/null +++ b/corpus/wpf/timer-stop-param-guarded/notes.md @@ -0,0 +1,12 @@ +# timer-stop-param-guarded + +**Pattern.** Stop() on a teardown path but behind a caller-parameter guard: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — the caller chooses whether the release runs — same rule as the parameter-guarded `-=`. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-uncalled-helper/after.cs b/corpus/wpf/timer-stop-uncalled-helper/after.cs new file mode 100644 index 00000000..e76351d4 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-helper/after.cs @@ -0,0 +1,37 @@ +// FIXED. The SAME helper — but now Dispose calls it, so the helper joins the +// teardown closure (symbol-resolved, transitive) and the Stop() inside it is +// proven to run at teardown. +using System; + +public sealed class ChartRefresher : IDisposable +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public ChartRefresher() + { + _timer.Tick += OnRefresh; + _timer.Start(); + } + + public void Dispose() + { + ReleaseTimer(); // the teardown call is the proof + } + + private void ReleaseTimer() + { + _timer.Stop(); + } + + private void OnRefresh(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-uncalled-helper/before.cs b/corpus/wpf/timer-stop-uncalled-helper/before.cs new file mode 100644 index 00000000..42a743ff --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-helper/before.cs @@ -0,0 +1,42 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The Stop() sits in a private helper (`ReleaseTimer`) that NO teardown ever +// calls — only an arbitrary public method does. Declaration is not execution; +// a helper joins the teardown closure only when a teardown provably CALLS it +// (the symbol-resolved transitive rule from #278). +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class ChartRefresher +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public ChartRefresher() + { + _timer.Tick += OnRefresh; + _timer.Start(); + } + + public void Reset() + { + ReleaseTimer(); // arbitrary method: nobody has to call this + } + + private void ReleaseTimer() + { + _timer.Stop(); + } + + private void OnRefresh(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-uncalled-helper/case.own b/corpus/wpf/timer-stop-uncalled-helper/case.own new file mode 100644 index 00000000..c5e24181 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-helper/case.own @@ -0,0 +1,17 @@ +module WpfTimerStopUncalledHelper + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The Stop() hides in a helper no teardown calls. Modelled as the ctor +// scope alone => OWN001. +fn ChartRefresher(interval: int) { + let t = acquire Timer(interval); + // helper Stop() without a teardown caller is not a release (before.cs) +} diff --git a/corpus/wpf/timer-stop-uncalled-helper/expected-diagnostics.txt b/corpus/wpf/timer-stop-uncalled-helper/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-helper/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-uncalled-helper/notes.md b/corpus/wpf/timer-stop-uncalled-helper/notes.md new file mode 100644 index 00000000..8b7e151a --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-helper/notes.md @@ -0,0 +1,12 @@ +# timer-stop-uncalled-helper + +**Pattern.** Stop() in a private helper no teardown calls: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — a helper joins the teardown closure only when a teardown provably calls it (symbol-resolved, transitive). + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-uncalled-lambda/after.cs b/corpus/wpf/timer-stop-uncalled-lambda/after.cs new file mode 100644 index 00000000..0a65c221 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-lambda/after.cs @@ -0,0 +1,29 @@ +// FIXED. The SAME lambda body — but now it is the handler wired to the pane's +// own Closed lifecycle event, so it provably runs at teardown. +using System; + +public sealed class PollingPane +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public event EventHandler Closed; // raised by the host at teardown + + public PollingPane() + { + _timer.Tick += OnPoll; + _timer.Start(); + this.Closed += (s, e) => _timer.Stop(); // wired lifecycle lambda + } + + private void OnPoll(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-uncalled-lambda/before.cs b/corpus/wpf/timer-stop-uncalled-lambda/before.cs new file mode 100644 index 00000000..3c29d5f0 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-lambda/before.cs @@ -0,0 +1,33 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The Stop() sits inside a lambda stored in a field — a deferred delegate +// nothing here proves is ever invoked. A lambda counts as teardown ONLY as +// the handler wired to a self lifecycle event (#278 rule). +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class PollingPane +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + private readonly Action _cleanup; + + public PollingPane() + { + _timer.Tick += OnPoll; + _timer.Start(); + _cleanup = () => _timer.Stop(); // declared, never proven invoked + } + + private void OnPoll(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-uncalled-lambda/case.own b/corpus/wpf/timer-stop-uncalled-lambda/case.own new file mode 100644 index 00000000..9028f58b --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-lambda/case.own @@ -0,0 +1,17 @@ +module WpfTimerStopUncalledLambda + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The Stop() hides in a stored, never-invoked lambda. Modelled as the ctor +// scope alone => OWN001. +fn PollingPane(interval: int) { + let t = acquire Timer(interval); + // a declared-but-unwired lambda Stop() is not a teardown path (before.cs) +} diff --git a/corpus/wpf/timer-stop-uncalled-lambda/expected-diagnostics.txt b/corpus/wpf/timer-stop-uncalled-lambda/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-lambda/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-uncalled-lambda/notes.md b/corpus/wpf/timer-stop-uncalled-lambda/notes.md new file mode 100644 index 00000000..7cc9c669 --- /dev/null +++ b/corpus/wpf/timer-stop-uncalled-lambda/notes.md @@ -0,0 +1,12 @@ +# timer-stop-uncalled-lambda + +**Pattern.** Stop() inside a stored, never-invoked lambda: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — a lambda is teardown only as the handler wired to a self lifecycle event. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-unwired-lifecycle/after.cs b/corpus/wpf/timer-stop-unwired-lifecycle/after.cs new file mode 100644 index 00000000..39bef765 --- /dev/null +++ b/corpus/wpf/timer-stop-unwired-lifecycle/after.cs @@ -0,0 +1,35 @@ +// FIXED. The SAME handler name — but now the ctor provably wires it to the +// view's own Closing lifecycle event, so the Stop() inside it runs at +// teardown. The release is credited by the wiring, never by the name. +using System; + +public sealed class SplashTicker +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public event EventHandler Closing; // raised by the host at teardown + + public SplashTicker() + { + _timer.Tick += OnTick; + _timer.Start(); + this.Closing += Window_Closing; // the wiring is the proof + } + + private void Window_Closing(object sender, EventArgs e) + { + _timer.Stop(); + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-unwired-lifecycle/before.cs b/corpus/wpf/timer-stop-unwired-lifecycle/before.cs new file mode 100644 index 00000000..0d5062f2 --- /dev/null +++ b/corpus/wpf/timer-stop-unwired-lifecycle/before.cs @@ -0,0 +1,37 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// The Stop() sits in a method NAMED like a XAML-wired lifecycle handler +// (`Window_Closing`) — but nothing in code attaches it to any event. The name +// alone proves nothing (same as the `-=` twin: the suffix-only exemption was +// removed in #278's follow-up). +// +// own-check MUST flag this OWN001 [resource: timer]. +using System; + +public sealed class SplashTicker +{ + private readonly DispatcherTimer _timer = new DispatcherTimer(); + + public SplashTicker() + { + _timer.Tick += OnTick; + _timer.Start(); + } + + private void Window_Closing(object sender, EventArgs e) + { + _timer.Stop(); // nothing wires this handler + } + + private void OnTick(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-unwired-lifecycle/case.own b/corpus/wpf/timer-stop-unwired-lifecycle/case.own new file mode 100644 index 00000000..f384a6a2 --- /dev/null +++ b/corpus/wpf/timer-stop-unwired-lifecycle/case.own @@ -0,0 +1,17 @@ +module WpfTimerStopUnwired + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// The Stop() hides in a lifecycle-looking method nothing wires. Modelled as +// the ctor scope alone => OWN001. +fn SplashTicker(interval: int) { + let t = acquire Timer(interval); + // unwired Window_Closing Stop() is not a teardown path (before.cs) +} diff --git a/corpus/wpf/timer-stop-unwired-lifecycle/expected-diagnostics.txt b/corpus/wpf/timer-stop-unwired-lifecycle/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-unwired-lifecycle/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-unwired-lifecycle/notes.md b/corpus/wpf/timer-stop-unwired-lifecycle/notes.md new file mode 100644 index 00000000..19a8fbda --- /dev/null +++ b/corpus/wpf/timer-stop-unwired-lifecycle/notes.md @@ -0,0 +1,12 @@ +# timer-stop-unwired-lifecycle + +**Pattern.** Stop() in a Window_Closing-named method with no wiring: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — a lifecycle-looking NAME is not evidence; only a code-wired handler counts. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/corpus/wpf/timer-stop-wrong-receiver/after.cs b/corpus/wpf/timer-stop-wrong-receiver/after.cs new file mode 100644 index 00000000..b2b6b657 --- /dev/null +++ b/corpus/wpf/timer-stop-wrong-receiver/after.cs @@ -0,0 +1,36 @@ +// FIXED. Dispose stops BOTH timers — each receiver released by its own +// Stop() in the teardown. +using System; + +public sealed class DualPoller : IDisposable +{ + private readonly DispatcherTimer _fast = new DispatcherTimer(); + private readonly DispatcherTimer _slow = new DispatcherTimer(); + + public DualPoller() + { + _fast.Tick += OnFast; + _fast.Start(); + _slow.Tick += OnSlow; + _slow.Start(); + } + + public void Dispose() + { + _fast.Stop(); + _slow.Stop(); + } + + private void OnFast(object sender, EventArgs e) { /* ... */ } + private void OnSlow(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-wrong-receiver/before.cs b/corpus/wpf/timer-stop-wrong-receiver/before.cs new file mode 100644 index 00000000..d7817175 --- /dev/null +++ b/corpus/wpf/timer-stop-wrong-receiver/before.cs @@ -0,0 +1,39 @@ +// BUGGY (WPF002 soundness slice; hand-reduced into case.own). +// +// Two timers; Dispose stops only ONE of them. A Stop() releases exactly its +// own receiver — the sibling's Stop() must not silence the other timer. +// +// own-check MUST flag the unstopped timer OWN001 [resource: timer]. +using System; + +public sealed class DualPoller : IDisposable +{ + private readonly DispatcherTimer _fast = new DispatcherTimer(); + private readonly DispatcherTimer _slow = new DispatcherTimer(); + + public DualPoller() + { + _fast.Tick += OnFast; + _fast.Start(); + _slow.Tick += OnSlow; + _slow.Start(); + } + + public void Dispose() + { + _slow.Stop(); // only the slow timer; _fast keeps running + } + + private void OnFast(object sender, EventArgs e) { /* ... */ } + private void OnSlow(object sender, EventArgs e) { /* ... */ } +} + +// In-file stand-in for System.Windows.Threading.DispatcherTimer (WPF is not on +// the corpus reference set; same shape as samples/SampleTypes.cs). NOT +// IDisposable — Stop() IS the release, which is exactly the WPF002 pattern. +public sealed class DispatcherTimer +{ + public event EventHandler Tick; + public void Start() { } + public void Stop() { } +} diff --git a/corpus/wpf/timer-stop-wrong-receiver/case.own b/corpus/wpf/timer-stop-wrong-receiver/case.own new file mode 100644 index 00000000..464627e3 --- /dev/null +++ b/corpus/wpf/timer-stop-wrong-receiver/case.own @@ -0,0 +1,19 @@ +module WpfTimerStopWrongReceiver + +// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner +// edge; the matching `Stop()` releases it. `kind` tags the resource so the +// generic ownership finding carries a [resource: timer] note. +resource Timer { + acquire Start + release Stop + kind "timer" +} + +// Two timers, only one stopped at teardown: the sibling's Stop() does not +// release the other receiver => OWN001 for the unstopped one. +fn DualPoller(fast: int, slow: int) { + let a = acquire Timer(fast); + let b = acquire Timer(slow); + release b; + // `a` has no release -> the sibling's Stop() does not silence it (before.cs) +} diff --git a/corpus/wpf/timer-stop-wrong-receiver/expected-diagnostics.txt b/corpus/wpf/timer-stop-wrong-receiver/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/timer-stop-wrong-receiver/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/timer-stop-wrong-receiver/notes.md b/corpus/wpf/timer-stop-wrong-receiver/notes.md new file mode 100644 index 00000000..87b5cc27 --- /dev/null +++ b/corpus/wpf/timer-stop-wrong-receiver/notes.md @@ -0,0 +1,12 @@ +# timer-stop-wrong-receiver + +**Pattern.** Dispose stops only the sibling timer: the WPF002 timer pattern's `Stop()`-based release must +use the same teardown doctrine as `-=` (#278) — a Stop() releases exactly its own receiver; receiver identity keeps the other timer honest. + +**Source.** Hand-reduced from the WPF002 `Stop()` soundness investigation (the +`stopped` set used to credit ANY `Stop()` on the receiver, anywhere in the +class — existence is not execution). + +**Honesty caveat.** `case.own` is a hand reduction pinning the ownership +logic; `before.cs`/`after.cs` are the real-C# recall/specificity pair the +corpus benchmark scores through the actual extractor. diff --git a/tests/fixtures/cfg_parity.json b/tests/fixtures/cfg_parity.json index 67d97e06..990bf4f1 100644 --- a/tests/fixtures/cfg_parity.json +++ b/tests/fixtures/cfg_parity.json @@ -289,6 +289,48 @@ "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/timer-stop-finalizer-release/case.own", + "source": "module WpfTimerStopFinalizer\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The only Stop() is in the finalizer, which the running timer itself keeps\n// from ever firing. Modelled as the ctor scope alone => OWN001.\nfn HeartbeatMonitor(interval: int) {\n let t = acquire Timer(interval);\n // finalizer Stop() is not a teardown path -> never-stopped timer (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 15,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"HeartbeatMonitor\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#15\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-nonteardown-release/case.own", + "source": "module WpfTimerStopNonTeardown\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The ctor starts the timer; the only `Stop()` lives in an arbitrary\n// non-teardown method nothing is proven to call. Modelled as the ctor scope\n// alone: acquired, never released on any teardown path => OWN001.\nfn TickerView(interval: int) {\n let t = acquire Timer(interval);\n // no `release t;` on any teardown path -> never-stopped timer (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 16,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"TickerView\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#15\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 16,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#16\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-param-guarded/case.own", + "source": "module WpfTimerStopParamGuarded\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() sits on a teardown path but behind a caller-controlled\n// parameter guard — the caller can skip it. Modelled as the ctor scope\n// alone => OWN001.\nfn FeedTicker(interval: int) {\n let t = acquire Timer(interval);\n // a caller-parameter-guarded Stop() is not a proven release (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 16,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"FeedTicker\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#15\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 16,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#16\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-uncalled-helper/case.own", + "source": "module WpfTimerStopUncalledHelper\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a helper no teardown calls. Modelled as the ctor\n// scope alone => OWN001.\nfn ChartRefresher(interval: int) {\n let t = acquire Timer(interval);\n // helper Stop() without a teardown caller is not a release (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 15,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"ChartRefresher\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#15\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-uncalled-lambda/case.own", + "source": "module WpfTimerStopUncalledLambda\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a stored, never-invoked lambda. Modelled as the ctor\n// scope alone => OWN001.\nfn PollingPane(interval: int) {\n let t = acquire Timer(interval);\n // a declared-but-unwired lambda Stop() is not a teardown path (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 15,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"PollingPane\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#15\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-unwired-lifecycle/case.own", + "source": "module WpfTimerStopUnwired\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a lifecycle-looking method nothing wires. Modelled as\n// the ctor scope alone => OWN001.\nfn SplashTicker(interval: int) {\n let t = acquire Timer(interval);\n // unwired Window_Closing Stop() is not a teardown path (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 15,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 1\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"SplashTicker\",\n \"params\": [\n 0\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"interval\",\n \"origin\": \"interval#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"t\",\n \"origin\": \"t#15\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n }\n ]\n }\n ],\n \"ownlang_cfg_version\": 0\n}", + "diags": [] + }, + { + "name": "corpus/wpf/timer-stop-wrong-receiver/case.own", + "source": "module WpfTimerStopWrongReceiver\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// Two timers, only one stopped at teardown: the sibling's Stop() does not\n// release the other receiver => OWN001 for the unstopped one.\nfn DualPoller(fast: int, slow: int) {\n let a = acquire Timer(fast);\n let b = acquire Timer(slow);\n release b;\n // `a` has no release -> the sibling's Stop() does not silence it (before.cs)\n}\n", + "cfg": "{\n \"functions\": [\n {\n \"blocks\": [\n {\n \"id\": 0,\n \"instrs\": [\n {\n \"line\": 15,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 2\n },\n {\n \"line\": 16,\n \"op\": \"acquire\",\n \"resource\": \"Timer\",\n \"sym\": 3\n },\n {\n \"line\": 17,\n \"op\": \"release\",\n \"sym\": 3\n }\n ],\n \"label\": \"entry\",\n \"succ\": []\n }\n ],\n \"entry\": 0,\n \"has_return_type\": false,\n \"name\": \"DualPoller\",\n \"params\": [\n 0,\n 1\n ],\n \"symbols\": [\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"fast\",\n \"origin\": \"fast#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 14,\n \"is_param_borrow\": false,\n \"kind\": \"plain\",\n \"name\": \"slow\",\n \"origin\": \"slow#14\",\n \"resource_kind\": null,\n \"type_name\": \"int\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 15,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"a\",\n \"origin\": \"a#15\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\n },\n {\n \"borrow_is_mut\": null,\n \"buffer\": null,\n \"def_line\": 16,\n \"is_param_borrow\": false,\n \"kind\": \"owned\",\n \"name\": \"b\",\n \"origin\": \"b#16\",\n \"resource_kind\": \"timer\",\n \"type_name\": \"Timer\"\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 e65a1dcb..7bf88728 100644 --- a/tests/fixtures/diag_parity.json +++ b/tests/fixtures/diag_parity.json @@ -485,6 +485,76 @@ ] ] }, + { + "name": "corpus/wpf/timer-stop-finalizer-release/case.own", + "source": "module WpfTimerStopFinalizer\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The only Stop() is in the finalizer, which the running timer itself keeps\n// from ever firing. Modelled as the ctor scope alone => OWN001.\nfn HeartbeatMonitor(interval: int) {\n let t = acquire Timer(interval);\n // finalizer Stop() is not a teardown path -> never-stopped timer (before.cs)\n}\n", + "diags": [ + [ + 15, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-nonteardown-release/case.own", + "source": "module WpfTimerStopNonTeardown\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The ctor starts the timer; the only `Stop()` lives in an arbitrary\n// non-teardown method nothing is proven to call. Modelled as the ctor scope\n// alone: acquired, never released on any teardown path => OWN001.\nfn TickerView(interval: int) {\n let t = acquire Timer(interval);\n // no `release t;` on any teardown path -> never-stopped timer (before.cs)\n}\n", + "diags": [ + [ + 16, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-param-guarded/case.own", + "source": "module WpfTimerStopParamGuarded\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() sits on a teardown path but behind a caller-controlled\n// parameter guard — the caller can skip it. Modelled as the ctor scope\n// alone => OWN001.\nfn FeedTicker(interval: int) {\n let t = acquire Timer(interval);\n // a caller-parameter-guarded Stop() is not a proven release (before.cs)\n}\n", + "diags": [ + [ + 16, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-uncalled-helper/case.own", + "source": "module WpfTimerStopUncalledHelper\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a helper no teardown calls. Modelled as the ctor\n// scope alone => OWN001.\nfn ChartRefresher(interval: int) {\n let t = acquire Timer(interval);\n // helper Stop() without a teardown caller is not a release (before.cs)\n}\n", + "diags": [ + [ + 15, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-uncalled-lambda/case.own", + "source": "module WpfTimerStopUncalledLambda\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a stored, never-invoked lambda. Modelled as the ctor\n// scope alone => OWN001.\nfn PollingPane(interval: int) {\n let t = acquire Timer(interval);\n // a declared-but-unwired lambda Stop() is not a teardown path (before.cs)\n}\n", + "diags": [ + [ + 15, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-unwired-lifecycle/case.own", + "source": "module WpfTimerStopUnwired\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// The Stop() hides in a lifecycle-looking method nothing wires. Modelled as\n// the ctor scope alone => OWN001.\nfn SplashTicker(interval: int) {\n let t = acquire Timer(interval);\n // unwired Window_Closing Stop() is not a teardown path (before.cs)\n}\n", + "diags": [ + [ + 15, + "OWN001" + ] + ] + }, + { + "name": "corpus/wpf/timer-stop-wrong-receiver/case.own", + "source": "module WpfTimerStopWrongReceiver\n\n// A running timer: `Elapsed += handler` + `Start()` acquires the timer<->owner\n// edge; the matching `Stop()` releases it. `kind` tags the resource so the\n// generic ownership finding carries a [resource: timer] note.\nresource Timer {\n acquire Start\n release Stop\n kind \"timer\"\n}\n\n// Two timers, only one stopped at teardown: the sibling's Stop() does not\n// release the other receiver => OWN001 for the unstopped one.\nfn DualPoller(fast: int, slow: int) {\n let a = acquire Timer(fast);\n let b = acquire Timer(slow);\n release b;\n // `a` has no release -> the sibling's Stop() does not silence it (before.cs)\n}\n", + "diags": [ + [ + 17, + "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", From 07ac2cf0ee7ed4f09816a7e06d24971ddfef148b Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 19 Jul 2026 03:01:35 +0000 Subject: [PATCH 2/3] =?UTF-8?q?fix(extractor):=20green=20=E2=80=94=20WPF00?= =?UTF-8?q?2=20Stop()=20shares=20the=20-=3D=20teardown/guard=20doctrine?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One predicate, one context model: InTeardownContext and IsParamGuardedRelease generalize from AssignmentExpressionSyntax to SyntaxNode (they only ever walked ancestors), and the stopped set now admits a receiver only when its .Stop() invocation passes BOTH — the exact gate the -= release has had since #278. A Stop() in an arbitrary method, a finalizer, an unwired lifecycle-looking handler, an uncalled helper or lambda, or behind a caller-parameter guard credits nothing; the timer fact keeps released: false and the honest OWN001 [resource: timer] stands. Receiver identity is unchanged: a sibling's Stop() never releases the checked timer. Verified on real C# through the extractor + core: all 7 red before.cs now flag OWN001 (released: false), all 7 after.cs twins stay silent (released: true); the extractor-S2 samples behave identically (TimerViewModel flagged / CleanTimerViewModel credited); full corpus benchmark 57/58 caught, 58/58 fixes clean, 0 false positives (the one miss is the documented pre-existing injected-source region-escape backlog case, which contains no Stop at all); build clean. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01MdYFKUaygHz1T9H1qJ7BqK --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 35 +++++++++++++------ 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index a1c07a94..ecfb6775 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -20,7 +20,10 @@ // or behind a caller-controlled flag, is not proven to run and keeps the honest // warning. // A `Tick`/`Elapsed` handler is tagged resource=timer (WPF002) and is released -// if the timer's receiver also has a `.Stop()` call. The IDisposable/pool/local detectors remain syntactic for now +// only by a `.Stop()` on the timer's receiver that is PROVEN to run at teardown +// (the same teardown/guard doctrine as the `-=` above — an arbitrary-method, +// finalizer, unwired-handler or parameter-guarded Stop() credits nothing). +// The IDisposable/pool/local detectors remain syntactic for now // (P-014 rollout: the event fact goes type-aware first). // // Usage: ownsharp-extract [extract] [more ...] [-o|--out facts.json] @@ -997,10 +1000,14 @@ void Add(IMethodSymbol? m) // proven teardown), a non-teardown method, a FINALIZER (never runs while the // publisher's delegate keeps the subscriber reachable), an unwired lambda, or an // uncalled local function => no. -static bool InTeardownContext(AssignmentExpressionSyntax sub, ClassDeclarationSyntax cls, +// The release SITE is any node whose execution-at-teardown must be proven — a +// `-=` unsubscribe assignment or a timer `.Stop()` invocation. One predicate, +// one context model: the two release kinds must never disagree about what a +// teardown is. +static bool InTeardownContext(SyntaxNode site, ClassDeclarationSyntax cls, HashSet teardownMethods, SemanticModel model) { - for (SyntaxNode? cur = sub.Parent; cur is not null; cur = cur.Parent) + for (SyntaxNode? cur = site.Parent; cur is not null; cur = cur.Parent) { switch (cur) { @@ -1047,9 +1054,9 @@ static bool InTeardownContext(AssignmentExpressionSyntax sub, ClassDeclarationSy // `if (disposing) { ... }` runs on every `Dispose()` call, so a POSITIVE use of // that single bool parameter does not demote; `if (!disposing)` (the finalizer // branch) still does. -static bool IsParamGuardedRelease(AssignmentExpressionSyntax sub, SemanticModel model) +static bool IsParamGuardedRelease(SyntaxNode site, SemanticModel model) { - for (SyntaxNode? cur = sub.Parent; cur is not null && cur is not MemberDeclarationSyntax; cur = cur.Parent) + for (SyntaxNode? cur = site.Parent; cur is not null && cur is not MemberDeclarationSyntax; cur = cur.Parent) { ExpressionSyntax? cond = cur switch { @@ -5173,8 +5180,9 @@ static bool IsPublicCtor(SyntaxTokenList modifiers) // pairing SectorTS GTD's ctor `+=` with a flag-skipped `-=` and silently // swallowed a heap-proven leak. Only a teardown-context, unguarded `-=` // credits release now; everything else keeps the honest OWN001/OWN014. - // (Self-detaching handlers, old->new rotation and timer `.Stop()` have - // their own dedicated checks below, unchanged.) + // (Self-detaching handlers and old->new rotation have their own + // dedicated checks below; a timer `.Stop()` shares THIS teardown/guard + // model — see the `stopped` collection just below.) var clsSymbol = model.GetDeclaredSymbol(cls); var teardownMethods = TeardownContextMethods(cls, model, clsSymbol); var unsub = new HashSet(); @@ -5185,12 +5193,19 @@ static bool IsPublicCtor(SyntaxTokenList modifiers) && !IsParamGuardedRelease(a, model)) unsub.Add($"{a.Left}|{NormalizeHandler(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). + // every receiver whose `.Stop()` is PROVEN to run at teardown: a timer + // detached this way counts as released even without an explicit + // `Tick -=` (e.g. Stop() in Dispose). WPF002 soundness: the same + // doctrine as the `-=` above — a Stop() in an arbitrary method, a + // finalizer, an unwired lifecycle-looking handler, an uncalled + // helper/lambda, or behind a caller-parameter guard is EXISTENCE, not + // execution, and credits nothing (the honest OWN001 stands). var stopped = new HashSet(); foreach (var inv in cls.DescendantNodes().OfType()) if (inv.Expression is MemberAccessExpressionSyntax m - && m.Name.Identifier.Text == "Stop") + && m.Name.Identifier.Text == "Stop" + && InTeardownContext(inv, cls, teardownMethods, model) + && !IsParamGuardedRelease(inv, model)) stopped.Add(m.Expression.ToString()); // Fields/locals this class constructs (`new`) — it OWNS them, so their From c1d4fe6f49e076cff94ff41dd461021513b10729 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 19 Jul 2026 03:01:35 +0000 Subject: [PATCH 3/3] docs(notes): WPF002 Stop() obeys the shared #278 teardown doctrine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit subscription-leaks-and-profiles.md records the extended doctrine: the WPF002 row's Stop() release uses the SAME teardown/guard context predicate as -=, with the seven timer-stop corpus cases listed beside the #278 subscription set. The extractor-header wording fix rode the green commit (it sits in Program.cs); tcplistener-stop-release.md is deliberately untouched — the flow-local TcpListener.Stop() release is a different mechanism, outside this slice. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01MdYFKUaygHz1T9H1qJ7BqK --- docs/notes/subscription-leaks-and-profiles.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/docs/notes/subscription-leaks-and-profiles.md b/docs/notes/subscription-leaks-and-profiles.md index 2d5207cc..59b8e3ea 100644 --- a/docs/notes/subscription-leaks-and-profiles.md +++ b/docs/notes/subscription-leaks-and-profiles.md @@ -56,6 +56,17 @@ SectorTS `GTD`; corpus: `subscription-param-guarded-unregister`, `subscription-xaml-name-only-release`, `subscription-overload-conflated-cleanup`, `subscription-uncalled-local-function`). +The WPF002 row's `Stop()` release obeys the SAME doctrine (the WPF002 Stop() +soundness slice): a timer is released only by a `Stop()` on ITS receiver that +is proven to run at teardown and is not caller-parameter-guarded — one shared +context predicate with `-=`, not a second copy. A `Stop()` that merely exists +(arbitrary method, finalizer, unwired `Window_Closing`-style name, uncalled +helper/lambda, caller-controlled flag) credits nothing (corpus: +`timer-stop-nonteardown-release`, `timer-stop-finalizer-release`, +`timer-stop-unwired-lifecycle`, `timer-stop-uncalled-helper`, +`timer-stop-uncalled-lambda`, `timer-stop-param-guarded`, +`timer-stop-wrong-receiver`). + ## The naming debt the critique correctly smells The capability is general. The *same* `source.Event += h` without `-=` leaks in