feat(P-007): pin POOL005 full-length view stored into a field; defer object-level escape

corpus/real-world/arraypool-field-fullspan-overread/notes.md

@@ -40,9 +40,14 @@ fields/members, so it pins the *core* OWN025 verdict the field pass produces, wh
 the field-vs-local distinction lives in `before.cs` / `after.cs` (scanned end to end
 by the dotnet `corpus-benchmark` CI job). `before.cs` / `after.cs` are representative
 of the bug and its fix, not a verbatim PR diff. v0 of the field pass fires on the
-*first* full-length view of each pooled field per member (a read site); a full-length
-view of a pooled field **stored into another field** and only read elsewhere is a
-deeper alias-tracking frontier, left honest.
+*first* full-length view of each pooled field per member (a read site). A full-length
+view of a pooled field **stored into another field** is caught too — the pass fires on
+the view *expression*, so the RHS of `_view = _buf.AsMemory()` is itself a full-length
+view (pinned separately by
+[`arraypool-view-into-field-overread`](../arraypool-view-into-field-overread/notes.md)).
+The one shape left honest is a **bounded** view cached in a field then read after the
+owner is `Return`ed in a *different* member — an object-level, cross-member escape that
+needs interprocedural call-ordering (a deliberate deferral; follow-up POOL004 issue #205).
 
 Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
 AiDotNet.Tensors pooled-buffer over-clear/over-read.

corpus/real-world/arraypool-view-into-field-overread/after.cs

@@ -0,0 +1,42 @@
+// AFTER (fixed). The cached field view is bounded to the LOGICAL length the buffer
+// was rented for (`_buf.AsMemory(0, _n)`, `_meta.AsMemory(0, _metaLen)`), so it spans
+// only the valid `[0, n)` bytes and never the stale `[n, Length)` tail — no over-read.
+// A bounded view is not a full-length view, so the extractor's POOL005 field pass
+// returns null on it and this file is silent (the specificity half of the corpus
+// gate: the real fix raises nothing). The buffers are still `Return`ed in `Dispose`.
+using System;
+using System.Buffers;
+
+sealed class FieldViewFramer : IDisposable
+{
+    private byte[] _buf;
+    private Memory<byte> _view;
+    private int _n;
+
+    private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(64);
+    private ReadOnlyMemory<byte> _metaView;
+    private int _metaLen;
+
+    public void Capture(int n)
+    {
+        _n = n;
+        _buf = ArrayPool<byte>.Shared.Rent(n);
+        Fill(_buf, n);
+        _view = _buf.AsMemory(0, _n);            // FIX: bounded to the logical length
+        _metaLen = 8;
+        Fill(_meta, _metaLen);                   // write the valid metadata bytes first...
+        _metaView = _meta.AsMemory(0, _metaLen); // ...then expose only those (bounded — no stale tail)
+    }
+
+    public byte[] Flush() => _view.ToArray();
+    public byte[] FlushMeta() => _metaView.ToArray();
+
+    public void Dispose()
+    {
+        if (_buf is not null)
+            ArrayPool<byte>.Shared.Return(_buf);
+        ArrayPool<byte>.Shared.Return(_meta);
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+}

corpus/real-world/arraypool-view-into-field-overread/before.cs

@@ -0,0 +1,55 @@
+// BEFORE (buggy). The "view STORED INTO A FIELD" twin of the ArrayPool
+// full-length view over-read (P-007 POOL005; see `arraypool-field-fullspan-overread`
+// for the inline-read twin). A pooled array is oversized — `ArrayPool<T>.Shared.Rent(n)`
+// returns `Length >= n` — so a FULL-length view of it reaches past the logical
+// length `n` into the stale `[n, Length)` tail a previous renter left behind.
+//
+// Here the full-length view is not read inline; it is captured into ANOTHER field
+// (`_view = _buf.AsMemory()`, `_metaView = _meta.AsMemory()`) in one member and read
+// through in a LATER member (`Flush`/`FlushMeta`). Whoever reads the stored view
+// processes the `n` valid bytes together with that stale tail: a wrong-length read
+// and an information disclosure. `Span<T>` is a ref struct and cannot be a field, so
+// the field-stored view is a `Memory<T>` / `ReadOnlyMemory<T>` — the extractor's
+// POOL005 field pass fires on the full-length view EXPRESSION at the store, so the
+// bug is caught where the unbounded view is materialized. The fix is a bounded view,
+// `_buf.AsMemory(0, _n)` (see after.cs). Representative of the pattern (a pooled
+// scratch field whose whole-array view is cached for later flush/serialize), not
+// verbatim from one PR.
+using System;
+using System.Buffers;
+
+sealed class FieldViewFramer : IDisposable
+{
+    private byte[] _buf;
+    private Memory<byte> _view;              // a FULL-length view stored into a field
+    private int _n;
+
+    // a SECOND pooled buffer, rented in the FIELD INITIALIZER, whose whole-array view
+    // is cached into a ReadOnlyMemory field below.
+    private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(64);   // Length >= 64
+    private ReadOnlyMemory<byte> _metaView;
+    private int _metaLen;
+
+    public void Capture(int n)
+    {
+        _n = n;
+        _buf = ArrayPool<byte>.Shared.Rent(n);   // pooled buffer stored in a FIELD (Length >= n)
+        Fill(_buf, n);                            // valid payload is _buf[0..n]
+        _metaLen = 8;
+        Fill(_meta, _metaLen);                    // valid payload is _meta[0.._metaLen)
+        _view = _buf.AsMemory();                  // <-- BUG: full-length view cached into a field
+        _metaView = _meta.AsMemory();             // <-- BUG: full view (past _metaLen) into a ReadOnlyMemory field
+    }
+
+    public byte[] Flush() => _view.ToArray();        // reads the cached full view: n bytes + stale [n, Length) tail
+    public byte[] FlushMeta() => _metaView.ToArray();
+
+    public void Dispose()
+    {
+        if (_buf is not null)                    // null until Capture; Return(null) would throw
+            ArrayPool<byte>.Shared.Return(_buf); // class-wide Return: no leak
+        ArrayPool<byte>.Shared.Return(_meta);    // initializer-rented, never null
+    }
+
+    static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
+}

corpus/real-world/arraypool-view-into-field-overread/case.own

@@ -0,0 +1,25 @@
+// OwnLang model of the ArrayPool full-length view over-read where the view is STORED
+// INTO A FIELD (P-007 POOL005; the "into a field" twin of arraypool-field-fullspan-
+// overread). `acquire` == ArrayPool.Rent into a field (the array is OVERSIZED:
+// Length >= n), `release` == ArrayPool.Return (in Dispose, class-wide). `overspan buf`
+// models the full-length view `_view = _buf.AsMemory()` cached into another field and
+// read through in a later member — it reaches past the logical length n into the stale
+// [n, Length) tail. The extractor's POOL005 field pass fires on the full-length view
+// EXPRESSION at the store, so the bug is caught where the unbounded view is
+// materialized; the bounded form `_buf.AsMemory(0, _n)` takes no full view, so the
+// fixed code has no `overspan` and is silent. `.own` has no fields/members, so this
+// single-function reduction pins the same core verdict the field pass produces; the
+// stored-into-a-field distinction lives in before.cs/after.cs (checked end to end by
+// the dotnet benchmark). The checker trips OWN025 (POOL005) at the view; the buffer is
+// still returned, so there is no leak (OWN001) and no use-after-return (OWN002).
+module Corpus
+resource Buffer {
+  acquire rent
+  release give
+  kind "pooled buffer"
+}
+fn capture_then_flush(n: int) {
+  let buf = acquire Buffer(n);   // _buf = ArrayPool.Rent(n)   (Length >= n)
+  overspan buf;                  // _view = _buf.AsMemory() cached into a field -> OWN025
+  release buf;                   // ArrayPool.Return (Dispose)
+}

corpus/real-world/arraypool-view-into-field-overread/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN025

corpus/real-world/arraypool-view-into-field-overread/notes.md

@@ -0,0 +1,44 @@
+# ArrayPool full-length view over-read where the view is STORED INTO A FIELD (POOL005)
+
+**Pattern:** the "into a field" twin of
+[`arraypool-field-fullspan-overread`](../arraypool-field-fullspan-overread/notes.md).
+A pooled array from `ArrayPool<T>.Shared.Rent(n)` is *oversized* — `Length >= n`, not
+exactly `n`. A **full-length** view of it (`_buf.AsMemory()`, no length bound) is not
+read inline; it is **cached into another field** (`_view = _buf.AsMemory()`,
+`_metaView = _meta.AsMemory()`) in one member and read through in a **later** member
+(`Flush`/`FlushMeta`). Whoever reads the stored view processes the `n` valid bytes
+**plus** the stale `[n, Length)` tail a *previous* renter left behind — a wrong-length
+read and an information disclosure. `Span<T>` is a `ref struct` and cannot be a field,
+so the field-stored view is a `Memory<T>` / `ReadOnlyMemory<T>`. The fix is a bounded
+view, `_buf.AsMemory(0, _n)`.
+
+**Why it is already caught.** The extractor's POOL005 **field pass** (`Program.cs`,
+`FullViewFieldOwner` + the per-member walk) fires on the full-length view
+**expression**, wherever its result goes: the RHS `_buf.AsMemory()` of the store
+`_view = _buf.AsMemory()` is exactly such an expression, so the over-read is caught
+**at the store** — where the unbounded view is materialized — via the same synthetic
+`acquire`/`overspan`/`release` flow the inline field twin uses (no new diagnostic, no
+new op). Verified end to end with the real extractor (`dotnet run … --flow-locals`) →
+OWN025 on both the `Memory` and `ReadOnlyMemory` field stores; the bounded `after.cs`
+is silent. This case turns that incidental coverage into a pinned contract (P-007 had
+it recorded as "the deeper alias-tracking frontier, left next").
+
+**What the checker says:** OWN025 `[resource: pooled buffer]` at the cached view. The
+buffers are still `Return`ed (in `Dispose`, class-wide via the POOL001 field pass), so
+there is no OWN001 leak and no OWN002 use-after-return; the only finding is the
+over-read itself.
+
+**Honesty / scope — the deferred boundary.** What is caught here is the full-length
+view *materialization* (the store). One shape past this is genuinely out of the
+current intraprocedural machinery and is **deliberately deferred** (P-007 §Non-goals;
+the issue's "a deliberate deferral beats a soft false positive"): a **bounded** view
+cached into a field and then read **after the owner is `Return`ed in a *different*
+member** — an object-level (cross-member) escape whose bug-ness depends on the caller's
+method-call order (`Setup → Done → Late` is a use-after-return; `Setup → Late → Done`
+is fine). Deciding that statically needs interprocedural / whole-program ordering the
+per-method + field passes do not have, so flagging it would be a soft false positive.
+Tracked as a follow-up (POOL004 object-level escape, #205). The `after.cs` here also exercises
+that safe bounded-and-cached shape and stays silent, pinning the non-firing side.
+
+Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
+AiDotNet.Tensors pooled-buffer over-clear/over-read.

docs/proposals/P-007-arraypool-span.md

@@ -32,8 +32,16 @@
   spelling) over-reads the oversized `[n, Length)` tail; the per-method flow pass only tracks LOCAL
   rents, so a class-level field pass collects the pooled fields (shared `IsPoolRent`) and emits a
   synthetic `acquire`/`overspan`/`release` flow at the view → OWN025 (corpus
-  `arraypool-field-fullspan-overread`). A full-length view STORED into another field (read only
-  elsewhere) is the deeper alias-tracking frontier, left next
+  `arraypool-field-fullspan-overread`). **A full-length view STORED into another field is covered
+  too** — because the field pass fires on the full-length view *expression*, the RHS of a store
+  `_view = _buf.AsMemory()` (a `Memory<T>`/`ReadOnlyMemory<T>` field; `Span<T>` is a ref struct and
+  cannot be a field) is itself such an expression, so the over-read is caught **at the store**, where
+  the unbounded view is materialized (corpus `arraypool-view-into-field-overread`). The one shape past
+  this is a **deliberate deferral** (§Non-goals; "a deliberate deferral beats a soft false positive"):
+  a **bounded** view cached in a field then read **after the owner is `Return`ed in a *different*
+  member** — an object-level, cross-member escape whose bug-ness depends on the caller's method-call
+  order, which needs interprocedural reasoning the per-method + field passes do not have. Tracked as a
+  follow-up (POOL004 object-level escape, #205)
 - **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
@@ -65,7 +73,7 @@ The corpus already pins two real cases (`corpus/real-world/arraypool-double-retu
 | **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` |
 | **POOL003** double return | `Return`/`Dispose` reachable twice for the same buffer (ArrayPool *and* MemoryPool) | `OWN003` ✅ |
 | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` |
-| **POOL005** read/copy past length | a full-length **view** (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`) reads/copies beyond the logical length (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is NOT flagged — it exposes nothing) | `OWN025` `[resource: pooled buffer]` ✅ (local **and** pooled `byte[]` FIELD; a view stored-into-a-field next) |
+| **POOL005** read/copy past length | a full-length **view** (`buf.AsSpan()`, no bound) **or** the `.Length` spelling (`buf.AsSpan(0, buf.Length)`) reads/copies beyond the logical length (a write/wipe like `Array.Clear(buf, 0, buf.Length)` is NOT flagged — it exposes nothing) | `OWN025` `[resource: pooled buffer]` ✅ (local, pooled `byte[]` FIELD, **and** a full-length view stored-into-a-field) |
 
 Resource mapping:
 

tests/fixtures/cfg_parity.json

@@ -55,6 +55,12 @@
       "cfg": "{\n  \"functions\": [\n    {\n      \"blocks\": [\n        {\n          \"id\": 0,\n          \"instrs\": [\n            {\n              \"line\": 15,\n              \"op\": \"acquire\",\n              \"resource\": \"Buffer\",\n              \"sym\": 1\n            },\n            {\n              \"line\": 16,\n              \"op\": \"release\",\n              \"sym\": 1\n            },\n            {\n              \"args\": [\n                {\n                  \"effect\": \"borrow\",\n                  \"sym\": 1\n                }\n              ],\n              \"callee\": \"BuildResult\",\n              \"line\": 17,\n              \"op\": \"invoke\"\n            }\n          ],\n          \"label\": \"entry\",\n          \"succ\": []\n        }\n      ],\n      \"entry\": 0,\n      \"has_return_type\": false,\n      \"name\": \"divide\",\n      \"params\": [\n        0\n      ],\n      \"symbols\": [\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 14,\n          \"is_param_borrow\": false,\n          \"kind\": \"plain\",\n          \"name\": \"n\",\n          \"origin\": \"n#14\",\n          \"resource_kind\": null,\n          \"type_name\": \"int\"\n        },\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 15,\n          \"is_param_borrow\": false,\n          \"kind\": \"owned\",\n          \"name\": \"quotient\",\n          \"origin\": \"quotient#15\",\n          \"resource_kind\": null,\n          \"type_name\": \"Buffer\"\n        }\n      ]\n    }\n  ],\n  \"ownlang_cfg_version\": 0\n}",
       "diags": []
     },
+    {
+      "name": "corpus/real-world/arraypool-view-into-field-overread/case.own",
+      "source": "// OwnLang model of the ArrayPool full-length view over-read where the view is STORED\n// INTO A FIELD (P-007 POOL005; the \"into a field\" twin of arraypool-field-fullspan-\n// overread). `acquire` == ArrayPool.Rent into a field (the array is OVERSIZED:\n// Length >= n), `release` == ArrayPool.Return (in Dispose, class-wide). `overspan buf`\n// models the full-length view `_view = _buf.AsMemory()` cached into another field and\n// read through in a later member — it reaches past the logical length n into the stale\n// [n, Length) tail. The extractor's POOL005 field pass fires on the full-length view\n// EXPRESSION at the store, so the bug is caught where the unbounded view is\n// materialized; the bounded form `_buf.AsMemory(0, _n)` takes no full view, so the\n// fixed code has no `overspan` and is silent. `.own` has no fields/members, so this\n// single-function reduction pins the same core verdict the field pass produces; the\n// stored-into-a-field distinction lives in before.cs/after.cs (checked end to end by\n// the dotnet benchmark). The checker trips OWN025 (POOL005) at the view; the buffer is\n// still returned, so there is no leak (OWN001) and no use-after-return (OWN002).\nmodule Corpus\nresource Buffer {\n  acquire rent\n  release give\n  kind \"pooled buffer\"\n}\nfn capture_then_flush(n: int) {\n  let buf = acquire Buffer(n);   // _buf = ArrayPool.Rent(n)   (Length >= n)\n  overspan buf;                  // _view = _buf.AsMemory() cached into a field -> OWN025\n  release buf;                   // ArrayPool.Return (Dispose)\n}\n",
+      "cfg": "{\n  \"functions\": [\n    {\n      \"blocks\": [\n        {\n          \"id\": 0,\n          \"instrs\": [\n            {\n              \"line\": 22,\n              \"op\": \"acquire\",\n              \"resource\": \"Buffer\",\n              \"sym\": 1\n            },\n            {\n              \"line\": 23,\n              \"op\": \"overspan\",\n              \"sym\": 1\n            },\n            {\n              \"line\": 24,\n              \"op\": \"release\",\n              \"sym\": 1\n            }\n          ],\n          \"label\": \"entry\",\n          \"succ\": []\n        }\n      ],\n      \"entry\": 0,\n      \"has_return_type\": false,\n      \"name\": \"capture_then_flush\",\n      \"params\": [\n        0\n      ],\n      \"symbols\": [\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 21,\n          \"is_param_borrow\": false,\n          \"kind\": \"plain\",\n          \"name\": \"n\",\n          \"origin\": \"n#21\",\n          \"resource_kind\": null,\n          \"type_name\": \"int\"\n        },\n        {\n          \"borrow_is_mut\": null,\n          \"buffer\": null,\n          \"def_line\": 22,\n          \"is_param_borrow\": false,\n          \"kind\": \"owned\",\n          \"name\": \"buf\",\n          \"origin\": \"buf#22\",\n          \"resource_kind\": \"pooled buffer\",\n          \"type_name\": \"Buffer\"\n        }\n      ]\n    }\n  ],\n  \"ownlang_cfg_version\": 0\n}",
+      "diags": []
+    },
     {
       "name": "corpus/real-world/field-dispose-via-exchange/case.own",
       "source": "// OwnLang model of NLog's TimeoutContinuation teardown (src/NLog/Internal/\n// TimeoutContinuation.cs, StopTimer). The owned Timer field is released by the atomic\n// detach-and-dispose idiom: `Interlocked.Exchange(ref _timeoutTimer, null)` hands back\n// the live timer and nulls the field, then `WaitForDispose(this Timer)` stops and\n// disposes it. before.cs omits the teardown — the generic OWN001 owned-field leak,\n// modelled here as an acquire with no `release`. after.cs releases it via the idiom,\n// which the extractor recognises by binding the exchange result to the field\n// (RefExchangeNulledField) and following the sink's dispose effect (CallReleasesReceiver).\nmodule Corpus\nresource Timer {\n  acquire create\n  release dispose\n  kind \"disposable\"\n  emit_type    \"Timer\"\n  emit_acquire \"new Timer({args})\"\n  emit_release \"Interlocked.Exchange(ref {0}, null)?.WaitForDispose()\"\n}\nfn Continuation(callback: int) {\n  let timer = acquire Timer(callback);   // _timer = new Timer(_ => { }, null, 0, 1000)\n  // no `release timer;` — the timer is never detached or disposed (OWN001)\n}\n",