Skip to content

Commit 9fc8c27

Browse files
PhysShellPhysShell
authored
Merge pull request #206 from PhysShell/claude/own-net-issue-198-pool45
feat(P-007): pin POOL005 full-length view stored into a field; defer object-level escape
2 parents 664f4d9 + 9de7cbd commit 9fc8c27

9 files changed

Lines changed: 210 additions & 6 deletions

File tree

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

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,14 @@ fields/members, so it pins the *core* OWN025 verdict the field pass produces, wh
4040
the field-vs-local distinction lives in `before.cs` / `after.cs` (scanned end to end
4141
by the dotnet `corpus-benchmark` CI job). `before.cs` / `after.cs` are representative
4242
of the bug and its fix, not a verbatim PR diff. v0 of the field pass fires on the
43-
*first* full-length view of each pooled field per member (a read site); a full-length
44-
view of a pooled field **stored into another field** and only read elsewhere is a
45-
deeper alias-tracking frontier, left honest.
43+
*first* full-length view of each pooled field per member (a read site). A full-length
44+
view of a pooled field **stored into another field** is caught too — the pass fires on
45+
the view *expression*, so the RHS of `_view = _buf.AsMemory()` is itself a full-length
46+
view (pinned separately by
47+
[`arraypool-view-into-field-overread`](../arraypool-view-into-field-overread/notes.md)).
48+
The one shape left honest is a **bounded** view cached in a field then read after the
49+
owner is `Return`ed in a *different* member — an object-level, cross-member escape that
50+
needs interprocedural call-ordering (a deliberate deferral; follow-up POOL004 issue #205).
4651

4752
Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); replay target
4853
AiDotNet.Tensors pooled-buffer over-clear/over-read.

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

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// AFTER (fixed). The cached field view is bounded to the LOGICAL length the buffer
2+
// was rented for (`_buf.AsMemory(0, _n)`, `_meta.AsMemory(0, _metaLen)`), so it spans
3+
// only the valid `[0, n)` bytes and never the stale `[n, Length)` tail — no over-read.
4+
// A bounded view is not a full-length view, so the extractor's POOL005 field pass
5+
// returns null on it and this file is silent (the specificity half of the corpus
6+
// gate: the real fix raises nothing). The buffers are still `Return`ed in `Dispose`.
7+
using System;
8+
using System.Buffers;
9+
10+
sealed class FieldViewFramer : IDisposable
11+
{
12+
private byte[] _buf;
13+
private Memory<byte> _view;
14+
private int _n;
15+
16+
private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(64);
17+
private ReadOnlyMemory<byte> _metaView;
18+
private int _metaLen;
19+
20+
public void Capture(int n)
21+
{
22+
_n = n;
23+
_buf = ArrayPool<byte>.Shared.Rent(n);
24+
Fill(_buf, n);
25+
_view = _buf.AsMemory(0, _n); // FIX: bounded to the logical length
26+
_metaLen = 8;
27+
Fill(_meta, _metaLen); // write the valid metadata bytes first...
28+
_metaView = _meta.AsMemory(0, _metaLen); // ...then expose only those (bounded — no stale tail)
29+
}
30+
31+
public byte[] Flush() => _view.ToArray();
32+
public byte[] FlushMeta() => _metaView.ToArray();
33+
34+
public void Dispose()
35+
{
36+
if (_buf is not null)
37+
ArrayPool<byte>.Shared.Return(_buf);
38+
ArrayPool<byte>.Shared.Return(_meta);
39+
}
40+
41+
static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
42+
}

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

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
// BEFORE (buggy). The "view STORED INTO A FIELD" twin of the ArrayPool
2+
// full-length view over-read (P-007 POOL005; see `arraypool-field-fullspan-overread`
3+
// for the inline-read twin). A pooled array is oversized — `ArrayPool<T>.Shared.Rent(n)`
4+
// returns `Length >= n` — so a FULL-length view of it reaches past the logical
5+
// length `n` into the stale `[n, Length)` tail a previous renter left behind.
6+
//
7+
// Here the full-length view is not read inline; it is captured into ANOTHER field
8+
// (`_view = _buf.AsMemory()`, `_metaView = _meta.AsMemory()`) in one member and read
9+
// through in a LATER member (`Flush`/`FlushMeta`). Whoever reads the stored view
10+
// processes the `n` valid bytes together with that stale tail: a wrong-length read
11+
// and an information disclosure. `Span<T>` is a ref struct and cannot be a field, so
12+
// the field-stored view is a `Memory<T>` / `ReadOnlyMemory<T>` — the extractor's
13+
// POOL005 field pass fires on the full-length view EXPRESSION at the store, so the
14+
// bug is caught where the unbounded view is materialized. The fix is a bounded view,
15+
// `_buf.AsMemory(0, _n)` (see after.cs). Representative of the pattern (a pooled
16+
// scratch field whose whole-array view is cached for later flush/serialize), not
17+
// verbatim from one PR.
18+
using System;
19+
using System.Buffers;
20+
21+
sealed class FieldViewFramer : IDisposable
22+
{
23+
private byte[] _buf;
24+
private Memory<byte> _view; // a FULL-length view stored into a field
25+
private int _n;
26+
27+
// a SECOND pooled buffer, rented in the FIELD INITIALIZER, whose whole-array view
28+
// is cached into a ReadOnlyMemory field below.
29+
private readonly byte[] _meta = ArrayPool<byte>.Shared.Rent(64); // Length >= 64
30+
private ReadOnlyMemory<byte> _metaView;
31+
private int _metaLen;
32+
33+
public void Capture(int n)
34+
{
35+
_n = n;
36+
_buf = ArrayPool<byte>.Shared.Rent(n); // pooled buffer stored in a FIELD (Length >= n)
37+
Fill(_buf, n); // valid payload is _buf[0..n]
38+
_metaLen = 8;
39+
Fill(_meta, _metaLen); // valid payload is _meta[0.._metaLen)
40+
_view = _buf.AsMemory(); // <-- BUG: full-length view cached into a field
41+
_metaView = _meta.AsMemory(); // <-- BUG: full view (past _metaLen) into a ReadOnlyMemory field
42+
}
43+
44+
public byte[] Flush() => _view.ToArray(); // reads the cached full view: n bytes + stale [n, Length) tail
45+
public byte[] FlushMeta() => _metaView.ToArray();
46+
47+
public void Dispose()
48+
{
49+
if (_buf is not null) // null until Capture; Return(null) would throw
50+
ArrayPool<byte>.Shared.Return(_buf); // class-wide Return: no leak
51+
ArrayPool<byte>.Shared.Return(_meta); // initializer-rented, never null
52+
}
53+
54+
static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; }
55+
}

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

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

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
OWN025

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

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

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,16 @@
3232
spelling) over-reads the oversized `[n, Length)` tail; the per-method flow pass only tracks LOCAL
3333
rents, so a class-level field pass collects the pooled fields (shared `IsPoolRent`) and emits a
3434
synthetic `acquire`/`overspan`/`release` flow at the view → OWN025 (corpus
35-
`arraypool-field-fullspan-overread`). A full-length view STORED into another field (read only
36-
elsewhere) is the deeper alias-tracking frontier, left next
35+
`arraypool-field-fullspan-overread`). **A full-length view STORED into another field is covered
36+
too** — because the field pass fires on the full-length view *expression*, the RHS of a store
37+
`_view = _buf.AsMemory()` (a `Memory<T>`/`ReadOnlyMemory<T>` field; `Span<T>` is a ref struct and
38+
cannot be a field) is itself such an expression, so the over-read is caught **at the store**, where
39+
the unbounded view is materialized (corpus `arraypool-view-into-field-overread`). The one shape past
40+
this is a **deliberate deferral** (§Non-goals; "a deliberate deferral beats a soft false positive"):
41+
a **bounded** view cached in a field then read **after the owner is `Return`ed in a *different*
42+
member** — an object-level, cross-member escape whose bug-ness depends on the caller's method-call
43+
order, which needs interprocedural reasoning the per-method + field passes do not have. Tracked as a
44+
follow-up (POOL004 object-level escape, #205)
3745
- **Depends on:** `spec/OwnCore.md` (OWN001 leak, OWN002 use-after-release,
3846
OWN003 double-release, OWN008 release-while-borrowed), the buffer/borrow model
3947
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
6573
| **POOL002** view after return | a `Span`/`Memory` view used after the owner is `Return`ed | `OWN002` |
6674
| **POOL003** double return | `Return`/`Dispose` reachable twice for the same buffer (ArrayPool *and* MemoryPool) | `OWN003` ✅ |
6775
| **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` |
68-
| **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) |
76+
| **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) |
6977

7078
Resource mapping:
7179

‎tests/fixtures/cfg_parity.json‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,12 @@
5555
"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}",
5656
"diags": []
5757
},
58+
{
59+
"name": "corpus/real-world/arraypool-view-into-field-overread/case.own",
60+
"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",
61+
"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}",
62+
"diags": []
63+
},
5864
{
5965
"name": "corpus/real-world/field-dispose-via-exchange/case.own",
6066
"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",

0 commit comments

Comments
 (0)