feat(pool): POOL005 — full-length view of a pooled buffer over-reads its logical length → OWN025

.github/workflows/ci.yml

@@ -787,9 +787,11 @@ jobs:
         # 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
+        # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. A
+        # FULL-length view of a pooled buffer (`buf.AsSpan()` with no length bound) reaches past the
+        # rented logical length into the oversized tail -> OWN025 (P-007 POOL005, the over-read; the
+        # `arraypool-fullspan-overread` case). 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 14
 

corpus/real-world/arraypool-fullspan-overread/after.cs

@@ -0,0 +1,22 @@
+// AFTER (fixed). Every view is BOUNDED to the logical length — `buf.AsSpan(0, n)` —
+// so only the `n` valid payload bytes are read; the oversized `[n, Length)` tail is
+// never touched. No unbounded full view remains in either spelling (expression or
+// initializer), so the extractor emits no `overspan` fact and the checker is silent.
+using System;
+using System.Buffers;
+
+static class PoolFullSpanOverread
+{
+    static byte[] Frame(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(buf, n);
+        Emit(buf.AsSpan(0, n));                    // bounded view: only the logical [0, n)
+        byte[] copy = buf.AsSpan(0, n).ToArray();  // bounded copy: only the logical [0, n)
+        ArrayPool<byte>.Shared.Return(buf);
+        return copy;
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+    static void Emit(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/arraypool-fullspan-overread/before.cs

@@ -0,0 +1,33 @@
+// BEFORE (buggy). Reduction of the ArrayPool "full-length view over-read" bug
+// (P-007 POOL005). A rented array is OVERSIZED: `ArrayPool<T>.Shared.Rent(n)`
+// returns an array of `Length >= n`, not exactly `n`. Here the code fills the
+// first `n` bytes, then takes a FULL-length view — `buf.AsSpan()` with no length —
+// so the `n` valid bytes are read together with the stale `[n, Length)` tail a
+// *previous* renter left behind: a wrong-length read and an information disclosure.
+// Both spellings are caught: the view used in an EXPRESSION (`Emit(buf.AsSpan())`)
+// and the view in a local-declaration INITIALIZER (`var copy = buf.AsSpan()...`).
+// The fix is a bounded view, `buf.AsSpan(0, n)` (see after.cs). Representative of
+// the pattern (pooled-buffer over-read/over-copy in tensor and serialization code),
+// 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;
+using System.Buffers;
+
+static class PoolFullSpanOverread
+{
+    static byte[] Frame(int n)
+    {
+        byte[] buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(buf, n);                          // valid payload is buf[0..n]
+        Emit(buf.AsSpan());                    // <-- BUG (expression): the WHOLE oversized array,
+                                               //     n payload bytes + the stale [n, Length) tail
+        byte[] copy = buf.AsSpan().ToArray();  // <-- BUG (initializer): the same over-read in a local
+        ArrayPool<byte>.Shared.Return(buf);
+        return copy;
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+    static void Emit(ReadOnlySpan<byte> data) { }
+}

corpus/real-world/arraypool-fullspan-overread/case.own

@@ -0,0 +1,19 @@
+// OwnLang model of the ArrayPool full-length view over-read. `acquire` ==
+// ArrayPool.Rent (the array is OVERSIZED: Length >= n), `release` ==
+// ArrayPool.Return. `overspan buf` models a FULL-length view `buf.AsSpan()` (no
+// length bound) handed to a consumer — it reaches past the logical length n into
+// the stale [n, Length) tail. The bounded form `buf.AsSpan(0, n)` takes no full
+// view, so the fixed code has no `overspan` and is silent. The checker trips
+// OWN025 (POOL005) at the view; the buffer is still correctly returned, so there
+// is no leak (OWN001) and no use-after-return (OWN002).
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  kind "pooled buffer"
+}
+fn frame(n: int) {
+  let buf = acquire Buffer(n);   // ArrayPool.Rent  (Length >= n)
+  overspan buf;                  // buf.AsSpan() — full-length view past n -> OWN025
+  release buf;                   // ArrayPool.Return
+}

corpus/real-world/arraypool-fullspan-overread/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN025

corpus/real-world/arraypool-fullspan-overread/notes.md

@@ -0,0 +1,35 @@
+# ArrayPool full-length view over-read (POOL005)
+
+**Pattern:** a pooled array from `ArrayPool<T>.Shared.Rent(n)` is *oversized* — the
+pool returns an array of `Length >= n`, not exactly `n`. Code that takes a
+FULL-length view of it (`buf.AsSpan()` / `buf.AsMemory()` / `new Span<T>(buf)`, all
+with **no length bound**) and reads, copies, or writes through that view processes
+the `n` valid bytes **plus** the stale `[n, Length)` tail — bytes a *previous*
+renter left behind. That is a correctness bug (wrong length) and an information
+disclosure (a prior renter's data leaks out). The fix is a bounded view:
+`buf.AsSpan(0, n)`.
+
+This is P-007's **POOL005** ("clear/copy past the logical length") — the over-read /
+over-copy vehicle is the unbounded view. It is distinct from **OWN024** (a
+*sensitive* buffer not cleared on release): POOL005 is reading/copying *too much*;
+OWN024 is clearing *too little*.
+
+**What the checker says:** the OwnLang model trips **OWN025**
+`[resource: pooled buffer]` at the view. The extractor recognises an unbounded
+`AsSpan()`/`AsMemory()`/`new Span<T>(buf)` over a `Rent`ed local (by the resolved
+`System.MemoryExtensions` / `System.Span<T>` BCL symbols, so a look-alike is not
+mistaken for it) and emits an `overspan` fact; the core — and the hand `case.own`
+reduction — raise OWN025. The buffer is still `Return`ed, so there is no OWN001
+leak and no OWN002 use-after-return; the only finding is the over-read itself.
+
+**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, not a
+verbatim PR diff. The extractor catches the unbounded view both as an *expression*
+(`Emit(buf.AsSpan())`, `buf.AsSpan().CopyTo(...)`) and in a local-declaration
+*initializer* — the over-copy `var copy = buf.AsSpan().ToArray();` and the
+view-local `Span<byte> s = buf.AsSpan();` alike, since the full view lives in the
+initializer either way. The remaining spelling is `Array.Clear(buf, 0, buf.Length)`
+(a length argument of `buf.Length` rather than an unbounded view), a follow-up.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
+AiDotNet.Tensors pooled-buffer over-clear/over-read.

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

@@ -6,8 +6,14 @@
   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
+  The borrow checker on real C#. **POOL005 (full-length view over-read → OWN025) first slice
+  built** — an unbounded `buf.AsSpan()` / `buf.AsMemory()` / `new Span<T>(buf)` over a `Rent`ed
+  local reaches past the logical length `n` into the oversized `[n, Length)` tail; the extractor
+  emits an `overspan` fact and the core raises OWN025 `[resource: pooled buffer]` at the view —
+  both when the view is used in an EXPRESSION (`Emit(buf.AsSpan())`) and when it is a local-decl
+  INITIALIZER (`var copy = buf.AsSpan().ToArray();`, `Span<T> s = buf.AsSpan();`) (corpus
+  `arraypool-fullspan-overread`). POOL003 (double-return — flow already catches OWN003), a view
+  stored in a FIELD, and the `Array.Clear(buf, 0, buf.Length)` spelling of POOL005 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
@@ -39,7 +45,7 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu
 | **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` |
 | **POOL003** double return | `Return` reachable twice for the same buffer | `OWN003` |
 | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` |
-| **POOL005** clear/copy past length | write/clear beyond the logical length of the rented region | (buffer-policy check) |
+| **POOL005** clear/copy past length | a full-length view (`buf.AsSpan()`, no bound) reads/copies beyond the logical length of the rented region | `OWN025` `[resource: pooled buffer]` ✅ (view in an expression or initializer; `Array.Clear(buf, 0, buf.Length)` next) |
 
 Resource mapping:
 

examples/gallery/11_overspan_full_view.own

@@ -0,0 +1,16 @@
+// POOL005 — a full-length Span view of a pooled buffer reaches past its logical
+// length. `ArrayPool.Rent(n)` hands back an OVERSIZED array (Length >= n); a view
+// with no length bound (`buf.AsSpan()`) spans the whole array, so reading or
+// copying through it exposes the stale [n, Length) tail a previous renter left.
+// Real C#: `Emit(buf.AsSpan())` where `Emit(buf.AsSpan(0, n))` was meant.
+module Gallery
+resource Buffer {
+  acquire rent
+  release give
+  kind "pooled buffer"
+}
+fn frame(n: int) {
+  let buf = acquire Buffer(n);
+  overspan buf;          // full-length view -> OWN025
+  release buf;
+}

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -450,12 +450,19 @@
             InjectThrowEdge(ld, nodes, onThrow);
             if (ld.UsingKeyword == default)
                 foreach (var v in ld.Declaration.Variables)
+                {
                     if (tracked.Contains(v.Identifier.Text)
                         && (v.Initializer?.Value is ObjectCreationExpressionSyntax
                                                  or ImplicitObjectCreationExpressionSyntax
                             || IsPoolRent(v.Initializer?.Value, model)        // ArrayPool<T> Rent
                             || IsOwningFactory(v.Initializer?.Value, model)))   // File / crypto Create* factory
                         nodes.Add(new { op = "acquire", var = v.Identifier.Text, line = LineOf(v) });
+                    // POOL005: a full-length view in the initializer — `var copy = buf.AsSpan().ToArray();`
+                    // — over-reads the pooled tail just as `Emit(buf.AsSpan());` does. EmitFlowExpr is not
+                    // called on a non-acquire initializer, so scan it here for the overspan (Codex review).
+                    if (v.Initializer?.Value is { } vinit)
+                        EmitOverspans(vinit, tracked, model, nodes);
+                }
             return true;
         case ExpressionStatementSyntax es:
             InjectThrowEdge(es, nodes, onThrow);
@@ -796,6 +803,25 @@
     }
     foreach (var u in used)
         nodes.Add(new { op = "use", var = u, line = LineOf(expr) });
+    // POOL005: a full-length view of a pooled buffer anywhere in this expression -> overspan/OWN025.
+    EmitOverspans(expr, tracked, model, nodes);
+}
+
+// POOL005: emit one `overspan` op per tracked pooled buffer that `expr` takes a FULL-LENGTH view of
+// (no length bound) — the core raises OWN025. Walks the whole expression so a view nested in a call
+// (`Sink.Write(buf.AsSpan())`), a chain (`buf.AsSpan().ToArray()`), or a local-declaration
+// initializer (`var copy = buf.AsSpan().ToArray();`) is found; a BOUNDED view (`buf.AsSpan(0, n)`)
+// is not matched (FullViewOwner returns null). Among `tracked` locals only pooled buffers are the
+// arrays the BCL AsSpan/Span symbols bind to, so this never fires on a tracked IDisposable / factory
+// result. Shared by the expression-statement and local-declaration lowering paths.
+static void EmitOverspans(ExpressionSyntax expr, HashSet<string> tracked, SemanticModel model, List<object> nodes)
+{
+    var overspanned = new SortedSet<string>(StringComparer.Ordinal);
+    foreach (var node in expr.DescendantNodesAndSelf().OfType<ExpressionSyntax>())
+        if (FullViewOwner(node, model) is { } owner && tracked.Contains(owner))
+            overspanned.Add(owner);
+    foreach (var o in overspanned)
+        nodes.Add(new { op = "overspan", var = o, line = LineOf(expr) });
 }
 
 // The field name an expression refers to: "_f" for `_f` or `this._f`, else null.
@@ -874,6 +900,35 @@
     return null;
 }
 
+// The tracked owner buffer a FULL-LENGTH view spans (no length bound), else null. POOL005:
+// `buf.AsSpan()` / `buf.AsMemory()` taken with NO arguments span `[0, Length)` — the WHOLE backing
+// array — and `new Span<T>(buf)` / `new Memory<T>(buf)` with only the array argument do the same. A
+// pooled array is oversized (`ArrayPool.Rent(n)` returns `Length >= n`), so such a view reaches past
+// the logical length `n` into the stale `[n, Length)` tail (a previous renter's bytes): reading or
+// copying through it processes that stale data — a correctness bug and a potential disclosure. A
+// BOUNDED view (`buf.AsSpan(0, n)`, `new Span<T>(buf, 0, n)`) has a length argument and returns null
+// here — it does not over-read. Recognised by the SAME resolved BCL symbols as `ViewOwner`, so a
+// project's own `AsSpan`/`Span` look-alike is not mistaken for the over-read.
+static string? FullViewOwner(ExpressionSyntax? e, SemanticModel model)
+{
+    if (e is InvocationExpressionSyntax inv
+        && inv.Expression is MemberAccessExpressionSyntax m
+        && m.Name.Identifier.Text is "AsSpan" or "AsMemory"
+        && inv.ArgumentList.Arguments.Count == 0                       // no start/length -> whole array
+        && 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 BaseObjectCreationExpressionSyntax oc
+        && oc.ArgumentList is { Arguments.Count: 1 }                   // only the array -> whole array
+        && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg
+        && model.GetSymbolInfo(oc).Symbol is IMethodSymbol
+            { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct }
+        && IsInNamespace(sct, "System"))
+        return arg.Identifier.Text;
+    return null;
+}
+
 // If `idn` references a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW local declared from an owner
 // buffer (`Memory<T> view = owner.AsMemory(…)`), the owner buffer's local name — so a use of the
 // view (including RETURNING it, an escape) lowers to a use of the owner (the borrow). Resolved
@@ -1470,7 +1525,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

ownlang/analysis.py

@@ -58,6 +58,7 @@
     Invoke,
     Kind,
     MoveInto,
+    Overspan,
     Release,
     Return,
     Symbol,
@@ -370,6 +371,18 @@ def step(self, ins: Instr, st: State) -> None:
                              f"region", ins.line)
             return
 
+        if isinstance(ins, Overspan):
+            # POOL005: a full-length view over the whole pooled array reaches past
+            # the logical length it was rented for (the oversized [n, Length) tail).
+            # A property of the view-creation site, not of the owner's flow state —
+            # so it raises regardless of OWNED/RELEASED and changes no state.
+            self.err("OWN025",
+                     f"'{ins.sym.name}' is viewed at its full backing length, past "
+                     f"the logical length it was rented for (over-read / "
+                     f"over-clear)", ins.line, subject=ins.sym.origin,
+                     resource_kind=ins.sym.resource_kind)
+            return
+
         if isinstance(ins, Invoke):
             for sym, eff in ins.args:
                 if sym is not None:

ownlang/ast_nodes.py

@@ -112,6 +112,18 @@ class Use:
     line: int
 
 
+@dataclass(frozen=True)
+class Overspan:
+    """`overspan x;` — a full-length view (`Span`/`Memory`) is taken over the
+    whole pooled buffer `x`, reaching past the logical length it was rented for.
+    A pooled array is oversized (`ArrayPool.Rent(n)` returns `Length >= n`), so a
+    view with no length bound (`buf.AsSpan()`, `new Span<T>(buf)`) exposes — and a
+    `.Clear()`/`.Fill()` through it overwrites — the stale `[n, Length)` tail. The
+    over-read / over-clear is POOL005; the fix is a bounded view `buf.AsSpan(0, n)`."""
+    var: str
+    line: int
+
+
 @dataclass(frozen=True)
 class Call:
     """callee(args);  -> a call to a declared extern or local fn"""
@@ -164,7 +176,8 @@ class Subscribe:
     line: int
 
 
-Stmt = Let | Release | Use | Call | BorrowBlock | If | While | Return | Subscribe
+Stmt = (Let | Release | Use | Overspan | Call | BorrowBlock | If | While
+        | Return | Subscribe)
 
 
 # ---- top level ------------------------------------------------------------

ownlang/cfg.py

@@ -117,6 +117,15 @@ class Use:
     line: int
 
 
+@dataclass
+class Overspan:
+    """A full-length view (`Span`/`Memory`) taken over the whole pooled buffer
+    `sym`, reaching past the logical length it was rented for (POOL005). Carries
+    no state transition — the owner stays OWNED; it only raises OWN025 at `line`."""
+    sym: Symbol
+    line: int
+
+
 @dataclass
 class Invoke:
     """A resolved call. `args` pairs each argument's resolved Symbol (or None
@@ -148,7 +157,7 @@ class Return:
     line: int
 
 
-Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Invoke
+Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Overspan | Invoke
          | BorrowStart | BorrowEnd | Return)
 
 
@@ -332,6 +341,17 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None:
             if sym is not None:
                 cur.instrs.append(Use(sym, st.line))
             return cur
+        if isinstance(st, A.Overspan):
+            sym = self.lookup(st.var, st.line)
+            if sym is not None:
+                if sym.kind != Kind.OWNED:
+                    self.diags.append(Diagnostic(
+                        "OWN034",
+                        f"cannot take a full-length view of '{st.var}': it is not "
+                        f"an owned resource ({sym.kind.name.lower()})", st.line))
+                else:
+                    cur.instrs.append(Overspan(sym, st.line))
+            return cur
         if isinstance(st, A.Call):
             return self.lower_call(st, cur)
         if isinstance(st, A.BorrowBlock):

ownlang/codegen.py

@@ -442,6 +442,12 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]:
             return [f"{ind}{self._release_stmt(st.var, rt)}"]
         if isinstance(st, A.Use):
             return [f"{ind}Use({st.var});"]
+        if isinstance(st, A.Overspan):
+            # POOL005: a full-length view over the whole pooled array (no length
+            # bound) — reaches past the logical length it was rented for. The
+            # bounded, correct form is `{st.var}.AsSpan(0, n)`.
+            return [f"{ind}{st.var}.AsSpan();  "
+                    f"// full-length view over the pooled tail (over-read)"]
         if isinstance(st, A.Call):
             return [f"{ind}{st.callee}({', '.join(self._arg(a) for a in st.args)});"]
         if isinstance(st, A.BorrowBlock):