feat(pool): MemoryPool view borrow — owner.Memory[.Span] used after Dispose → OWN002 (POOL002)

.github/workflows/ci.yml

@@ -792,10 +792,11 @@ jobs:
         # (P-007 POOL005, the over-read): the unbounded `buf.AsSpan()` AND the `.Length` view spelling
         # (`buf.AsSpan(0, buf.Length)`) — the `arraypool-fullspan-overread` / `arraypool-length-
         # overread` cases (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is not flagged).
-        # MemoryPool is now tracked too: a
-        # `MemoryPool<T>.Rent` IMemoryOwner is released by Dispose, so its leak / double-dispose /
-        # use-after-dispose ride the flow (POOL001/002/003 — the `memorypool-double-dispose` case ->
-        # OWN003). Remaining backlog: a FIELD-mediated cross-method use-after-dispose, a view stored in
+        # MemoryPool is tracked too: a `MemoryPool<T>.Rent` IMemoryOwner is released by Dispose, so its
+        # 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 16
+        run: python scripts/benchmark.py --min-recall 17
 

corpus/real-world/memorypool-view-after-dispose/after.cs

@@ -0,0 +1,17 @@
+// AFTER (fixed). A `using` declaration owns the `IMemoryOwner` lifetime: the buffer is
+// returned to the pool exactly once, at the end of the scope, AFTER the view has been
+// read. The `owner.Memory.Span` borrow is consumed while the owner is still alive, so it
+// is never read past the buffer's return. The checker is silent.
+using System;
+using System.Buffers;
+
+static class MemoryPoolViewAfterDispose
+{
+    static void Run(int n)
+    {
+        using IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n);
+        Consume(owner.Memory.Span);   // read while the owner is still alive
+    }
+
+    static void Consume(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/memorypool-view-after-dispose/before.cs

@@ -0,0 +1,25 @@
+// BEFORE (buggy). POOL002 for MemoryPool: an `IMemoryOwner<T>` from `MemoryPool<T>`
+// exposes its pooled buffer as a `Memory<T>` via `owner.Memory`. That Memory (and the
+// `Span` taken from it) is a BORROW of the owner — it is only valid while the owner is
+// alive. Reading the view AFTER `owner.Dispose()` (which returns the memory to the pool)
+// reads memory that may already have been handed to another renter: a use-after-free.
+// The fix is to read the view BEFORE disposing — or let a `using` own the lifetime
+// (see after.cs). The MemoryPool twin of `arraypool-span-view-after-return`.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it; the helper is
+// stubbed so the reduction is self-contained.
+using System;
+using System.Buffers;
+
+static class MemoryPoolViewAfterDispose
+{
+    static void Run(int n)
+    {
+        IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n);
+        Memory<byte> view = owner.Memory;   // a borrow of the owner's pooled buffer
+        owner.Dispose();                    // returns the memory to the pool ...
+        Consume(view.Span);                 // <-- BUG: ... but the view is read AFTER (use-after-free)
+    }
+
+    static void Consume(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/memorypool-view-after-dispose/case.own

@@ -0,0 +1,16 @@
+// OwnLang model of the MemoryPool view-after-dispose. `acquire` == MemoryPool.Rent,
+// `release` == owner.Dispose(). A `Memory<T>` view (`owner.Memory`, and the `Span` from
+// it) is a BORROW of the owner — the extractor lowers a use of the view to a use of the
+// OWNER, so reading it after Dispose is the generic use-after-release (OWN002), the same
+// code reading the owner directly would give. The borrow is resolved to its owner in the
+// extractor; the core sees a plain use-after-release.
+module Corpus
+resource MemoryOwner {
+  acquire Rent
+  release Dispose
+}
+fn run(n: int) {
+  let owner = acquire MemoryOwner(n);   // MemoryPool.Rent
+  release owner;                        // owner.Dispose()  <-- too early
+  use owner;                            // read the Memory view AFTER Dispose -> OWN002
+}

corpus/real-world/memorypool-view-after-dispose/expected-diagnostics.txt

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

corpus/real-world/memorypool-view-after-dispose/notes.md

@@ -0,0 +1,33 @@
+# MemoryPool view used after dispose (POOL002, the Dispose-released pool)
+
+**Pattern:** `MemoryPool<T>.Shared.Rent(n)` returns an `IMemoryOwner<T>` whose pooled
+buffer is exposed as a `Memory<T>` via `owner.Memory` (and a `Span<T>` via
+`owner.Memory.Span`). That view is a **borrow** of the owner — valid only while the
+owner is alive. Reading it after `owner.Dispose()` (which returns the memory to the
+pool) reads memory that may already belong to another renter: a use-after-free. The
+fix is to read the view *before* disposing, or to let a `using` own the lifetime.
+
+This is the MemoryPool twin of `arraypool-span-view-after-return`: there a `Span`
+view of a `Rent`ed array is used after `Return`; here a `Memory`/`Span` view of an
+`IMemoryOwner` is used after `Dispose`. Both lower the view to a use of the **owner**
+(`ViewOwner` in the extractor), so the core sees a plain use-after-release.
+
+**What it adds:** the extractor now recognises `owner.Memory` / `owner.Memory.Span`
+(resolved via the `System.Buffers.IMemoryOwner<T>.Memory` property) as a borrow of the
+owner — completing the MemoryPool story begun in #72 (which tracked the owner's
+acquire / release lifecycle: POOL001 leak, POOL003 double-dispose). With the view
+recognised, a view-local read after an explicit `owner.Dispose()` is
+**POOL002 → OWN002**. (The *returned*-`Memory` dangle from the idiomatic `using`
+owner — `using owner; return owner.Memory;`, where the implicit scope-exit dispose
+hands a stale view to the caller — is a follow-up: `using` locals are skipped as
+non-leak candidates, so that escape needs the scope-exit dispose modelled as a
+release on the return path, like the ArrayPool try/finally `Memory` escape.)
+
+**What the checker says:** the OwnLang model and the real `before.cs` both trip
+**OWN002** (use after release). The `using` fix in `after.cs` reads the view while the
+owner is alive and is silent.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction (not C# ingested by the
+checker); `before.cs` / `after.cs` are representative of the bug and its fix.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md).

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

@@ -19,9 +19,10 @@
   read-capable VIEW is the over-read. **POOL003 (double-return → OWN003) is built** for ArrayPool
   (try/finally + aliased-receiver, corpus `arraypool-double-return` / `arraypool-aliased-receiver`),
   and **MemoryPool is now tracked** — a `MemoryPool<T>.Rent` `IMemoryOwner` is released by Dispose,
-  so its leak / double-dispose / use-after-dispose ride the same flow as POOL001/002/003 (corpus
-  `memorypool-double-dispose` → OWN003). A POOL005 view stored in a FIELD, and the
-  `IMemoryOwner.Memory.Span` view borrow, are next
+  so its leak / double-dispose ride the same flow as POOL001/003 (corpus `memorypool-double-dispose`
+  → OWN003), and its `owner.Memory` / `owner.Memory.Span` is a borrow lowered to a use of the OWNER
+  (`ViewOwner`), so reading the view after `Dispose` trips **POOL002 → OWN002** (corpus
+  `memorypool-view-after-dispose`). A POOL005 view stored in a FIELD is 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

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -900,8 +900,9 @@
     && IsMemoryPoolType(sym.ContainingType);
 
 // The owner buffer a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW expression borrows from:
-// `owner.AsSpan(...)` / `owner.AsMemory(...)`, or `new Span<T>(owner, …)` / `new Memory<T>(owner)`
-// (and the ReadOnly* forms), where the source is a local identifier. Returns the owner local name,
+// `owner.AsSpan(...)` / `owner.AsMemory(...)`, `new Span<T>(owner, …)` / `new Memory<T>(owner)`
+// (and the ReadOnly* forms), or `owner.Memory` / `owner.Memory.Span` of a `System.Buffers.
+// IMemoryOwner<T>` (a MemoryPool rental), where the source is a local identifier. Returns the owner local name,
 // else null. The BORROW is recognised by the RESOLVED BCL symbols — `System.MemoryExtensions`
 // `AsSpan`/`AsMemory` (which alias the receiver array) and the `System.Span<T>` / `ReadOnlySpan<T>`
 // / `Memory<T>` / `ReadOnlyMemory<T>` constructor (which wraps the array argument) — NOT by name, so
@@ -926,6 +927,23 @@
             { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct }
         && IsInNamespace(sct, "System"))
         return arg.Identifier.Text;
+    // owner.Memory — a Memory<T> view of a System.Buffers.IMemoryOwner<T> (e.g. a MemoryPool rental).
+    // Like array.AsMemory(), the Memory CAN escape (return / field); a use of the view after the
+    // owner's Dispose is a use of the owner after release (OWN002), and a returned Memory after
+    // Dispose is a dangling borrow. Recognised by the resolved `IMemoryOwner<T>.Memory` property.
+    if (e is MemberAccessExpressionSyntax mem
+        && mem.Name.Identifier.Text == "Memory"
+        && mem.Expression is IdentifierNameSyntax mo
+        && model.GetSymbolInfo(mem).Symbol is IPropertySymbol { ContainingType: { Name: "IMemoryOwner" } ict }
+        && IsInNamespace(ict, "System", "Buffers"))
+        return mo.Identifier.Text;
+    // owner.Memory.Span — the Span<T> of that Memory view (a ref-struct borrow that cannot escape).
+    if (e is MemberAccessExpressionSyntax { Name.Identifier.Text: "Span" } spanAcc
+        && spanAcc.Expression is MemberAccessExpressionSyntax
+            { Name.Identifier.Text: "Memory", Expression: IdentifierNameSyntax mo2 } innerMem
+        && model.GetSymbolInfo(innerMem).Symbol is IPropertySymbol { ContainingType: { Name: "IMemoryOwner" } ict2 }
+        && IsInNamespace(ict2, "System", "Buffers"))
+        return mo2.Identifier.Text;
     return null;
 }
 
@@ -1583,7 +1601,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