From e67ad628125470077736f23128526b447902ea68 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 25 Jun 2026 15:50:08 +0000 Subject: [PATCH 1/5] docs: correct stale POOL002/P-007 status (it shipped, ROADMAP lagged) ROADMAP.md still listed "POOL002 next" and P-007 as draft, but POOL002 (view-after-return -> OWN002), POOL003 (double-return) and POOL005 (full-length over-read) are built and pinned by corpus (arraypool-span-view-after-return et al.). Update the three ROADMAP spots and the proposals index to match the verified reality. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- docs/ROADMAP.md | 10 ++++++++-- docs/proposals/README.md | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index 0d6f0cba..aa2a633b 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -100,7 +100,8 @@ architectural strictness, and the borrow-checker showcase): 4. `DI001` — singleton captures a scoped dependency ✅ (core check + C# registration-graph extractor built; end-to-end on real C#) 5. `POOL001` — `ArrayPool` buffer `Rent`ed but never `Return`ed ✅ - (`POOL002` `Span`/view used after `Return` next) + (`POOL002` `Span`/view used after `Return` ✅; `POOL003` double-return, + `POOL005` full-length over-read built too — see P-007) ### Milestones @@ -151,6 +152,11 @@ architectural strictness, and the borrow-checker showcase): root-`GetService` form of DI003, and the consuming-constructor anchor. 4. **Pool/Span** — `Rent`/`Return`, borrowed views, return-invalidates-views, known-bug replay corpus (P-007). The borrow checker on stage at full height. + ◑ *In progress* — POOL001 (leak), POOL002 (view-after-return → OWN002), + POOL003 (double-return/dispose, ArrayPool *and* MemoryPool) built end to end; + POOL004 (view escape) and POOL005 (full-length over-read) first slices built. + Remaining: POOL005 view stored in a FIELD, deeper POOL004 escape, and the + real-world replay targets (dotnet/runtime, Nethermind, AiDotNet.Tensors). 5. **Effects** — `pure` / `use !Db` / `use !Log` / `use Clock`, layer policies (P-008). The architectural X-ray — landed *after* the leak checkers prove value. @@ -219,7 +225,7 @@ own scan. Label them as estimates wherever they appear. | [P-004](proposals/P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | P0 | in progress (WPF001–005 built) | | [P-005](proposals/P-005-idisposable-ownership.md) | `IDisposable` ownership profile | P0 | draft | | [P-006](proposals/P-006-di-lifetimes.md) | DI lifetime / captive dependency | P0 | in progress (DI001 end-to-end: core + extractor) | -| [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | draft | +| [P-007](proposals/P-007-arraypool-span.md) | ArrayPool / Span borrow-view | P1 | in progress (POOL001–003 built; 004/005 first slices) | | [P-008](proposals/P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | P1/P2 | draft | | [P-009](proposals/P-009-nogc-regions.md) | No-GC / allocation-free regions | horizon | draft | | [P-010](proposals/P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | P2/horizon | draft | diff --git a/docs/proposals/README.md b/docs/proposals/README.md index 41cd183b..4ea230c8 100644 --- a/docs/proposals/README.md +++ b/docs/proposals/README.md @@ -28,7 +28,7 @@ proposal is marked `done` with a pointer. | [P-004](P-004-wpf-lifetime-profile.md) | WPF / UI lifetime leak profile | draft | | [P-005](P-005-idisposable-ownership.md) | `IDisposable` ownership profile | draft | | [P-006](P-006-di-lifetimes.md) | DI lifetime / captive dependency | draft | -| [P-007](P-007-arraypool-span.md) | ArrayPool / Span borrow-view | draft | +| [P-007](P-007-arraypool-span.md) | ArrayPool / Span borrow-view | in progress (POOL001–003 built; 004/005 first slices) | | [P-008](P-008-effects-and-resources.md) | Effects & resources (`Own.Effects`) | draft | | [P-009](P-009-nogc-regions.md) | No-GC / allocation-free regions | draft | | [P-010](P-010-type-disciplines.md) | Richer type disciplines (`Own.Types`) | draft | From a4fbc1ec5db02d9c36a94751a7d88088f945c2d4 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 25 Jun 2026 16:05:36 +0000 Subject: [PATCH 2/5] feat(pool): POOL005 over-read of a pooled byte[] FIELD viewed full-length MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The path-sensitive flow pass only tracks pooled buffers held in LOCALS, so a buffer Rent'ed into a FIELD (`_buf = ArrayPool.Shared.Rent(n)`) and viewed full-length in a LATER member over-reads the oversized [n, Length) tail with no diagnostic. Add a class-level POOL005 field pass to the extractor: - collect the fields a class Rents (shared IsPoolRent — aliased pool receiver binds, a non-pool `.Rent` does not); - for each member that takes a full-length view of such a field — `_buf.AsSpan()` / `this._buf.AsMemory()` / `new Span(_buf)` / the `.Length` spelling, the receiver resolved through the this/bare ThisFieldName shape and the over-read recognised by the same resolved System.MemoryExtensions / System.Span BCL symbols as the local path — emit a synthetic acquire/overspan/release flow so the existing OwnIR bridge raises OWN025 at the view. No new diagnostic, no new core code (the synthetic-flow trick the field-UAF / MemoryPool slices use). A write/wipe (`Array.Clear(_buf, 0, _buf.Length)`) is not a view, so it is not flagged — only a read-capable VIEW is the over-read. Corpus `arraypool-field-fullspan-overread` (before/after/case.own/notes) pins it; case.own (the core OWN025 verdict) is validated by the Python-only test_corpus suite here, the field-vs-local extraction by the dotnet corpus-benchmark CI job. Bump --min-recall 23 -> 24 to pin the newly-caught case and strike the "ArrayPool byte[]-buffer-field view" item from the benchmark backlog. P-007 / ROADMAP updated; the remaining POOL005 frontier is a view stored INTO another field. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- .github/workflows/ci.yml | 6 +- .../after.cs | 29 +++++ .../before.cs | 36 +++++++ .../case.own | 22 ++++ .../expected-diagnostics.txt | 1 + .../notes.md | 42 ++++++++ docs/ROADMAP.md | 7 +- docs/proposals/P-007-arraypool-span.md | 11 +- frontend/roslyn/OwnSharp.Extractor/Program.cs | 102 ++++++++++++++++++ 9 files changed, 249 insertions(+), 7 deletions(-) create mode 100644 corpus/real-world/arraypool-field-fullspan-overread/after.cs create mode 100644 corpus/real-world/arraypool-field-fullspan-overread/before.cs create mode 100644 corpus/real-world/arraypool-field-fullspan-overread/case.own create mode 100644 corpus/real-world/arraypool-field-fullspan-overread/expected-diagnostics.txt create mode 100644 corpus/real-world/arraypool-field-fullspan-overread/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 13d0ed60..3610f9fd 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1106,7 +1106,9 @@ jobs: # — lowered to a synthetic acquire/release/use flow -> OWN002. That pass also covers POOLED owners: # an `IMemoryOwner` field released in `Dispose()` and a `Memory` VIEW field of it (`_view = # _owner.Memory`) read in such a handler is the view-in-a-field dangle -> OWN002 (`pooled-view-after- - # dispose`). Remaining backlog: an ArrayPool `byte[]`-buffer-field view, a TWO-plus-hop indirect field + # dispose`). The POOL005 field pass now also catches a full-length view of an ArrayPool `byte[]` + # buffer FIELD read past its logical length -> OWN025 (`arraypool-field-fullspan-overread`). + # Remaining backlog: a full-length view STORED into another field, a TWO-plus-hop indirect field # use, and an injected-source region-escape. A drop below the floor is a regression. - run: python scripts/benchmark.py --min-recall 23 + run: python scripts/benchmark.py --min-recall 24 diff --git a/corpus/real-world/arraypool-field-fullspan-overread/after.cs b/corpus/real-world/arraypool-field-fullspan-overread/after.cs new file mode 100644 index 00000000..dff48fed --- /dev/null +++ b/corpus/real-world/arraypool-field-fullspan-overread/after.cs @@ -0,0 +1,29 @@ +// AFTER (fixed). The full-length view of the pooled field 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. With no unbounded view (and no +// `.Length`-spelled view) over the field, the extractor emits no `overspan` fact and +// the checker is silent. +using System; +using System.Buffers; + +sealed class FieldPoolFramer : IDisposable +{ + private byte[] _buf; + private int _n; + + public void Capture(int n) + { + _n = n; + _buf = ArrayPool.Shared.Rent(n); + Fill(_buf, n); + } + + public byte[] Flush() + { + return _buf.AsSpan(0, _n).ToArray(); // bounded view: only the logical [0, n) + } + + public void Dispose() => ArrayPool.Shared.Return(_buf); + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } +} diff --git a/corpus/real-world/arraypool-field-fullspan-overread/before.cs b/corpus/real-world/arraypool-field-fullspan-overread/before.cs new file mode 100644 index 00000000..6b225ef7 --- /dev/null +++ b/corpus/real-world/arraypool-field-fullspan-overread/before.cs @@ -0,0 +1,36 @@ +// BEFORE (buggy). The FIELD twin of the ArrayPool "full-length view over-read" +// bug (P-007 POOL005). A pooled array is rented into a FIELD — `_buf = +// ArrayPool.Shared.Rent(n)` — so the oversized buffer (`Length >= n`) outlives +// the method that filled it. A LATER member then takes a FULL-length view of the +// field (`_buf.AsSpan()`, no length bound) and reads through it, so the `n` valid +// bytes are processed together with the stale `[n, Length)` tail a *previous* +// renter left behind: a wrong-length read and an information disclosure. The +// per-method flow pass only tracks LOCAL rents, so this field-backed over-read is +// out of its reach; the field pass catches it. The fix is a bounded view, +// `_buf.AsSpan(0, _n)` (see after.cs). Representative of the pattern (a pooled +// scratch field viewed full-length on flush/serialize), not verbatim from one PR. +using System; +using System.Buffers; + +sealed class FieldPoolFramer : IDisposable +{ + private byte[] _buf; + private int _n; + + public void Capture(int n) + { + _n = n; + _buf = ArrayPool.Shared.Rent(n); // pooled buffer stored in a FIELD (Length >= n) + Fill(_buf, n); // valid payload is _buf[0..n] + } + + public byte[] Flush() + { + return _buf.AsSpan().ToArray(); // <-- BUG: full-length view of the pooled FIELD, + // n payload bytes + the stale [n, Length) tail + } + + public void Dispose() => ArrayPool.Shared.Return(_buf); // class-wide Return: no leak + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } +} diff --git a/corpus/real-world/arraypool-field-fullspan-overread/case.own b/corpus/real-world/arraypool-field-fullspan-overread/case.own new file mode 100644 index 00000000..4c6789c5 --- /dev/null +++ b/corpus/real-world/arraypool-field-fullspan-overread/case.own @@ -0,0 +1,22 @@ +// OwnLang model of the ArrayPool full-length view over-read on a FIELD-backed pooled +// buffer. `acquire` == ArrayPool.Rent into a field (the array is OVERSIZED: +// Length >= n), `release` == ArrayPool.Return (here in Dispose, class-wide). +// `overspan buf` models a FULL-length view `_buf.AsSpan()` (no length bound) taken +// in a LATER member and read through — 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. `.own` has no fields/members, so +// this single-function reduction pins the same core verdict the field pass produces; +// the field-vs-local distinction lives in before.cs/after.cs (checked end to end by +// the dotnet benchmark). The checker trips OWN025 (POOL005) at the view; the buffer +// is still 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 capture_then_flush(n: int) { + let buf = acquire Buffer(n); // _buf = ArrayPool.Rent(n) (Length >= n) + overspan buf; // _buf.AsSpan() in a later member — full view past n -> OWN025 + release buf; // ArrayPool.Return (Dispose) +} diff --git a/corpus/real-world/arraypool-field-fullspan-overread/expected-diagnostics.txt b/corpus/real-world/arraypool-field-fullspan-overread/expected-diagnostics.txt new file mode 100644 index 00000000..511ccfa9 --- /dev/null +++ b/corpus/real-world/arraypool-field-fullspan-overread/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN025 diff --git a/corpus/real-world/arraypool-field-fullspan-overread/notes.md b/corpus/real-world/arraypool-field-fullspan-overread/notes.md new file mode 100644 index 00000000..1beb6b6e --- /dev/null +++ b/corpus/real-world/arraypool-field-fullspan-overread/notes.md @@ -0,0 +1,42 @@ +# ArrayPool full-length view over-read on a FIELD-backed buffer (POOL005, field) + +**Pattern:** the FIELD twin of [`arraypool-fullspan-overread`](../arraypool-fullspan-overread/notes.md). +A pooled array from `ArrayPool.Shared.Rent(n)` is *oversized* — `Length >= n`, not +exactly `n`. Here it is rented into a **field** (`_buf = ArrayPool.Shared.Rent(n)`) +in one member and viewed full-length in a **later** member (`_buf.AsSpan()`, +`this._buf.AsMemory()`, `new Span(_buf)`, or the `.Length` spelling +`_buf.AsSpan(0, _buf.Length)`). Reading or copying through that unbounded view +processes the `n` valid bytes **plus** the stale `[n, Length)` tail a *previous* +renter left behind — a correctness bug (wrong length) and an information disclosure. +The fix is a bounded view: `_buf.AsSpan(0, _n)`. + +**Why a separate case.** The path-sensitive flow detector only tracks pooled buffers +held in **locals**, so a field-backed rent — rented in one member, viewed in another — +is out of its reach. The extractor's POOL005 **field pass** closes that gap: it +collects the fields a class `Rent`s (the shared `IsPoolRent`, so an aliased pool +receiver binds and a non-pool `.Rent` does not), and for each member that takes a +full-length view of such a field (receiver resolved through the `this`/bare +`ThisFieldName` shape, the over-read recognised by the same resolved +`System.MemoryExtensions` / `System.Span` BCL symbols as the local path) emits a +synthetic `acquire`/`overspan`/`release` flow so the core raises **OWN025** at the +view — no new diagnostic, the same synthetic-flow trick the field use-after-dispose +and MemoryPool slices use. A *write*/wipe (`Array.Clear(_buf, 0, _buf.Length)`) is not +a view, so it is deliberately **not** flagged — only a read-capable VIEW is the +over-read. + +**What the checker says:** OWN025 `[resource: pooled buffer]` at the view. The buffer +is still `Return`ed (in `Dispose`, found class-wide by the POOL001 field pass), 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 — `.own` has no +fields/members, so it pins the *core* OWN025 verdict the field pass produces, while +the field-vs-local distinction lives in `before.cs` / `after.cs` (scanned end to end +by the dotnet `corpus-benchmark` CI job). `before.cs` / `after.cs` are representative +of the bug and its fix, not a verbatim PR diff. v0 of the field pass fires on the +*first* full-length view of each pooled field per member (a read site); a full-length +view of a pooled field **stored into another field** and only read elsewhere is a +deeper alias-tracking frontier, left honest. + +Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target +AiDotNet.Tensors pooled-buffer over-clear/over-read. diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index aa2a633b..edc2abec 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -154,9 +154,10 @@ architectural strictness, and the borrow-checker showcase): known-bug replay corpus (P-007). The borrow checker on stage at full height. ◑ *In progress* — POOL001 (leak), POOL002 (view-after-return → OWN002), POOL003 (double-return/dispose, ArrayPool *and* MemoryPool) built end to end; - POOL004 (view escape) and POOL005 (full-length over-read) first slices built. - Remaining: POOL005 view stored in a FIELD, deeper POOL004 escape, and the - real-world replay targets (dotnet/runtime, Nethermind, AiDotNet.Tensors). + POOL004 (view escape) and POOL005 (full-length over-read, local **and** pooled + `byte[]` FIELD) first slices built. Remaining: a POOL005 view stored INTO another + field, deeper POOL004 escape, and the real-world replay targets (dotnet/runtime, + Nethermind, AiDotNet.Tensors). 5. **Effects** — `pure` / `use !Db` / `use !Log` / `use Clock`, layer policies (P-008). The architectural X-ray — landed *after* the leak checkers prove value. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 295e5792..d061fb2b 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -26,7 +26,14 @@ owner.Memory;` — which dangles after the implicit scope-exit dispose — is caught too: the flow desugars a tracked `using IMemoryOwner` declaration to `acquire; try { rest } finally { release }`, so the returned view is read after the release (**POOL004 → OWN002**; - corpus `memorypool-using-view-escape`). A POOL005 view stored in a FIELD is next + corpus `memorypool-using-view-escape`). **POOL005 now also covers a pooled `byte[]` FIELD** — a + buffer `Rent`ed into a field (`_buf = ArrayPool.Shared.Rent(n)`) and viewed full-length in a + LATER member (`_buf.AsSpan()` / `this._buf.AsMemory()` / `new Span(_buf)` / the `.Length` + spelling) over-reads the oversized `[n, Length)` tail; the per-method flow pass only tracks LOCAL + rents, so a class-level field pass collects the pooled fields (shared `IsPoolRent`) and emits a + synthetic `acquire`/`overspan`/`release` flow at the view → OWN025 (corpus + `arraypool-field-fullspan-overread`). A full-length view STORED into another field (read only + elsewhere) is the deeper alias-tracking frontier, left 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 @@ -58,7 +65,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** 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) | +| **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]` ✅ (local **and** pooled `byte[]` FIELD; a view stored-into-a-field next) | Resource mapping: diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 73873c4d..eaf51d13 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -1506,6 +1506,52 @@ static bool IsLengthOf(ExpressionSyntax arg, string owner) => static bool IsZeroInt(ExpressionSyntax arg, SemanticModel model) => model.GetConstantValue(arg) is { HasValue: true, Value: int v } && v == 0; +// The this/bare FIELD a FULL-LENGTH view spans, else null. The POOL005 FIELD twin of FullViewOwner: +// `_buf.AsSpan()` / `this._buf.AsMemory()` (no bound), `_buf.AsSpan(0, _buf.Length)` (the `.Length` +// spelling), `new Span(_buf)` / `new Span(_buf, 0, _buf.Length)` over a buffer the class held +// in a FIELD. The receiver is resolved through `ThisFieldName` (a bare `_buf` or `this._buf`, never +// `other._buf`), so a full-length view of a pooled FIELD — whose over-read the LOCAL-only flow pass +// never reaches — is found; the caller gates on the field actually being a pooled rent. Recognised by +// the SAME resolved BCL symbols as FullViewOwner (`System.MemoryExtensions` AsSpan/AsMemory, the +// `System.Span`/… constructor), so a project's own look-alike is not mistaken for the over-read. A +// view bounded to the real rented `n` (`_buf.AsSpan(0, n)`) returns null — it does not over-read. +static string? FullViewFieldOwner(ExpressionSyntax? e, SemanticModel model) +{ + if (e is InvocationExpressionSyntax inv + && inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text is "AsSpan" or "AsMemory" + && ThisFieldName(m.Expression) is { } recv + && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct } + && IsInNamespace(mct, "System")) + { + var args = inv.ArgumentList.Arguments; + if (args.Count == 0 + || (args.Count == 2 && IsZeroInt(args[0].Expression, model) + && IsFieldLengthOf(args[1].Expression, recv))) + return recv; + } + if (e is BaseObjectCreationExpressionSyntax oc + && oc.ArgumentList is { Arguments.Count: > 0 } al + && ThisFieldName(al.Arguments[0].Expression) is { } arg + && model.GetSymbolInfo(oc).Symbol is IMethodSymbol + { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct } + && IsInNamespace(sct, "System")) + { + if (al.Arguments.Count == 1 + || (al.Arguments.Count == 3 && IsZeroInt(al.Arguments[1].Expression, model) + && IsFieldLengthOf(al.Arguments[2].Expression, arg))) + return arg; + } + return null; +} + +// `arg` is the pooled FIELD's own `.Length` (`_buf.Length` / `this._buf.Length`) — the FIELD twin of +// IsLengthOf, resolving the `.Length` receiver through `ThisFieldName` so the this-qualified spelling +// counts and `other._buf.Length` does not. +static bool IsFieldLengthOf(ExpressionSyntax arg, string field) => + arg is MemberAccessExpressionSyntax { Name.Identifier.Text: "Length" } ma + && ThisFieldName(ma.Expression) == field; + // 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 @@ -2720,6 +2766,62 @@ or ImplicitObjectCreationExpressionSyntax } } + // POOL005 (field): a FULL-LENGTH view of a pooled FIELD — `_buf.AsSpan()` / `this._buf.AsMemory()` + // / `new Span(_buf)` / the `.Length` spelling (`_buf.AsSpan(0, _buf.Length)`) — over a buffer + // the class `Rent`ed into a FIELD (`_buf = ArrayPool.Shared.Rent(n)`). The pooled array is + // oversized (`Length >= n`), so a member that views the field full-length reads past the logical + // length `n` into the stale `[n, Length)` tail (a previous renter's bytes). The per-method flow + // pass only tracks LOCAL rents, so a FIELD-backed rent's over-read is unreached there; emit a + // synthetic acquire/overspan/release flow per such field so the existing OwnIR bridge raises + // OWN025 at the view — the synthetic-flow trick the field-UAF / MemoryPool slices use, no new + // diagnostic. The trailing `release` is synthetic (the real `Return` is class-wide, handled by + // the POOL001 field pass) and only keeps this one-function flow from reading as a leak. A + // write/wipe (`Array.Clear(_buf, 0, _buf.Length)`) is not a view, so FullViewFieldOwner returns + // null on it — only a read-capable VIEW is the over-read. Gated on --flow-locals like the rest of + // the synthetic-flow emission. + if (flowLocals) + { + // pooled FIELD -> the line it was `Rent`ed, via the shared IsPoolRent (an aliased pool + // receiver binds; a non-pool `.Rent` does not false-match). First rent line per field is + // enough to anchor the synthetic acquire. + var pooledFieldRent = new Dictionary(StringComparer.Ordinal); + foreach (var inv in cls.DescendantNodes().OfType()) + if (IsPoolRent(inv, model) + && inv.Parent is AssignmentExpressionSyntax asg + && FieldName(asg.Left) is { } pf + && !pooledFieldRent.ContainsKey(pf)) + pooledFieldRent[pf] = LineOf(inv); + if (pooledFieldRent.Count > 0) + foreach (var member in cls.Members) + { + // first full-length view of each pooled field in this member (one finding per field + // per member — repeated views of the same field do not multiply the diagnostic). + var seen = new HashSet(StringComparer.Ordinal); + var ops = new List(); + foreach (var node in member.DescendantNodes().OfType()) + if (FullViewFieldOwner(node, model) is { } fld + && pooledFieldRent.TryGetValue(fld, out var rentLine) + && seen.Add(fld)) + { + var vline = LineOf(node); + ops.Add(new { op = "acquire", var = fld, line = rentLine, kind = "pool" }); + ops.Add(new { op = "overspan", var = fld, line = vline }); + ops.Add(new { op = "release", var = fld, line = vline }); + } + if (ops.Count > 0) + { + var mname = member switch + { + MethodDeclarationSyntax md => md.Identifier.Text, + ConstructorDeclarationSyntax cd => cd.Identifier.Text, + PropertyDeclarationSyntax pd => pd.Identifier.Text, + _ => "member", + }; + flowFunctions.Add(new { name = $"{cls.Identifier.Text}.{mname}", file, body = ops }); + } + } + } + // WPF004: a `X.Subscribe(...)` whose IDisposable result is ignored — the // call stands as a bare statement (not assigned/returned/added), so the // token is dropped and never disposed. Member-access only (`x.Subscribe`), From 6ea5adfc058532f6ca45cad2c24d9ab67eeadd35 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 25 Jun 2026 16:10:28 +0000 Subject: [PATCH 3/5] fix(pool): restrict POOL005 field-rent collection to this instance (Codex) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `pooledFieldRent` collected the rent TARGET via `FieldName`, which accepts an arbitrary receiver (`other._buf = ArrayPool.Rent(n)`) and a bare local — so a class that rents into another object's `_buf` and separately full-spans its OWN same-named, non-pooled `_buf` would seed the set and trip a false OWN025. Switch to `ThisFieldName` (bare `_buf` / `this._buf`, never `other._buf`) — the same this-instance shape FullViewFieldOwner reads the view through, so the two halves agree and the cross-instance false positive is gone. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index eaf51d13..d948f606 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -2782,13 +2782,17 @@ or ImplicitObjectCreationExpressionSyntax if (flowLocals) { // pooled FIELD -> the line it was `Rent`ed, via the shared IsPoolRent (an aliased pool - // receiver binds; a non-pool `.Rent` does not false-match). First rent line per field is - // enough to anchor the synthetic acquire. + // receiver binds; a non-pool `.Rent` does not false-match). The rent TARGET is resolved + // through `ThisFieldName` — a bare `_buf` or `this._buf`, NEVER `other._buf` — the SAME + // this-instance shape FullViewFieldOwner reads the view through, so a rent into another + // object's field cannot seed `pooledFieldRent` and then false-match this class's own + // same-named (non-pooled) field at the view (Codex). First rent line per field is enough to + // anchor the synthetic acquire. var pooledFieldRent = new Dictionary(StringComparer.Ordinal); foreach (var inv in cls.DescendantNodes().OfType()) if (IsPoolRent(inv, model) && inv.Parent is AssignmentExpressionSyntax asg - && FieldName(asg.Left) is { } pf + && ThisFieldName(asg.Left) is { } pf && !pooledFieldRent.ContainsKey(pf)) pooledFieldRent[pf] = LineOf(inv); if (pooledFieldRent.Count > 0) From d3d817ad5b36b83fedc02288db37af1077315849 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 25 Jun 2026 16:19:31 +0000 Subject: [PATCH 4/5] =?UTF-8?q?fix(pool):=20POOL005=20field=20pass=20?= =?UTF-8?q?=E2=80=94=20handle=20initializers,=20scope=20to=20own=20type=20?= =?UTF-8?q?(CodeRabbit)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two correctness improvements to the POOL005 field over-read pass: - Field-declaration initializers (`byte[] _buf = ArrayPool.Shared.Rent(n);`) now seed `pooledFieldRent`, not just `_buf = Rent(...)` assignments — an idiomatic pooled-scratch-field shape that was previously missed (recall gap). - The pass is scoped to the class's OWN (direct) members: a `FirstAncestorOrSelf == cls` guard drops an assignment rent nested in an inner type, and the per-member loop skips `BaseTypeDeclarationSyntax` members, so a nested type's rents/views can no longer be mis-attributed to the outer class's synthetic flow. Not done: resolving the field receiver to an `IFieldSymbol` (CodeRabbit's symbol-binding suggestion). The codebase deliberately matches fields syntactically via `ThisFieldName` (documented at its definition — binding on the field's type is unreliable for the unresolved types the corpus depends on); `this._buf` is unambiguous and the bare-`_buf` residual matches every sibling field pass. Corpus `arraypool-field-fullspan-overread` now also exercises an initializer-rented field viewed via the `.Length` spelling (`_meta.AsSpan(0, _meta.Length)`), pinning both the new initializer seeding and the IsFieldLengthOf branch end to end in the dotnet benchmark; the fixed `after.cs` bounds both views and stays silent. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- .../after.cs | 28 ++++++++++--- .../before.cs | 39 ++++++++++++++----- .../notes.md | 24 +++++++----- frontend/roslyn/OwnSharp.Extractor/Program.cs | 31 +++++++++++---- 4 files changed, 91 insertions(+), 31 deletions(-) diff --git a/corpus/real-world/arraypool-field-fullspan-overread/after.cs b/corpus/real-world/arraypool-field-fullspan-overread/after.cs index dff48fed..17b6f5cc 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/after.cs +++ b/corpus/real-world/arraypool-field-fullspan-overread/after.cs @@ -1,8 +1,9 @@ -// AFTER (fixed). The full-length view of the pooled field 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. With no unbounded view (and no -// `.Length`-spelled view) over the field, the extractor emits no `overspan` fact and -// the checker is silent. +// AFTER (fixed). Every full-length view of a pooled field is BOUNDED to the logical +// length — `_buf.AsSpan(0, _n)` and `_meta.AsSpan(0, _metaLen)` — so only the valid +// payload bytes are read; the oversized `[len, Length)` tail is never touched. With +// no unbounded view (and no `.Length`-spelled view) over either field — the +// assignment-rented `_buf` or the initializer-rented `_meta` — the extractor emits +// no `overspan` fact and the checker is silent. using System; using System.Buffers; @@ -11,11 +12,17 @@ sealed class FieldPoolFramer : IDisposable private byte[] _buf; private int _n; + private const int MetaCap = 64; + private readonly byte[] _meta = ArrayPool.Shared.Rent(MetaCap); + private int _metaLen; + public void Capture(int n) { _n = n; _buf = ArrayPool.Shared.Rent(n); Fill(_buf, n); + _metaLen = 8; + Fill(_meta, _metaLen); } public byte[] Flush() @@ -23,7 +30,16 @@ public byte[] Flush() return _buf.AsSpan(0, _n).ToArray(); // bounded view: only the logical [0, n) } - public void Dispose() => ArrayPool.Shared.Return(_buf); + public byte[] FlushMeta() + { + return _meta.AsSpan(0, _metaLen).ToArray(); // bounded view: only the logical [0, _metaLen) + } + + public void Dispose() + { + ArrayPool.Shared.Return(_buf); + ArrayPool.Shared.Return(_meta); + } static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } } diff --git a/corpus/real-world/arraypool-field-fullspan-overread/before.cs b/corpus/real-world/arraypool-field-fullspan-overread/before.cs index 6b225ef7..0a1b0eec 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/before.cs +++ b/corpus/real-world/arraypool-field-fullspan-overread/before.cs @@ -1,12 +1,15 @@ // BEFORE (buggy). The FIELD twin of the ArrayPool "full-length view over-read" -// bug (P-007 POOL005). A pooled array is rented into a FIELD — `_buf = -// ArrayPool.Shared.Rent(n)` — so the oversized buffer (`Length >= n`) outlives -// the method that filled it. A LATER member then takes a FULL-length view of the -// field (`_buf.AsSpan()`, no length bound) and reads through it, so the `n` valid -// bytes are processed together with the stale `[n, Length)` tail a *previous* -// renter left behind: a wrong-length read and an information disclosure. The -// per-method flow pass only tracks LOCAL rents, so this field-backed over-read is -// out of its reach; the field pass catches it. The fix is a bounded view, +// bug (P-007 POOL005). A pooled array is rented into a FIELD — by assignment +// (`_buf = ArrayPool.Shared.Rent(n)`) OR a field initializer (`byte[] _meta = +// ArrayPool.Shared.Rent(MetaCap)`) — so the oversized buffer (`Length >= n`) +// outlives the method that filled it. A LATER member then takes a FULL-length +// view of the field and reads through it, so the `n` valid bytes are processed +// together with the stale `[n, Length)` tail a *previous* renter left behind: a +// wrong-length read and an information disclosure. Two view spellings are pinned: +// the bare `_buf.AsSpan()` over the assignment-rented field, and the `.Length` +// spelling `_meta.AsSpan(0, _meta.Length)` over the initializer-rented field. The +// per-method flow pass only tracks LOCAL rents, so these field-backed over-reads +// are out of its reach; the field pass catches them. The fix is a bounded view, // `_buf.AsSpan(0, _n)` (see after.cs). Representative of the pattern (a pooled // scratch field viewed full-length on flush/serialize), not verbatim from one PR. using System; @@ -17,11 +20,19 @@ sealed class FieldPoolFramer : IDisposable private byte[] _buf; private int _n; + // a SECOND pooled buffer, rented in the FIELD INITIALIZER (not an assignment) and viewed full-length + // below via the `.Length` spelling — exercises the field-initializer rent + the IsFieldLengthOf branch. + private const int MetaCap = 64; + private readonly byte[] _meta = ArrayPool.Shared.Rent(MetaCap); // Length >= MetaCap + private int _metaLen; + public void Capture(int n) { _n = n; _buf = ArrayPool.Shared.Rent(n); // pooled buffer stored in a FIELD (Length >= n) Fill(_buf, n); // valid payload is _buf[0..n] + _metaLen = 8; + Fill(_meta, _metaLen); // valid payload is _meta[0.._metaLen] } public byte[] Flush() @@ -30,7 +41,17 @@ public byte[] Flush() // n payload bytes + the stale [n, Length) tail } - public void Dispose() => ArrayPool.Shared.Return(_buf); // class-wide Return: no leak + public byte[] FlushMeta() + { + return _meta.AsSpan(0, _meta.Length).ToArray(); // <-- BUG (`.Length` spelling): the WHOLE + // oversized array, past _metaLen + } + + public void Dispose() + { + ArrayPool.Shared.Return(_buf); // class-wide Return: no leak + ArrayPool.Shared.Return(_meta); + } static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } } diff --git a/corpus/real-world/arraypool-field-fullspan-overread/notes.md b/corpus/real-world/arraypool-field-fullspan-overread/notes.md index 1beb6b6e..2da86869 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/notes.md +++ b/corpus/real-world/arraypool-field-fullspan-overread/notes.md @@ -13,15 +13,21 @@ The fix is a bounded view: `_buf.AsSpan(0, _n)`. **Why a separate case.** The path-sensitive flow detector only tracks pooled buffers held in **locals**, so a field-backed rent — rented in one member, viewed in another — is out of its reach. The extractor's POOL005 **field pass** closes that gap: it -collects the fields a class `Rent`s (the shared `IsPoolRent`, so an aliased pool -receiver binds and a non-pool `.Rent` does not), and for each member that takes a -full-length view of such a field (receiver resolved through the `this`/bare -`ThisFieldName` shape, the over-read recognised by the same resolved -`System.MemoryExtensions` / `System.Span` BCL symbols as the local path) emits a -synthetic `acquire`/`overspan`/`release` flow so the core raises **OWN025** at the -view — no new diagnostic, the same synthetic-flow trick the field use-after-dispose -and MemoryPool slices use. A *write*/wipe (`Array.Clear(_buf, 0, _buf.Length)`) is not -a view, so it is deliberately **not** flagged — only a read-capable VIEW is the +collects the fields a class `Rent`s — by **assignment** (`_buf = ArrayPool.Rent(n)`, +target resolved through the `this`/bare `ThisFieldName` shape so `other._buf` never +seeds it) **and** by **field initializer** (`byte[] _meta = ArrayPool.Rent(MetaCap)`), +the rent recognised by the shared `IsPoolRent` so an aliased pool receiver binds and a +non-pool `.Rent` does not — and for each member that takes a full-length view of such +a field (the over-read recognised by the same resolved `System.MemoryExtensions` / +`System.Span` BCL symbols as the local path) emits a synthetic +`acquire`/`overspan`/`release` flow so the core raises **OWN025** at the view — no new +diagnostic, the same synthetic-flow trick the field use-after-dispose and MemoryPool +slices use. The scan is scoped to the class's **own (direct) members** — a nested +type is analysed by its own pass, so its rents/views are never mixed into the outer +class's flow. This case pins both view spellings: the bare `_buf.AsSpan()` over the +assignment-rented field and the `.Length` spelling `_meta.AsSpan(0, _meta.Length)` +over the initializer-rented field. A *write*/wipe (`Array.Clear(_buf, 0, _buf.Length)`) +is not a view, so it is deliberately **not** flagged — only a read-capable VIEW is the over-read. **What the checker says:** OWN025 `[resource: pooled buffer]` at the view. The buffer diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index d948f606..7189d5c5 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -2768,7 +2768,8 @@ or ImplicitObjectCreationExpressionSyntax // POOL005 (field): a FULL-LENGTH view of a pooled FIELD — `_buf.AsSpan()` / `this._buf.AsMemory()` // / `new Span(_buf)` / the `.Length` spelling (`_buf.AsSpan(0, _buf.Length)`) — over a buffer - // the class `Rent`ed into a FIELD (`_buf = ArrayPool.Shared.Rent(n)`). The pooled array is + // the class `Rent`ed into a FIELD (by assignment `_buf = ArrayPool.Shared.Rent(n)` OR a field + // initializer `byte[] _buf = ArrayPool.Shared.Rent(n);`). The pooled array is // oversized (`Length >= n`), so a member that views the field full-length reads past the logical // length `n` into the stale `[n, Length)` tail (a previous renter's bytes). The per-method flow // pass only tracks LOCAL rents, so a FIELD-backed rent's over-read is unreached there; emit a @@ -2782,22 +2783,38 @@ or ImplicitObjectCreationExpressionSyntax if (flowLocals) { // pooled FIELD -> the line it was `Rent`ed, via the shared IsPoolRent (an aliased pool - // receiver binds; a non-pool `.Rent` does not false-match). The rent TARGET is resolved - // through `ThisFieldName` — a bare `_buf` or `this._buf`, NEVER `other._buf` — the SAME - // this-instance shape FullViewFieldOwner reads the view through, so a rent into another - // object's field cannot seed `pooledFieldRent` and then false-match this class's own - // same-named (non-pooled) field at the view (Codex). First rent line per field is enough to - // anchor the synthetic acquire. + // receiver binds; a non-pool `.Rent` does not false-match). Two rent spellings, BOTH scoped + // to THIS class — a nested type is analysed by its OWN `cls` pass, so its rents/views must + // neither seed nor fire here (else an inner field could be mis-attributed to the outer class, + // CodeRabbit): + // * an assignment `_buf = ArrayPool.Shared.Rent(n)` (ctor/Capture), target resolved + // through `ThisFieldName` — a bare `_buf` / `this._buf`, NEVER `other._buf` — the SAME + // this-instance shape FullViewFieldOwner reads the view through, so a rent into another + // object's field cannot seed and then false-match this class's own same-named (non-pooled) + // field at the view (Codex); the `FirstAncestorOrSelf == cls` guard drops a rent nested + // in an inner type; and + // * a field-declaration INITIALIZER `byte[] _buf = ArrayPool.Shared.Rent(n);` — a direct + // member of `cls`, so inherently this-class-scoped (CodeRabbit). + // First rent line per field anchors the synthetic acquire. var pooledFieldRent = new Dictionary(StringComparer.Ordinal); foreach (var inv in cls.DescendantNodes().OfType()) if (IsPoolRent(inv, model) + && inv.FirstAncestorOrSelf() == cls && inv.Parent is AssignmentExpressionSyntax asg && ThisFieldName(asg.Left) is { } pf && !pooledFieldRent.ContainsKey(pf)) pooledFieldRent[pf] = LineOf(inv); + foreach (var fdecl in cls.Members.OfType()) + foreach (var fv in fdecl.Declaration.Variables) + if (fv.Initializer?.Value is InvocationExpressionSyntax finv + && IsPoolRent(finv, model) + && !pooledFieldRent.ContainsKey(fv.Identifier.Text)) + pooledFieldRent[fv.Identifier.Text] = LineOf(finv); if (pooledFieldRent.Count > 0) foreach (var member in cls.Members) { + if (member is BaseTypeDeclarationSyntax) + continue; // a nested type is covered by its OWN class pass, not the outer's // first full-length view of each pooled field in this member (one finding per field // per member — repeated views of the same field do not multiply the diagnostic). var seen = new HashSet(StringComparer.Ordinal); From 4ed26804eddbba0e5aaa5de0cd7b73d39c63b01b Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 25 Jun 2026 16:22:50 +0000 Subject: [PATCH 5/5] fix(corpus): guard Return(_buf) against pre-Capture Dispose (CodeRabbit) `_buf` is null until Capture(), so a Dispose() before Capture() would call ArrayPool.Return(null) and throw. Guard the assignment-rented field's return with an `is not null` check in both before.cs/after.cs; `_meta` is initializer- rented (never null) and stays unguarded. The Return invocation is still present for the POOL001 field-release scan, and no view site changes, so before.cs still flags the two over-reads and after.cs stays silent. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF --- corpus/real-world/arraypool-field-fullspan-overread/after.cs | 5 +++-- .../real-world/arraypool-field-fullspan-overread/before.cs | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/corpus/real-world/arraypool-field-fullspan-overread/after.cs b/corpus/real-world/arraypool-field-fullspan-overread/after.cs index 17b6f5cc..fa9fce58 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/after.cs +++ b/corpus/real-world/arraypool-field-fullspan-overread/after.cs @@ -37,8 +37,9 @@ public byte[] FlushMeta() public void Dispose() { - ArrayPool.Shared.Return(_buf); - ArrayPool.Shared.Return(_meta); + if (_buf is not null) // null until Capture; Return(null) would throw + ArrayPool.Shared.Return(_buf); + ArrayPool.Shared.Return(_meta); // initializer-rented, never null } static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } diff --git a/corpus/real-world/arraypool-field-fullspan-overread/before.cs b/corpus/real-world/arraypool-field-fullspan-overread/before.cs index 0a1b0eec..768af162 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/before.cs +++ b/corpus/real-world/arraypool-field-fullspan-overread/before.cs @@ -49,8 +49,9 @@ public byte[] FlushMeta() public void Dispose() { - ArrayPool.Shared.Return(_buf); // class-wide Return: no leak - ArrayPool.Shared.Return(_meta); + if (_buf is not null) // null until Capture; Return(null) would throw + ArrayPool.Shared.Return(_buf); // class-wide Return: no leak + ArrayPool.Shared.Return(_meta); // initializer-rented, never null } static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }