fix(ownir): drop pooled-view provenance on reassignment (POOL002 FP)

.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 ->

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<T>(buf)`; `Memory<T>` (which *can* escape) and view reassignment are deliberately left for
-later rounds.
+`new Span<T>(buf)`; `Memory<T>` (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.

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<T>` 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

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -1145,6 +1145,13 @@
     var used = new SortedSet<string>(StringComparer.Ordinal);
     foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
     {
+        // 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 @@
         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 @@
     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<AssignmentExpressionSyntax>();
+    int lo = decl.SpanStart, hi = use.SpanStart;
+    foreach (var id in scope.DescendantNodes().OfType<IdentifierNameSyntax>())
+    {
+        if (id.SpanStart <= lo || id.SpanStart >= hi || !IsRebind(id))
+            continue;
+        if (useAssign is not null && id.FirstAncestorOrSelf<AssignmentExpressionSyntax>() == 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<ForStatementSyntax>()
+               .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
@@ -2122,7 +2215,7 @@
     .Split(Path.PathSeparator, StringSplitOptions.RemoveEmptyEntries)
     .Where(p => p.EndsWith(".dll", StringComparison.OrdinalIgnoreCase))
     .ToList();
 var refNames = new HashSet<string>(tpa.Select(Path.GetFileName), StringComparer.OrdinalIgnoreCase);
 var references = tpa.Select(p => (MetadataReference)MetadataReference.CreateFromFile(p)).ToList();
 // P-004 WPF profile: widen the reference set with assemblies named by the
 // OWN_EXTRA_REF_DIRS env var (colon-separated dirs) — e.g. the WindowsDesktop ref

frontend/roslyn/samples/FlowLocalsSample.cs

@@ -597,6 +597,92 @@
         var ctorMoved = ArrayPool<byte>.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<byte>.Shared.Rent(n);
+        byte[] bufB = ArrayPool<byte>.Shared.Rent(m);
+        Span<byte> v = bufA.AsSpan(0, n);            // v BORROWS bufA
+        ArrayPool<byte>.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<byte>.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<byte>.Shared.Rent(n);
+        Span<byte> sliced = sb.AsSpan(0, n);
+        ArrayPool<byte>.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<byte>.Shared.Rent(n);
+        Span<byte> rv = rb.AsSpan(0, n);
+        ArrayPool<byte>.Shared.Return(rb);
+        Touch(ref rv);                               // ref passes the stale view (a read) -> OWN002 on 'rb'
+    }
+
+    private static void Touch(ref Span<byte> 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<byte>.Shared.Rent(n);
+        Span<byte> ov = ob.AsSpan(0, n);
+        ArrayPool<byte>.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<byte> 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<byte>.Shared.Rent(n);
+        Span<byte> fv = fb.AsSpan(0, n);
+        ArrayPool<byte>.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<byte>.Shared.Rent(n);
+        Span<byte> ov = obuf.AsSpan(0, n);
+        ArrayPool<byte>.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<byte> s) => s = default;
 }
 
 // Takes ownership of a pooled buffer (Returns it on teardown) — the wrapper that