feat(extractor): inter-procedural consume contract → use-after-handoff OWN002 (recall 8/10→9/11)

.github/workflows/ci.yml

@@ -625,13 +625,13 @@ jobs:
       - name: Score the corpus on real C#
         # Precision is gated absolutely (every fix silent, zero false positives);
         # recall is pinned at the measured floor and ratchets up as the extractor
-        # improves. Now 8/10 — pooled buffers ride the path-sensitive flow engine
-        # (Rent = acquire, Return = release: OWN003/OWN002, pool resolved via the Roslyn
-        # SemanticModel so an ALIASED receiver is caught), and ownership-transferring
-        # factory acquires (System.IO.File.Open*/Create*) are now recognised alongside
-        # `new`, so the leak arm of the interprocedural-handoff case fires OWN001.
-        # Remaining backlog: the use-after-handoff (OWN002) arm of that case, a
-        # cross-method use-after-dispose, and an injected-source region-escape. A drop
-        # below the floor is a regression.
-        run: python scripts/benchmark.py --min-recall 8
+        # improves. Now 9/11 — pooled buffers ride the path-sensitive flow engine
+        # (Rent/Return: OWN003/OWN002, pool resolved via the Roslyn SemanticModel so an
+        # ALIASED receiver is caught), factory acquires (System.IO.File.Open*/Create*) are
+        # recognised alongside `new`, and the inter-procedural CONSUME contract is modelled:
+        # a first-party method owning a by-value IDisposable param is a handoff (a `call`
+        # op), so a use after the handoff trips OWN002 (the cut is the signature, like
+        # Rust's move). Remaining backlog: a cross-method use-after-dispose and an
+        # injected-source region-escape. A drop below the floor is a regression.
+        run: python scripts/benchmark.py --min-recall 9
 

corpus/real-world/ownership-handoff-use/after.cs

@@ -0,0 +1,20 @@
+using System;
+using System.IO;
+
+// FIX: read everything we need BEFORE handing ownership off, then never touch the stream.
+static class HandoffUse
+{
+    public static void Consume(Stream sink)
+    {
+        sink.CopyTo(Stream.Null);
+        sink.Dispose();
+    }
+
+    static long Run(string path)
+    {
+        var s = File.OpenRead(path);
+        long len = s.Length;            // read first ...
+        Consume(s);                     // ... then move ownership last
+        return len;
+    }
+}

corpus/real-world/ownership-handoff-use/before.cs

@@ -0,0 +1,26 @@
+using System;
+using System.IO;
+
+// A pure inter-procedural use-after-handoff (no leak arm): a stream is handed to a
+// consumer that takes OWNERSHIP (reads it, then disposes it), and the caller then touches
+// the stream again. Unlike ownership-handoff-consume there is no leak arm -- the handoff
+// itself is correct, so the ONLY bug is the use AFTER ownership moved. Common shape:
+// serialize/compress into a stream, hand it to a sink that owns it, then accidentally read
+// it once more (an ObjectDisposedException at runtime).
+static class HandoffUse
+{
+    // Consumer: takes ownership of `sink` and closes it. `sink` is `consume Stream`.
+    public static void Consume(Stream sink)
+    {
+        sink.CopyTo(Stream.Null);
+        sink.Dispose();                 // Consume owns and closes it
+    }
+
+    // BUG: ownership moved into Consume (which disposed it), then the stream is read. -> OWN002
+    static long Run(string path)
+    {
+        var s = File.OpenRead(path);
+        Consume(s);                     // ownership moves to Consume
+        return s.Length;                // use-after-handoff (s is disposed) -> OWN002
+    }
+}

corpus/real-world/ownership-handoff-use/case.own

@@ -0,0 +1,21 @@
+// OwnLang model of a PURE inter-procedural use-after-handoff (no leak arm). `take` takes
+// the stream BY VALUE (a resource type => CONSUME): ownership moves in and it closes the
+// stream, so a caller must not touch it after the handoff. `run` hands off then reads ->
+// OWN002 (use after the resource was consumed by the callee). The fix reads BEFORE the
+// handoff. The signature is the cut -- the caller is checked against `take`'s contract,
+// not its body; no whole-program analysis. (`consume` is an OwnLang keyword, so the
+// reduction names the consumer `take`; the C# consumer is `Consume`.)
+module Corpus
+resource Stream {
+  acquire open
+  release close
+}
+fn take(s: Stream) {
+  use s;
+  release s;
+}
+fn run() {
+  let s = acquire Stream();
+  take(s);             // ownership moves into the consumer
+  use s;               // <-- touched after handoff -> OWN002
+}

corpus/real-world/ownership-handoff-use/expected-diagnostics.txt

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

corpus/real-world/ownership-handoff-use/notes.md

@@ -0,0 +1,26 @@
+# Inter-procedural use-after-handoff (pure)
+
+**Pattern:** a stream is handed to a consumer that takes **ownership** (reads it, then
+`Dispose()`s it), and the caller then touches the stream again. Unlike
+`ownership-handoff-consume` there is **no leak arm** — the handoff itself is correct, so the
+*only* bug is the use **after** ownership moved. Common shape: serialize/compress into a
+stream, hand it to a sink that owns it, then accidentally read it once more (an
+`ObjectDisposedException` at runtime).
+
+**What the checker says:** using a resource after it was consumed by a callee is the generic
+**OWN002** (use after release) — the same code `.own` produces for use-after-dispose.
+
+**Why this case exists (the consume-contract proof).** The extractor used to treat any
+argument-passing as an *escape* (untracked), so a stream handed to `Consume(s)` simply
+vanished and the later `s.Length` was invisible — a **miss**. Now a call to a first-party
+**consumer** — a method whose own body disposes a by-value `IDisposable` parameter — is
+modelled as a **release of the argument at the call site**, the same shape as pool
+`Return(buf)` (the resource leaves the caller's hands right there). The use *after* that
+release then trips **OWN002**. The signal is the callee's own body, so it is inter-procedural
+without a cross-call signature table (and so without a dangling-callee crash). This fixture is
+a *miss* before and a *catch* after; `ownership-handoff-consume` is caught for its leak arm
+either way, so this is the row that makes the use-after-handoff capability a measurable ratchet.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction of the C# pattern, not C# the
+`.own` checker ingested. `before.cs` / `after.cs` are representative of the bug and its fix,
+not a verbatim copy of one PR.

docs/notes/corpus-benchmark.md

@@ -26,7 +26,7 @@ correct code), and **recall was 3/9** — the three caught are exactly the
 subscription/region class the extractor is strongest at (`zombie-viewmodel` →
 OWN001, two static-event escapes → OWN014).
 
-## Ratchet → 8/10 (four ratchets)
+## Ratchet → 9/11 (five ratchets)
 
 ### → 4/9: a fixture was understating us
 
@@ -89,14 +89,33 @@ handed back by some other API is never mistaken for an acquire). With it the lea
 8/10**. The blast radius is exactly one file: nothing else in the corpus or the samples opens
 a `File.*` stream, so no `after.cs` and no dog-food scan can newly cry wolf.
 
-The remaining gaps are genuine **frontend extraction** islands. The *use-after-handoff*
-(`OWN002`) arm of `ownership-handoff-consume` — caught only as the leak today — needs the
-inter-procedural **consume** contract (a method that disposes a by-value parameter, checked at
-call sites like Rust's move; the cut is the *signature*, no whole-program points-to). A
-field/cross-method use-after-dispose needs cross-method field-state. And the injected-source
-region-escape (`viewmodel-escapes-to-app`) needs the source's lifetime *proven* — its DI
-registration — which the fixture does not even carry. The `.own` reductions catch all three;
-the C# extractor does not yet. Each is a real capability the floor will ratchet up to as it lands.
+### → 9/11: the inter-procedural consume contract
+
+The last handoff gap was the *use-after-handoff* arm — a stream handed to a consumer that
+disposes it, then touched again (`OWN002`). The extractor treated every argument-pass as an
+*escape* (untracked), so the handed-off stream vanished and the later read was invisible. Now
+a call to a first-party **consumer** — a method whose own body disposes a by-value
+`IDisposable` parameter — is modelled as a **release of the argument at the call site**, the
+same shape as pool `Return(buf)` (the resource leaves the caller's hands right there). A use of
+the argument *after* that call is then a use-after-release, `OWN002`; the matching argument is
+exempted from the escape set so it stays tracked through the handoff. It is inter-procedural —
+the signal is the *callee's own body* — but there is **no cross-call signature table**, so a
+callee with no body to inspect (interface / abstract / extern) or that doesn't dispose the
+parameter yields nothing and the argument stays an ordinary escape. Crucially there is no
+dangling `call` op to a method the flow pass never lowered (the early call-op design crashed
+the bridge on exactly that — `UnitOfWorkFlowSample`'s consumer, whose body the pass skips), and
+the escape exemption is gated on the *same* body-inspection as the release, so an argument is
+exempted **iff** it is also released — never a tracked-but-unreleased local that would read as a
+false leak. A new fixture `ownership-handoff-use` (a *pure* use-after-handoff, no leak arm) is a
+miss before and a catch after, so **recall is now 9/11**; `ownership-handoff-consume` now fires
+both its arms (`OWN001`+`OWN002`). The verdicts were pinned locally (hand-built facts →
+`check_facts` → the exact `OWN001`/`OWN002` and silence on the fixes).
+
+The remaining gaps are genuine **frontend extraction** islands: a field/cross-method
+use-after-dispose needs cross-method field-state, and the injected-source region-escape
+(`viewmodel-escapes-to-app`) needs the source's lifetime *proven* — its DI registration —
+which the fixture does not even carry. The `.own` reductions catch both; the C# extractor does
+not yet. Each is a real capability the floor will ratchet up to as it lands.
 
 ## Why catch/clean, not exact-code match
 

docs/proposals/P-012-bug-corpus-mining.md

@@ -6,7 +6,7 @@
   (the bug is caught) and specificity (the fix is silent), gated in the
   `corpus-benchmark` CI job. This is the measurement spine — the defensible number,
   and the verifiable reward for any future learning loop. First measurement **3/9
-  caught · 9/9 clean · 0 FP**, ratcheted to **8/10** over four steps: (1) a *fixture*
+  caught · 9/9 clean · 0 FP**, ratcheted to **9/11** over five steps: (1) a *fixture*
   was understating us — `screentogif-loaded-subscription` referenced an undeclared VM
   type → `OWN050`, fixed by making it self-contained; (2) a real *capability* —
   pooled buffers are now routed through the path-sensitive flow engine (Rent =
@@ -17,10 +17,14 @@
   receiver (`var p = ArrayPool<int>.Shared; p.Return(buf)`) — a miss for the text
   heuristic — is caught (`arraypool-aliased-receiver`, +1 row); (4) ownership-transferring
   **factory acquires** (`System.IO.File.Open*`/`Create*`) are recognised alongside `new`,
-  so the leak arm of the interprocedural-handoff case fires `OWN001`. Perfect precision
-  throughout. The remaining gaps: the use-after-handoff (`OWN002`) arm of that case (needs
-  the inter-procedural *consume* contract), a cross-method use-after-dispose, and an
-  injected-source region-escape — the tracked recall backlog the floor ratchets up to.
+  so the leak arm of the interprocedural-handoff case fires `OWN001`; (5) the inter-procedural
+  **consume handoff** — a call to a first-party consumer (a method whose own body disposes a
+  by-value `IDisposable` param) is modelled as a *release* of the argument at the call site (the
+  pool-`Return` shape), so a use after the handoff trips `OWN002`; the signal is the callee's
+  own body, so there is no cross-call signature table and no dangling-callee crash
+  (`ownership-handoff-use`, +1 row). Perfect precision throughout. The remaining gaps: a
+  cross-method use-after-dispose,
+  and an injected-source region-escape — the tracked recall backlog the floor ratchets up to.
   Still ahead: those, GitHub mining at scale (stage 1) and the 50–100-repo prevalence
   scan (stage 2). See
   [docs/notes/corpus-benchmark.md](../notes/corpus-benchmark.md).

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -704,10 +704,20 @@
         nodes.Add(new { op = "release", var = pbuf, line = LineOf(expr) });
         return;
     }
-    // any other reference to a tracked local -> use (once per local in this expr).
+    // Foo(s) where Foo consumes (disposes) a by-value IDisposable parameter -> the handoff
+    // RELEASES the matching argument(s) here (the inter-procedural consume contract,
+    // modelled at the call site like pool Return). A later use of an argument is then a
+    // use-after-handoff (OWN002). Do NOT return — other tracked arguments of the same call
+    // (`Consume(s, t)`) still need their `use` below; a consumed arg is excluded from it.
+    var consumed = ConsumeReleaseArgs(expr, model);
+    foreach (var c in consumed)
+        if (tracked.Contains(c))
+            nodes.Add(new { op = "release", var = c, line = LineOf(expr) });
+    // any other reference to a tracked local -> use (once per local; a consumed arg is a
+    // release above, never also a use).
     var used = new SortedSet<string>(StringComparer.Ordinal);
     foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
-        if (tracked.Contains(idn.Identifier.Text))
+        if (tracked.Contains(idn.Identifier.Text) && !consumed.Contains(idn.Identifier.Text))
             used.Add(idn.Identifier.Text);
     foreach (var u in used)
         nodes.Add(new { op = "use", var = u, line = LineOf(expr) });
@@ -783,6 +793,58 @@
     return ns is { Name: "System" } && ns.ContainingNamespace is { IsGlobalNamespace: true };
 }
 
+// The local names of arguments handed to a first-party CONSUMER at this call — a method
+// whose own body disposes the by-value IDisposable parameter the argument binds to. Such
+// an argument's ownership moves into the callee and is discharged there, so the handoff is
+// modelled as a RELEASE of the argument at the call site (the same shape as pool
+// `Return(buf)`); a later use is then a use-after-handoff (OWN002). Inspecting the callee's
+// OWN body means no cross-call signature table and no dangling-callee crash — a callee with
+// no body (interface / abstract / extern) or that does not dispose the param contributes
+// nothing, and the argument stays an ordinary escape. Arguments resolve to parameters by
+// NAME when `name:` is used, else by position; partial declarations are scanned for a body.
+static List<string> ConsumeReleaseArgs(ExpressionSyntax e, SemanticModel model)
+{
+    var consumed = new List<string>();
+    if (e is not InvocationExpressionSyntax inv
+        || model.GetSymbolInfo(inv).Symbol is not IMethodSymbol sym)
+        return consumed;
+    SyntaxNode? body = null;
+    foreach (var r in sym.DeclaringSyntaxReferences)
+        if (r.GetSyntax() is BaseMethodDeclarationSyntax d
+            && ((SyntaxNode?)d.Body ?? d.ExpressionBody) is { } b)
+        {
+            body = b;
+            break;
+        }
+    if (body is null)
+        return consumed;
+    var args = inv.ArgumentList.Arguments;
+    for (int i = 0; i < args.Count; i++)
+    {
+        // map argument -> parameter: by name for `name: value`, else by position.
+        var p = args[i].NameColon is { } nc
+            ? sym.Parameters.FirstOrDefault(q => q.Name == nc.Name.Identifier.Text)
+            : (i < sym.Parameters.Length ? sym.Parameters[i] : null);
+        if (p is { RefKind: RefKind.None } && ImplementsIDisposable(p.Type)
+            && DisposesLocal(body, p.Name)
+            && args[i].Expression is IdentifierNameSyntax aid)
+            consumed.Add(aid.Identifier.Text);
+    }
+    return consumed;
+}
+
+// Does `body` dispose the local/parameter named `name` — a `name.Dispose()` / `.Close()` /
+// `.DisposeAsync()` call (the consume signal)?
+static bool DisposesLocal(SyntaxNode body, string name)
+{
+    foreach (var i in body.DescendantNodesAndSelf().OfType<InvocationExpressionSyntax>())
+        if (i.Expression is MemberAccessExpressionSyntax m
+            && m.Name.Identifier.Text is "Dispose" or "Close" or "DisposeAsync"
+            && m.Expression is IdentifierNameSyntax id && id.Identifier.Text == name)
+            return true;
+    return false;
+}
+
 // A field/local type treated as owned-disposable (syntax-only heuristic — no
 // semantic model): a curated set plus a few suffixes. Gated on the class `new`ing
 // the value, so injected/borrowed disposables are not flagged. Timer types are
@@ -974,7 +1036,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
@@ -1343,9 +1405,21 @@
                     var nm = idn.Identifier.Text;
                     if (!candidates.Contains(nm))
                         continue;
+                    // ... unless it is handed to a CONSUMER (a first-party method that
+                    // disposes a by-value IDisposable param) as a bare `Consume(s);`
+                    // statement: that is a handoff RELEASED at the call site, not an escape
+                    // (else the use-after-handoff would be hidden). Tied to the statement
+                    // form the flow pass lowers, so a local is never exempted without a
+                    // matching release (a `var n = Consume(s)` initializer is NOT lowered
+                    // here, so it stays an escape rather than a false leak).
+                    bool consumedArg = idn.Parent is ArgumentSyntax
+                        && idn.Parent.Parent is ArgumentListSyntax
+                        && idn.Parent.Parent.Parent is InvocationExpressionSyntax cinv
+                        && cinv.Parent is ExpressionStatementSyntax
+                        && ConsumeReleaseArgs(cinv, model).Contains(nm);
                     if (idn.Parent is ReturnStatementSyntax
                         || (idn.Parent is AssignmentExpressionSyntax asg && asg.Right == idn)
-                        || (idn.Parent is ArgumentSyntax && !poolBuffers.Contains(nm)))
+                        || (idn.Parent is ArgumentSyntax && !poolBuffers.Contains(nm) && !consumedArg))
                         escapedLocals.Add(nm);
                 }
                 var tracked = new HashSet<string>(candidates);