feat(extractor): resolve pool Rent/Return via SemanticModel → aliased receivers (recall 6/9→7/10)

.github/workflows/ci.yml

@@ -625,10 +625,12 @@ 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 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
+        # improves. Now 7/10 — pooled buffers ride the path-sensitive flow engine
+        # (Rent = acquire, Return = release: OWN003/OWN002), and pool recognition is
+        # now resolved through the Roslyn SemanticModel, so a double-return reached via
+        # an ALIASED pool receiver (`var p = ArrayPool<int>.Shared; p.Return(buf)`) — a
+        # miss for the old text heuristic — is caught. 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 7
 

corpus/real-world/arraypool-aliased-receiver/after.cs

@@ -0,0 +1,22 @@
+// AFTER (fixed): return exactly once, in finally — through the same aliased receiver.
+// (Wrapped in a class so the extractor's per-class flow pass visits it; Work stubbed.)
+using System.Buffers;
+
+static class PoolAliasedReceiver
+{
+    static void Use(int n)
+    {
+        ArrayPool<int> p = ArrayPool<int>.Shared;
+        int[] rented = p.Rent(n);
+        try
+        {
+            Work(rented);
+        }
+        finally
+        {
+            p.Return(rented);   // returned exactly once
+        }
+    }
+
+    static void Work(int[] buffer) { }
+}

corpus/real-world/arraypool-aliased-receiver/before.cs

@@ -0,0 +1,34 @@
+// BEFORE (buggy). The same double-return bug as arraypool-double-return, but the pool
+// is reached through an ALIASED receiver: `ArrayPool<int> p = ArrayPool<int>.Shared;`
+// then `p.Rent(...)` / `p.Return(...)`. Caching the pool in a local (or a field) rather
+// than repeating `ArrayPool<int>.Shared` at every call site is common real C#.
+//
+// This case is the proof for semantic-model pool recognition. A purely TEXTUAL detector
+// keyed on the receiver spelling ("Pool"/"pool") cannot see `p.Rent` — the receiver `p`
+// carries no "Pool" — so the buffer was invisible and this double-return was MISSED.
+// Binding the call to System.Buffers.ArrayPool<T> via the Roslyn SemanticModel resolves
+// the pool no matter how the receiver is spelled; the path-sensitive flow engine then
+// flags the double release (OWN003).
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it; Work stubbed.
+using System.Buffers;
+
+static class PoolAliasedReceiver
+{
+    static void Use(int n)
+    {
+        ArrayPool<int> p = ArrayPool<int>.Shared;   // the pool, via an aliased receiver
+        int[] rented = p.Rent(n);
+        try
+        {
+            Work(rented);
+            p.Return(rented);   // returned here ...
+        }
+        finally
+        {
+            p.Return(rented);   // <-- ... and again here (double) -> OWN003
+        }
+    }
+
+    static void Work(int[] buffer) { }
+}

corpus/real-world/arraypool-aliased-receiver/case.own

@@ -0,0 +1,17 @@
+// OwnLang model: the same buffer returned twice is a double `release` -> OWN003. The C#
+// reduction reaches the pool through an aliased receiver (`ArrayPool<int> p = ArrayPool<
+// int>.Shared`), which the extractor binds via the SemanticModel; the ownership logic is
+// identical to arraypool-double-return.
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  emit_type    "int[]"
+  emit_acquire "p.Rent({args})"
+  emit_release "p.Return({0})"
+}
+fn run(n: int) {
+  let rented = acquire Buffer(n);   // p.Rent
+  release rented;                   // p.Return
+  release rented;                   // returned again -> OWN003
+}

corpus/real-world/arraypool-aliased-receiver/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN003

corpus/real-world/arraypool-aliased-receiver/notes.md

@@ -0,0 +1,24 @@
+# ArrayPool double-return through an aliased receiver
+
+**Pattern:** the same rented array is returned to the pool twice (a `Return` on the
+normal path plus another in `finally`), exactly like `arraypool-double-return` — but the
+pool is reached through an **aliased receiver**: `ArrayPool<int> p = ArrayPool<int>.Shared;`
+then `p.Rent(...)` / `p.Return(...)`. Caching the pool in a local or field is common real
+C#; the bug is the double `Return`, which corrupts the pool (the array can be handed to
+two renters at once). See dotnet/runtime#33767.
+
+**What the checker says:** the OwnLang model trips **OWN003** (double release).
+
+**Why this case exists (the semantic-model proof).** A purely *textual* pool detector
+keyed on the receiver spelling (`Contains("Pool")`) cannot recognise `p.Rent`/`p.Return` —
+the receiver `p` carries no "Pool" — so this buffer was invisible and the double-return was
+**MISSED**. Binding the call to `System.Buffers.ArrayPool<T>` via the Roslyn SemanticModel
+resolves the pool regardless of how the receiver is spelled, and the path-sensitive flow
+engine then flags the double release. This fixture both proves and pins that upgrade — it
+is a miss under the old text heuristic and a catch (OWN003) under the semantic one.
+
+**Honesty / scope.** As with the other cases, `case.own` is a faithful hand reduction of
+the pattern (not C# ingested by the checker); `before.cs` / `after.cs` are representative
+of the bug and its fix, not a verbatim PR diff.
+
+Reference: https://github.com/dotnet/runtime/issues/33767

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 → 6/9 (two ratchets)
+## Ratchet → 7/10 (three ratchets)
 
 ### → 4/9: a fixture was understating us
 
@@ -59,6 +59,22 @@ a *use*. The core's CFG analysis then flags the double-release and the use-after
 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.**
 
+### → 7/10: pool recognition goes semantic
+
+The pool pass recognised a `Rent`/`Return` by the **text** of the receiver — `Contains("Pool")` —
+which is structurally blind to an *aliased* receiver: `ArrayPool<int> p = ArrayPool<int>.Shared;
+p.Rent(...); p.Return(buf);` spells the receiver `p`, with no "Pool" in it, so the buffer was
+invisible and a double-return through it was a **miss** (the symmetric hazard is a false match on
+an unrelated `_connectionPool.Rent()`). Both are gone now that `IsPoolRent` / `PoolReturnBuffer`
+bind the call through the **Roslyn SemanticModel** to `System.Buffers.ArrayPool<T>` — the receiver
+may be spelled any way. That one definition is shared by the syntactic `POOL001` pass and the flow
+engine (no divergence between the two), and it is ArrayPool-specific on purpose: `MemoryPool<T>.Rent`
+hands back an `IMemoryOwner<T>` released by `Dispose`, so there is no `Return` to model. A new
+fixture — `arraypool-aliased-receiver`, a double-return reached through `var p = ArrayPool<int>.Shared`
+— is a *miss* under the old text heuristic and a *catch* (`OWN003`) under the semantic one. The
+heuristic's failure mode was recall-leaning (a missed alias is a missed catch, never a false alarm),
+so the upgrade only adds — precision stays absolute. **Recall is now 7/10.**
+
 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.

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

@@ -6,12 +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**, ratcheted to **6/9** over two steps: (1) a *fixture*
+  caught · 9/9 clean · 0 FP**, ratcheted to **7/10** over three 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
+  (`OWN002`) are caught *soundly* (not "count Returns", which FPs); (3) pool
+  recognition moved off the receiver-text heuristic onto the **Roslyn SemanticModel**
+  (binding `System.Buffers.ArrayPool<T>`), so a double-return through an *aliased* pool
+  receiver (`var p = ArrayPool<int>.Shared; p.Return(buf)`) — a miss for the text
+  heuristic — is caught (`arraypool-aliased-receiver`, +1 row). 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