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..0c5e6ad9 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,47 @@ 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) +{ + 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 { ContainingType: { Name: "MemoryExtensions" } mct } + && IsInNamespace(mct, "System")) + return recv.Identifier.Text; + 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 } + && 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). +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: