diff --git a/corpus/real-world/arraypool-field-fullspan-overread/notes.md b/corpus/real-world/arraypool-field-fullspan-overread/notes.md index 2da86869..3e153f33 100644 --- a/corpus/real-world/arraypool-field-fullspan-overread/notes.md +++ b/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. diff --git a/corpus/real-world/arraypool-view-into-field-overread/after.cs b/corpus/real-world/arraypool-view-into-field-overread/after.cs new file mode 100644 index 00000000..6ec2e76f --- /dev/null +++ b/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 _view; + private int _n; + + private readonly byte[] _meta = ArrayPool.Shared.Rent(64); + private ReadOnlyMemory _metaView; + private int _metaLen; + + public void Capture(int n) + { + _n = n; + _buf = ArrayPool.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.Shared.Return(_buf); + ArrayPool.Shared.Return(_meta); + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } +} diff --git a/corpus/real-world/arraypool-view-into-field-overread/before.cs b/corpus/real-world/arraypool-view-into-field-overread/before.cs new file mode 100644 index 00000000..5c72fc72 --- /dev/null +++ b/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.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` is a ref struct and cannot be a field, so +// the field-stored view is a `Memory` / `ReadOnlyMemory` — 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 _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.Shared.Rent(64); // Length >= 64 + private ReadOnlyMemory _metaView; + private int _metaLen; + + public void Capture(int n) + { + _n = n; + _buf = ArrayPool.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.Shared.Return(_buf); // class-wide Return: no leak + ArrayPool.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; } +} diff --git a/corpus/real-world/arraypool-view-into-field-overread/case.own b/corpus/real-world/arraypool-view-into-field-overread/case.own new file mode 100644 index 00000000..6dfe863a --- /dev/null +++ b/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) +} diff --git a/corpus/real-world/arraypool-view-into-field-overread/expected-diagnostics.txt b/corpus/real-world/arraypool-view-into-field-overread/expected-diagnostics.txt new file mode 100644 index 00000000..511ccfa9 --- /dev/null +++ b/corpus/real-world/arraypool-view-into-field-overread/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN025 diff --git a/corpus/real-world/arraypool-view-into-field-overread/notes.md b/corpus/real-world/arraypool-view-into-field-overread/notes.md new file mode 100644 index 00000000..a7b153df --- /dev/null +++ b/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.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` is a `ref struct` and cannot be a field, +so the field-stored view is a `Memory` / `ReadOnlyMemory`. 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. diff --git a/docs/proposals/P-007-arraypool-span.md b/docs/proposals/P-007-arraypool-span.md index d061fb2b..5717c9ab 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/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`/`ReadOnlyMemory` field; `Span` 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: diff --git a/tests/fixtures/cfg_parity.json b/tests/fixtures/cfg_parity.json index 96dba05f..1b084db7 100644 --- a/tests/fixtures/cfg_parity.json +++ b/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", diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 89f5da28..3e56bd0f 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -2617,6 +2617,24 @@ def _bcl(body: list) -> list: fails.append(f"OWN025 Rent->view reachability flow wrong: " f"{osp[0].flow if osp else None!r}") + # POOL005, view STORED INTO A FIELD (P-007 / issue #198). A full-length view of a + # pooled FIELD assigned into another field (`_view = _buf.AsMemory()`, read only + # elsewhere) is caught at the STORE: the extractor's field pass fires on the view + # EXPRESSION regardless of where the result is stored, so it emits the SAME + # pool-tagged acquire/overspan/release flow the inline field over-read does. This + # pins that fact shape — the frozen target the extractor is validated against — + # exactly as `dotnet run … --flow-locals` emits it (acquire carries `kind:"pool"`). + checks += 1 + vif = check_facts({"module": "M", "functions": [ + {"name": "FieldViewFramer.Capture", "file": "Framer.cs", + "body": [{"op": "acquire", "var": "_buf", "line": 13, "kind": "pool"}, + {"op": "overspan", "var": "_buf", "line": 14}, + {"op": "release", "var": "_buf", "line": 14}]}]}) + if [(x.code, x.line, x.kind) for x in vif] != [("OWN025", 14, "pooled buffer")]: + fails.append(f"POOL005 view-into-field: a pool-tagged acquire/overspan/release " + f"flow should raise OWN025 at the store/view line (14) tagged a " + f"pooled buffer, got {[(x.code, x.line, x.kind) for x in vif]}") + # --- output surfaces (Уровень 1): the same finding renders for a human, a # GitHub annotation, and an MSBuild/VS Error List line. The format lives # in the core (one checker), so the Action/script stay thin wrappers.