From b3bf5b10957b0624cd6b84b179c64e6591f44ff8 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 00:07:37 +0000 Subject: [PATCH 1/2] feat(pool): POOL005 .Length spelling + MemoryPool tracking (POOL001/002/003) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two pooled-buffer extractor additions, both riding machinery that already exists in the core — so there are NO core changes, only the Roslyn extractor + corpus + spec. POOL005 — the `.Length` spelling of the over-read/over-clear (sibling of #71's unbounded `buf.AsSpan()`). A pooled array is oversized (Rent(n) -> Length >= n), so passing the buffer's OWN `buf.Length` as the operative length reaches the whole array, past the rented n, into the stale [n, Length) tail: - FullViewOwner now also matches buf.AsSpan(0, buf.Length) / buf.AsMemory(0, buf.Length) and new Span(buf, 0, buf.Length) (length arg is the receiver's own .Length); - a new ArrayClearOverOwner matches Array.Clear(buf, 0, buf.Length) (the over-clear). A real bound (buf.AsSpan(0, n), Array.Clear(buf, 0, n)) is not matched; the single-arg Array.Clear(buf) wipe is deliberately left alone. All emit the existing `overspan` fact -> OWN025. Corpus: arraypool-clear-past-length. MemoryPool — the OTHER pool was untracked entirely. MemoryPool.Shared.Rent returns an IMemoryOwner released by Dispose (no Return), so it is tracked as a regular Dispose-released local (IsMemoryPoolRent, mirroring IsPoolRent but NOT a poolBuffer: arg-passing is an escape, like any IDisposable). With that one acquire recognised, the existing flow covers POOL001 (never disposed -> OWN001), POOL002 (use after Dispose -> OWN002) and POOL003 (double Dispose -> OWN003). Corpus: memorypool-double-dispose (the MemoryPool twin of arraypool-double-return) -> OWN003. POOL003 for ArrayPool was already green (try/finally + aliased-receiver, both in the benchmark) — this adds its MemoryPool sibling. Benchmark recall floor 14 -> 16. Spec: BufferPolicies B9 (the .Length spelling), P-007 (status, scope, open Q#4 resolved). metamorphic.py already knows `overspan`; the new .own models reuse acquire/release. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 13 +- .../arraypool-clear-past-length/after.cs | 21 ++++ .../arraypool-clear-past-length/before.cs | 28 +++++ .../arraypool-clear-past-length/case.own | 18 +++ .../expected-diagnostics.txt | 1 + .../arraypool-clear-past-length/notes.md | 30 +++++ .../memorypool-double-dispose/after.cs | 16 +++ .../memorypool-double-dispose/before.cs | 30 +++++ .../memorypool-double-dispose/case.own | 14 +++ .../expected-diagnostics.txt | 1 + .../memorypool-double-dispose/notes.md | 26 ++++ docs/proposals/P-007-arraypool-span.md | 21 +++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 113 ++++++++++++++---- spec/BufferPolicies.md | 19 +-- 14 files changed, 311 insertions(+), 40 deletions(-) create mode 100644 corpus/real-world/arraypool-clear-past-length/after.cs create mode 100644 corpus/real-world/arraypool-clear-past-length/before.cs create mode 100644 corpus/real-world/arraypool-clear-past-length/case.own create mode 100644 corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt create mode 100644 corpus/real-world/arraypool-clear-past-length/notes.md create mode 100644 corpus/real-world/memorypool-double-dispose/after.cs create mode 100644 corpus/real-world/memorypool-double-dispose/before.cs create mode 100644 corpus/real-world/memorypool-double-dispose/case.own create mode 100644 corpus/real-world/memorypool-double-dispose/expected-diagnostics.txt create mode 100644 corpus/real-world/memorypool-double-dispose/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 38f03c53..2a2d2fb9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -788,10 +788,13 @@ jobs: # `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` view (which, unlike a # 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 + # view of a pooled buffer reaches past the rented length into the oversized tail -> OWN025 + # (P-007 POOL005, the over-read): the unbounded `buf.AsSpan()` AND the `.Length` spelling + # (`buf.AsSpan(0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`) — the `arraypool-fullspan- + # overread` / `arraypool-clear-past-length` cases. MemoryPool is now tracked too: a + # `MemoryPool.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 # a FIELD, and an injected-source region-escape. A drop below the floor is a regression. - run: python scripts/benchmark.py --min-recall 14 + run: python scripts/benchmark.py --min-recall 16 diff --git a/corpus/real-world/arraypool-clear-past-length/after.cs b/corpus/real-world/arraypool-clear-past-length/after.cs new file mode 100644 index 00000000..1277093d --- /dev/null +++ b/corpus/real-world/arraypool-clear-past-length/after.cs @@ -0,0 +1,21 @@ +// AFTER (fixed). Every length/count argument is bound to the logical length `n`, +// not the oversized `buf.Length`: `buf.AsSpan(0, n)` views only the valid payload +// and `Array.Clear(buf, 0, n)` clears only it. The `[n, Length)` tail is never +// touched, so the extractor emits no `overspan` fact and the checker is silent. +using System; +using System.Buffers; + +static class PoolClearPastLength +{ + static void Roundtrip(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); + Emit(buf.AsSpan(0, n)); // bounded by the rented length n + Array.Clear(buf, 0, n); // clears only the logical [0, n) + ArrayPool.Shared.Return(buf); + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-clear-past-length/before.cs b/corpus/real-world/arraypool-clear-past-length/before.cs new file mode 100644 index 00000000..10da2b85 --- /dev/null +++ b/corpus/real-world/arraypool-clear-past-length/before.cs @@ -0,0 +1,28 @@ +// BEFORE (buggy). POOL005, the `.Length` spelling of the over-read / over-clear. +// A rented array is OVERSIZED: `ArrayPool.Shared.Rent(n)` returns an array of +// `Length >= n`. This code uses `buf.Length` — the oversized backing length — as +// the operative length instead of the rented `n`: `buf.AsSpan(0, buf.Length)` +// hands off the stale `[n, Length)` tail (a previous renter's bytes), and +// `Array.Clear(buf, 0, buf.Length)` clears past `n` into that tail. The fix is to +// bound by the logical length `n` (`buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`, +// see after.cs). Representative of the pattern, 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 PoolClearPastLength +{ + static void Roundtrip(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); // valid payload is buf[0..n] + Emit(buf.AsSpan(0, buf.Length)); // <-- BUG: length is buf.Length, not n -> stale tail + Array.Clear(buf, 0, buf.Length); // <-- BUG: clears past n into the pooled tail + ArrayPool.Shared.Return(buf); + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-clear-past-length/case.own b/corpus/real-world/arraypool-clear-past-length/case.own new file mode 100644 index 00000000..afa1e151 --- /dev/null +++ b/corpus/real-world/arraypool-clear-past-length/case.own @@ -0,0 +1,18 @@ +// OwnLang model of the POOL005 `.Length` over-read / over-clear. `acquire` == +// ArrayPool.Rent (oversized: Length >= n), `release` == ArrayPool.Return. +// `overspan buf` models using the buffer's OWN oversized `.Length` as the +// operative length — `buf.AsSpan(0, buf.Length)` / `Array.Clear(buf, 0, buf.Length)` +// — which reaches past the rented `n` into the stale tail. Bounding by `n` takes no +// full view, so the fixed code has no `overspan` and is silent. -> OWN025. The +// buffer is still returned, so there is no leak (OWN001). +module Corpus +resource Buffer { + acquire rent + release give + kind "pooled buffer" +} +fn roundtrip(n: int) { + let buf = acquire Buffer(n); // ArrayPool.Rent (Length >= n) + overspan buf; // buf.AsSpan(0, buf.Length) / Array.Clear(buf, 0, buf.Length) -> OWN025 + release buf; // ArrayPool.Return +} diff --git a/corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt b/corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt new file mode 100644 index 00000000..511ccfa9 --- /dev/null +++ b/corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN025 diff --git a/corpus/real-world/arraypool-clear-past-length/notes.md b/corpus/real-world/arraypool-clear-past-length/notes.md new file mode 100644 index 00000000..96bec428 --- /dev/null +++ b/corpus/real-world/arraypool-clear-past-length/notes.md @@ -0,0 +1,30 @@ +# ArrayPool over-read / over-clear — the `.Length` spelling (POOL005) + +**Pattern:** a pooled array from `ArrayPool.Shared.Rent(n)` is *oversized* +(`Length >= n`). Code that uses `buf.Length` — the oversized backing length — as +the operative length, rather than the rented `n`, reaches past the valid payload +into the stale `[n, Length)` tail a previous renter left: + +- `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)` — an over-**read** + (the consumer sees `n` valid bytes plus the stale tail: a wrong-length read and a + potential information disclosure); +- `Array.Clear(buf, 0, buf.Length)` — an over-**clear** (touches the pool's tail + past the data that was actually written). + +The fix is to bound by the logical length: `buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`. + +This is the `.Length` sibling of `arraypool-fullspan-overread` (which catches the +unbounded `buf.AsSpan()`): same OWN025, a different way of writing the oversized +length. The extractor recognises the `.Length` argument on the buffer's own view / +`Array.Clear` (resolved BCL symbols) and emits an `overspan` fact. + +**What the checker says:** **OWN025** `[resource: pooled buffer]` at each over-reach +site. The buffer is still `Return`ed, so there is no OWN001 leak. + +**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. The +single-arg `Array.Clear(buf)` (a deliberate whole-buffer wipe) is intentionally not +flagged — only the explicit oversized `buf.Length` count is. + +Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target +AiDotNet.Tensors pooled-buffer over-clear/over-read. diff --git a/corpus/real-world/memorypool-double-dispose/after.cs b/corpus/real-world/memorypool-double-dispose/after.cs new file mode 100644 index 00000000..c7d52d6e --- /dev/null +++ b/corpus/real-world/memorypool-double-dispose/after.cs @@ -0,0 +1,16 @@ +// AFTER (fixed). A `using` declaration disposes the owner exactly once, at the end +// of the scope, on every path — no second Dispose. The pooled memory is released +// once and returned to the pool cleanly, so the checker is silent. +using System; +using System.Buffers; + +static class MemoryPoolDoubleDispose +{ + static void Run(int n) + { + using IMemoryOwner owner = MemoryPool.Shared.Rent(n); + Work(owner.Memory); + } + + static void Work(Memory data) { } +} diff --git a/corpus/real-world/memorypool-double-dispose/before.cs b/corpus/real-world/memorypool-double-dispose/before.cs new file mode 100644 index 00000000..b0a3acd9 --- /dev/null +++ b/corpus/real-world/memorypool-double-dispose/before.cs @@ -0,0 +1,30 @@ +// BEFORE (buggy). POOL003 for the OTHER pool: a `MemoryPool` hands back an +// `IMemoryOwner` released by `Dispose()` (there is no `Return`). Disposing the +// same owner twice — here on the success path AND again in `finally` — is a double +// release: the same memory can later be handed to two renters at once, exactly the +// corruption dotnet/runtime#33767 describes for ArrayPool double-return. The fix is +// to dispose exactly once (a `using` owner, see after.cs). +// +// 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 MemoryPoolDoubleDispose +{ + static void Run(int n) + { + IMemoryOwner owner = MemoryPool.Shared.Rent(n); + try + { + Work(owner.Memory); + owner.Dispose(); // disposed here ... + } + finally + { + owner.Dispose(); // <-- ... and again here (double release) + } + } + + static void Work(Memory data) { } +} diff --git a/corpus/real-world/memorypool-double-dispose/case.own b/corpus/real-world/memorypool-double-dispose/case.own new file mode 100644 index 00000000..90a517cc --- /dev/null +++ b/corpus/real-world/memorypool-double-dispose/case.own @@ -0,0 +1,14 @@ +// OwnLang model of the MemoryPool double-dispose. A MemoryPool owner is +// `acquire`d by Rent and `release`d by Dispose (there is no Return). Disposing it +// twice is a double release -> OWN003 — the same verdict as an ArrayPool +// double-return; the pool can then hand the same memory to two renters at once. +module Corpus +resource MemoryOwner { + acquire Rent + release Dispose +} +fn run(n: int) { + let owner = acquire MemoryOwner(n); // MemoryPool.Rent + release owner; // owner.Dispose() + release owner; // owner.Dispose() again -> OWN003 +} diff --git a/corpus/real-world/memorypool-double-dispose/expected-diagnostics.txt b/corpus/real-world/memorypool-double-dispose/expected-diagnostics.txt new file mode 100644 index 00000000..574370e9 --- /dev/null +++ b/corpus/real-world/memorypool-double-dispose/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN003 diff --git a/corpus/real-world/memorypool-double-dispose/notes.md b/corpus/real-world/memorypool-double-dispose/notes.md new file mode 100644 index 00000000..74ad9605 --- /dev/null +++ b/corpus/real-world/memorypool-double-dispose/notes.md @@ -0,0 +1,26 @@ +# MemoryPool double-dispose (POOL003, the Dispose-released pool) + +**Pattern:** `MemoryPool.Shared.Rent(n)` returns an `IMemoryOwner` whose +backing memory is returned to the pool by **`Dispose()`** (there is no `Return`). +Disposing the same owner twice — classically once on the normal path and again in a +`finally`/`Dispose`, or two explicit `Dispose()` calls — double-releases the memory, +so the pool can hand it to two renters simultaneously. This is the MemoryPool twin of +`arraypool-double-return` (dotnet/runtime#33767). + +**What it adds:** the extractor now tracks `MemoryPool.Shared.Rent` as an owned +resource (an `IMemoryOwner` released by `Dispose`, the IDisposable path — *not* a +`Return`-based pool buffer). With that one acquire recognised, the existing +flow-sensitive checker covers the whole MemoryPool family: **POOL001** (never +disposed → OWN001), **POOL002** (owner used after `Dispose` → OWN002), and +**POOL003** (this case — disposed twice → **OWN003**). + +**What the checker says:** the OwnLang model and the real `before.cs` both trip +**OWN003** (double release). The `using` fix in `after.cs` disposes exactly once 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. The +`IMemoryOwner.Memory.Span` *view* tracking (a borrow of the owner) is a follow-up; +this slice covers the owner's own acquire / use / release lifecycle. + +Reference: dotnet/runtime#33767; [P-007](../../../docs/proposals/P-007-arraypool-span.md). diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 61134c3a..308ac483 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -12,8 +12,14 @@ 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 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 + `arraypool-fullspan-overread`) — and the **`.Length` spelling** too (`buf.AsSpan(0, buf.Length)`, + `Array.Clear(buf, 0, buf.Length)`, where the oversized self-`.Length` is the operative length; + corpus `arraypool-clear-past-length`). **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.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 - **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 @@ -43,9 +49,9 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu |---------|---------|--------------| | **POOL001** rented not returned | `Rent(...)` with no matching `Return(buf)` in the same member | `OWN001` `[resource: pooled buffer]` ✅ | | **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` | +| **POOL003** double return | `Return`/`Dispose` reachable twice for the same buffer (ArrayPool *and* MemoryPool) | `OWN003` ✅ | | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` | -| **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) | +| **POOL005** clear/copy past length | a full-length view (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`) reads/copies/clears beyond the logical length | `OWN025` `[resource: pooled buffer]` ✅ (a view stored in a FIELD next) | Resource mapping: @@ -97,5 +103,8 @@ Catching a real one of these is the milestone-4 success condition. the existing sensitive-buffer/clear-on-release check (OWN024)? 3. How much of POOL004 (view escape) overlaps the existing OWN004/OWN015 escape rules — reuse, don't duplicate. -4. `IMemoryOwner` / `MemoryPool` `Dispose`-based release vs `ArrayPool`'s - explicit `Return` — one model with two release spellings? +4. **(resolved)** `IMemoryOwner` / `MemoryPool` `Dispose`-based release vs + `ArrayPool`'s explicit `Return` — yes, one flow model, two release spellings: a + `MemoryPool.Rent` owner is tracked as an IDisposable (released by `Dispose`, + arg-passing is an escape), an `ArrayPool.Rent` buffer by `Return` (arg-passing is + a borrow). Both feed the same acquire/use/release lattice → POOL001/002/003. diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 8d40f695..e449baa3 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -455,6 +455,7 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, SemanticM && (v.Initializer?.Value is ObjectCreationExpressionSyntax or ImplicitObjectCreationExpressionSyntax || IsPoolRent(v.Initializer?.Value, model) // ArrayPool Rent + || IsMemoryPoolRent(v.Initializer?.Value, model) // MemoryPool Rent (IMemoryOwner) || 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();` @@ -807,19 +808,25 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet tracked, Semanti 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. +// POOL005: emit one `overspan` op per tracked pooled buffer that `expr` reaches past the rented +// length of — the core raises OWN025. Two over-reach shapes: a FULL-LENGTH view (`buf.AsSpan()` with +// no bound, or `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)` whose length is the +// oversized self-`.Length`), and an over-clear (`Array.Clear(buf, 0, buf.Length)`). 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()...`) is +// found; a view bounded to the real `n` (`buf.AsSpan(0, n)`) is not matched. Among `tracked` locals +// only pooled buffers are the arrays the BCL AsSpan/Span/Array.Clear 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 tracked, SemanticModel model, List nodes) { var overspanned = new SortedSet(StringComparer.Ordinal); foreach (var node in expr.DescendantNodesAndSelf().OfType()) - if (FullViewOwner(node, model) is { } owner && tracked.Contains(owner)) + { + var owner = FullViewOwner(node, model) ?? ArrayClearOverOwner(node, model); + if (owner is not null && tracked.Contains(owner)) overspanned.Add(owner); + } foreach (var o in overspanned) nodes.Add(new { op = "overspan", var = o, line = LineOf(expr) }); } @@ -870,6 +877,30 @@ e is InvocationExpressionSyntax i && i.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax buf ? buf.Identifier.Text : null; +// Is `t` the System.Buffers.MemoryPool type — the Dispose-based pool. Mirrors IsArrayPoolType +// (checked on the resolved symbol, so an aliased/injected `MemoryPool` receiver binds and a +// look-alike does not). +static bool IsMemoryPoolType(INamedTypeSymbol? t) +{ + if (t is null || t.Name != "MemoryPool") + return false; + INamespaceSymbol? ns = t.ContainingNamespace; // System.Buffers + if (ns is null || ns.Name != "Buffers") + return false; + ns = ns.ContainingNamespace; // System.Buffers -> System + return ns is not null && ns.Name == "System" + && ns.ContainingNamespace is { IsGlobalNamespace: true }; +} + +// A MemoryPool.Shared.Rent(...) call — the acquire of an IMemoryOwner. There is NO +// MemoryPool.Return: the owner is released by Dispose (the IDisposable path), so unlike an ArrayPool +// buffer it is NOT a `poolBuffer`. A Rent'd owner never disposed leaks (OWN001), a second Dispose is +// a double release (OWN003), and a use of the owner after Dispose is a use-after-release (OWN002). +static bool IsMemoryPoolRent(ExpressionSyntax? e, SemanticModel model) => + e is InvocationExpressionSyntax i + && model.GetSymbolInfo(i).Symbol is IMethodSymbol { Name: "Rent" } sym + && IsMemoryPoolType(sym.ContainingType); + // The owner buffer a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW expression borrows from: // `owner.AsSpan(...)` / `owner.AsMemory(...)`, or `new Span(owner, …)` / `new Memory(owner)` // (and the ReadOnly* forms), where the source is a local identifier. Returns the owner local name, @@ -900,35 +931,73 @@ e is InvocationExpressionSyntax i 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(buf)` / `new Memory(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(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 +// The tracked owner buffer a FULL-LENGTH view spans, else null. POOL005: `buf.AsSpan()` / +// `buf.AsMemory()` with NO arguments span `[0, Length)` — the WHOLE backing array — and so does +// `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)`, whose length argument is the +// buffer's OWN oversized `.Length` (the `.Length` spelling); `new Span(buf)` (only the array) too. +// 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 +// view bounded to the REAL rented length (`buf.AsSpan(0, n)`, `new Span(buf, 0, n)`) returns null +// — 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; + { + var args = inv.ArgumentList.Arguments; + // `buf.AsSpan()` (no bound) spans the whole array; so does `buf.AsSpan(0, buf.Length)`, + // whose length argument is the buffer's OWN oversized `.Length` (the `.Length` spelling). + if (args.Count == 0 + || (args.Count == 2 && IsLengthOf(args[1].Expression, recv.Identifier.Text))) + 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 + && oc.ArgumentList is { Arguments.Count: > 0 } al + && al.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; + { + // `new Span(buf)` (whole array) or `new Span(buf, 0, buf.Length)` (length is the + // oversized self-length). + if (al.Arguments.Count == 1 + || (al.Arguments.Count == 3 && IsLengthOf(al.Arguments[2].Expression, arg.Identifier.Text))) + return arg.Identifier.Text; + } return null; } +// `arg` is the buffer's own `.Length` (`buf.Length`) — the POOL005 `.Length` spelling, where the +// oversized backing length is passed as the operative length/count instead of the rented `n`. +static bool IsLengthOf(ExpressionSyntax arg, string owner) => + arg is MemberAccessExpressionSyntax { Name.Identifier.Text: "Length", + Expression: IdentifierNameSyntax id } + && id.Identifier.Text == owner; + +// Array.Clear(buf, 0, buf.Length) — clears the WHOLE oversized backing array, past the rented +// length (POOL005 over-clear). Returns the buffer name; Array.Clear(buf, 0, n) with a real bound +// returns null. The single-arg Array.Clear(buf) is intentionally NOT matched — wiping the whole +// buffer is a common, safe idiom; only the explicit oversized `.Length` count is flagged. +static string? ArrayClearOverOwner(ExpressionSyntax? e, SemanticModel model) +{ + if (e is not InvocationExpressionSyntax inv + || model.GetSymbolInfo(inv).Symbol is not IMethodSymbol + { Name: "Clear", ContainingType: { Name: "Array" } act } + || !IsInNamespace(act, "System")) + return null; + var args = inv.ArgumentList.Arguments; + return args.Count == 3 + && args[0].Expression is IdentifierNameSyntax buf + && IsLengthOf(args[2].Expression, buf.Identifier.Text) + ? buf.Identifier.Text : null; +} + // If `idn` references a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW local declared from an owner // buffer (`Memory 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 @@ -1879,6 +1948,8 @@ or ImplicitObjectCreationExpressionSyntax } init } else if (IsOwningFactory(v.Initializer?.Value, model)) // File / crypto Create* factory candidates.Add(v.Identifier.Text); + else if (IsMemoryPoolRent(v.Initializer?.Value, model)) // MemoryPool IMemoryOwner (Dispose-released, NOT a poolBuffer) + candidates.Add(v.Identifier.Text); } if (candidates.Count == 0) continue; diff --git a/spec/BufferPolicies.md b/spec/BufferPolicies.md index 7b2c720d..a07341df 100644 --- a/spec/BufferPolicies.md +++ b/spec/BufferPolicies.md @@ -39,15 +39,18 @@ inline = 256)`. The namespace is `Buffer`; the method selects the mode. - **B7 — requested length preserved.** `scratch` lowering preserves the *requested* logical length, independent of whether the stack or pool branch is taken. -- **B9 — full view stays within the logical length.** A pooled buffer is +- **B9 — operations stay within the logical length.** A pooled buffer is *oversized*: `ArrayPool.Rent(n)` returns an array of `Length >= n`, not - exactly `n`. A FULL-length view of it — `buf.AsSpan()` / `buf.AsMemory()` / - `new Span(buf)` with **no length bound** — reaches past the requested length - `n` into the stale `[n, Length)` tail (a previous renter's bytes); reading or - copying through it is an over-read / over-copy → **OWN025**. The fix is a bounded - view, `buf.AsSpan(0, n)`. (P-007 POOL005; the OwnLang model op is `overspan b`. - Distinct from B6/OWN024, which is clearing *too little* of a sensitive buffer — - this is reading *too much*.) + exactly `n`. An operation that reaches the whole backing array rather than the + requested `n` touches the stale `[n, Length)` tail (a previous renter's bytes); + reading or copying through it is an over-read / over-copy → **OWN025**. Two + spellings: a FULL-length **view** with no bound (`buf.AsSpan()` / `buf.AsMemory()` + / `new Span(buf)`), and the **`.Length`** form that passes the buffer's own + oversized `.Length` as the operative length (`buf.AsSpan(0, buf.Length)`, + `new Span(buf, 0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`). The fix is + to bound by `n`: `buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`. (P-007 POOL005; the + OwnLang model op is `overspan b`. Distinct from B6/OWN024, which is clearing *too + little* of a sensitive buffer — this is touching *too much*.) ## Buffer options and `policy` blocks From 5a9f22fc2775d53113d1c58506f900e31a178f68 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 00:19:57 +0000 Subject: [PATCH 2/2] =?UTF-8?q?fix(pool):=20POOL005=20is=20a=20VIEW=20over?= =?UTF-8?q?-read=20only=20=E2=80=94=20drop=20Array.Clear,=20require=20zero?= =?UTF-8?q?=20start?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review feedback on #72 (Codex + CodeRabbit), all precision tightening on an already-green PR: 1. Codex: do not flag Array.Clear(buf, 0, buf.Length). It is a WRITE/wipe — it only zeros the pooled tail (a safe clear-before-Return idiom) and exposes nothing; the over-read bug is READING/COPYING the tail through a view. Removed ArrayClearOverOwner entirely; EmitOverspans now flags only read-capable VIEWS (FullViewOwner). Renamed the corpus case arraypool-clear-past-length -> arraypool-length-overread and made it the `.Length` VIEW over-read (buf.AsSpan(0, buf.Length)); after.cs bounds by n. 2. CodeRabbit: the `.Length` view match now also requires the START/index to be the constant 0 (IsZeroInt via the SemanticModel) — buf.AsSpan(k, buf.Length) for k != 0 is out of range, not this pattern. Applies to AsSpan/AsMemory(0, buf.Length) and new Span(buf, 0, buf.Length). 3. CodeRabbit (spec nitpick): B9 now notes the oversize principle covers MemoryPool too (IMemoryOwner.Memory wraps an oversized backing via .Memory.Length), and that a write/wipe is not flagged. NOT changed: --min-recall stays 16. CodeRabbit flagged it as "impossible (corpus is 14)" but that miscounts — the benchmark scores corpus/real-world (14) AND corpus/wpf (4) = 18 total, and --min-recall is the CAUGHT floor, not the corpus size. #72's benchmark is green at 16 (16 caught of 18); the `.Length` VIEW form still catches arraypool-length- overread after dropping Array.Clear. spec/P-007/ci.yml comments updated to match. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 7 ++- .../arraypool-clear-past-length/after.cs | 21 ------- .../arraypool-clear-past-length/before.cs | 28 --------- .../arraypool-clear-past-length/case.own | 18 ------ .../arraypool-clear-past-length/notes.md | 30 ---------- .../arraypool-length-overread/after.cs | 20 +++++++ .../arraypool-length-overread/before.cs | 29 ++++++++++ .../arraypool-length-overread/case.own | 17 ++++++ .../expected-diagnostics.txt | 0 .../arraypool-length-overread/notes.md | 28 +++++++++ docs/proposals/P-007-arraypool-span.md | 10 ++-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 57 ++++++++----------- spec/BufferPolicies.md | 26 +++++---- 13 files changed, 141 insertions(+), 150 deletions(-) delete mode 100644 corpus/real-world/arraypool-clear-past-length/after.cs delete mode 100644 corpus/real-world/arraypool-clear-past-length/before.cs delete mode 100644 corpus/real-world/arraypool-clear-past-length/case.own delete mode 100644 corpus/real-world/arraypool-clear-past-length/notes.md create mode 100644 corpus/real-world/arraypool-length-overread/after.cs create mode 100644 corpus/real-world/arraypool-length-overread/before.cs create mode 100644 corpus/real-world/arraypool-length-overread/case.own rename corpus/real-world/{arraypool-clear-past-length => arraypool-length-overread}/expected-diagnostics.txt (100%) create mode 100644 corpus/real-world/arraypool-length-overread/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2a2d2fb9..5f5bc69c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -789,9 +789,10 @@ jobs: # after `Return(buf)` trips OWN002 — including RETURNING a `Memory` view (which, unlike a # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. A # view of a pooled buffer reaches past the rented length into the oversized tail -> OWN025 - # (P-007 POOL005, the over-read): the unbounded `buf.AsSpan()` AND the `.Length` spelling - # (`buf.AsSpan(0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`) — the `arraypool-fullspan- - # overread` / `arraypool-clear-past-length` cases. MemoryPool is now tracked too: a + # (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.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 diff --git a/corpus/real-world/arraypool-clear-past-length/after.cs b/corpus/real-world/arraypool-clear-past-length/after.cs deleted file mode 100644 index 1277093d..00000000 --- a/corpus/real-world/arraypool-clear-past-length/after.cs +++ /dev/null @@ -1,21 +0,0 @@ -// AFTER (fixed). Every length/count argument is bound to the logical length `n`, -// not the oversized `buf.Length`: `buf.AsSpan(0, n)` views only the valid payload -// and `Array.Clear(buf, 0, n)` clears only it. The `[n, Length)` tail is never -// touched, so the extractor emits no `overspan` fact and the checker is silent. -using System; -using System.Buffers; - -static class PoolClearPastLength -{ - static void Roundtrip(int n) - { - byte[] buf = ArrayPool.Shared.Rent(n); - Fill(buf, n); - Emit(buf.AsSpan(0, n)); // bounded by the rented length n - Array.Clear(buf, 0, n); // clears only the logical [0, n) - ArrayPool.Shared.Return(buf); - } - - static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } - static void Emit(ReadOnlySpan data) { } -} diff --git a/corpus/real-world/arraypool-clear-past-length/before.cs b/corpus/real-world/arraypool-clear-past-length/before.cs deleted file mode 100644 index 10da2b85..00000000 --- a/corpus/real-world/arraypool-clear-past-length/before.cs +++ /dev/null @@ -1,28 +0,0 @@ -// BEFORE (buggy). POOL005, the `.Length` spelling of the over-read / over-clear. -// A rented array is OVERSIZED: `ArrayPool.Shared.Rent(n)` returns an array of -// `Length >= n`. This code uses `buf.Length` — the oversized backing length — as -// the operative length instead of the rented `n`: `buf.AsSpan(0, buf.Length)` -// hands off the stale `[n, Length)` tail (a previous renter's bytes), and -// `Array.Clear(buf, 0, buf.Length)` clears past `n` into that tail. The fix is to -// bound by the logical length `n` (`buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`, -// see after.cs). Representative of the pattern, 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 PoolClearPastLength -{ - static void Roundtrip(int n) - { - byte[] buf = ArrayPool.Shared.Rent(n); - Fill(buf, n); // valid payload is buf[0..n] - Emit(buf.AsSpan(0, buf.Length)); // <-- BUG: length is buf.Length, not n -> stale tail - Array.Clear(buf, 0, buf.Length); // <-- BUG: clears past n into the pooled tail - ArrayPool.Shared.Return(buf); - } - - static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } - static void Emit(ReadOnlySpan data) { } -} diff --git a/corpus/real-world/arraypool-clear-past-length/case.own b/corpus/real-world/arraypool-clear-past-length/case.own deleted file mode 100644 index afa1e151..00000000 --- a/corpus/real-world/arraypool-clear-past-length/case.own +++ /dev/null @@ -1,18 +0,0 @@ -// OwnLang model of the POOL005 `.Length` over-read / over-clear. `acquire` == -// ArrayPool.Rent (oversized: Length >= n), `release` == ArrayPool.Return. -// `overspan buf` models using the buffer's OWN oversized `.Length` as the -// operative length — `buf.AsSpan(0, buf.Length)` / `Array.Clear(buf, 0, buf.Length)` -// — which reaches past the rented `n` into the stale tail. Bounding by `n` takes no -// full view, so the fixed code has no `overspan` and is silent. -> OWN025. The -// buffer is still returned, so there is no leak (OWN001). -module Corpus -resource Buffer { - acquire rent - release give - kind "pooled buffer" -} -fn roundtrip(n: int) { - let buf = acquire Buffer(n); // ArrayPool.Rent (Length >= n) - overspan buf; // buf.AsSpan(0, buf.Length) / Array.Clear(buf, 0, buf.Length) -> OWN025 - release buf; // ArrayPool.Return -} diff --git a/corpus/real-world/arraypool-clear-past-length/notes.md b/corpus/real-world/arraypool-clear-past-length/notes.md deleted file mode 100644 index 96bec428..00000000 --- a/corpus/real-world/arraypool-clear-past-length/notes.md +++ /dev/null @@ -1,30 +0,0 @@ -# ArrayPool over-read / over-clear — the `.Length` spelling (POOL005) - -**Pattern:** a pooled array from `ArrayPool.Shared.Rent(n)` is *oversized* -(`Length >= n`). Code that uses `buf.Length` — the oversized backing length — as -the operative length, rather than the rented `n`, reaches past the valid payload -into the stale `[n, Length)` tail a previous renter left: - -- `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)` — an over-**read** - (the consumer sees `n` valid bytes plus the stale tail: a wrong-length read and a - potential information disclosure); -- `Array.Clear(buf, 0, buf.Length)` — an over-**clear** (touches the pool's tail - past the data that was actually written). - -The fix is to bound by the logical length: `buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`. - -This is the `.Length` sibling of `arraypool-fullspan-overread` (which catches the -unbounded `buf.AsSpan()`): same OWN025, a different way of writing the oversized -length. The extractor recognises the `.Length` argument on the buffer's own view / -`Array.Clear` (resolved BCL symbols) and emits an `overspan` fact. - -**What the checker says:** **OWN025** `[resource: pooled buffer]` at each over-reach -site. The buffer is still `Return`ed, so there is no OWN001 leak. - -**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. The -single-arg `Array.Clear(buf)` (a deliberate whole-buffer wipe) is intentionally not -flagged — only the explicit oversized `buf.Length` count is. - -Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target -AiDotNet.Tensors pooled-buffer over-clear/over-read. diff --git a/corpus/real-world/arraypool-length-overread/after.cs b/corpus/real-world/arraypool-length-overread/after.cs new file mode 100644 index 00000000..8f1c0de9 --- /dev/null +++ b/corpus/real-world/arraypool-length-overread/after.cs @@ -0,0 +1,20 @@ +// AFTER (fixed). The view is bound to the logical length `n` — `buf.AsSpan(0, n)` — +// so only the `n` valid payload bytes are read; the oversized `[n, Length)` tail is +// never touched. No `.Length`-spelled view remains, so the extractor emits no +// `overspan` fact and the checker is silent. +using System; +using System.Buffers; + +static class PoolLengthOverread +{ + static void Frame(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); + Emit(buf.AsSpan(0, n)); // bounded by the rented length n + ArrayPool.Shared.Return(buf); + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-length-overread/before.cs b/corpus/real-world/arraypool-length-overread/before.cs new file mode 100644 index 00000000..0c7d64c1 --- /dev/null +++ b/corpus/real-world/arraypool-length-overread/before.cs @@ -0,0 +1,29 @@ +// BEFORE (buggy). POOL005, the `.Length` spelling of the over-read. A rented array +// is OVERSIZED: `ArrayPool.Shared.Rent(n)` returns an array of `Length >= n`. +// Viewing it with `buf.Length` — the oversized backing length — as the bound, +// `buf.AsSpan(0, buf.Length)`, spans the WHOLE array, so a consumer reads the `n` +// valid bytes PLUS the stale `[n, Length)` tail a previous renter left: a wrong- +// length read and an information disclosure. The fix is `buf.AsSpan(0, n)` (after.cs). +// +// Note: an over-CLEAR like `Array.Clear(buf, 0, buf.Length)` is deliberately NOT +// flagged — it only overwrites the pooled tail with zeros (a safe clear-before-Return +// idiom) and exposes nothing. The bug is READING/COPYING the tail, which the view +// spelling does. +// +// Wrapped in a class so the extractor's per-class flow pass visits it; helpers stubbed. +using System; +using System.Buffers; + +static class PoolLengthOverread +{ + static void Frame(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); // valid payload is buf[0..n] + Emit(buf.AsSpan(0, buf.Length)); // <-- BUG: length is buf.Length, not n -> reads the stale tail + ArrayPool.Shared.Return(buf); + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-length-overread/case.own b/corpus/real-world/arraypool-length-overread/case.own new file mode 100644 index 00000000..6f57fcd5 --- /dev/null +++ b/corpus/real-world/arraypool-length-overread/case.own @@ -0,0 +1,17 @@ +// OwnLang model of the POOL005 `.Length` over-read. `acquire` == ArrayPool.Rent +// (oversized: Length >= n), `release` == ArrayPool.Return. `overspan buf` models a +// view whose length is the buffer's OWN oversized `.Length` (`buf.AsSpan(0, buf.Length)`), +// which spans the whole array — a consumer reads past the rented `n` into the stale +// tail. Bounding by `n` takes no full view, so the fix has no `overspan` and is silent. +// -> OWN025. The buffer is still returned, so there is no leak (OWN001). +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(0, buf.Length) — spans the whole array -> OWN025 + release buf; // ArrayPool.Return +} diff --git a/corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt b/corpus/real-world/arraypool-length-overread/expected-diagnostics.txt similarity index 100% rename from corpus/real-world/arraypool-clear-past-length/expected-diagnostics.txt rename to corpus/real-world/arraypool-length-overread/expected-diagnostics.txt diff --git a/corpus/real-world/arraypool-length-overread/notes.md b/corpus/real-world/arraypool-length-overread/notes.md new file mode 100644 index 00000000..117f44cf --- /dev/null +++ b/corpus/real-world/arraypool-length-overread/notes.md @@ -0,0 +1,28 @@ +# ArrayPool over-read — the `.Length` spelling (POOL005) + +**Pattern:** a pooled array from `ArrayPool.Shared.Rent(n)` is *oversized* +(`Length >= n`). A view that uses `buf.Length` — the oversized backing length — as +its bound (`buf.AsSpan(0, buf.Length)`, `new Span(buf, 0, buf.Length)`) spans the +whole array, so reading or copying through it processes the `n` valid bytes **plus** +the stale `[n, Length)` tail a previous renter left: a wrong-length read and a +potential information disclosure. The fix is to bound by the logical length: +`buf.AsSpan(0, n)`. + +This is the `.Length` sibling of `arraypool-fullspan-overread` (which catches the +unbounded `buf.AsSpan()`): same OWN025, a different way of writing the oversized +length. The extractor recognises the `.Length`-as-length argument on the buffer's +own view (start `0`, resolved BCL symbols) and emits an `overspan` fact. + +**Not flagged: the over-clear.** `Array.Clear(buf, 0, buf.Length)` (and the single-arg +`Array.Clear(buf)`) only *overwrite* the pooled tail with zeros — a safe +clear-before-`Return` idiom that exposes nothing. POOL005 is about *reading/copying* +too much, not *writing* too much (Codex review); only the **view** is flagged. + +**What the checker says:** **OWN025** `[resource: pooled buffer]` at the view. The +buffer is still `Return`ed, so there is no OWN001 leak. + +**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); replay target +AiDotNet.Tensors pooled-buffer over-read. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 308ac483..9f6821f3 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -12,9 +12,11 @@ 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 s = buf.AsSpan();`) (corpus - `arraypool-fullspan-overread`) — and the **`.Length` spelling** too (`buf.AsSpan(0, buf.Length)`, - `Array.Clear(buf, 0, buf.Length)`, where the oversized self-`.Length` is the operative length; - corpus `arraypool-clear-past-length`). **POOL003 (double-return → OWN003) is built** for ArrayPool + `arraypool-fullspan-overread`) — and the **`.Length` view spelling** too (`buf.AsSpan(0, buf.Length)` + / `new Span(buf, 0, buf.Length)`, where the oversized self-`.Length` is the bound; corpus + `arraypool-length-overread`). A *write*/wipe like `Array.Clear(buf, 0, buf.Length)` is deliberately + NOT flagged — it zeros the tail (a safe clear-before-`Return`) and exposes nothing; only a + 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.Rent` `IMemoryOwner` is released by Dispose, so its leak / double-dispose / use-after-dispose ride the same flow as POOL001/002/003 (corpus @@ -51,7 +53,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`/`Dispose` reachable twice for the same buffer (ArrayPool *and* MemoryPool) | `OWN003` ✅ | | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` | -| **POOL005** clear/copy past length | a full-length view (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`) reads/copies/clears beyond the logical length | `OWN025` `[resource: pooled buffer]` ✅ (a view stored in a FIELD next) | +| **POOL005** read/copy past length | a full-length **view** (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`) reads/copies beyond the logical length (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is NOT flagged — it exposes nothing) | `OWN025` `[resource: pooled buffer]` ✅ (a view stored in a FIELD next) | Resource mapping: diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index e449baa3..ff5357d2 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -808,25 +808,23 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet tracked, Semanti EmitOverspans(expr, tracked, model, nodes); } -// POOL005: emit one `overspan` op per tracked pooled buffer that `expr` reaches past the rented -// length of — the core raises OWN025. Two over-reach shapes: a FULL-LENGTH view (`buf.AsSpan()` with -// no bound, or `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)` whose length is the -// oversized self-`.Length`), and an over-clear (`Array.Clear(buf, 0, buf.Length)`). Walks the whole -// expression so a view nested in a call (`Sink.Write(buf.AsSpan())`), a chain +// POOL005: emit one `overspan` op per tracked pooled buffer that `expr` takes a FULL-LENGTH VIEW of +// — the core raises OWN025. The view spans the whole oversized array (`buf.AsSpan()` with no bound, +// or `buf.AsSpan(0, buf.Length)` / `new Span(buf, 0, buf.Length)` whose length is the oversized +// self-`.Length`), so reading or copying through it processes the stale `[n, Length)` tail. 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()...`) is -// found; a view bounded to the real `n` (`buf.AsSpan(0, n)`) is not matched. Among `tracked` locals -// only pooled buffers are the arrays the BCL AsSpan/Span/Array.Clear symbols bind to, so this never -// fires on a tracked IDisposable / factory result. Shared by the expression-statement and -// local-declaration lowering paths. +// found; a view bounded to the real `n` (`buf.AsSpan(0, n)`) is not matched. Only the VIEW is +// flagged, not a write/wipe: `Array.Clear(buf, 0, buf.Length)` merely overwrites the pooled tail +// (a safe clear-before-Return idiom), it does not expose stale bytes (Codex review). 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-decl paths. static void EmitOverspans(ExpressionSyntax expr, HashSet tracked, SemanticModel model, List nodes) { var overspanned = new SortedSet(StringComparer.Ordinal); foreach (var node in expr.DescendantNodesAndSelf().OfType()) - { - var owner = FullViewOwner(node, model) ?? ArrayClearOverOwner(node, model); - if (owner is not null && tracked.Contains(owner)) + 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) }); } @@ -952,9 +950,11 @@ e is InvocationExpressionSyntax i { var args = inv.ArgumentList.Arguments; // `buf.AsSpan()` (no bound) spans the whole array; so does `buf.AsSpan(0, buf.Length)`, - // whose length argument is the buffer's OWN oversized `.Length` (the `.Length` spelling). + // whose length argument is the buffer's OWN oversized `.Length` (the `.Length` spelling). The + // start must be 0 — `buf.AsSpan(k, buf.Length)` for k != 0 is out of range, not this pattern. if (args.Count == 0 - || (args.Count == 2 && IsLengthOf(args[1].Expression, recv.Identifier.Text))) + || (args.Count == 2 && IsZeroInt(args[0].Expression, model) + && IsLengthOf(args[1].Expression, recv.Identifier.Text))) return recv.Identifier.Text; } if (e is BaseObjectCreationExpressionSyntax oc @@ -964,10 +964,11 @@ e is InvocationExpressionSyntax i { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct } && IsInNamespace(sct, "System")) { - // `new Span(buf)` (whole array) or `new Span(buf, 0, buf.Length)` (length is the + // `new Span(buf)` (whole array) or `new Span(buf, 0, buf.Length)` (start 0, length the // oversized self-length). if (al.Arguments.Count == 1 - || (al.Arguments.Count == 3 && IsLengthOf(al.Arguments[2].Expression, arg.Identifier.Text))) + || (al.Arguments.Count == 3 && IsZeroInt(al.Arguments[1].Expression, model) + && IsLengthOf(al.Arguments[2].Expression, arg.Identifier.Text))) return arg.Identifier.Text; } return null; @@ -980,23 +981,11 @@ static bool IsLengthOf(ExpressionSyntax arg, string owner) => Expression: IdentifierNameSyntax id } && id.Identifier.Text == owner; -// Array.Clear(buf, 0, buf.Length) — clears the WHOLE oversized backing array, past the rented -// length (POOL005 over-clear). Returns the buffer name; Array.Clear(buf, 0, n) with a real bound -// returns null. The single-arg Array.Clear(buf) is intentionally NOT matched — wiping the whole -// buffer is a common, safe idiom; only the explicit oversized `.Length` count is flagged. -static string? ArrayClearOverOwner(ExpressionSyntax? e, SemanticModel model) -{ - if (e is not InvocationExpressionSyntax inv - || model.GetSymbolInfo(inv).Symbol is not IMethodSymbol - { Name: "Clear", ContainingType: { Name: "Array" } act } - || !IsInNamespace(act, "System")) - return null; - var args = inv.ArgumentList.Arguments; - return args.Count == 3 - && args[0].Expression is IdentifierNameSyntax buf - && IsLengthOf(args[2].Expression, buf.Identifier.Text) - ? buf.Identifier.Text : null; -} +// `arg` is the constant `0` — the start/index of a `.Length`-spelled view (`buf.AsSpan(0, buf.Length)`) +// so the view spans the WHOLE array, not an interior slice. Resolved via the constant value, so a +// `const`, `0x0`, etc. all count. +static bool IsZeroInt(ExpressionSyntax arg, SemanticModel model) => + model.GetConstantValue(arg) is { HasValue: true, Value: int v } && v == 0; // If `idn` references a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW local declared from an owner // buffer (`Memory view = owner.AsMemory(…)`), the owner buffer's local name — so a use of the diff --git a/spec/BufferPolicies.md b/spec/BufferPolicies.md index a07341df..6d91e0d7 100644 --- a/spec/BufferPolicies.md +++ b/spec/BufferPolicies.md @@ -39,18 +39,20 @@ inline = 256)`. The namespace is `Buffer`; the method selects the mode. - **B7 — requested length preserved.** `scratch` lowering preserves the *requested* logical length, independent of whether the stack or pool branch is taken. -- **B9 — operations stay within the logical length.** A pooled buffer is - *oversized*: `ArrayPool.Rent(n)` returns an array of `Length >= n`, not - exactly `n`. An operation that reaches the whole backing array rather than the - requested `n` touches the stale `[n, Length)` tail (a previous renter's bytes); - reading or copying through it is an over-read / over-copy → **OWN025**. Two - spellings: a FULL-length **view** with no bound (`buf.AsSpan()` / `buf.AsMemory()` - / `new Span(buf)`), and the **`.Length`** form that passes the buffer's own - oversized `.Length` as the operative length (`buf.AsSpan(0, buf.Length)`, - `new Span(buf, 0, buf.Length)`, `Array.Clear(buf, 0, buf.Length)`). The fix is - to bound by `n`: `buf.AsSpan(0, n)`, `Array.Clear(buf, 0, n)`. (P-007 POOL005; the - OwnLang model op is `overspan b`. Distinct from B6/OWN024, which is clearing *too - little* of a sensitive buffer — this is touching *too much*.) +- **B9 — a view stays within the logical length.** A pooled buffer is *oversized*: + `ArrayPool.Rent(n)` returns an array of `Length >= n`, not exactly `n` (and + `MemoryPool.Rent(n)` likewise wraps an oversized backing, exposed via + `.Memory.Length`). A **view** that spans the whole backing array rather than the + requested `n` — a FULL-length view with no bound (`buf.AsSpan()` / `buf.AsMemory()` + / `new Span(buf)`), or the **`.Length`** form that passes the buffer's own + oversized `.Length` as the length (`buf.AsSpan(0, buf.Length)`, + `new Span(buf, 0, buf.Length)`) — exposes the stale `[n, Length)` tail (a + previous renter's bytes); reading or copying through it is an over-read / over-copy + → **OWN025**. The fix is to bound by `n`: `buf.AsSpan(0, n)`. Only a *read*-capable + view is flagged: a *write*/wipe such as `Array.Clear(buf, 0, buf.Length)` merely + zeros the tail (a safe clear-before-`Return` idiom) and exposes nothing. (P-007 + POOL005; the OwnLang model op is `overspan b`. Distinct from B6/OWN024, which is + clearing *too little* of a sensitive buffer — this is *reading* too much.) ## Buffer options and `policy` blocks