feat(extractor): borrow checker — Memory<T> view that escapes after Return → OWN002 (POOL004)

.github/workflows/ci.yml

@@ -784,11 +784,12 @@ jobs:
         # directly OR by forwarding it to another first-party consumer (the TRANSITIVE chain,
         # `ConsumesParam`) — is a handoff that releases the argument at the call site, so a use
         # after the handoff trips OWN002 (the cut is the signature, like Rust's move). The BORROW
-        # checker has its first bite: a `Span`/`ReadOnlySpan` view of a pooled buffer
-        # (`buf.AsSpan()`) is a ref-struct borrow lowered to a use of the OWNER, so writing through
-        # the view after `Return(buf)` trips OWN002 (`ViewOwnerOf`). Remaining backlog: a
-        # FIELD-mediated cross-method use-after-dispose (dispose in one method, use in another via
-        # shared state), `Memory<T>`/escaping views, and an injected-source region-escape. A drop
-        # below the floor is a regression.
-        run: python scripts/benchmark.py --min-recall 12
+        # checker covers both view kinds: a `Span`/`Memory` view of a pooled buffer (`buf.AsSpan()` /
+        # `buf.AsMemory()`) is a borrow lowered to a use of the OWNER (`ViewOwner`), so using it
+        # after `Return(buf)` trips OWN002 — including RETURNING a `Memory<T>` view (which, unlike a
+        # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. Remaining
+        # backlog: a FIELD-mediated cross-method use-after-dispose (dispose in one method, use in
+        # another via shared state), 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 13
 

corpus/real-world/README.md

@@ -44,5 +44,6 @@ exception-path (анализ не моделирует исключения), co
 | `arraypool-use-after-return` | OWN002 | rented-буфер вернули в пул, потом ещё читали slice |
 | `arraypool-double-return` | OWN003 | один и тот же массив вернули в ArrayPool дважды ([#33767](https://github.com/dotnet/runtime/issues/33767)) |
 | `arraypool-span-view-after-return` | OWN002 | `Span`-вью пула (`buf.AsSpan()`) записали ПОСЛЕ `Return` — заём пережил владельца (borrow-checker) |
+| `arraypool-memory-view-escape` | OWN002 | `Memory`-вью пула вернули наружу (escape) ПОСЛЕ `Return` — dangling-заём ушёл вызывающему (POOL004) |
 | `ownership-handoff-use` | OWN002 | поток отдали потребителю (он его закрыл), потом ещё читали — use-after-handoff |
 | `ownership-handoff-use-transitive` | OWN002 | то же, но потребитель не закрывает сам, а **пробрасывает** владение дальше (transitive consume) |

corpus/real-world/arraypool-memory-view-escape/after.cs

@@ -0,0 +1,21 @@
+// FIX: copy the data OUT of the pooled buffer and return the COPY — no view of the recycled buffer
+// escapes. Same try/finally cleanup, but nothing borrowed leaves the method, so it stays SILENT
+// (the no-false-positive arm).
+using System;
+using System.Buffers;
+
+static class PoolMemoryViewEscape
+{
+    static byte[] Render(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        try
+        {
+            return buf.AsSpan(0, n).ToArray();          // copy OUT -> a fresh array escapes, not a view
+        }
+        finally
+        {
+            ArrayPool<byte>.Shared.Return(buf);
+        }
+    }
+}

corpus/real-world/arraypool-memory-view-escape/before.cs

@@ -0,0 +1,28 @@
+// A Memory<T> VIEW of a pooled buffer ESCAPES the method — returned from inside a `try` whose
+// `finally` returns the buffer to the pool (THE idiomatic ArrayPool cleanup). The `return view`
+// expression is evaluated before the finally runs, but the caller receives the `Memory<byte>` only
+// AFTER the finally has recycled the buffer — so the caller then reads/writes memory the pool has
+// already handed to someone else (a silent cross-tenant corruption). Unlike a `Span` (a ref struct
+// the compiler keeps inside the method), a `Memory<T>` CAN leave the method, so the borrow outlives
+// its owner: a dangling escape past the finally.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it.
+using System;
+using System.Buffers;
+
+static class PoolMemoryViewEscape
+{
+    static Memory<byte> Render(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        try
+        {
+            Memory<byte> view = buf.AsMemory(0, n);     // view BORROWS buf
+            return view;                                // escapes -> caller gets it AFTER the finally
+        }
+        finally
+        {
+            ArrayPool<byte>.Shared.Return(buf);         // buf recycled here -> returned view dangles (OWN002)
+        }
+    }
+}

corpus/real-world/arraypool-memory-view-escape/case.own

@@ -0,0 +1,16 @@
+// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return (run by the `finally`).
+// The C# returns a Memory<byte> VIEW of the buffer from inside a `try` whose `finally` returns the
+// buffer to the pool. A Memory<T> — unlike a ref-struct Span — can leave the method, so the caller
+// receives the view AFTER the finally recycled the buffer: a dangling escape. The extractor models
+// the escaped view's use AFTER the finally release, so it reduces to a plain use-after-return
+// (OWN002), the same code reading the buffer directly after return would give.
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+}
+fn render(n: int) {
+  let buf = acquire Buffer(n);   // ArrayPool.Rent
+  release buf;                   // ArrayPool.Return  <-- the finally, before the caller sees the view
+  use buf;                       // the escaped Memory view, used by the caller AFTER the finally -> OWN002
+}

corpus/real-world/arraypool-memory-view-escape/expected-diagnostics.txt

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

corpus/real-world/arraypool-memory-view-escape/notes.md

@@ -0,0 +1,41 @@
+# Pooled-buffer `Memory<T>` view that ESCAPES after return — the borrow checker, second bite
+
+**Pattern:** a rented `ArrayPool<T>` buffer is sliced into a `Memory<T>` local
+(`Memory<byte> view = buf.AsMemory(0, n)`) and **returned from inside a `try` whose `finally`
+returns the buffer to the pool** — *the* idiomatic ArrayPool cleanup. The `return view` is evaluated
+before the finally, but the caller receives the `Memory<byte>` only **after** the finally has
+recycled the array, so the borrow **escapes** its owner: the caller holds a view into an array the
+pool has already handed to someone else — a silent cross-tenant corruption (read/write of
+freed-and-reused memory).
+
+**What the checker says:** the view's escape (the `return`) is a use of the owner after it was
+released → the generic **OWN002** (use-after-release), surfaced at the escape site.
+
+**Why this case exists (P-007 POOL004 — view escape).** [`arraypool-span-view-after-return`](../arraypool-span-view-after-return)
+caught a `Span` view used after `Return` **inside** the method. But a `Span` is a **ref struct** —
+the C# compiler keeps it inside the method, so it cannot escape. A **`Memory<T>` is not a ref
+struct**: it *can* be returned or stored in a field, which is the genuinely dangerous escape the
+borrow checker must catch. The view recognition (`ViewOwner`) is now extended from `AsSpan` /
+`new Span<T>` to **`AsMemory` / `new Memory<T>`** (and the `ReadOnly*` forms), resolved via the same
+BCL symbols (`System.MemoryExtensions`, `System.Memory<T>`). Because a reference to the view lowers
+to a use of the owner — and `return view` is such a reference — the escape of a dangling view after
+`Return(buf)` trips OWN002. Before this slice the `Memory` view was unrecognised, so the dangling
+return looked balanced (acquire + release) — a **miss**.
+
+Crucially, the escaped view's use is modelled **after the `finally`**: a returned borrow is used by
+the caller *after* the method's cleanup, so the owner-use is re-emitted just before the method exits
+the `onReturn` (finally) chain. That is what catches the idiomatic
+`try { return view; } finally { Return(buf); }` — where the `return` is evaluated first but the
+caller only receives the view once the finally has recycled the buffer (a dangling escape the C#
+compiler does **not** prevent for `Memory<T>`).
+
+**Conservative (0 FP).** Only a view of a **tracked** owner that is used/returned **after** the
+owner's release fires. The fix (`after.cs`) copies out of the buffer (`AsSpan(..).ToArray()`) and
+returns the **copy**, so no view escapes — silent. A view used before the return, or a view of an
+untracked buffer, adds no finding; the borrow can never invent a release.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction (the escaping view collapses to a use
+of the owner, exactly what the extractor emits), not C# the `.own` checker ingested.
+`before.cs`/`after.cs` are representative of the bug and its fix. This slice covers the **return**
+escape; storing the view in a **field** (object-level escape) and view **reassignment** are left for
+later rounds.

docs/proposals/P-007-arraypool-span.md

@@ -1,11 +1,13 @@
 # P-007 — ArrayPool / Span borrow-view profile
 
-- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; **POOL002
-  (Span/ReadOnlySpan view used after `Return` → OWN002) first slice built** — a
-  `buf.AsSpan()` / `new Span<T>(buf)` view is a ref-struct borrow lowered to a use of the
-  owner (`ViewOwnerOf` in the extractor; corpus `arraypool-span-view-after-return`); the
-  borrow checker's first bite on real C#. POOL003–005 (double-return via flow already
-  catches OWN003, `Memory<T>`/escaping views, clear-past-length) next
+- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; **POOL002 (Span/Memory
+  view used after `Return` → OWN002) built** and **POOL004 (view ESCAPE) first slice built** — a
+  `buf.AsSpan()` / `buf.AsMemory()` / `new Span<T>(buf)` view is a borrow lowered to a use of the
+  owner (`ViewOwner` in the extractor), so using it after `Return` trips OWN002; because a
+  `Memory<T>` (unlike a ref-struct `Span`) can leave the method, RETURNING a dangling `Memory` view
+  is caught at the escape (corpus `arraypool-span-view-after-return`, `arraypool-memory-view-escape`).
+  The borrow checker on real C#. POOL003 (double-return — flow already catches OWN003), a view
+  stored in a FIELD, and POOL005 (clear-past-length) next
 - **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release,
   OWN003 double-release, OWN008 release-while-borrowed), the buffer/borrow model
   in `spec/`, [P-001](P-001-csharp-extractor.md). See