feat(extractor): borrow checker — pooled-buffer Span view used after Return → OWN002 (POOL002)

.github/workflows/ci.yml

@@ -783,9 +783,12 @@ jobs:
         # a first-party method that owns a by-value IDisposable param — by disposing it
         # 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). Remaining
-        # backlog: a FIELD-mediated cross-method use-after-dispose (dispose in one method, use in
-        # another via shared state) and an injected-source region-escape. A drop below the floor
-        # is a regression.
-        run: python scripts/benchmark.py --min-recall 11
+        # 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
 

corpus/real-world/README.md

@@ -43,5 +43,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) |
 | `ownership-handoff-use` | OWN002 | поток отдали потребителю (он его закрыл), потом ещё читали — use-after-handoff |
 | `ownership-handoff-use-transitive` | OWN002 | то же, но потребитель не закрывает сам, а **пробрасывает** владение дальше (transitive consume) |

corpus/real-world/arraypool-span-view-after-return/after.cs

@@ -0,0 +1,16 @@
+// AFTER (fixed). Finish all work through the Span view BEFORE returning the buffer to the pool, so
+// the borrow's lifetime ends before the owner is recycled and nothing aliases freed memory. Same
+// view, correct order — the case must stay SILENT (the no-false-positive arm).
+using System;
+using System.Buffers;
+
+static class PoolSpanViewAfterReturn
+{
+    static void Scramble(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Span<byte> view = buf.AsSpan(0, n);          // view BORROWS buf
+        view[0] = 42;                                // written through the view BEFORE return
+        ArrayPool<byte>.Shared.Return(buf);          // returned only after the borrow is done -> silent
+    }
+}

corpus/real-world/arraypool-span-view-after-return/before.cs

@@ -0,0 +1,22 @@
+// BEFORE (buggy). A Span VIEW of a pooled buffer is written THROUGH after the buffer was returned
+// to the pool. `buf.AsSpan(..)` borrows the buffer's memory into a `Span<byte>` local; once
+// `Return(buf)` recycles the array the pool may hand it to another caller, so writing through the
+// view now corrupts someone else's data — a silent, nasty aliasing bug. The view is a ref-struct
+// BORROW: a use of it after the owner's release is a use-after-return. Unlike
+// `arraypool-use-after-return` (the array itself is read after return), here the read goes through
+// a STORED Span view, which the flat pass misses — the borrow has to be resolved to its owner.
+//
+// Wrapped in a class so the extractor's per-class flow pass visits it.
+using System;
+using System.Buffers;
+
+static class PoolSpanViewAfterReturn
+{
+    static void Scramble(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Span<byte> view = buf.AsSpan(0, n);          // view BORROWS buf
+        ArrayPool<byte>.Shared.Return(buf);          // buf goes back to the pool (recycled) ...
+        view[0] = 42;                                // ... but written through here (use-after-return)
+    }
+}

corpus/real-world/arraypool-span-view-after-return/case.own

@@ -0,0 +1,17 @@
+// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return. The C# stores a Span
+// VIEW of the buffer in a local (`Span<byte> view = buf.AsSpan()`) and writes through it AFTER the
+// buffer was returned. A Span is a ref-struct BORROW of the buffer that cannot outlive the method,
+// so the extractor lowers a use of the view to a use of the OWNER buffer — the write after
+// `release` is the generic use-after-return (OWN002), the same code reading the buffer directly
+// would give. The borrow is resolved to its owner in the extractor; the core sees a plain
+// use-after-release.
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+}
+fn scramble(n: int) {
+  let buf = acquire Buffer(n);   // ArrayPool.Rent
+  release buf;                   // ArrayPool.Return  <-- too early
+  use buf;                       // write through the Span view AFTER return -> OWN002
+}

corpus/real-world/arraypool-span-view-after-return/expected-diagnostics.txt

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

corpus/real-world/arraypool-span-view-after-return/notes.md

@@ -0,0 +1,34 @@
+# Pooled-buffer Span VIEW used after return — the borrow checker's first bite
+
+**Pattern:** a rented `ArrayPool<T>` buffer is sliced into a `Span<T>`/`ReadOnlySpan<T>` local
+(`Span<byte> view = buf.AsSpan(0, n)`), the buffer is `Return`ed to the pool, and the code then
+reads/writes **through the view**. The `Span` borrows the buffer's memory; once the array is
+recycled the pool may hand it to another caller, so the view now aliases someone else's data — a
+silent corruption (the same family as a use-after-free). It is the use of a **borrow after its
+owner was released**.
+
+**What the checker says:** using a resource after it was released is the generic **OWN002**
+(use-after-release) — the same code `arraypool-use-after-return` produces when the buffer itself is
+read after return.
+
+**Why this case exists (the borrow / B4 frontier).** The flat pass and the existing pool flow only
+saw a use-after-return when the **buffer local itself** was referenced after `Return`. When the read
+goes through a **stored Span view** (`view[0]`), the buffer name never appears at the use site, so
+the buffer looked released-and-untouched — a **miss**. Now the extractor models a
+`Span`/`ReadOnlySpan` view of a tracked buffer as a **borrow**: a reference to the view local lowers
+to a **use of the owner** (`ViewOwnerOf` resolves the view through its declaration's `AsSpan(..)` /
+`new Span<T>(buf)` initializer, the owner confirmed via the SemanticModel). The use after `Return`
+then trips OWN002. This is the first slice of the **borrow checker on real C#** — lifetime/aliasing
+analysis that the flat "disposed anywhere?" tools (and most general scanners) do not do — kept
+purely in the extractor (the core needs no borrow concept; it sees a plain use-after-release).
+
+**Conservative (0 FP).** A view of an untracked/escaped buffer, or a view used **before** the
+return (`after.cs`), adds no finding — the borrow only lowers to a use of an owner that is still
+tracked, so it can never invent a release. Ref-struct `Span` cannot escape the method, which is
+what makes "use of the view = use of the owner, here" sound.
+
+**Honesty / scope.** `case.own` is a faithful hand reduction (the borrow 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. First slice: `Span`/`ReadOnlySpan` views via `AsSpan()` /
+`new Span<T>(buf)`; `Memory<T>` (which *can* escape) and view reassignment are deliberately left for
+later rounds.

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

@@ -1,7 +1,11 @@
 # P-007 — ArrayPool / Span borrow-view profile
 
-- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**;
-  POOL002–005 (views, escape, double-return) next
+- **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
 - **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

@@ -760,11 +760,23 @@
         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).
+    // release above, never also a use). A Span/ReadOnlySpan VIEW of a tracked buffer is a BORROW:
+    // a reference to the view is a use of the OWNER, so using it after the owner was
+    // Returned/Disposed trips OWN002 (the ref-struct view cannot outlive the method, so this is a
+    // genuine use-after-release of the owner — `Span<byte> v = buf.AsSpan(); Return(buf); v[0]=…`).
     var used = new SortedSet<string>(StringComparer.Ordinal);
     foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
-        if (tracked.Contains(idn.Identifier.Text) && !consumed.Contains(idn.Identifier.Text))
-            used.Add(idn.Identifier.Text);
+    {
+        var nm = idn.Identifier.Text;
+        if (tracked.Contains(nm))
+        {
+            if (!consumed.Contains(nm))
+                used.Add(nm);
+        }
+        else if (ViewOwnerOf(idn, model) is { } owner
+                 && tracked.Contains(owner) && !consumed.Contains(owner))
+            used.Add(owner);
+    }
     foreach (var u in used)
         nodes.Add(new { op = "use", var = u, line = LineOf(expr) });
 }
@@ -815,6 +827,47 @@
         && i.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax buf
         ? buf.Identifier.Text : null;
 
+// The owner buffer a Span/ReadOnlySpan VIEW expression borrows from: `owner.AsSpan(...)` or
+// `new Span<T>(owner, …)` / `new ReadOnlySpan<T>(owner)`, 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` (which aliases its receiver array) and the `System.Span<T>` /
+// `System.ReadOnlySpan<T>` constructor (which wraps its array argument) — NOT by name, so a
+// project's own `AsSpan` extension, a non-`System` type named `Span<T>`, or an `AsSpan` returning a
+// span over a fresh copy is not mistaken for a borrow of `owner` (Codex). A `Span` is a ref-struct
+// borrow that cannot escape the method, so a use of the view after the owner is released is a use of
+// the owner after its release.
+static string? SpanViewOwner(ExpressionSyntax? e, SemanticModel model)
+{
+    if (e is InvocationExpressionSyntax inv
+        && inv.Expression is MemberAccessExpressionSyntax m
+        && m.Name.Identifier.Text == "AsSpan"
+        && m.Expression is IdentifierNameSyntax recv
+        && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct }
+        && IsInNamespace(mct, "System"))
+        return recv.Identifier.Text;
+    if (e is ObjectCreationExpressionSyntax oc
+        && oc.ArgumentList is { Arguments.Count: > 0 }
+        && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg
+        && model.GetSymbolInfo(oc).Symbol is IMethodSymbol { ContainingType: { Name: "Span" or "ReadOnlySpan" } sct }
+        && IsInNamespace(sct, "System"))
+        return arg.Identifier.Text;
+    return null;
+}
+
+// If `idn` references a Span/ReadOnlySpan VIEW local declared from an owner buffer
+// (`Span<T> view = owner.AsSpan(…)`), the owner buffer's local name — so a use of the view lowers
+// to a use of the owner (the borrow). Resolved through the view local's own declaration, so it is
+// inert for any identifier that is not such a view (returns null -> ordinary handling).
+static string? ViewOwnerOf(IdentifierNameSyntax idn, SemanticModel model)
+{
+    if (model.GetSymbolInfo(idn).Symbol is not ILocalSymbol sym)
+        return null;
+    foreach (var r in sym.DeclaringSyntaxReferences)
+        if (r.GetSyntax() is VariableDeclaratorSyntax { Initializer.Value: { } init })
+            return SpanViewOwner(init, model);
+    return null;
+}
+
 // A factory call that CREATES and hands back a fresh owned IDisposable the caller must
 // release — recognised via the resolved symbol (curated, the same spirit as
 // IsDisposableType is for `new`). Two families:
@@ -1355,7 +1408,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