diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 38f03c53..5f5bc69c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -788,10 +788,14 @@ 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` 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 # 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-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-length-overread/expected-diagnostics.txt b/corpus/real-world/arraypool-length-overread/expected-diagnostics.txt new file mode 100644 index 00000000..511ccfa9 --- /dev/null +++ b/corpus/real-world/arraypool-length-overread/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN025 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/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..9f6821f3 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -12,8 +12,16 @@ 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` 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 + `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 +51,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** 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: @@ -97,5 +105,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..ff5357d2 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,13 +808,17 @@ 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` 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. 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); @@ -870,6 +875,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 +929,64 @@ 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). 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 && IsZeroInt(args[0].Expression, model) + && 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)` (start 0, length the + // oversized self-length). + if (al.Arguments.Count == 1 + || (al.Arguments.Count == 3 && IsZeroInt(al.Arguments[1].Expression, model) + && 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; + +// `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 // view (including RETURNING it, an escape) lowers to a use of the owner (the borrow). Resolved @@ -1879,6 +1937,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..6d91e0d7 100644 --- a/spec/BufferPolicies.md +++ b/spec/BufferPolicies.md @@ -39,15 +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 — full view stays 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*.) +- **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