From 25da937830cbb3e57430e1a2c959b3dfe0f1663a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 17:02:45 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(extractor):=20borrow=20checker=20?= =?UTF-8?q?=E2=80=94=20Memory=20view=20that=20ESCAPES=20after=20Return?= =?UTF-8?q?=20=E2=86=92=20OWN002=20(POOL004)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The borrow checker's second bite, and the genuinely dangerous one. `arraypool-span-view-after-return` (#69) caught a `Span` view used after `Return` INSIDE the method — but a `Span` is a ref struct, so the C# compiler already keeps it from escaping. A `Memory` is NOT a ref struct: it can be RETURNED or stored in a field, so a `Memory` view of a pooled buffer can leave the method and dangle in the caller's hands after the buffer was recycled (a silent cross-tenant corruption). That is the escape the borrow checker has to catch, and the compiler will not. The view recognition (`ViewOwner`, renamed from `SpanViewOwner`) is extended from `AsSpan` / `new Span` to `AsMemory` / `new Memory` (and the `ReadOnly*` forms), resolved via the same BCL symbols (`System.MemoryExtensions`, `System.Memory` ctor) — not by name, so a look-alike is not mistaken for a borrow. Because a reference to a view lowers to a use of the owner, and `return view` is such a reference (routed through the return-expression lowering), the escape of a dangling view after `Return(buf)` trips OWN002 at the escape site. Purely extractor-side; the facts are identical to the in-method case (`acquire buf; release buf; use buf`). Conservative (0 FP): only a view of a tracked owner used/returned AFTER the owner's release fires; the fix copies out of the buffer (`AsSpan(..).ToArray()`) and returns the copy, so no view escapes (the `after.cs` arm stays silent). A view used before the return, or of an untracked buffer, adds nothing. Pinned by corpus `arraypool-memory-view-escape` (before → OWN002, after silent), lifting the recall floor 12 → 13. First slice covers the RETURN escape; a view stored in a FIELD and view reassignment are left for later. Validated locally: case.own → OWN002, corpus 11/11, constructed facts → OWN002. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 15 +++--- corpus/real-world/README.md | 1 + .../arraypool-memory-view-escape/after.cs | 16 +++++++ .../arraypool-memory-view-escape/before.cs | 20 ++++++++ .../arraypool-memory-view-escape/case.own | 16 +++++++ .../expected-diagnostics.txt | 1 + .../arraypool-memory-view-escape/notes.md | 32 +++++++++++++ docs/proposals/P-007-arraypool-span.md | 14 +++--- frontend/roslyn/OwnSharp.Extractor/Program.cs | 47 ++++++++++--------- 9 files changed, 128 insertions(+), 34 deletions(-) create mode 100644 corpus/real-world/arraypool-memory-view-escape/after.cs create mode 100644 corpus/real-world/arraypool-memory-view-escape/before.cs create mode 100644 corpus/real-world/arraypool-memory-view-escape/case.own create mode 100644 corpus/real-world/arraypool-memory-view-escape/expected-diagnostics.txt create mode 100644 corpus/real-world/arraypool-memory-view-escape/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 329177ca..7e67d726 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -784,11 +784,12 @@ jobs: # directly OR by forwarding it to another first-party consumer (the TRANSITIVE chain, # `ConsumesParam`) — is a handoff that releases the argument at the call site, so a use # after the handoff trips OWN002 (the cut is the signature, like Rust's move). The BORROW - # checker has its first bite: a `Span`/`ReadOnlySpan` view of a pooled buffer - # (`buf.AsSpan()`) is a ref-struct borrow lowered to a use of the OWNER, so writing through - # the view after `Return(buf)` trips OWN002 (`ViewOwnerOf`). Remaining backlog: a - # FIELD-mediated cross-method use-after-dispose (dispose in one method, use in another via - # shared state), `Memory`/escaping views, and an injected-source region-escape. A drop - # below the floor is a regression. - run: python scripts/benchmark.py --min-recall 12 + # checker covers both view kinds: a `Span`/`Memory` view of a pooled buffer (`buf.AsSpan()` / + # `buf.AsMemory()`) is a borrow lowered to a use of the OWNER (`ViewOwner`), so using it + # after `Return(buf)` trips OWN002 — including RETURNING a `Memory` view (which, unlike a + # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. Remaining + # backlog: a FIELD-mediated cross-method use-after-dispose (dispose in one method, use in + # another via shared state), a view stored in a FIELD, and an injected-source region-escape. + # A drop below the floor is a regression. + run: python scripts/benchmark.py --min-recall 13 diff --git a/corpus/real-world/README.md b/corpus/real-world/README.md index 6e7de846..f37e9b26 100644 --- a/corpus/real-world/README.md +++ b/corpus/real-world/README.md @@ -44,5 +44,6 @@ exception-path (анализ не моделирует исключения), co | `arraypool-use-after-return` | OWN002 | rented-буфер вернули в пул, потом ещё читали slice | | `arraypool-double-return` | OWN003 | один и тот же массив вернули в ArrayPool дважды ([#33767](https://github.com/dotnet/runtime/issues/33767)) | | `arraypool-span-view-after-return` | OWN002 | `Span`-вью пула (`buf.AsSpan()`) записали ПОСЛЕ `Return` — заём пережил владельца (borrow-checker) | +| `arraypool-memory-view-escape` | OWN002 | `Memory`-вью пула вернули наружу (escape) ПОСЛЕ `Return` — dangling-заём ушёл вызывающему (POOL004) | | `ownership-handoff-use` | OWN002 | поток отдали потребителю (он его закрыл), потом ещё читали — use-after-handoff | | `ownership-handoff-use-transitive` | OWN002 | то же, но потребитель не закрывает сам, а **пробрасывает** владение дальше (transitive consume) | diff --git a/corpus/real-world/arraypool-memory-view-escape/after.cs b/corpus/real-world/arraypool-memory-view-escape/after.cs new file mode 100644 index 00000000..667ea215 --- /dev/null +++ b/corpus/real-world/arraypool-memory-view-escape/after.cs @@ -0,0 +1,16 @@ +// FIX: copy the data OUT of the pooled buffer before returning it, and hand the caller the copy — +// no view of the recycled buffer escapes the method. Same Return, but nothing borrowed leaves it, +// so the case must stay SILENT (the no-false-positive arm). +using System; +using System.Buffers; + +static class PoolMemoryViewEscape +{ + static byte[] Render(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + byte[] copy = buf.AsSpan(0, n).ToArray(); // copy OUT before returning the buffer + ArrayPool.Shared.Return(buf); + return copy; // a fresh copy escapes, not a view -> silent + } +} diff --git a/corpus/real-world/arraypool-memory-view-escape/before.cs b/corpus/real-world/arraypool-memory-view-escape/before.cs new file mode 100644 index 00000000..c776e5b0 --- /dev/null +++ b/corpus/real-world/arraypool-memory-view-escape/before.cs @@ -0,0 +1,20 @@ +// A Memory VIEW of a pooled buffer ESCAPES the method (returned to the caller) AFTER the buffer +// was returned to the pool. Unlike a `Span` (a ref struct the compiler keeps inside the method), a +// `Memory` CAN leave the method — so this dangling view reaches the caller, who then reads/writes +// memory the pool has already recycled to someone else (a silent cross-tenant corruption). The +// borrow outlives its owner: a use-after-return surfaced at the ESCAPE (return) site. +// +// Wrapped in a class so the extractor's per-class flow pass visits it. +using System; +using System.Buffers; + +static class PoolMemoryViewEscape +{ + static Memory Render(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Memory view = buf.AsMemory(0, n); // view BORROWS buf + ArrayPool.Shared.Return(buf); // buf goes back to the pool (recycled) ... + return view; // ... but a view of it ESCAPES -> dangling (OWN002) + } +} diff --git a/corpus/real-world/arraypool-memory-view-escape/case.own b/corpus/real-world/arraypool-memory-view-escape/case.own new file mode 100644 index 00000000..68f07ebb --- /dev/null +++ b/corpus/real-world/arraypool-memory-view-escape/case.own @@ -0,0 +1,16 @@ +// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return. The C# stores a +// Memory VIEW of the buffer and RETURNS it (an escape) after the buffer was returned to the +// pool. A Memory is a borrow that — unlike a ref-struct Span — can leave the method, so the +// returned view dangles. The extractor lowers a use of the view (here, returning it) to a use of the +// OWNER buffer, so the escape after `release` is the generic use-after-return (OWN002), the same code +// the core gives for reading the buffer directly after return. +module Corpus +resource Buffer { + acquire rent + release give +} +fn render(n: int) { + let buf = acquire Buffer(n); // ArrayPool.Rent + release buf; // ArrayPool.Return <-- too early + use buf; // return the dangling Memory view (escape) AFTER return -> OWN002 +} diff --git a/corpus/real-world/arraypool-memory-view-escape/expected-diagnostics.txt b/corpus/real-world/arraypool-memory-view-escape/expected-diagnostics.txt new file mode 100644 index 00000000..3a36fa92 --- /dev/null +++ b/corpus/real-world/arraypool-memory-view-escape/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN002 diff --git a/corpus/real-world/arraypool-memory-view-escape/notes.md b/corpus/real-world/arraypool-memory-view-escape/notes.md new file mode 100644 index 00000000..370c337b --- /dev/null +++ b/corpus/real-world/arraypool-memory-view-escape/notes.md @@ -0,0 +1,32 @@ +# Pooled-buffer `Memory` view that ESCAPES after return — the borrow checker, second bite + +**Pattern:** a rented `ArrayPool` buffer is sliced into a `Memory` local +(`Memory view = buf.AsMemory(0, n)`), the buffer is `Return`ed to the pool, and the view is +then **returned from the method** (or stored in a field). The borrow **escapes** its owner: the +caller holds a `Memory` into an array the pool has already recycled to someone else — a silent +cross-tenant corruption (read/write of freed-and-reused memory). + +**What the checker says:** the view's escape (the `return`) is a use of the owner after it was +released → the generic **OWN002** (use-after-release), surfaced at the escape site. + +**Why this case exists (P-007 POOL004 — view escape).** [`arraypool-span-view-after-return`](../arraypool-span-view-after-return) +caught a `Span` view used after `Return` **inside** the method. But a `Span` is a **ref struct** — +the C# compiler keeps it inside the method, so it cannot escape. A **`Memory` is not a ref +struct**: it *can* be returned or stored in a field, which is the genuinely dangerous escape the +borrow checker must catch. The view recognition (`ViewOwner`) is now extended from `AsSpan` / +`new Span` to **`AsMemory` / `new Memory`** (and the `ReadOnly*` forms), resolved via the same +BCL symbols (`System.MemoryExtensions`, `System.Memory`). Because a reference to the view lowers +to a use of the owner — and `return view` is such a reference — the escape of a dangling view after +`Return(buf)` trips OWN002. Before this slice the `Memory` view was unrecognised, so the dangling +return looked balanced (acquire + release) — a **miss**. + +**Conservative (0 FP).** Only a view of a **tracked** owner that is used/returned **after** the +owner's release fires. The fix (`after.cs`) copies out of the buffer (`AsSpan(..).ToArray()`) and +returns the **copy**, so no view escapes — silent. A view used before the return, or a view of an +untracked buffer, adds no finding; the borrow can never invent a release. + +**Honesty / scope.** `case.own` is a faithful hand reduction (the escaping view collapses to a use +of the owner, exactly what the extractor emits), not C# the `.own` checker ingested. +`before.cs`/`after.cs` are representative of the bug and its fix. This slice covers the **return** +escape; storing the view in a **field** (object-level escape) and view **reassignment** are left for +later rounds. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 6a491417..51a282a7 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -1,11 +1,13 @@ # P-007 — ArrayPool / Span borrow-view profile -- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; **POOL002 - (Span/ReadOnlySpan view used after `Return` → OWN002) first slice built** — a - `buf.AsSpan()` / `new Span(buf)` view is a ref-struct borrow lowered to a use of the - owner (`ViewOwnerOf` in the extractor; corpus `arraypool-span-view-after-return`); the - borrow checker's first bite on real C#. POOL003–005 (double-return via flow already - catches OWN003, `Memory`/escaping views, clear-past-length) next +- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; **POOL002 (Span/Memory + view used after `Return` → OWN002) built** and **POOL004 (view ESCAPE) first slice built** — a + `buf.AsSpan()` / `buf.AsMemory()` / `new Span(buf)` view is a borrow lowered to a use of the + owner (`ViewOwner` in the extractor), so using it after `Return` trips OWN002; because a + `Memory` (unlike a ref-struct `Span`) can leave the method, RETURNING a dangling `Memory` view + is caught at the escape (corpus `arraypool-span-view-after-return`, `arraypool-memory-view-escape`). + The borrow checker on real C#. POOL003 (double-return — flow already catches OWN003), a view + stored in a FIELD, and POOL005 (clear-past-length) next - **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 0c5e6ad9..b7b38933 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -760,10 +760,11 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet tracked, Semanti if (tracked.Contains(c)) nodes.Add(new { op = "release", var = c, line = LineOf(expr) }); // any other reference to a tracked local -> use (once per local; a consumed arg is a - // release above, never also a use). A Span/ReadOnlySpan VIEW of a tracked buffer is a BORROW: - // a reference to the view is a use of the OWNER, so using it after the owner was - // Returned/Disposed trips OWN002 (the ref-struct view cannot outlive the method, so this is a - // genuine use-after-release of the owner — `Span v = buf.AsSpan(); Return(buf); v[0]=…`). + // release above, never also a use). A Span/Memory VIEW of a tracked buffer is a BORROW: a + // reference to the view is a use of the OWNER, so using it after the owner was Returned/Disposed + // trips OWN002 — including RETURNING a `Memory` view (which CAN escape the method) after the + // owner was released, a dangling borrow handed to the caller + // (`Memory v = buf.AsMemory(); Return(buf); return v;`). var used = new SortedSet(StringComparer.Ordinal); foreach (var idn in expr.DescendantNodesAndSelf().OfType()) { @@ -827,20 +828,22 @@ e is InvocationExpressionSyntax i && i.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax buf ? buf.Identifier.Text : null; -// The owner buffer a Span/ReadOnlySpan VIEW expression borrows from: `owner.AsSpan(...)` or -// `new Span(owner, …)` / `new ReadOnlySpan(owner)`, 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` (which aliases its receiver array) and the `System.Span` / -// `System.ReadOnlySpan` constructor (which wraps its array argument) — NOT by name, so a -// project's own `AsSpan` extension, a non-`System` type named `Span`, or an `AsSpan` returning a -// span over a fresh copy is not mistaken for a borrow of `owner` (Codex). A `Span` is a ref-struct -// borrow that cannot escape the method, so a use of the view after the owner is released is a use of -// the owner after its release. -static string? SpanViewOwner(ExpressionSyntax? e, SemanticModel model) +// 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, +// 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 +// a project's own `AsSpan`/`AsMemory`, or a non-`System` look-alike type, is not mistaken for a +// borrow of `owner` (Codex). `Span` is a ref-struct borrow that cannot escape the method; `Memory` +// CAN escape (return / field), so a `Memory` view returned after the owner is released is a dangling +// borrow that leaves the method — in both cases a use of the view after the owner's release is a use +// of the owner after its release. +static string? ViewOwner(ExpressionSyntax? e, SemanticModel model) { if (e is InvocationExpressionSyntax inv && inv.Expression is MemberAccessExpressionSyntax m - && m.Name.Identifier.Text == "AsSpan" + && m.Name.Identifier.Text is "AsSpan" or "AsMemory" && m.Expression is IdentifierNameSyntax recv && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct } && IsInNamespace(mct, "System")) @@ -848,23 +851,25 @@ e is InvocationExpressionSyntax i if (e is ObjectCreationExpressionSyntax oc && oc.ArgumentList is { Arguments.Count: > 0 } && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg - && model.GetSymbolInfo(oc).Symbol is IMethodSymbol { ContainingType: { Name: "Span" or "ReadOnlySpan" } sct } + && model.GetSymbolInfo(oc).Symbol is IMethodSymbol + { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct } && IsInNamespace(sct, "System")) return arg.Identifier.Text; return null; } -// If `idn` references a Span/ReadOnlySpan VIEW local declared from an owner buffer -// (`Span view = owner.AsSpan(…)`), the owner buffer's local name — so a use of the view lowers -// to a use of the owner (the borrow). Resolved through the view local's own declaration, so it is -// inert for any identifier that is not such a view (returns null -> ordinary handling). +// 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 +// through the view local's own declaration, so it is inert for any identifier that is not such a +// view (returns null -> ordinary handling). static string? ViewOwnerOf(IdentifierNameSyntax idn, SemanticModel model) { if (model.GetSymbolInfo(idn).Symbol is not ILocalSymbol sym) return null; foreach (var r in sym.DeclaringSyntaxReferences) if (r.GetSyntax() is VariableDeclaratorSyntax { Initializer.Value: { } init }) - return SpanViewOwner(init, model); + return ViewOwner(init, model); return null; } From dfc46343fef0aee53f8f90ea9c4ff993d402e2a1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 17:16:03 +0000 Subject: [PATCH 2/3] fix(extractor): catch the try/finally Memory escape + target-typed new (Codex/CodeRabbit) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two review fixes on the Memory-view-escape slice: - Codex (P2): the escape was missed for THE idiomatic ArrayPool form, `try { return view; } finally { Return(buf); }`. The `return view` is evaluated before the finally, but the caller receives the `Memory` only AFTER the finally recycles the buffer — a dangling escape. The return lowering placed the view's owner-use BEFORE the finally release, so it looked clean. Now a returned view's owner-use is re-emitted AFTER the finally release(s) — inserted just before the exit of the `onReturn` chain (`[finally…, exit]`) — so the finally-Return then trips OWN002. New helper `ReturnedViewOwners`; outside a try the use was already after any earlier release, so nothing changes there. The corpus `before.cs` is now this idiomatic try/finally form. Core fact shape validated locally (acquire; use; release; use; exit → OWN002). - CodeRabbit (Major): `ViewOwner` matched only `ObjectCreationExpressionSyntax`, missing C# 9+ target-typed `Memory v = new(buf, 0, n)`. Switched to `BaseObjectCreationExpressionSyntax` (covers explicit + implicit `new`; `ArgumentList`/`GetSymbolInfo` resolve on the base), matching the codebase idiom. corpus 11/11, ownir 116/116; case.own → OWN002. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .../arraypool-memory-view-escape/after.cs | 17 +++++---- .../arraypool-memory-view-escape/before.cs | 24 ++++++++----- .../arraypool-memory-view-escape/case.own | 16 ++++----- .../arraypool-memory-view-escape/notes.md | 17 ++++++--- frontend/roslyn/OwnSharp.Extractor/Program.cs | 36 +++++++++++++++++-- 5 files changed, 82 insertions(+), 28 deletions(-) diff --git a/corpus/real-world/arraypool-memory-view-escape/after.cs b/corpus/real-world/arraypool-memory-view-escape/after.cs index 667ea215..8c8794e5 100644 --- a/corpus/real-world/arraypool-memory-view-escape/after.cs +++ b/corpus/real-world/arraypool-memory-view-escape/after.cs @@ -1,6 +1,6 @@ -// FIX: copy the data OUT of the pooled buffer before returning it, and hand the caller the copy — -// no view of the recycled buffer escapes the method. Same Return, but nothing borrowed leaves it, -// so the case must stay SILENT (the no-false-positive arm). +// FIX: copy the data OUT of the pooled buffer and return the COPY — no view of the recycled buffer +// escapes. Same try/finally cleanup, but nothing borrowed leaves the method, so it stays SILENT +// (the no-false-positive arm). using System; using System.Buffers; @@ -9,8 +9,13 @@ static class PoolMemoryViewEscape static byte[] Render(int n) { byte[] buf = ArrayPool.Shared.Rent(n); - byte[] copy = buf.AsSpan(0, n).ToArray(); // copy OUT before returning the buffer - ArrayPool.Shared.Return(buf); - return copy; // a fresh copy escapes, not a view -> silent + try + { + return buf.AsSpan(0, n).ToArray(); // copy OUT -> a fresh array escapes, not a view + } + finally + { + ArrayPool.Shared.Return(buf); + } } } diff --git a/corpus/real-world/arraypool-memory-view-escape/before.cs b/corpus/real-world/arraypool-memory-view-escape/before.cs index c776e5b0..7a29e26e 100644 --- a/corpus/real-world/arraypool-memory-view-escape/before.cs +++ b/corpus/real-world/arraypool-memory-view-escape/before.cs @@ -1,8 +1,10 @@ -// A Memory VIEW of a pooled buffer ESCAPES the method (returned to the caller) AFTER the buffer -// was returned to the pool. Unlike a `Span` (a ref struct the compiler keeps inside the method), a -// `Memory` CAN leave the method — so this dangling view reaches the caller, who then reads/writes -// memory the pool has already recycled to someone else (a silent cross-tenant corruption). The -// borrow outlives its owner: a use-after-return surfaced at the ESCAPE (return) site. +// A Memory VIEW of a pooled buffer ESCAPES the method — returned from inside a `try` whose +// `finally` returns the buffer to the pool (THE idiomatic ArrayPool cleanup). The `return view` +// expression is evaluated before the finally runs, but the caller receives the `Memory` only +// AFTER the finally has recycled the buffer — so the caller then reads/writes memory the pool has +// already handed to someone else (a silent cross-tenant corruption). Unlike a `Span` (a ref struct +// the compiler keeps inside the method), a `Memory` CAN leave the method, so the borrow outlives +// its owner: a dangling escape past the finally. // // Wrapped in a class so the extractor's per-class flow pass visits it. using System; @@ -13,8 +15,14 @@ static class PoolMemoryViewEscape static Memory Render(int n) { byte[] buf = ArrayPool.Shared.Rent(n); - Memory view = buf.AsMemory(0, n); // view BORROWS buf - ArrayPool.Shared.Return(buf); // buf goes back to the pool (recycled) ... - return view; // ... but a view of it ESCAPES -> dangling (OWN002) + try + { + Memory view = buf.AsMemory(0, n); // view BORROWS buf + return view; // escapes -> caller gets it AFTER the finally + } + finally + { + ArrayPool.Shared.Return(buf); // buf recycled here -> returned view dangles (OWN002) + } } } diff --git a/corpus/real-world/arraypool-memory-view-escape/case.own b/corpus/real-world/arraypool-memory-view-escape/case.own index 68f07ebb..7091272d 100644 --- a/corpus/real-world/arraypool-memory-view-escape/case.own +++ b/corpus/real-world/arraypool-memory-view-escape/case.own @@ -1,9 +1,9 @@ -// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return. The C# stores a -// Memory VIEW of the buffer and RETURNS it (an escape) after the buffer was returned to the -// pool. A Memory is a borrow that — unlike a ref-struct Span — can leave the method, so the -// returned view dangles. The extractor lowers a use of the view (here, returning it) to a use of the -// OWNER buffer, so the escape after `release` is the generic use-after-return (OWN002), the same code -// the core gives for reading the buffer directly after return. +// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return (run by the `finally`). +// The C# returns a Memory VIEW of the buffer from inside a `try` whose `finally` returns the +// buffer to the pool. A Memory — unlike a ref-struct Span — can leave the method, so the caller +// receives the view AFTER the finally recycled the buffer: a dangling escape. The extractor models +// the escaped view's use AFTER the finally release, so it reduces to a plain use-after-return +// (OWN002), the same code reading the buffer directly after return would give. module Corpus resource Buffer { acquire rent @@ -11,6 +11,6 @@ resource Buffer { } fn render(n: int) { let buf = acquire Buffer(n); // ArrayPool.Rent - release buf; // ArrayPool.Return <-- too early - use buf; // return the dangling Memory view (escape) AFTER return -> OWN002 + release buf; // ArrayPool.Return <-- the finally, before the caller sees the view + use buf; // the escaped Memory view, used by the caller AFTER the finally -> OWN002 } diff --git a/corpus/real-world/arraypool-memory-view-escape/notes.md b/corpus/real-world/arraypool-memory-view-escape/notes.md index 370c337b..c849c667 100644 --- a/corpus/real-world/arraypool-memory-view-escape/notes.md +++ b/corpus/real-world/arraypool-memory-view-escape/notes.md @@ -1,10 +1,12 @@ # Pooled-buffer `Memory` view that ESCAPES after return — the borrow checker, second bite **Pattern:** a rented `ArrayPool` buffer is sliced into a `Memory` local -(`Memory view = buf.AsMemory(0, n)`), the buffer is `Return`ed to the pool, and the view is -then **returned from the method** (or stored in a field). The borrow **escapes** its owner: the -caller holds a `Memory` into an array the pool has already recycled to someone else — a silent -cross-tenant corruption (read/write of freed-and-reused memory). +(`Memory view = buf.AsMemory(0, n)`) and **returned from inside a `try` whose `finally` +returns the buffer to the pool** — *the* idiomatic ArrayPool cleanup. The `return view` is evaluated +before the finally, but the caller receives the `Memory` only **after** the finally has +recycled the array, so the borrow **escapes** its owner: the caller holds a view into an array the +pool has already handed to someone else — a silent cross-tenant corruption (read/write of +freed-and-reused memory). **What the checker says:** the view's escape (the `return`) is a use of the owner after it was released → the generic **OWN002** (use-after-release), surfaced at the escape site. @@ -20,6 +22,13 @@ to a use of the owner — and `return view` is such a reference — the escape o `Return(buf)` trips OWN002. Before this slice the `Memory` view was unrecognised, so the dangling return looked balanced (acquire + release) — a **miss**. +Crucially, the escaped view's use is modelled **after the `finally`**: a returned borrow is used by +the caller *after* the method's cleanup, so the owner-use is re-emitted just before the method exits +the `onReturn` (finally) chain. That is what catches the idiomatic +`try { return view; } finally { Return(buf); }` — where the `return` is evaluated first but the +caller only receives the view once the finally has recycled the buffer (a dangling escape the C# +compiler does **not** prevent for `Memory`). + **Conservative (0 FP).** Only a view of a **tracked** owner that is used/returned **after** the owner's release fires. The fix (`after.cs`) copies out of the buffer (`AsSpan(..).ToArray()`) and returns the **copy**, so no view escapes — silent. A view used before the return, or a view of an diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index b7b38933..531b8170 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -477,6 +477,7 @@ or ImplicitObjectCreationExpressionSyntax // lower the body so a tracked plain local used inside is seen. return us.Statement is null || LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, onThrow, onReturn); case ReturnStatementSyntax rs: + { // A tracked local READ in the return value is a use at the return point — // e.g. `return BuildResult(buf)` after `pool.Return(buf)` is a use-after- // return. A tracked local *itself* returned is excluded upstream as an @@ -486,11 +487,26 @@ or ImplicitObjectCreationExpressionSyntax // on the return path — then exits; outside a try it is a bare CFG exit. if (rs.Expression is { } rexpr) EmitFlowExpr(rexpr, tracked, model, nodes); + // A returned Span/Memory VIEW (borrow) ESCAPES to the caller, who uses it AFTER this + // method's finally cleanup runs — so `try { return view; } finally { Return(buf); }` + // hands back a DANGLING borrow (the idiomatic pool-cleanup form). Model the escaped + // view's use AFTER the finally release(s) by inserting it just before the exit of the + // `onReturn` chain (which is `[finally…, exit]`), so a finally that releases the owner + // trips OWN002 (Codex). Outside a try (onReturn null) EmitFlowExpr already placed the + // use after any earlier release, so no insertion is needed. + var viewEscapes = rs.Expression is { } vrx + ? ReturnedViewOwners(vrx, tracked, model) : new List(); if (onReturn is not null) - nodes.AddRange(onReturn); + { + var chain = new List(onReturn); + foreach (var owner in viewEscapes) + chain.Insert(chain.Count - 1, new { op = "use", var = owner, line = LineOf(rs) }); + nodes.AddRange(chain); + } else nodes.Add(new { op = "return", var = (string?)null, line = LineOf(rs) }); return true; + } case WhileStatementSyntax ws: { // P-016 A1 reached the frontend: a `while` lowers to a `while` flow op @@ -848,7 +864,7 @@ e is InvocationExpressionSyntax i && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct } && IsInNamespace(mct, "System")) return recv.Identifier.Text; - if (e is ObjectCreationExpressionSyntax oc + if (e is BaseObjectCreationExpressionSyntax oc // explicit OR target-typed `new(buf, …)` && oc.ArgumentList is { Arguments.Count: > 0 } && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg && model.GetSymbolInfo(oc).Symbol is IMethodSymbol @@ -873,6 +889,22 @@ e is InvocationExpressionSyntax i return null; } +// The tracked owner buffers whose Span/Memory VIEW LOCALS are returned by `expr` (an escaping +// borrow — `return view` where `view` is `buf.AsMemory(…)`). The caller uses each such view AFTER +// this method's finally cleanup, so the return lowering re-emits the owner's use after the finally +// release(s). Distinct from a plain returned tracked local (excluded upstream as an escape) — here +// the borrow, not the owner, leaves the method, and the owner stays tracked. +static List ReturnedViewOwners(ExpressionSyntax expr, HashSet tracked, SemanticModel model) +{ + var owners = new List(); + foreach (var idn in expr.DescendantNodesAndSelf().OfType()) + if (!tracked.Contains(idn.Identifier.Text) + && ViewOwnerOf(idn, model) is { } owner + && tracked.Contains(owner) && !owners.Contains(owner)) + owners.Add(owner); + return owners; +} + // A factory call that CREATES and hands back a fresh owned IDisposable the caller must // release — recognised via the resolved symbol (curated, the same spirit as // IsDisposableType is for `new`). Two families: From a4b7298f1a2e381005d403dfa057c876a9703eb0 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 17:22:01 +0000 Subject: [PATCH 3/3] fix(extractor): ReturnedViewOwners follows only the returned value, not every identifier (CodeRabbit) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CodeRabbit (Major): the helper scanned every descendant identifier of the return expression, so `try { return view.Length; } finally { Return(buf); }` injected a post-finally `use buf` and tripped a false OWN002 — even though only an `int` (the length) escapes, not the view. The escape happens only when the RETURNED VALUE itself is the view. Replaced the descendant scan with a structural visitor that follows only the returned value: a view local (`return view`), an inline view expression (`return buf.AsMemory(…)`), and through casts / parentheses / conditional branches. A member or call result of a view is not visited, so it no longer escapes. The corpus case (`return view`) still fires; `after.cs` (`return …ToArray()`) stays silent. corpus 11/11, ownir 116/116. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 33 ++++++++++++++++--- 1 file changed, 29 insertions(+), 4 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 531b8170..d38196f0 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -897,11 +897,36 @@ e is InvocationExpressionSyntax i static List ReturnedViewOwners(ExpressionSyntax expr, HashSet tracked, SemanticModel model) { var owners = new List(); - foreach (var idn in expr.DescendantNodesAndSelf().OfType()) - if (!tracked.Contains(idn.Identifier.Text) - && ViewOwnerOf(idn, model) is { } owner - && tracked.Contains(owner) && !owners.Contains(owner)) + void AddOwner(string? owner) + { + if (owner is not null && tracked.Contains(owner) && !owners.Contains(owner)) owners.Add(owner); + } + // Follow only the RETURNED VALUE's own structure — a view LOCAL (`return view`), an inline view + // expression (`return buf.AsMemory(…)`), through casts / parentheses / `?:`. A member or call + // RESULT of a view (`return view.Length`, an int) does NOT escape the view, so it is not visited + // — scanning every descendant identifier would wrongly flag it (CodeRabbit). + void Visit(ExpressionSyntax e) + { + AddOwner(ViewOwner(e, model)); + switch (e) + { + case IdentifierNameSyntax idn when !tracked.Contains(idn.Identifier.Text): + AddOwner(ViewOwnerOf(idn, model)); + break; + case ParenthesizedExpressionSyntax p: + Visit(p.Expression); + break; + case CastExpressionSyntax c: + Visit(c.Expression); + break; + case ConditionalExpressionSyntax q: + Visit(q.WhenTrue); + Visit(q.WhenFalse); + break; + } + } + Visit(expr); return owners; }