diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cadee87b..dea05e03 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -655,6 +655,43 @@ jobs: # the mislabel fix surfaced by the --body-throw-edges Npgsql capstone. echo "$out" | grep -qE "OWN001.*pooled buffer 'partialBuf' may not be returned to the pool on every path" \ || { echo "FAIL: expected the flow-path pooled-buffer partial-path label on 'partialBuf'"; exit 1; } + # b′ pooled-view REASSIGNMENT FP (ReassignedView): a Span view local reused for a SECOND + # rented buffer no longer borrows the first. The pre-reassignment read (`v[0]` while bufA is + # returned) is a REAL use-after-return -> EXACTLY ONE OWN002 on 'bufA'; the reassignment's own + # LHS and the post-reassignment read (`v[1]`, now bufB) must NOT be re-attributed to the + # released bufA (were two extra false OWN002 before the fix). bufB is returned after its last + # read -> silent. The exact count is the guard: a regression re-introduces 2 more on bufA. + nrv=$(echo "$out" | grep -cE "OWN002.*'bufA'") + [ "$nrv" = "1" ] \ + || { echo "FAIL: expected exactly 1 OWN002 on 'bufA' (pre-reassignment use-after-return), got $nrv"; exit 1; } + if echo "$out" | grep -qE "OWN002.*'bufB'"; then + echo "FAIL: a Span view reassigned to the live 'bufB' was wrongly flagged use-after-return"; exit 1 + fi + # Codex review on #98 — reslice-after-return: `sliced = sliced.Slice(1)` reads the STALE view + # on the RHS, so it still trips OWN002 on 'sb' (the assignment's own LHS must not suppress its + # own RHS). One finding only — the resliced view's forward owner is not tracked. + echo "$out" | grep -qE "OWN002.*'sb'" \ + || { echo "FAIL: expected OWN002 on 'sb' (reslice reads the returned buffer on the RHS)"; exit 1; } + # Codex review on #98 — `ref` arg is a USE: passing a stale view by `ref` after return reads + # the current value, so it is a use-after-return -> OWN002 on 'rb' (only `out` is exempt). + echo "$out" | grep -qE "OWN002.*'rb'" \ + || { echo "FAIL: expected OWN002 on 'rb' (ref arg reads the stale view after return)"; exit 1; } + # Codex review on #98 (follow-up) — same-call out arg: `Reinit(out ov, ov[0])` reads the stale + # view in a SIBLING argument (args evaluate before the callee writes the out param), so it + # trips OWN002 on 'ob'; the out rebind must not suppress a use in the same invocation. + echo "$out" | grep -qE "OWN002.*'ob'" \ + || { echo "FAIL: expected OWN002 on 'ob' (sibling-arg read before the out-write)"; exit 1; } + # Codex review on #98 (follow-up) — for-incrementor: the incrementor runs AFTER the body, so + # `fv[0]` reads the stale view on iteration 1 even though `fv = default` sits earlier in the + # header; the incrementor rebind must not suppress the body use -> OWN002 on 'fb'. + echo "$out" | grep -qE "OWN002.*'fb'" \ + || { echo "FAIL: expected OWN002 on 'fb' (for-incrementor must not suppress the body use)"; exit 1; } + # CodeRabbit review on #98 — out-arg rebind: after `Reset(out ov)` the view no longer borrows + # the returned 'obuf' (callee wrote an unknown value), so the later read is conservatively + # SILENT (an honest miss, never a false positive). + if echo "$out" | grep -qE "OWN002.*'obuf'"; then + echo "FAIL: an out-rebound view must not be attributed to the returned 'obuf'"; exit 1 + fi # closure-capture escape (precision): a SemaphoreSlim captured by a returned async # lambda outlives the method, so it cannot be disposed at method scope -> escaped -> # silent ('captured'). A SemaphoreSlim NOT captured and never disposed STILL leaks -> diff --git a/corpus/real-world/arraypool-span-view-after-return/notes.md b/corpus/real-world/arraypool-span-view-after-return/notes.md index 8b1f6784..fefff77e 100644 --- a/corpus/real-world/arraypool-span-view-after-return/notes.md +++ b/corpus/real-world/arraypool-span-view-after-return/notes.md @@ -30,5 +30,7 @@ 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. +`new Span(buf)`; `Memory` (which *can* escape) followed in the same round. **View reassignment** +is now handled too (b′, P-007 OQ#1): a view local reused for a different rented buffer no longer +attributes later reads to the original owner — see `FlowLocalsSample.ReassignedView`. Full +flow-sensitive per-path provenance (branch-merge, loop back-edges) is still deferred. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index e5572b6a..295e5792 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -103,9 +103,18 @@ Catching a real one of these is the milestone-4 success condition. ## Open questions -1. View provenance: track `arr.AsSpan()` → view-of-`arr` precisely, or - conservatively treat any `Span` derived from a rented array as a loan of it? - (Conservative first.) +1. **(resolved)** View provenance: track `arr.AsSpan()` → view-of-`arr` precisely, or + conservatively treat any `Span` derived from a rented array as a loan of it? — + **precise-by-identifier** was the implemented behaviour from the start (`ViewOwnerOf` + resolves the view through its declaration's `AsSpan`/`new Span` initializer to the + *specific* owner; two live buffers never conflate). The one gap was **reassignment**: the + owner was read from the declaration only, so after `v = otherBuf.AsSpan()` every later + reference to `v` was still attributed to the original buffer — a false OWN002 when that + original was already `Return`ed. Closed (b′): an assignment *target* is not a use, and a + reference past a reassignment of the view local drops the declared owner (silent). The fix + only ever removes a use, so it cannot manufacture a false positive; full flow-sensitive + per-path provenance (branch-merge, loop back-edges) is still deferred. Pinned by + `FlowLocalsSample.ReassignedView` (exactly one OWN002 on the pre-reassignment owner). 2. `Return(arr, clearArray: true)` vs sensitive buffers — does POOL005 tie into the existing sensitive-buffer/clear-on-release check (OWN024)? 3. How much of POOL004 (view escape) overlaps the existing OWN004/OWN015 escape diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 3b508f3b..73873c4d 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -1145,6 +1145,13 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet tracked, Semanti var used = new SortedSet(StringComparer.Ordinal); foreach (var idn in expr.DescendantNodesAndSelf().OfType()) { + // A pure DEF of the variable — the bare LHS of `v = …` or an `out` argument — writes it without + // reading it, so it is NOT a use of the resource (nor of a view's owner). Skipping it removes the + // over-count where the LHS of a view REASSIGNMENT (`v = other.AsSpan()`) was scanned as a use of + // the OLD owner (the pooled-view reassignment FP). A `ref` argument and an element/member write + // (`v[0] = …`, `v.X = …`) still READ `v`, so they are deliberately not skipped (Codex review on #98). + if (IsPureWrite(idn)) + continue; var nm = idn.Identifier.Text; if (tracked.Contains(nm)) { @@ -1182,6 +1189,30 @@ static void EmitOverspans(ExpressionSyntax expr, HashSet tracked, Semant nodes.Add(new { op = "overspan", var = o, line = LineOf(expr) }); } +// A pure DEF of its variable — a bare identifier that is the LHS of a SIMPLE assignment (`v = …`) or +// an `out` argument (`F(out v)`): it WRITES the variable without reading the current value, so it is +// not a use of the resource. A `ref` argument is deliberately NOT a pure write — the callee receives +// (and may read) the current value, so `ref v` is a USE as well as a possible rebind (Codex review on +// #98). Element/member writes (`v[0] = …`, `v.X = …`) read `v` to reach the target, so only a bare +// identifier on the assignment's Left (or an `out` slot) qualifies. Excludes pure defs from the use scan. +static bool IsPureWrite(IdentifierNameSyntax idn) => + (idn.Parent is AssignmentExpressionSyntax asg + && asg.IsKind(SyntaxKind.SimpleAssignmentExpression) + && asg.Left == idn) + || (idn.Parent is ArgumentSyntax arg + && arg.RefKindKeyword.IsKind(SyntaxKind.OutKeyword) + && arg.Expression == idn); + +// A REBINDING of its variable — a pure write (above) OR a `ref` argument (the callee may reassign it). +// The b′ reassignment check treats any of these, between a view local's declaration and a later +// reference, as dropping the declared owner. A `ref` is also a USE (it is not an IsPureWrite), so it +// still emits a use of the current owner at its own position and only suppresses LATER references. +static bool IsRebind(IdentifierNameSyntax idn) => + IsPureWrite(idn) + || (idn.Parent is ArgumentSyntax arg + && arg.RefKindKeyword.IsKind(SyntaxKind.RefKeyword) + && arg.Expression == idn); + // The field name an expression refers to: "_f" for `_f` or `this._f`, else null. static string? FieldName(ExpressionSyntax expr) => expr switch { @@ -1485,11 +1516,73 @@ static bool IsZeroInt(ExpressionSyntax arg, 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 }) + if (r.GetSyntax() is VariableDeclaratorSyntax { Initializer.Value: { } init } decl) + { + // b′ (pooled-view reassignment FP): the declaration's owner holds only until `view` is + // REASSIGNED. If a `view = …` (or a `ref`/`out` rebinding) of this same local sits between + // the declaration and THIS reference (source order), the reference no longer borrows the + // declared owner — its current owner is unknown, so go silent rather than attribute it to a + // possibly-released buffer. This only ever REMOVES a use (errs to a false negative, never a + // false positive). Matched on the resolved symbol, so a same-named local elsewhere is not + // mistaken for a rebinding. (Full flow-sensitive per-path provenance is left for later.) + if (ReassignedBetween(sym, decl, idn, model)) + return null; return ViewOwner(init, model); + } return null; } +// Is the local `sym` REBOUND (IsRebind: a direct `=` target, an `out`, or a `ref` argument) at a +// source position strictly after its declaration `decl` and strictly before the reference `use`, +// within the declaring member? Source-order and intraprocedural: straight-line code is exact; a +// reassignment on a non-taken branch suppresses conservatively (a possible miss, never a false +// positive). The b′ predicate behind ViewOwnerOf's reassignment suppression. Four writes do NOT +// count, because their effect is not yet visible to the use (all Codex/CodeRabbit review on #98): +// one in the SAME assignment as the use (`v = v.Slice(1)` — the RHS reads the still-current view); +// one that is a `ref`/`out` ARGUMENT of the same call as the use (`Reinit(out v, v[0])` — arguments +// evaluate before the callee writes the parameter); one in a `for` INCREMENTOR enclosing the use +// (`for (;;v=default) { v[0]=…; }` — the incrementor runs after the body, not at its header position); +// and one nested in a deferred body (a lambda / local function runs on invoke, not at its textual position). +static bool ReassignedBetween(ILocalSymbol sym, VariableDeclaratorSyntax decl, + IdentifierNameSyntax use, SemanticModel model) +{ + var scope = decl.Ancestors().FirstOrDefault(n => + n is BaseMethodDeclarationSyntax or AccessorDeclarationSyntax or LocalFunctionStatementSyntax); + if (scope is null) + return false; + var useAssign = use.FirstAncestorOrSelf(); + int lo = decl.SpanStart, hi = use.SpanStart; + foreach (var id in scope.DescendantNodes().OfType()) + { + if (id.SpanStart <= lo || id.SpanStart >= hi || !IsRebind(id)) + continue; + if (useAssign is not null && id.FirstAncestorOrSelf() == useAssign) + continue; // the use's OWN assignment, not a prior rebind + if (id.Parent is ArgumentSyntax { Parent: ArgumentListSyntax args } && args.Span.Contains(use.Span)) + continue; // ref/out rebind in the SAME call: args evaluate before the callee writes + if (id.Ancestors().OfType() + .FirstOrDefault(f => f.Incrementors.Any(i => i.Span.Contains(id.Span))) is { } forInc + && forInc.Span.Contains(use.Span)) + continue; // for-incrementor rebind runs AFTER the body, not at its header position + if (InDeferredBody(id, scope)) + continue; // a write inside a lambda/local fn does not run here + if (SymbolEqualityComparer.Default.Equals(model.GetSymbolInfo(id).Symbol, sym)) + return true; + } + return false; +} + +// Is `node` nested inside a lambda or local function that lies between it and `scope`? Such a body is +// DEFERRED — its statements run when it is invoked, not at their textual position — so the source- +// order reassignment scan must not treat a write inside one as a straight-line rebind (CodeRabbit #98). +static bool InDeferredBody(SyntaxNode node, SyntaxNode scope) +{ + for (var p = node.Parent; p is not null && p != scope; p = p.Parent) + if (p is AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax) + return true; + return false; +} + // 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 diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index b51fcaa6..8139f06f 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -597,6 +597,92 @@ public PooledHolder PooledIntoReturnedCtor(int n) var ctorMoved = ArrayPool.Shared.Rent(n); return new PooledHolder(ctorMoved); } + + // b′ pooled-view REASSIGNMENT FP (P-007 POOL002): a `Span` view of one rented buffer is reused for + // a SECOND rented buffer. Provenance is read from the view's declaration only, so before the fix + // every later reference to `v` was attributed to the original `bufA` — flagging the reassignment's + // own LHS and the post-reassignment read as use-after-return on `bufA` (two false OWN002). The fix: + // (1) an assignment TARGET is not a use, and (2) a reference past a reassignment drops the declared + // owner (silent). The pre-reassignment read `v[0]` (while `bufA` is returned) is a REAL + // use-after-return -> exactly ONE OWN002 on `bufA`; `bufB` is returned after its last read -> silent. + public void ReassignedView(int n, int m) + { + byte[] bufA = ArrayPool.Shared.Rent(n); + byte[] bufB = ArrayPool.Shared.Rent(m); + Span v = bufA.AsSpan(0, n); // v BORROWS bufA + ArrayPool.Shared.Return(bufA); // bufA recycled + v[0] = 1; // (i) read through v while bufA is gone -> OWN002 (bufA) + v = bufB.AsSpan(0, m); // reassign: v now borrows bufB (LHS v is a def, not a read) + v[1] = 2; // (ii) reads bufB, not bufA -> must be SILENT + ArrayPool.Shared.Return(bufB); + } + + // Codex review on #98: `sliced = sliced.Slice(1)` — the RHS reads the STILL-stale view, so the + // assignment's own LHS must not count as a prior rebind of its own RHS; a reslice of a returned + // buffer keeps tripping OWN002 on 'sb'. (Tracking the resliced owner FORWARD to later lines is the + // deferred re-slice gap, so this method has exactly the one RHS finding.) + public void SliceReassignAfterReturn(int n) + { + byte[] sb = ArrayPool.Shared.Rent(n); + Span sliced = sb.AsSpan(0, n); + ArrayPool.Shared.Return(sb); + sliced = sliced.Slice(1); // RHS reads the returned 'sb' -> OWN002 on 'sb' + } + + // Codex review on #98: a `ref` argument is NOT a pure write — the callee receives (and may read) + // the current value — so passing a stale view by `ref` after the buffer was returned is a + // use-after-return -> OWN002 on 'rb'. Only `out` is the pure def that is exempt from the use scan. + public void RefArgUseAfterReturn(int n) + { + byte[] rb = ArrayPool.Shared.Rent(n); + Span rv = rb.AsSpan(0, n); + ArrayPool.Shared.Return(rb); + Touch(ref rv); // ref passes the stale view (a read) -> OWN002 on 'rb' + } + + private static void Touch(ref Span s) => s = s.Slice(0); + + // Codex review on #98 (follow-up): arguments evaluate BEFORE the callee writes an `out` parameter, + // so `Reinit(out ov, ov[0])` reads the STALE view in the second argument while `ov` still aliases + // the returned 'ob' — a use-after-return -> OWN002 on 'ob'. The `out ov` rebind must not suppress a + // sibling argument of the same call (it is not yet in effect during argument evaluation). + public void OutArgSiblingUseAfterReturn(int n) + { + byte[] ob = ArrayPool.Shared.Rent(n); + Span ov = ob.AsSpan(0, n); + ArrayPool.Shared.Return(ob); + Reinit(out ov, ov[0]); // ov[0] reads the stale view before the out-write -> OWN002 on 'ob' + } + + private static void Reinit(out Span s, byte first) => s = default; + + // Codex review on #98 (follow-up): a `for` INCREMENTOR runs AFTER the body each iteration (and not + // at all before the first), so `fv[0]` reads the stale view on iteration 1 even though `fv = default` + // sits textually earlier in the loop header -> OWN002 on 'fb'. The incrementor rebind must not + // suppress a use in the loop body. + public void ForIncrementorBodyUseAfterReturn(int n) + { + byte[] fb = ArrayPool.Shared.Rent(n); + Span fv = fb.AsSpan(0, n); + ArrayPool.Shared.Return(fb); + for (int i = 0; i < n; fv = default, i++) // incrementor rebinds fv AFTER the body runs + fv[0] = 1; // reads the stale 'fb' on iteration 1 -> OWN002 on 'fb' + } + + // CodeRabbit review on #98: an `out` argument is a pure write that both drops the view from the use + // scan AND rebinds it, so a reference AFTER `Reset(out ov)` no longer borrows the returned 'obuf' — + // the callee wrote an unknown value, so we conservatively go silent (an honest miss, never a false + // positive). Documents the `out` contract (the `ref` case is `RefArgUseAfterReturn`): NO OWN002 on 'obuf'. + public void OutArgRebindSuppressesLaterUse(int n) + { + byte[] obuf = ArrayPool.Shared.Rent(n); + Span ov = obuf.AsSpan(0, n); + ArrayPool.Shared.Return(obuf); + Reset(out ov); // out-rebind: ov no longer borrows obuf + ov[0] = 1; // reads the callee's unknown value, not obuf -> SILENT + } + + private static void Reset(out Span s) => s = default; } // Takes ownership of a pooled buffer (Returns it on teardown) — the wrapper that