From 8284055bb1a0e0fc5665c130de53f92a70ada9fe Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 03:15:15 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(pool):=20MemoryPool=20view=20borrow=20?= =?UTF-8?q?=E2=80=94=20owner.Memory[.Span]=20used=20after=20Dispose=20?= =?UTF-8?q?=E2=86=92=20OWN002=20(POOL002)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #72 tracked the MemoryPool OWNER lifecycle (acquire/release: POOL001 leak, POOL003 double-dispose). This adds the VIEW borrow: `owner.Memory` / `owner.Memory.Span` of a System.Buffers.IMemoryOwner is a borrow of the owner — exactly like `buf.AsSpan()` is of a Rent'd array. ViewOwner now resolves it (by the IMemoryOwner.Memory property symbol), so a view-local read after `owner.Dispose()` is a use of the owner after release -> OWN002 (POOL002), and a returned Memory view dangles. Reuses the whole borrow lattice — no core changes, extractor + corpus only. Corpus: memorypool-view-after-dispose (before: `Memory v = owner.Memory; owner.Dispose(); Consume(v.Span)` -> OWN002; after: a `using` owner read while alive -> silent) — the MemoryPool twin of arraypool-span-view-after-return. Benchmark recall floor 16 -> 17. P-007 status + ci.yml comment updated. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 11 +++---- .../memorypool-view-after-dispose/after.cs | 17 +++++++++++ .../memorypool-view-after-dispose/before.cs | 25 ++++++++++++++++ .../memorypool-view-after-dispose/case.own | 16 ++++++++++ .../expected-diagnostics.txt | 1 + .../memorypool-view-after-dispose/notes.md | 29 +++++++++++++++++++ docs/proposals/P-007-arraypool-span.md | 7 +++-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 22 ++++++++++++-- 8 files changed, 118 insertions(+), 10 deletions(-) create mode 100644 corpus/real-world/memorypool-view-after-dispose/after.cs create mode 100644 corpus/real-world/memorypool-view-after-dispose/before.cs create mode 100644 corpus/real-world/memorypool-view-after-dispose/case.own create mode 100644 corpus/real-world/memorypool-view-after-dispose/expected-diagnostics.txt create mode 100644 corpus/real-world/memorypool-view-after-dispose/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5f5bc69c..3a88abe0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -792,10 +792,11 @@ jobs: # (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 + # MemoryPool is tracked too: a `MemoryPool.Rent` IMemoryOwner is released by Dispose, so its + # leak / double-dispose ride the flow (POOL001/003 — `memorypool-double-dispose` -> OWN003), and + # its `owner.Memory` / `owner.Memory.Span` view is a borrow lowered to a use of the OWNER + # (`ViewOwner`), so reading it after Dispose trips OWN002 (POOL002 — `memorypool-view-after- + # dispose`). 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 16 + run: python scripts/benchmark.py --min-recall 17 diff --git a/corpus/real-world/memorypool-view-after-dispose/after.cs b/corpus/real-world/memorypool-view-after-dispose/after.cs new file mode 100644 index 00000000..7327ffa1 --- /dev/null +++ b/corpus/real-world/memorypool-view-after-dispose/after.cs @@ -0,0 +1,17 @@ +// AFTER (fixed). A `using` declaration owns the `IMemoryOwner` lifetime: the buffer is +// returned to the pool exactly once, at the end of the scope, AFTER the view has been +// read. The `owner.Memory.Span` borrow is consumed while the owner is still alive, so it +// is never read past the buffer's return. The checker is silent. +using System; +using System.Buffers; + +static class MemoryPoolViewAfterDispose +{ + static void Run(int n) + { + using IMemoryOwner owner = MemoryPool.Shared.Rent(n); + Consume(owner.Memory.Span); // read while the owner is still alive + } + + static void Consume(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/memorypool-view-after-dispose/before.cs b/corpus/real-world/memorypool-view-after-dispose/before.cs new file mode 100644 index 00000000..072dfa92 --- /dev/null +++ b/corpus/real-world/memorypool-view-after-dispose/before.cs @@ -0,0 +1,25 @@ +// BEFORE (buggy). POOL002 for MemoryPool: an `IMemoryOwner` from `MemoryPool` +// exposes its pooled buffer as a `Memory` via `owner.Memory`. That Memory (and the +// `Span` taken from it) is a BORROW of the owner — it is only valid while the owner is +// alive. Reading the view AFTER `owner.Dispose()` (which returns the memory to the pool) +// reads memory that may already have been handed to another renter: a use-after-free. +// The fix is to read the view BEFORE disposing — or let a `using` own the lifetime +// (see after.cs). The MemoryPool twin of `arraypool-span-view-after-return`. +// +// 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 MemoryPoolViewAfterDispose +{ + static void Run(int n) + { + IMemoryOwner owner = MemoryPool.Shared.Rent(n); + Memory view = owner.Memory; // a borrow of the owner's pooled buffer + owner.Dispose(); // returns the memory to the pool ... + Consume(view.Span); // <-- BUG: ... but the view is read AFTER (use-after-free) + } + + static void Consume(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/memorypool-view-after-dispose/case.own b/corpus/real-world/memorypool-view-after-dispose/case.own new file mode 100644 index 00000000..70d2c7cc --- /dev/null +++ b/corpus/real-world/memorypool-view-after-dispose/case.own @@ -0,0 +1,16 @@ +// OwnLang model of the MemoryPool view-after-dispose. `acquire` == MemoryPool.Rent, +// `release` == owner.Dispose(). A `Memory` view (`owner.Memory`, and the `Span` from +// it) is a BORROW of the owner — the extractor lowers a use of the view to a use of the +// OWNER, so reading it after Dispose is the generic use-after-release (OWN002), the same +// code reading the owner directly would give. The borrow is resolved to its owner in the +// extractor; the core sees a plain use-after-release. +module Corpus +resource MemoryOwner { + acquire Rent + release Dispose +} +fn run(n: int) { + let owner = acquire MemoryOwner(n); // MemoryPool.Rent + release owner; // owner.Dispose() <-- too early + use owner; // read the Memory view AFTER Dispose -> OWN002 +} diff --git a/corpus/real-world/memorypool-view-after-dispose/expected-diagnostics.txt b/corpus/real-world/memorypool-view-after-dispose/expected-diagnostics.txt new file mode 100644 index 00000000..3a36fa92 --- /dev/null +++ b/corpus/real-world/memorypool-view-after-dispose/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN002 diff --git a/corpus/real-world/memorypool-view-after-dispose/notes.md b/corpus/real-world/memorypool-view-after-dispose/notes.md new file mode 100644 index 00000000..eb76d33e --- /dev/null +++ b/corpus/real-world/memorypool-view-after-dispose/notes.md @@ -0,0 +1,29 @@ +# MemoryPool view used after dispose (POOL002, the Dispose-released pool) + +**Pattern:** `MemoryPool.Shared.Rent(n)` returns an `IMemoryOwner` whose pooled +buffer is exposed as a `Memory` via `owner.Memory` (and a `Span` via +`owner.Memory.Span`). That view is a **borrow** of the owner — valid only while the +owner is alive. Reading it after `owner.Dispose()` (which returns the memory to the +pool) reads memory that may already belong to another renter: a use-after-free. The +fix is to read the view *before* disposing, or to let a `using` own the lifetime. + +This is the MemoryPool twin of `arraypool-span-view-after-return`: there a `Span` +view of a `Rent`ed array is used after `Return`; here a `Memory`/`Span` view of an +`IMemoryOwner` is used after `Dispose`. Both lower the view to a use of the **owner** +(`ViewOwner` in the extractor), so the core sees a plain use-after-release. + +**What it adds:** the extractor now recognises `owner.Memory` / `owner.Memory.Span` +(resolved via the `System.Buffers.IMemoryOwner.Memory` property) as a borrow of the +owner — completing the MemoryPool story begun in #72 (which tracked the owner's +acquire / release lifecycle: POOL001 leak, POOL003 double-dispose). With the view +recognised, a view-local read after `Dispose` is **POOL002 → OWN002**, and a returned +`Memory` view dangles like the ArrayPool case. + +**What the checker says:** the OwnLang model and the real `before.cs` both trip +**OWN002** (use after release). The `using` fix in `after.cs` reads the view while the +owner is alive 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. + +Reference: [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 9f6821f3..7883fc1e 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -19,9 +19,10 @@ 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 + so its leak / double-dispose ride the same flow as POOL001/003 (corpus `memorypool-double-dispose` + → OWN003), and its `owner.Memory` / `owner.Memory.Span` is a borrow lowered to a use of the OWNER + (`ViewOwner`), so reading the view after `Dispose` trips **POOL002 → OWN002** (corpus + `memorypool-view-after-dispose`). A POOL005 view stored in a FIELD is 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 diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index ff5357d2..1c18864a 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -900,8 +900,9 @@ e is InvocationExpressionSyntax i && 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, +// `owner.AsSpan(...)` / `owner.AsMemory(...)`, `new Span(owner, …)` / `new Memory(owner)` +// (and the ReadOnly* forms), or `owner.Memory` / `owner.Memory.Span` of a `System.Buffers. +// IMemoryOwner` (a MemoryPool rental), where the source is a local identifier. Returns the owner local name, // else null. The BORROW is recognised by the RESOLVED BCL symbols — `System.MemoryExtensions` // `AsSpan`/`AsMemory` (which alias the receiver array) and the `System.Span` / `ReadOnlySpan` // / `Memory` / `ReadOnlyMemory` constructor (which wraps the array argument) — NOT by name, so @@ -926,6 +927,23 @@ e is InvocationExpressionSyntax i { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct } && IsInNamespace(sct, "System")) return arg.Identifier.Text; + // owner.Memory — a Memory view of a System.Buffers.IMemoryOwner (e.g. a MemoryPool rental). + // Like array.AsMemory(), the Memory CAN escape (return / field); a use of the view after the + // owner's Dispose is a use of the owner after release (OWN002), and a returned Memory after + // Dispose is a dangling borrow. Recognised by the resolved `IMemoryOwner.Memory` property. + if (e is MemberAccessExpressionSyntax mem + && mem.Name.Identifier.Text == "Memory" + && mem.Expression is IdentifierNameSyntax mo + && model.GetSymbolInfo(mem).Symbol is IPropertySymbol { ContainingType: { Name: "IMemoryOwner" } ict } + && IsInNamespace(ict, "System", "Buffers")) + return mo.Identifier.Text; + // owner.Memory.Span — the Span of that Memory view (a ref-struct borrow that cannot escape). + if (e is MemberAccessExpressionSyntax { Name.Identifier.Text: "Span" } spanAcc + && spanAcc.Expression is MemberAccessExpressionSyntax + { Name.Identifier.Text: "Memory", Expression: IdentifierNameSyntax mo2 } innerMem + && model.GetSymbolInfo(innerMem).Symbol is IPropertySymbol { ContainingType: { Name: "IMemoryOwner" } ict2 } + && IsInNamespace(ict2, "System", "Buffers")) + return mo2.Identifier.Text; return null; } From c000057ccaa82f1285343aafb9cb1c307be14704 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 22 Jun 2026 03:24:10 +0000 Subject: [PATCH 2/2] docs(pool): scope the MemoryPool dangling-view claim to explicit Dispose (Codex review) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex P2: this PR catches a view-local read after an explicit owner.Dispose() (OWN002, the corpus case) — but the dangling-Memory ESCAPE via the idiomatic `using owner; return owner.Memory;` is NOT caught, because `using` locals are skipped as non-leak candidates so the owner never enters `tracked`. Correct notes.md to not overstate: the returned-view dangle from a `using` owner (modelling the implicit scope-exit dispose as a release on the return path) is a follow-up, like the ArrayPool try/finally Memory escape. The use-after-explicit-Dispose catch and the corpus case are unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- corpus/real-world/memorypool-view-after-dispose/notes.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/corpus/real-world/memorypool-view-after-dispose/notes.md b/corpus/real-world/memorypool-view-after-dispose/notes.md index eb76d33e..167cff91 100644 --- a/corpus/real-world/memorypool-view-after-dispose/notes.md +++ b/corpus/real-world/memorypool-view-after-dispose/notes.md @@ -16,8 +16,12 @@ view of a `Rent`ed array is used after `Return`; here a `Memory`/`Span` view of (resolved via the `System.Buffers.IMemoryOwner.Memory` property) as a borrow of the owner — completing the MemoryPool story begun in #72 (which tracked the owner's acquire / release lifecycle: POOL001 leak, POOL003 double-dispose). With the view -recognised, a view-local read after `Dispose` is **POOL002 → OWN002**, and a returned -`Memory` view dangles like the ArrayPool case. +recognised, a view-local read after an explicit `owner.Dispose()` is +**POOL002 → OWN002**. (The *returned*-`Memory` dangle from the idiomatic `using` +owner — `using owner; return owner.Memory;`, where the implicit scope-exit dispose +hands a stale view to the caller — is a follow-up: `using` locals are skipped as +non-leak candidates, so that escape needs the scope-exit dispose modelled as a +release on the return path, like the ArrayPool try/finally `Memory` escape.) **What the checker says:** the OwnLang model and the real `before.cs` both trip **OWN002** (use after release). The `using` fix in `after.cs` reads the view while the