feat(extractor): pooled buffers through the flow engine → OWN003/OWN002 (recall 4/9→6/9)

.github/workflows/ci.yml

@@ -625,10 +625,10 @@ 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
- # (and the corpus fixtures) improve. Now 4/9 — the loaded-subscription case
- # was understated (its reduction referenced an undeclared VM type -> OWN050,
- # not a verdict); with a self-contained fixture our subscription detection
- # catches it. pool/dispose/handoff shapes are the remaining backlog. Raise
- # the floor whenever recall improves — a drop below it is a regression.
- run: python scripts/benchmark.py --min-recall 4
+ # improves. Now 6/9 — pooled buffers are routed through the path-sensitive
+ # flow engine (Rent = acquire, Return = release), so double-return (OWN003)
+ # and use-after-return (OWN002) join the already-caught subscription/region
+ # class. Remaining backlog: interprocedural handoff, cross-method
+ # use-after-dispose, a region-escape shape. A drop below the floor is a regression.
+ run: python scripts/benchmark.py --min-recall 6
 

corpus/real-world/arraypool-double-return/after.cs

@@ -1,15 +1,21 @@
-// AFTER (fixed): return exactly once, in finally.
+// AFTER (fixed): return exactly once, in finally. (Wrapped in a class so the
+// extractor's per-class flow pass visits it; helper stubbed for self-containment.)
 using System.Buffers;
 
-static void Use(int n)
+static class PoolDoubleReturn
 {
- int[] rented = ArrayPool<int>.Shared.Rent(n);
- try
+ static void Use(int n)
  {
- Work(rented);
- }
- finally
- {
- ArrayPool<int>.Shared.Return(rented);
+ int[] rented = ArrayPool<int>.Shared.Rent(n);
+ try
+ {
+ Work(rented);
+ }
+ finally
+ {
+ ArrayPool<int>.Shared.Return(rented);
+ }
  }
+
+ static void Work(int[] buffer) { }
 }

corpus/real-world/arraypool-double-return/before.cs

@@ -2,18 +2,27 @@
 // arrays to ArrayPool": the same rented array is returned twice (here a Return
 // on the success path AND a Return in finally). A double-return corrupts the
 // pool — the array can later be rented out to two callers at once.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it (a
+// file-scope method parses as a top-level local function, which the pass does not
+// walk); the helper is stubbed so the reduction is self-contained.
 using System.Buffers;
 
-static void Use(int n)
+static class PoolDoubleReturn
 {
- int[] rented = ArrayPool<int>.Shared.Rent(n);
- try
+ static void Use(int n)
  {
- Work(rented);
- ArrayPool<int>.Shared.Return(rented); // returned here ...
- }
- finally
- {
- ArrayPool<int>.Shared.Return(rented); // <-- ... and again here (double)
+ int[] rented = ArrayPool<int>.Shared.Rent(n);
+ try
+ {
+ Work(rented);
+ ArrayPool<int>.Shared.Return(rented); // returned here ...
+ }
+ finally
+ {
+ ArrayPool<int>.Shared.Return(rented); // <-- ... and again here (double)
+ }
  }
+
+ static void Work(int[] buffer) { }
 }

corpus/real-world/arraypool-use-after-return/after.cs

@@ -1,11 +1,21 @@
-// AFTER (fixed): consume the buffer BEFORE returning it to the pool.
+// AFTER (fixed): consume the buffer BEFORE returning it to the pool. (Wrapped in
+// a class so the extractor's per-class flow pass visits it; helpers stubbed.)
 using System.Buffers;
 
-static int[] Divide(int dividend, int divisor)
+static class PoolUseAfterReturn
 {
- int[] quotient = ArrayPool<int>.Shared.Rent(Size(dividend));
- Compute(quotient, dividend, divisor);
- int[] result = BuildResult(quotient); // consume first ...
- ArrayPool<int>.Shared.Return(quotient); // ... then return
- return result;
+ static int[] Divide(int dividend, int divisor)
+ {
+ int[] quotient = ArrayPool<int>.Shared.Rent(Size(dividend));
+ Compute(quotient, dividend, divisor);
+ int[] result = BuildResult(quotient); // consume first ...
+ ArrayPool<int>.Shared.Return(quotient); // ... then return
+ return result;
+ }
+
+ static int Size(int n) => n;
+ static void Compute(int[] buffer, int a, int b) { }
+ // Materialize a DISTINCT result (a copy) so it does not alias the pooled buffer:
+ // the fix must hand back its own array, never the array it returns to the pool.
+ static int[] BuildResult(int[] buffer) => (int[])buffer.Clone();
 }

corpus/real-world/arraypool-use-after-return/before.cs

@@ -3,12 +3,24 @@
 // path): a rented buffer is returned to the pool, then a slice of it is still
 // read while building the result. Representative of the pattern, not verbatim
 // from one PR.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it; helpers
+// stubbed so the reduction is self-contained.
 using System.Buffers;
 
-static int[] Divide(int dividend, int divisor)
+static class PoolUseAfterReturn
 {
- int[] quotient = ArrayPool<int>.Shared.Rent(Size(dividend));
- Compute(quotient, dividend, divisor);
- ArrayPool<int>.Shared.Return(quotient); // <-- returned to the pool here ...
- return BuildResult(quotient); // <-- ... but still read here (UAF)
+ static int[] Divide(int dividend, int divisor)
+ {
+ int[] quotient = ArrayPool<int>.Shared.Rent(Size(dividend));
+ Compute(quotient, dividend, divisor);
+ ArrayPool<int>.Shared.Return(quotient); // <-- returned to the pool here ...
+ return BuildResult(quotient); // <-- ... but still read here (UAF)
+ }
+
+ static int Size(int n) => n;
+ static void Compute(int[] buffer, int a, int b) { }
+ // Returns a distinct copy (mirrors after.cs); the BUG here is reading `buffer`
+ // in the return *after* it was returned to the pool — a use-after-return.
+ static int[] BuildResult(int[] buffer) => (int[])buffer.Clone();
 }

docs/notes/corpus-benchmark.md

@@ -26,7 +26,9 @@ 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 → 4/9: a fixture was understating us
+## Ratchet → 6/9 (two ratchets)
+
+### → 4/9: a fixture was understating us
 
 The first thing the number bought was a *diagnosis*. `screentogif-loaded-subscription`
 is a **subscription** leak — our strongest class — yet it scored a miss. The cause
@@ -41,12 +43,27 @@ ScreenToGif repo. **Recall is now 4/9** and the floor is raised to match. (Lesso
 benchmark fixture that references an undeclared type silently degrades to `OWN050`;
 self-contained fixtures, like the samples, measure honestly.)
 
-The remaining five misses are genuine **frontend extraction gaps** — pool
-double-return (`OWN003`) and use-after-return (`OWN002`), the interprocedural
+### → 6/9: pooled buffers join the flow engine
+
+The next two misses were a real **capability** gap, not a fixture: `arraypool-double-return`
+(`OWN003`) and `arraypool-use-after-return` (`OWN002`). The extractor's pool pass was
+purely syntactic — *"was this buffer `Return`ed anywhere?"* — so it only ever produced
+`POOL001` (rent-without-return); a second `Return` or a read after `Return` was invisible.
+Counting `Return`s would be unsound (it false-positives on `if (x) Return(b); else Return(b);`),
+and **precision is sacred** here. So instead pooled buffers are now **routed through the
+path-sensitive flow engine** that already proves `OWN002`/`OWN003` for IDisposable locals:
+a `*Pool.Rent(...)` local is an *acquire*, `*Pool.Return(buf)` is a *release* (the buffer is
+the argument, not the receiver), and a read of the buffer — including in a `return` value — is
+a *use*. The core's CFG analysis then flags the double-release and the use-after-release
+*soundly*, path-sensitive. Pooled buffers deliberately do **not** escape on arg-passing (the
+ArrayPool convention is the renter returns), and the syntactic `POOL001` is suppressed under
+`--flow-locals` so there is no double-report. **Recall is now 6/9.**
+
+The remaining three misses are genuine **frontend extraction gaps** — the interprocedural
 ownership-handoff (`OWN001`+`OWN002`), a field/cross-method use-after-dispose, and a
-region-escape shape — the `.own` reductions all catch them, the C# extractor does not
-yet. That is the itemized recall backlog; each is a real capability the floor will
-ratchet up to as it lands.
+region-escape shape — the `.own` reductions all catch them, the C# extractor does not yet.
+That is the itemized recall backlog; 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,15 +6,16 @@
  (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**, already ratcheted to **4/9**: the
- `screentogif-loaded-subscription` miss was a *fixture* understating us (its
- reduction referenced an undeclared VM type → `OWN050`, not a verdict); a
- self-contained fixture lets our subscription detection catch it. Perfect precision
- throughout. The remaining 5 misses are genuine frontend extraction gaps
- (pool double-return/use-after-return, interprocedural handoff, a cross-method
- use-after-dispose, a region-escape shape) — the tracked recall backlog the floor
- ratchets up to. Still ahead: more case-by-case recall, GitHub mining at scale
- (stage 1) and the 50–100-repo prevalence scan (stage 2). See
+ caught · 9/9 clean · 0 FP**, ratcheted to **6/9** over two 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 =
+ acquire, Return = release), so double-return (`OWN003`) and use-after-return
+ (`OWN002`) are caught *soundly* (not "count Returns", which FPs). Perfect precision
+ throughout. The remaining 3 misses are genuine frontend extraction gaps
+ (interprocedural handoff, a cross-method use-after-dispose, a region-escape shape)
+ — 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).
 - **Depends on:** P-001 (C# → OwnIR extractor — the scanner that does stage 2);
  the existing `corpus/` layout (`before.cs`, `after.cs`,

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -440,8 +440,9 @@
  if (ld.UsingKeyword == default)
  foreach (var v in ld.Declaration.Variables)
  if (tracked.Contains(v.Identifier.Text)
- && v.Initializer?.Value is ObjectCreationExpressionSyntax
- or ImplicitObjectCreationExpressionSyntax)
+ && (v.Initializer?.Value is ObjectCreationExpressionSyntax
+ or ImplicitObjectCreationExpressionSyntax
+ || IsPoolRent(v.Initializer?.Value))) // ArrayPool/MemoryPool Rent
  nodes.Add(new { op = "acquire", var = v.Identifier.Text, line = LineOf(v) });
  return true;
  case ExpressionStatementSyntax es:
@@ -464,10 +465,15 @@
  // lower the body so a tracked plain local used inside is seen.
  return us.Statement is null || LowerFlowStmt(us.Statement, tracked, nodes, canEscape, onThrow, onReturn);
  case ReturnStatementSyntax rs:
- // a tracked local never escapes (excluded), so a returned value is not a tracked
- // resource. A `return` first runs any enclosing `finally`(s) — threaded as
- // `onReturn`, so a resource the finally disposes is released on the return path —
- // then exits; outside a try it is a bare CFG exit edge.
+ // A tracked local READ in the return value is a use at the return point —
+ // e.g. `return BuildResult(buf)` after `pool.Return(buf)` is a use-after-
+ // return. A tracked local *itself* returned is excluded upstream as an
+ // escape, so lowering the return expression only adds uses, never a
+ // spurious escape. Then: a `return` first runs any enclosing `finally`(s)
+ // — threaded as `onReturn`, so a resource the finally releases is released
+ // on the return path — then exits; outside a try it is a bare CFG exit.
+ if (rs.Expression is { } rexpr)
+ EmitFlowExpr(rexpr, tracked, nodes);
  if (onReturn is not null)
  nodes.AddRange(onReturn);
  else
@@ -689,6 +695,14 @@
  nodes.Add(new { op = "release", var = cid.Identifier.Text, line = LineOf(cond) });
  return;
  }
+ // XPool.Return(buf) on a tracked pooled buffer -> release. The buffer is the
+ // ARGUMENT (the pool is the receiver), unlike Dispose where the local is the
+ // receiver; `return` early so the argument is not also counted as a use.
+ if (PoolReturnBuffer(expr) is { } pbuf && tracked.Contains(pbuf))
+ {
+ 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).
  var used = new SortedSet<string>(StringComparer.Ordinal);
  foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
@@ -706,6 +720,26 @@
  _ => null,
 };
 
+// An ArrayPool/MemoryPool `Rent(...)` call — the acquire of a pooled buffer. The
+// receiver carries "Pool" (`ArrayPool<T>.Shared`, `MemoryPool<T>.Shared`, `_pool`).
+static bool IsPoolRent(ExpressionSyntax? e) =>
+ e is InvocationExpressionSyntax i
+ && i.Expression is MemberAccessExpressionSyntax m
+ && m.Name.Identifier.Text == "Rent"
+ && (m.Expression.ToString().Contains("Pool") || m.Expression.ToString().Contains("pool"));
+
+// An ArrayPool/MemoryPool `Return(buf)` call — the RELEASE of the pooled buffer
+// `buf`. Unlike Dispose (where the tracked local is the receiver), the buffer is
+// the first ARGUMENT and the pool is the receiver. Returns the buffer name or null.
+static string? PoolReturnBuffer(ExpressionSyntax e) =>
+ e is InvocationExpressionSyntax i
+ && i.Expression is MemberAccessExpressionSyntax m
+ && m.Name.Identifier.Text == "Return"
+ && (m.Expression.ToString().Contains("Pool") || m.Expression.ToString().Contains("pool"))
+ && i.ArgumentList.Arguments.Count > 0
+ && i.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax buf
+ ? buf.Identifier.Text : null;
+
 // 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
@@ -897,7 +931,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
@@ -1120,7 +1154,12 @@
 
  // POOL001: an ArrayPool/MemoryPool buffer `Rent`ed but never `Return`ed,
  // matched per member so a `buf` returned in one method does not mask a
- // leak of a same-named `buf` in another.
+ // leak of a same-named `buf` in another. Under --flow-locals the
+ // path-sensitive flow detector supersedes this for buffers held in LOCALS
+ // (and additionally catches double-return / use-after-return) — but it only
+ // tracks local declarations, so field/assignment-backed rents still need
+ // this syntactic pass; the local-declaration rents are skipped below to
+ // avoid double-reporting them (Codex).
  foreach (var member in cls.Members)
  {
  var rented = new List<(string Name, int Line)>();
@@ -1132,8 +1171,12 @@
  {
  string? name = inv.Parent switch
  {
+ // a local-declaration rent is the flow pass's job under
+ // --flow-locals; skip it here so it is not double-reported.
  EqualsValueClauseSyntax { Parent: VariableDeclaratorSyntax vd }
- => vd.Identifier.Text,
+ => flowLocals ? null : vd.Identifier.Text,
+ // a field/assignment rent (`_buf = pool.Rent(...)`) is NOT a
+ // flow candidate, so this pass keeps it in both modes.
  AssignmentExpressionSyntax asg => FieldName(asg.Left),
  _ => null,
  };
@@ -1224,6 +1267,7 @@
  if (method.Body is not { } mbody)
  continue;
  var candidates = new HashSet<string>();
+ var poolBuffers = new HashSet<string>(); // candidates that are ArrayPool/MemoryPool buffers
  foreach (var ld in mbody.DescendantNodes().OfType<LocalDeclarationStatementSyntax>())
  {
  if (ld.UsingKeyword != default)
@@ -1234,17 +1278,31 @@
  && model.GetTypeInfo(init.Value).Type is { } dt
  && ImplementsIDisposable(dt) && !IsDisposeOptional(dt))
  candidates.Add(v.Identifier.Text);
+ else if (IsPoolRent(v.Initializer?.Value)) // an ArrayPool/MemoryPool buffer
+ {
+ candidates.Add(v.Identifier.Text);
+ poolBuffers.Add(v.Identifier.Text);
+ }
  }
  if (candidates.Count == 0)
  continue;
- // a local that escapes (returned / passed as arg / assigned out) is
- // conservatively not tracked — its disposal may be the callee's job.
+ // A local that escapes (returned / assigned out) is conservatively not
+ // tracked — its release may be the caller's job. For an IDisposable,
+ // passing it as an argument is an ambiguous ownership transfer too; for
+ // a pooled buffer the convention is the RENTER returns it, so arg-passing
+ // is a borrow (a use), not an escape — else `pool.Return(buf)` and
+ // `Work(buf)` would untrack it and hide the double-return / use-after-return.
  var escapedLocals = new HashSet<string>();
  foreach (var idn in mbody.DescendantNodes().OfType<IdentifierNameSyntax>())
- if (candidates.Contains(idn.Identifier.Text)
- && (idn.Parent is ReturnStatementSyntax or ArgumentSyntax
- || (idn.Parent is AssignmentExpressionSyntax asg && asg.Right == idn)))
- escapedLocals.Add(idn.Identifier.Text);
+ {
+ var nm = idn.Identifier.Text;
+ if (!candidates.Contains(nm))
+ continue;
+ if (idn.Parent is ReturnStatementSyntax
+ || (idn.Parent is AssignmentExpressionSyntax asg && asg.Right == idn)
+ || (idn.Parent is ArgumentSyntax && !poolBuffers.Contains(nm)))
+ escapedLocals.Add(nm);
+ }
  var tracked = new HashSet<string>(candidates);
  tracked.ExceptWith(escapedLocals);
  if (tracked.Count == 0)