From 98ec9252555fc3b69fe8693781600e2ae329ac9d Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 16:25:12 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(extractor):=20borrow=20checker=20?= =?UTF-8?q?=E2=80=94=20Span=20view=20of=20a=20pooled=20buffer=20used=20aft?= =?UTF-8?q?er=20Return=20=E2=86=92=20OWN002=20(POOL002)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first bite of the borrow checker on real C#, and the heavy-artillery frontier (B4 / P-007 POOL002). The flat pass and the existing pool flow only caught a use-after-return when the BUFFER LOCAL ITSELF was referenced after Return. When the read goes through a stored Span view — `Span view = buf.AsSpan(0, n); pool.Return(buf); view[0] = 42;` — the buffer name never appears at the use site, so the buffer looked released-and-untouched: a miss (and a nasty silent aliasing bug, since the array is recycled to another caller). A `Span`/`ReadOnlySpan` view of a tracked buffer is now modelled as a BORROW: a reference to the view local lowers to a USE OF THE OWNER (`ViewOwnerOf` resolves the view through its declaration's `buf.AsSpan(..)` / `new Span(buf)` initializer, the Span-returning symbol confirmed via the SemanticModel). A use after `Return(buf)` then trips OWN002. Purely extractor-side — the core needs no borrow concept; it sees a plain use-after-release (the emitted facts are identical to arraypool-use-after-return: acquire buf; release buf; use buf). A ref-struct `Span` cannot escape the method, which is exactly what makes "use of the view = use of the owner, here" sound. Conservative (0 FP): a view of an untracked/escaped buffer, or one used BEFORE the Return (after.cs), adds no finding — the borrow only lowers to a use of an owner that is still tracked, so it can never invent a release. Pinned by corpus `arraypool-span-view-after-return` (before → OWN002, after silent), lifting the benchmark recall floor 11 → 12. First slice: `Span`/`ReadOnlySpan` via `AsSpan()` / `new Span`; `Memory` (escapable) and view reassignment are left for later rounds. Validated locally: case.own → OWN002, corpus 10/10, constructed extractor facts → OWN002. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 13 +++-- corpus/real-world/README.md | 1 + .../arraypool-span-view-after-return/after.cs | 16 ++++++ .../before.cs | 22 ++++++++ .../arraypool-span-view-after-return/case.own | 17 ++++++ .../expected-diagnostics.txt | 1 + .../arraypool-span-view-after-return/notes.md | 34 ++++++++++++ docs/proposals/P-007-arraypool-span.md | 8 ++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 54 +++++++++++++++++-- 9 files changed, 156 insertions(+), 10 deletions(-) create mode 100644 corpus/real-world/arraypool-span-view-after-return/after.cs create mode 100644 corpus/real-world/arraypool-span-view-after-return/before.cs create mode 100644 corpus/real-world/arraypool-span-view-after-return/case.own create mode 100644 corpus/real-world/arraypool-span-view-after-return/expected-diagnostics.txt create mode 100644 corpus/real-world/arraypool-span-view-after-return/notes.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e04c0f3d..329177ca 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -783,9 +783,12 @@ jobs: # a first-party method that owns a by-value IDisposable param — by disposing it # 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). Remaining - # backlog: a FIELD-mediated cross-method use-after-dispose (dispose in one method, use in - # another via shared state) and an injected-source region-escape. A drop below the floor - # is a regression. - run: python scripts/benchmark.py --min-recall 11 + # 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 diff --git a/corpus/real-world/README.md b/corpus/real-world/README.md index 7510991e..6e7de846 100644 --- a/corpus/real-world/README.md +++ b/corpus/real-world/README.md @@ -43,5 +43,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) | | `ownership-handoff-use` | OWN002 | поток отдали потребителю (он его закрыл), потом ещё читали — use-after-handoff | | `ownership-handoff-use-transitive` | OWN002 | то же, но потребитель не закрывает сам, а **пробрасывает** владение дальше (transitive consume) | diff --git a/corpus/real-world/arraypool-span-view-after-return/after.cs b/corpus/real-world/arraypool-span-view-after-return/after.cs new file mode 100644 index 00000000..debff6f8 --- /dev/null +++ b/corpus/real-world/arraypool-span-view-after-return/after.cs @@ -0,0 +1,16 @@ +// AFTER (fixed). Finish all work through the Span view BEFORE returning the buffer to the pool, so +// the borrow's lifetime ends before the owner is recycled and nothing aliases freed memory. Same +// view, correct order — the case must stay SILENT (the no-false-positive arm). +using System; +using System.Buffers; + +static class PoolSpanViewAfterReturn +{ + static void Scramble(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Span view = buf.AsSpan(0, n); // view BORROWS buf + view[0] = 42; // written through the view BEFORE return + ArrayPool.Shared.Return(buf); // returned only after the borrow is done -> silent + } +} diff --git a/corpus/real-world/arraypool-span-view-after-return/before.cs b/corpus/real-world/arraypool-span-view-after-return/before.cs new file mode 100644 index 00000000..818d3c8c --- /dev/null +++ b/corpus/real-world/arraypool-span-view-after-return/before.cs @@ -0,0 +1,22 @@ +// BEFORE (buggy). A Span VIEW of a pooled buffer is written THROUGH after the buffer was returned +// to the pool. `buf.AsSpan(..)` borrows the buffer's memory into a `Span` local; once +// `Return(buf)` recycles the array the pool may hand it to another caller, so writing through the +// view now corrupts someone else's data — a silent, nasty aliasing bug. The view is a ref-struct +// BORROW: a use of it after the owner's release is a use-after-return. Unlike +// `arraypool-use-after-return` (the array itself is read after return), here the read goes through +// a STORED Span view, which the flat pass misses — the borrow has to be resolved to its owner. +// +// Wrapped in a class so the extractor's per-class flow pass visits it. +using System; +using System.Buffers; + +static class PoolSpanViewAfterReturn +{ + static void Scramble(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Span view = buf.AsSpan(0, n); // view BORROWS buf + ArrayPool.Shared.Return(buf); // buf goes back to the pool (recycled) ... + view[0] = 42; // ... but written through here (use-after-return) + } +} diff --git a/corpus/real-world/arraypool-span-view-after-return/case.own b/corpus/real-world/arraypool-span-view-after-return/case.own new file mode 100644 index 00000000..34533e51 --- /dev/null +++ b/corpus/real-world/arraypool-span-view-after-return/case.own @@ -0,0 +1,17 @@ +// OwnLang model. `acquire` == ArrayPool.Rent, `release` == ArrayPool.Return. The C# stores a Span +// VIEW of the buffer in a local (`Span view = buf.AsSpan()`) and writes through it AFTER the +// buffer was returned. A Span is a ref-struct BORROW of the buffer that cannot outlive the method, +// so the extractor lowers a use of the view to a use of the OWNER buffer — the write after +// `release` is the generic use-after-return (OWN002), the same code reading the buffer directly +// would give. The borrow is resolved to its owner in the extractor; the core sees a plain +// use-after-release. +module Corpus +resource Buffer { + acquire rent + release give +} +fn scramble(n: int) { + let buf = acquire Buffer(n); // ArrayPool.Rent + release buf; // ArrayPool.Return <-- too early + use buf; // write through the Span view AFTER return -> OWN002 +} diff --git a/corpus/real-world/arraypool-span-view-after-return/expected-diagnostics.txt b/corpus/real-world/arraypool-span-view-after-return/expected-diagnostics.txt new file mode 100644 index 00000000..3a36fa92 --- /dev/null +++ b/corpus/real-world/arraypool-span-view-after-return/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN002 diff --git a/corpus/real-world/arraypool-span-view-after-return/notes.md b/corpus/real-world/arraypool-span-view-after-return/notes.md new file mode 100644 index 00000000..8b1f6784 --- /dev/null +++ b/corpus/real-world/arraypool-span-view-after-return/notes.md @@ -0,0 +1,34 @@ +# Pooled-buffer Span VIEW used after return — the borrow checker's first bite + +**Pattern:** a rented `ArrayPool` buffer is sliced into a `Span`/`ReadOnlySpan` local +(`Span view = buf.AsSpan(0, n)`), the buffer is `Return`ed to the pool, and the code then +reads/writes **through the view**. The `Span` borrows the buffer's memory; once the array is +recycled the pool may hand it to another caller, so the view now aliases someone else's data — a +silent corruption (the same family as a use-after-free). It is the use of a **borrow after its +owner was released**. + +**What the checker says:** using a resource after it was released is the generic **OWN002** +(use-after-release) — the same code `arraypool-use-after-return` produces when the buffer itself is +read after return. + +**Why this case exists (the borrow / B4 frontier).** The flat pass and the existing pool flow only +saw a use-after-return when the **buffer local itself** was referenced after `Return`. When the read +goes through a **stored Span view** (`view[0]`), the buffer name never appears at the use site, so +the buffer looked released-and-untouched — a **miss**. Now the extractor models a +`Span`/`ReadOnlySpan` view of a tracked buffer as a **borrow**: a reference to the view local lowers +to a **use of the owner** (`ViewOwnerOf` resolves the view through its declaration's `AsSpan(..)` / +`new Span(buf)` initializer, the owner confirmed via the SemanticModel). The use after `Return` +then trips OWN002. This is the first slice of the **borrow checker on real C#** — lifetime/aliasing +analysis that the flat "disposed anywhere?" tools (and most general scanners) do not do — kept +purely in the extractor (the core needs no borrow concept; it sees a plain use-after-release). + +**Conservative (0 FP).** A view of an untracked/escaped buffer, or a view used **before** the +return (`after.cs`), adds no finding — the borrow only lowers to a use of an owner that is still +tracked, so it can never invent a release. Ref-struct `Span` cannot escape the method, which is +what makes "use of the view = use of the owner, here" sound. + +**Honesty / scope.** `case.own` is a faithful hand reduction (the borrow 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. First slice: `Span`/`ReadOnlySpan` views via `AsSpan()` / +`new Span(buf)`; `Memory` (which *can* escape) and view reassignment are deliberately left for +later rounds. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index 8987e682..6a491417 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -1,7 +1,11 @@ # P-007 — ArrayPool / Span borrow-view profile -- **Status:** in progress (P1) — **POOL001 (rented-not-returned) built**; - POOL002–005 (views, escape, double-return) next +- **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 - **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 4d04c897..3690a24b 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -760,11 +760,23 @@ 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). + // 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]=…`). var used = new SortedSet(StringComparer.Ordinal); foreach (var idn in expr.DescendantNodesAndSelf().OfType()) - if (tracked.Contains(idn.Identifier.Text) && !consumed.Contains(idn.Identifier.Text)) - used.Add(idn.Identifier.Text); + { + var nm = idn.Identifier.Text; + if (tracked.Contains(nm)) + { + if (!consumed.Contains(nm)) + used.Add(nm); + } + else if (ViewOwnerOf(idn, model) is { } owner + && tracked.Contains(owner) && !consumed.Contains(owner)) + used.Add(owner); + } foreach (var u in used) nodes.Add(new { op = "use", var = u, line = LineOf(expr) }); } @@ -815,6 +827,42 @@ 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(...)` +// (resolved via the symbol so it is the BCL Span-returning extension, not an unrelated method +// named AsSpan) or `new Span(owner, …)` / `new ReadOnlySpan(owner)`, where the source is a +// local identifier. Returns the owner local name, else null. A Span is a ref-struct BORROW — it +// 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) +{ + if (e is InvocationExpressionSyntax inv + && inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text == "AsSpan" + && m.Expression is IdentifierNameSyntax recv + && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ReturnType.Name: "Span" or "ReadOnlySpan" }) + return recv.Identifier.Text; + if (e is ObjectCreationExpressionSyntax oc + && oc.Type is GenericNameSyntax { Identifier.Text: "Span" or "ReadOnlySpan" } + && oc.ArgumentList is { Arguments.Count: > 0 } + && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg) + 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). +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 null; +} + // 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 ca02820abf370da1cdff291b1c5e3c2ac6f4dff3 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 16:31:39 +0000 Subject: [PATCH 2/2] fix(extractor): require resolved BCL Span symbols before lowering a view borrow MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex P2: SpanViewOwner matched on the NAME `AsSpan` / `Span` only, so a project's own `AsSpan` extension, a non-System type named `Span`, or an `AsSpan` that returns a span over a fresh copy would be treated as a borrow of the pooled buffer — a false OWN002 after `Return(buf)` even though the view does not alias it. Now the borrow is recognised by the RESOLVED symbols: `System.MemoryExtensions.AsSpan` (aliases its receiver array) and the `System.Span` / `System.ReadOnlySpan` constructor (wraps its array argument), both confirmed via `IsInNamespace(..., "System")`. A look-alike in another namespace is no longer mistaken for a borrow. The corpus case (`buf.AsSpan(0,n)` — the genuine BCL extension) still fires; behaviour on real BCL spans is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- frontend/roslyn/OwnSharp.Extractor/Program.cs | 23 +++++++++++-------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 3690a24b..0c5e6ad9 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -827,24 +827,29 @@ 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(...)` -// (resolved via the symbol so it is the BCL Span-returning extension, not an unrelated method -// named AsSpan) or `new Span(owner, …)` / `new ReadOnlySpan(owner)`, where the source is a -// local identifier. Returns the owner local name, else null. A Span is a ref-struct BORROW — it -// cannot escape the method — so a use of the view after the owner is released is a use of the -// owner after its release. +// 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) { if (e is InvocationExpressionSyntax inv && inv.Expression is MemberAccessExpressionSyntax m && m.Name.Identifier.Text == "AsSpan" && m.Expression is IdentifierNameSyntax recv - && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ReturnType.Name: "Span" or "ReadOnlySpan" }) + && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct } + && IsInNamespace(mct, "System")) return recv.Identifier.Text; if (e is ObjectCreationExpressionSyntax oc - && oc.Type is GenericNameSyntax { Identifier.Text: "Span" or "ReadOnlySpan" } && oc.ArgumentList is { Arguments.Count: > 0 } - && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg) + && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg + && model.GetSymbolInfo(oc).Symbol is IMethodSymbol { ContainingType: { Name: "Span" or "ReadOnlySpan" } sct } + && IsInNamespace(sct, "System")) return arg.Identifier.Text; return null; }