feat(wpf): field-mediated cross-method use-after-dispose → OWN002

.github/workflows/ci.yml

@@ -796,7 +796,11 @@ jobs:
         # leak / double-dispose ride the flow (POOL001/003 — `memorypool-double-dispose` -> OWN003), and
         # its `owner.Memory` / `owner.Memory.Span` view is a borrow lowered to a use of the OWNER
         # (`ViewOwner`), so reading it after Dispose trips OWN002 (POOL002 — `memorypool-view-after-
-        # dispose`). Remaining backlog: a FIELD-mediated cross-method use-after-dispose, a view stored in
-        # a FIELD, and an injected-source region-escape. A drop below the floor is a regression.
-        run: python scripts/benchmark.py --min-recall 19
+        # dispose`). A FIELD-mediated cross-method use-after-dispose is caught too: an IDisposable field
+        # disposed in `Dispose()` and DIRECTLY read (`_field.Member`) in a live subscription-target handler
+        # (RHS of a `+=` / arg of a `.Subscribe(...)`, not torn down, no `if (_disposed) return;` guard) is
+        # lowered to a synthetic acquire/release/use flow -> OWN002 (`field-use-after-dispose`). Remaining
+        # backlog: a view stored in a FIELD, an INDIRECT (helper-mediated) field use after dispose, and an
+        # injected-source region-escape. A drop below the floor is a regression.
+        run: python scripts/benchmark.py --min-recall 20
 

corpus/wpf/field-use-after-dispose/after.cs

@@ -0,0 +1,44 @@
+// FIXED. The handler guards on the disposed flag, so a late dispatcher callback
+// bails before touching the connection. (Equivalently, drain the dispatcher queue
+// before disposing.) Nothing reads the connection after Dispose(), so the
+// extractor's field-mediated use-after-dispose detector — which excludes a handler
+// that opens with a `if (_disposed) return;` guard — stays silent.
+using System;
+using System.Data.SqlClient;
+
+public sealed class ReportViewModel : IDisposable
+{
+    private readonly SqlConnection _conn;
+    private readonly IDisposable _sub;
+    private bool _disposed;
+
+    public ReportViewModel(IEventBus bus)
+    {
+        _conn = new SqlConnection("Server=.;Database=Reports");
+        _sub = bus.Subscribe(OnDataChanged);
+    }
+
+    private void OnDataChanged(DataChanged e)
+    {
+        if (_disposed) return;   // do not touch disposed state
+        _conn.ChangeDatabase(e.Database);
+    }
+
+    public void Dispose()
+    {
+        _disposed = true;
+        _sub.Dispose();
+        _conn.Dispose();
+    }
+}
+
+// Minimal in-file stand-ins so the reduction is self-contained.
+public interface IEventBus
+{
+    IDisposable Subscribe(Action<DataChanged> handler);
+}
+
+public sealed class DataChanged
+{
+    public string Database { get; set; } = "";
+}

corpus/wpf/field-use-after-dispose/before.cs

@@ -0,0 +1,52 @@
+// BUGGY (representative WPF/MVVM pattern; the C# extractor now catches this
+// directly under --flow-locals).
+//
+// A ViewModel OWNS a SqlConnection field and subscribes a handler to an injected
+// event bus. On teardown Dispose() disposes the connection (and the subscription
+// token), but a callback that was ALREADY queued on the dispatcher can still run
+// after Dispose() and DIRECTLY touch the disposed connection
+// (`_conn.ChangeDatabase(...)` on a connection already returned to the pool): an
+// ObjectDisposedException / use-after-dispose.
+//
+// Unlike handler-use-after-dispose — whose handler reaches the disposed state
+// INDIRECTLY through a `Refresh()` helper, which the extractor cannot follow — this
+// handler reads the disposed FIELD directly, so the extractor's field-mediated
+// cross-method detector lowers it to a synthetic acquire/release/use flow and the
+// core reports OWN002. The fix (after.cs) guards the handler on the disposed flag.
+using System;
+using System.Data.SqlClient;
+
+public sealed class ReportViewModel : IDisposable
+{
+    private readonly SqlConnection _conn;
+    private readonly IDisposable _sub;
+
+    public ReportViewModel(IEventBus bus)
+    {
+        _conn = new SqlConnection("Server=.;Database=Reports");
+        _sub = bus.Subscribe(OnDataChanged);   // token captured + disposed below
+    }
+
+    private void OnDataChanged(DataChanged e)
+    {
+        // a late, already-dispatched callback: may run AFTER Dispose()
+        _conn.ChangeDatabase(e.Database);   // <-- BUG: _conn may already be disposed
+    }
+
+    public void Dispose()
+    {
+        _sub.Dispose();    // unsubscribe
+        _conn.Dispose();   // dispose the owned connection
+    }
+}
+
+// Minimal in-file stand-ins so the reduction is self-contained.
+public interface IEventBus
+{
+    IDisposable Subscribe(Action<DataChanged> handler);
+}
+
+public sealed class DataChanged
+{
+    public string Database { get; set; } = "";
+}

corpus/wpf/field-use-after-dispose/case.own

@@ -0,0 +1,26 @@
+// OwnLang model of the field-mediated cross-method use-after-dispose the C#
+// extractor now lowers DIRECTLY (a disposed IDisposable field read in a subscribed
+// handler). `acquire` == the owned connection field's construction, `release` ==
+// its `Dispose()` in the ViewModel's Dispose(), `use` == a late dispatcher callback
+// (the subscribed handler) reading the connection AFTER it was disposed. Using a
+// disposable after its release is the generic OWN002, tagged with the resource kind.
+//
+// Contrast handler-use-after-dispose, whose handler reaches the disposed state
+// INDIRECTLY through a helper (`Refresh()`): the extractor only catches the DIRECT
+// `_field.Member` read, so that sibling case stays an honest extractor miss while
+// this one is caught end-to-end.
+module WpfFieldUseAfterDispose
+
+// The owned IDisposable field (a SqlConnection): acquired when the ViewModel
+// constructs it, released by Dispose(). `kind` tags the verdict as a disposable.
+resource Connection {
+    acquire Open
+    release Dispose
+    kind "disposable"
+}
+
+fn OnDataChanged(bus: int) {
+    let conn = acquire Connection(bus);
+    release conn;   // ViewModel.Dispose() disposes the owned connection
+    use conn;       // a late queued callback still touches it -> OWN002
+}

corpus/wpf/field-use-after-dispose/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN002

corpus/wpf/field-use-after-dispose/notes.md

@@ -0,0 +1,45 @@
+# WPF field-mediated use-after-dispose (a disposed field touched in a handler)
+
+**Pattern:** a ViewModel owns an `IDisposable` field (here a `SqlConnection`) and
+subscribes a handler to an event source. On teardown `Dispose()` disposes the field
+(and the subscription token), but a callback that was **already queued on the
+dispatcher** still runs after `Dispose()` and **directly reads the disposed field**
+(`_conn.ChangeDatabase(...)`). In real code this is an `ObjectDisposedException` or a
+read of torn state — the field-mediated cousin of the zombie-ViewModel leak. The
+defensive fix (the canonical one) is a disposed-flag guard at the top of the handler;
+relying on unsubscribe-ordering alone does not close the already-queued-callback race.
+
+**What's new — the extractor catches this end-to-end.** The Roslyn extractor's
+field-mediated cross-method use-after-dispose pass (under `--flow-locals`) recognises
+an `IDisposable` field that is
+
+  1. disposed in this class's `Dispose()` / `DisposeAsync()` (the lifecycle release),
+  2. directly read (`_field.Member`) inside a **live subscription target** — a method
+     that is the RHS of a `+=` or the argument of a `.Subscribe(...)`, and whose
+     subscription is **not** torn down by a matching `-=` (an unsubscribed callback
+     cannot fire post-dispose, so it is exempt), and
+  3. read in a handler with **no** `if (_disposed) return;` guard,
+
+and lowers it to a synthetic `acquire`/`release`/`use` flow. That rides the existing
+OwnIR bridge — the same machinery the local-disposable and MemoryPool slices use — so
+the core raises **OWN002** ("use after release") with no new diagnostic and no second
+checker. `case.own` is the hand reduction of exactly that flow; on the real C# the
+`corpus-benchmark` job scores `before.cs` as caught (OWN002) and `after.cs` (the
+guarded fix) as silent.
+
+**Precision (why it stays low-FP).** The check fires only on a field disposed in the
+dispose *lifecycle*, used in a *live* subscription target, with no guard, via a
+**direct** field member access. The guard exclusion is the canonical fix, so a fixed
+handler is silent; an unsubscribed (`-=`) or empty handler never fires; and an
+*indirect* use through a helper is deliberately **not** chased.
+
+**Honesty / scope.** This catches the **direct** `_field.Member` read. Its sibling
+`handler-use-after-dispose` reaches the disposed state **indirectly** (`Refresh()`
+touches subscription-backed state) — the extractor does not follow that hop, so that
+case remains an honest extractor miss (a tracked recall gap, not a logic gap: its
+`case.own` reduction still fires OWN002). `case.own` here is a faithful hand reduction
+of the ownership logic; `before.cs` / `after.cs` are representative of the bug and its
+fix, not a verbatim copy of one PR.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); the indirect twin
+is `handler-use-after-dispose`; the late-callback framing matches `zombie-viewmodel`.

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -907,6 +907,37 @@
     _ => null,
 };
 
+// The field name an expression refers to ONLY when it names a field of THIS object — a bare
+// `_f` or `this._f`, NOT `other._f` (a same-named field on a DIFFERENT receiver, which plain
+// text matching would conflate into a phantom release/use, CodeRabbit). Deliberately syntactic,
+// not symbol-bound: the field-UAF corpus uses types that do not resolve in the project-local
+// compilation, so binding on the field's TYPE is unreliable — the `this`/bare receiver shape is
+// exact regardless.
+static string? ThisFieldName(ExpressionSyntax expr) => expr switch
+{
+    IdentifierNameSyntax id => id.Identifier.Text,
+    MemberAccessExpressionSyntax m when m.Expression is ThisExpressionSyntax
+        => m.Name.Identifier.Text,
+    _ => null,
+};
+
+// Is there a disposed-flag early-return guard (`if (_disposed) return;`, `if (IsDisposed) return;`)
+// among a handler body's TOP-LEVEL statements that OPENS before source position `before`? Such a
+// guard makes a later disposed-field read safe (the canonical fix), so the field-UAF pass excludes
+// it. Tight on purpose (CodeRabbit/Codex): (1) the guard must PRECEDE the read — a guard only after
+// the read does not protect it, so that finding still stands; (2) the THEN branch must be an
+// IMMEDIATE `return` (the guard's own action), not a `return` buried in a nested/`else` branch; and
+// (3) the flag identifier matches "dispos" case-INsensitively, so the PascalCase `IsDisposed` form
+// is recognised as well as `_disposed`.
+static bool DisposedGuardBefore(BlockSyntax body, int before) =>
+    body.Statements.OfType<IfStatementSyntax>().Any(ifs =>
+        ifs.SpanStart < before
+        && ifs.Condition.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>()
+            .Any(id => id.Identifier.Text.Contains("ispos", StringComparison.OrdinalIgnoreCase))
+        && (ifs.Statement is ReturnStatementSyntax
+            || (ifs.Statement is BlockSyntax gb
+                && gb.Statements.FirstOrDefault() is ReturnStatementSyntax)));
+
 // Is `t` the System.Buffers.ArrayPool<T> type — the Return-based pool we model?
 // Checked on the resolved SYMBOL, not the receiver's text, so an aliased receiver
 // (`ArrayPool<int> p = ArrayPool<int>.Shared; p.Rent(n)`) binds correctly and an
@@ -1671,7 +1702,7 @@
     .Split(Path.PathSeparator, StringSplitOptions.RemoveEmptyEntries)
     .Where(p => p.EndsWith(".dll", StringComparison.OrdinalIgnoreCase))
     .ToList();
 var refNames = new HashSet<string>(tpa.Select(Path.GetFileName), StringComparer.OrdinalIgnoreCase);
 var references = tpa.Select(p => (MetadataReference)MetadataReference.CreateFromFile(p)).ToList();
 // P-004 WPF profile: widen the reference set with assemblies named by the
 // OWN_EXTRA_REF_DIRS env var (colon-separated dirs) — e.g. the WindowsDesktop ref
@@ -1872,6 +1903,123 @@
             }
         }
 
+        // P-007 / WPF: a field-mediated cross-method USE-AFTER-DISPOSE. An IDisposable
+        // field disposed in this class's Dispose()/DisposeAsync() is then DIRECTLY read
+        // (`_f.Member`) in an event-handler method — a callback an external event source
+        // can still invoke AFTER the object is disposed (the very reason WPF handler
+        // leaks matter). With no `if (_disposed) return;` guard the handler touches a
+        // field already disposed: a use-after-dispose. We lower it to a synthetic
+        // acquire/release/use flow so the existing OwnIR bridge raises OWN002 at the
+        // field — no new diagnostic, no second checker (the synthetic-flow trick the
+        // MemoryPool slices use). Precise by construction to stay low-FP: fires only when
+        //   (a) the field is disposed in the dispose LIFECYCLE (not an ad-hoc `_f.Dispose()`),
+        //   (b) the touching method is a LIVE subscription target — RHS of a `+=` / arg of
+        //       a `.Subscribe(...)` — whose subscription is NOT torn down (`-= handler`
+        //       means the callback cannot fire post-dispose, so it is safe),
+        //   (c) the method has no disposed-guard (the canonical fix silences it), and
+        //   (d) the use is a DIRECT field member access (an INDIRECT use via a helper is
+        //       deliberately not chased — that is the harder frontier, left honest).
+        // Gated on --flow-locals like the rest of the synthetic-flow emission.
+        if (flowLocals)
+        {
+            // IDisposable fields -> declaration line (the synthetic `acquire`).
+            var dispoFieldLine = new Dictionary<string, int>(StringComparer.Ordinal);
+            foreach (var fd in cls.Members.OfType<FieldDeclarationSyntax>())
+            {
+                if (fd.Modifiers.Any(mm => mm.IsKind(SyntaxKind.StaticKeyword)))
+                    continue;
+                if (!IsDisposableType(fd.Declaration.Type.ToString()))
+                    continue;
+                foreach (var v in fd.Declaration.Variables)
+                    dispoFieldLine[v.Identifier.Text] = LineOf(v);
+            }
+            // field -> line of its `.Dispose()` INSIDE Dispose()/DisposeAsync() (the
+            // release event). Restricted to the dispose methods so an ordinary
+            // `_f.Dispose()` helper is not misread as object teardown.
+            var releasedAt = new Dictionary<string, int>(StringComparer.Ordinal);
+            if (dispoFieldLine.Count > 0)
+                foreach (var dm in cls.Members.OfType<MethodDeclarationSyntax>())
+                {
+                    if (dm.Identifier.Text is not ("Dispose" or "DisposeAsync"))
+                        continue;
+                    foreach (var inv in dm.DescendantNodes().OfType<InvocationExpressionSyntax>())
+                        if (inv.Expression is MemberAccessExpressionSyntax dmm
+                            && dmm.Name.Identifier.Text is "Dispose" or "DisposeAsync"
+                            && ThisFieldName(dmm.Expression) is { } df
+                            && dispoFieldLine.ContainsKey(df)
+                            && !releasedAt.ContainsKey(df))
+                            releasedAt[df] = LineOf(inv);
+                }
+            if (releasedAt.Count > 0)
+            {
+                // handler method names that are LIVE subscription targets. `+=` subscriptions are
+                // keyed by SOURCE|handler so a `-=` removes only the MATCHING one — a handler still
+                // `+=`'d to another live source stays live (a name-only set would let one `-=` drop
+                // it globally, CodeRabbit/Codex). A `.Subscribe(handler)` token is released by
+                // disposing the token (the Rx idiom), not a `-=`, so those handlers are always live.
+                var liveEventKeys = new HashSet<string>(StringComparer.Ordinal);
+                foreach (var a in assigns)
+                    if (IsHandler(a.Right) && FieldName(a.Right) is { } hn)
+                    {
+                        var key = $"{a.Left}|{hn}";
+                        if (a.IsKind(SyntaxKind.AddAssignmentExpression)) liveEventKeys.Add(key);
+                        else if (a.IsKind(SyntaxKind.SubtractAssignmentExpression)) liveEventKeys.Remove(key);
+                    }
+                var subscribed = new HashSet<string>(
+                    liveEventKeys.Select(k => k[(k.LastIndexOf('|') + 1)..]), StringComparer.Ordinal);
+                foreach (var inv in cls.DescendantNodes().OfType<InvocationExpressionSyntax>())
+                    if (inv.Expression is MemberAccessExpressionSyntax sm
+                        && sm.Name.Identifier.Text == "Subscribe")
+                        foreach (var arg in inv.ArgumentList.Arguments)
+                            if (FieldName(arg.Expression) is { } hn)
+                                subscribed.Add(hn);
+
+                foreach (var hm in cls.Members.OfType<MethodDeclarationSyntax>())
+                {
+                    if (hm.Body is not { } hbody)
+                        continue;
+                    var hname = hm.Identifier.Text;
+                    if (hname is "Dispose" or "DisposeAsync")
+                        continue;
+                    if (!subscribed.Contains(hname))
+                        continue;
+                    // the FIRST direct read of a disposed field of THIS class (`_f` / `this._f`,
+                    // not `other._f`) in the handler, if any.
+                    MemberAccessExpressionSyntax? use = null;
+                    string? useField = null;
+                    foreach (var ma in hbody.DescendantNodes().OfType<MemberAccessExpressionSyntax>())
+                    {
+                        if (ma.Name.Identifier.Text is "Dispose" or "DisposeAsync")
+                            continue;
+                        if (ThisFieldName(ma.Expression) is { } uf && releasedAt.ContainsKey(uf))
+                        {
+                            use = ma;
+                            useField = uf;
+                            break;
+                        }
+                    }
+                    // no direct disposed-field read, or an opening disposed-guard PRECEDES it ->
+                    // not a use-after-dispose (an INDIRECT use via a helper is left an honest miss).
+                    // Otherwise emit ONE synthetic acquire/release/use flow -> OWN002 via the bridge.
+                    if (use is null || useField is null)
+                        continue;
+                    if (DisposedGuardBefore(hbody, use.SpanStart))
+                        continue;
+                    flowFunctions.Add(new
+                    {
+                        name = $"{cls.Identifier.Text}.{hname}",
+                        file,
+                        body = new List<object>
+                        {
+                            new { op = "acquire", var = useField, line = dispoFieldLine[useField] },
+                            new { op = "release", var = useField, line = releasedAt[useField] },
+                            new { op = "use", var = useField, line = LineOf(use) },
+                        },
+                    });
+                }
+            }
+        }
+
         // WPF004: a `X.Subscribe(...)` whose IDisposable result is ignored — the
         // call stands as a bare statement (not assigned/returned/added), so the
         // token is dropped and never disposed. Member-access only (`x.Subscribe`),