diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7e67d726..38f03c53 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -787,9 +787,11 @@ jobs: # checker covers both view kinds: a `Span`/`Memory` view of a pooled buffer (`buf.AsSpan()` / # `buf.AsMemory()`) is a borrow lowered to a use of the OWNER (`ViewOwner`), so using it # after `Return(buf)` trips OWN002 — including RETURNING a `Memory` view (which, unlike a - # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. Remaining - # backlog: a FIELD-mediated cross-method use-after-dispose (dispose in one method, use in - # another via shared state), a view stored in a FIELD, and an injected-source region-escape. - # A drop below the floor is a regression. - run: python scripts/benchmark.py --min-recall 13 + # ref-struct `Span`, can ESCAPE the method), a dangling borrow handed to the caller. A + # FULL-length view of a pooled buffer (`buf.AsSpan()` with no length bound) reaches past the + # rented logical length into the oversized tail -> OWN025 (P-007 POOL005, the over-read; the + # `arraypool-fullspan-overread` case). Remaining backlog: a FIELD-mediated cross-method + # use-after-dispose (dispose in one method, use in another via shared state), a view stored in + # a FIELD, and an injected-source region-escape. A drop below the floor is a regression. + run: python scripts/benchmark.py --min-recall 14 diff --git a/corpus/real-world/arraypool-fullspan-overread/after.cs b/corpus/real-world/arraypool-fullspan-overread/after.cs new file mode 100644 index 00000000..3c45a054 --- /dev/null +++ b/corpus/real-world/arraypool-fullspan-overread/after.cs @@ -0,0 +1,22 @@ +// AFTER (fixed). Every view is BOUNDED to the logical length — `buf.AsSpan(0, n)` — +// so only the `n` valid payload bytes are read; the oversized `[n, Length)` tail is +// never touched. No unbounded full view remains in either spelling (expression or +// initializer), so the extractor emits no `overspan` fact and the checker is silent. +using System; +using System.Buffers; + +static class PoolFullSpanOverread +{ + static byte[] Frame(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); + Emit(buf.AsSpan(0, n)); // bounded view: only the logical [0, n) + byte[] copy = buf.AsSpan(0, n).ToArray(); // bounded copy: only the logical [0, n) + ArrayPool.Shared.Return(buf); + return copy; + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-fullspan-overread/before.cs b/corpus/real-world/arraypool-fullspan-overread/before.cs new file mode 100644 index 00000000..991b898c --- /dev/null +++ b/corpus/real-world/arraypool-fullspan-overread/before.cs @@ -0,0 +1,33 @@ +// BEFORE (buggy). Reduction of the ArrayPool "full-length view over-read" bug +// (P-007 POOL005). A rented array is OVERSIZED: `ArrayPool.Shared.Rent(n)` +// returns an array of `Length >= n`, not exactly `n`. Here the code fills the +// first `n` bytes, then takes a FULL-length view — `buf.AsSpan()` with no length — +// so the `n` valid bytes are read together with the stale `[n, Length)` tail a +// *previous* renter left behind: a wrong-length read and an information disclosure. +// Both spellings are caught: the view used in an EXPRESSION (`Emit(buf.AsSpan())`) +// and the view in a local-declaration INITIALIZER (`var copy = buf.AsSpan()...`). +// The fix is a bounded view, `buf.AsSpan(0, n)` (see after.cs). Representative of +// the pattern (pooled-buffer over-read/over-copy in tensor and serialization code), +// not verbatim from one PR. +// +// Wrapped in a class so the extractor's per-class flow pass visits it; helpers +// stubbed so the reduction is self-contained. +using System; +using System.Buffers; + +static class PoolFullSpanOverread +{ + static byte[] Frame(int n) + { + byte[] buf = ArrayPool.Shared.Rent(n); + Fill(buf, n); // valid payload is buf[0..n] + Emit(buf.AsSpan()); // <-- BUG (expression): the WHOLE oversized array, + // n payload bytes + the stale [n, Length) tail + byte[] copy = buf.AsSpan().ToArray(); // <-- BUG (initializer): the same over-read in a local + ArrayPool.Shared.Return(buf); + return copy; + } + + static void Fill(byte[] b, int n) { for (int i = 0; i < n; i++) b[i] = (byte)i; } + static void Emit(ReadOnlySpan data) { } +} diff --git a/corpus/real-world/arraypool-fullspan-overread/case.own b/corpus/real-world/arraypool-fullspan-overread/case.own new file mode 100644 index 00000000..27e175fc --- /dev/null +++ b/corpus/real-world/arraypool-fullspan-overread/case.own @@ -0,0 +1,19 @@ +// OwnLang model of the ArrayPool full-length view over-read. `acquire` == +// ArrayPool.Rent (the array is OVERSIZED: Length >= n), `release` == +// ArrayPool.Return. `overspan buf` models a FULL-length view `buf.AsSpan()` (no +// length bound) handed to a consumer — it reaches past the logical length n into +// the stale [n, Length) tail. The bounded form `buf.AsSpan(0, n)` takes no full +// view, so the fixed code has no `overspan` and is silent. The checker trips +// OWN025 (POOL005) at the view; the buffer is still correctly 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 frame(n: int) { + let buf = acquire Buffer(n); // ArrayPool.Rent (Length >= n) + overspan buf; // buf.AsSpan() — full-length view past n -> OWN025 + release buf; // ArrayPool.Return +} diff --git a/corpus/real-world/arraypool-fullspan-overread/expected-diagnostics.txt b/corpus/real-world/arraypool-fullspan-overread/expected-diagnostics.txt new file mode 100644 index 00000000..511ccfa9 --- /dev/null +++ b/corpus/real-world/arraypool-fullspan-overread/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN025 diff --git a/corpus/real-world/arraypool-fullspan-overread/notes.md b/corpus/real-world/arraypool-fullspan-overread/notes.md new file mode 100644 index 00000000..0cee5e68 --- /dev/null +++ b/corpus/real-world/arraypool-fullspan-overread/notes.md @@ -0,0 +1,35 @@ +# ArrayPool full-length view over-read (POOL005) + +**Pattern:** a pooled array from `ArrayPool.Shared.Rent(n)` is *oversized* — the +pool returns an array of `Length >= n`, not exactly `n`. Code that takes a +FULL-length view of it (`buf.AsSpan()` / `buf.AsMemory()` / `new Span(buf)`, all +with **no length bound**) and reads, copies, or writes through that view processes +the `n` valid bytes **plus** the stale `[n, Length)` tail — bytes a *previous* +renter left behind. That is a correctness bug (wrong length) and an information +disclosure (a prior renter's data leaks out). The fix is a bounded view: +`buf.AsSpan(0, n)`. + +This is P-007's **POOL005** ("clear/copy past the logical length") — the over-read / +over-copy vehicle is the unbounded view. It is distinct from **OWN024** (a +*sensitive* buffer not cleared on release): POOL005 is reading/copying *too much*; +OWN024 is clearing *too little*. + +**What the checker says:** the OwnLang model trips **OWN025** +`[resource: pooled buffer]` at the view. The extractor recognises an unbounded +`AsSpan()`/`AsMemory()`/`new Span(buf)` over a `Rent`ed local (by the resolved +`System.MemoryExtensions` / `System.Span` BCL symbols, so a look-alike is not +mistaken for it) and emits an `overspan` fact; the core — and the hand `case.own` +reduction — raise OWN025. The buffer is still `Return`ed, so there is no OWN001 +leak and no OWN002 use-after-return; the only finding is the over-read itself. + +**Honesty / scope.** `case.own` is a faithful hand reduction (not C# ingested by the +checker); `before.cs` / `after.cs` are representative of the bug and its fix, not a +verbatim PR diff. The extractor catches the unbounded view both as an *expression* +(`Emit(buf.AsSpan())`, `buf.AsSpan().CopyTo(...)`) and in a local-declaration +*initializer* — the over-copy `var copy = buf.AsSpan().ToArray();` and the +view-local `Span s = buf.AsSpan();` alike, since the full view lives in the +initializer either way. The remaining spelling is `Array.Clear(buf, 0, buf.Length)` +(a length argument of `buf.Length` rather than an unbounded view), a follow-up. + +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 51a282a7..61134c3a 100644 --- a/docs/proposals/P-007-arraypool-span.md +++ b/docs/proposals/P-007-arraypool-span.md @@ -6,8 +6,14 @@ owner (`ViewOwner` in the extractor), so using it after `Return` trips OWN002; because a `Memory` (unlike a ref-struct `Span`) can leave the method, RETURNING a dangling `Memory` view is caught at the escape (corpus `arraypool-span-view-after-return`, `arraypool-memory-view-escape`). - The borrow checker on real C#. POOL003 (double-return — flow already catches OWN003), a view - stored in a FIELD, and POOL005 (clear-past-length) next + The borrow checker on real C#. **POOL005 (full-length view over-read → OWN025) first slice + built** — an unbounded `buf.AsSpan()` / `buf.AsMemory()` / `new Span(buf)` over a `Rent`ed + local reaches past the logical length `n` into the oversized `[n, Length)` tail; the extractor + emits an `overspan` fact and the core raises OWN025 `[resource: pooled buffer]` at the view — + both when the view is used in an EXPRESSION (`Emit(buf.AsSpan())`) and when it is a local-decl + INITIALIZER (`var copy = buf.AsSpan().ToArray();`, `Span s = buf.AsSpan();`) (corpus + `arraypool-fullspan-overread`). POOL003 (double-return — flow already catches OWN003), a view + stored in a FIELD, and the `Array.Clear(buf, 0, buf.Length)` spelling of POOL005 next - **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 @@ -39,7 +45,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` reachable twice for the same buffer | `OWN003` | | **POOL004** view escapes | a borrowed `Span` returned/stored beyond the owner's lifetime | `OWN004`/`OWN008` | -| **POOL005** clear/copy past length | write/clear beyond the logical length of the rented region | (buffer-policy check) | +| **POOL005** clear/copy past length | a full-length view (`buf.AsSpan()`, no bound) reads/copies beyond the logical length of the rented region | `OWN025` `[resource: pooled buffer]` ✅ (view in an expression or initializer; `Array.Clear(buf, 0, buf.Length)` next) | Resource mapping: diff --git a/examples/gallery/11_overspan_full_view.own b/examples/gallery/11_overspan_full_view.own new file mode 100644 index 00000000..711046be --- /dev/null +++ b/examples/gallery/11_overspan_full_view.own @@ -0,0 +1,16 @@ +// POOL005 — a full-length Span view of a pooled buffer reaches past its logical +// length. `ArrayPool.Rent(n)` hands back an OVERSIZED array (Length >= n); a view +// with no length bound (`buf.AsSpan()`) spans the whole array, so reading or +// copying through it exposes the stale [n, Length) tail a previous renter left. +// Real C#: `Emit(buf.AsSpan())` where `Emit(buf.AsSpan(0, n))` was meant. +module Gallery +resource Buffer { + acquire rent + release give + kind "pooled buffer" +} +fn frame(n: int) { + let buf = acquire Buffer(n); + overspan buf; // full-length view -> OWN025 + release buf; +} diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index d38196f0..8d40f695 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -450,12 +450,19 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, SemanticM InjectThrowEdge(ld, nodes, onThrow); if (ld.UsingKeyword == default) foreach (var v in ld.Declaration.Variables) + { if (tracked.Contains(v.Identifier.Text) && (v.Initializer?.Value is ObjectCreationExpressionSyntax or ImplicitObjectCreationExpressionSyntax || IsPoolRent(v.Initializer?.Value, model) // ArrayPool Rent || IsOwningFactory(v.Initializer?.Value, model))) // File / crypto Create* factory nodes.Add(new { op = "acquire", var = v.Identifier.Text, line = LineOf(v) }); + // POOL005: a full-length view in the initializer — `var copy = buf.AsSpan().ToArray();` + // — over-reads the pooled tail just as `Emit(buf.AsSpan());` does. EmitFlowExpr is not + // called on a non-acquire initializer, so scan it here for the overspan (Codex review). + if (v.Initializer?.Value is { } vinit) + EmitOverspans(vinit, tracked, model, nodes); + } return true; case ExpressionStatementSyntax es: InjectThrowEdge(es, nodes, onThrow); @@ -796,6 +803,25 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet tracked, Semanti } foreach (var u in used) nodes.Add(new { op = "use", var = u, line = LineOf(expr) }); + // POOL005: a full-length view of a pooled buffer anywhere in this expression -> overspan/OWN025. + EmitOverspans(expr, tracked, model, nodes); +} + +// POOL005: emit one `overspan` op per tracked pooled buffer that `expr` takes a FULL-LENGTH view of +// (no length bound) — the core raises OWN025. Walks the whole expression so a view nested in a call +// (`Sink.Write(buf.AsSpan())`), a chain (`buf.AsSpan().ToArray()`), or a local-declaration +// initializer (`var copy = buf.AsSpan().ToArray();`) is found; a BOUNDED view (`buf.AsSpan(0, n)`) +// is not matched (FullViewOwner returns null). Among `tracked` locals only pooled buffers are the +// arrays the BCL AsSpan/Span symbols bind to, so this never fires on a tracked IDisposable / factory +// result. Shared by the expression-statement and local-declaration lowering paths. +static void EmitOverspans(ExpressionSyntax expr, HashSet tracked, SemanticModel model, List nodes) +{ + var overspanned = new SortedSet(StringComparer.Ordinal); + foreach (var node in expr.DescendantNodesAndSelf().OfType()) + if (FullViewOwner(node, model) is { } owner && tracked.Contains(owner)) + overspanned.Add(owner); + foreach (var o in overspanned) + nodes.Add(new { op = "overspan", var = o, line = LineOf(expr) }); } // The field name an expression refers to: "_f" for `_f` or `this._f`, else null. @@ -874,6 +900,35 @@ e is InvocationExpressionSyntax i return null; } +// The tracked owner buffer a FULL-LENGTH view spans (no length bound), else null. POOL005: +// `buf.AsSpan()` / `buf.AsMemory()` taken with NO arguments span `[0, Length)` — the WHOLE backing +// array — and `new Span(buf)` / `new Memory(buf)` with only the array argument do the same. A +// pooled array is oversized (`ArrayPool.Rent(n)` returns `Length >= n`), so such a view reaches past +// the logical length `n` into the stale `[n, Length)` tail (a previous renter's bytes): reading or +// copying through it processes that stale data — a correctness bug and a potential disclosure. A +// BOUNDED view (`buf.AsSpan(0, n)`, `new Span(buf, 0, n)`) has a length argument and returns null +// here — it does not over-read. Recognised by the SAME resolved BCL symbols as `ViewOwner`, so a +// project's own `AsSpan`/`Span` look-alike is not mistaken for the over-read. +static string? FullViewOwner(ExpressionSyntax? e, SemanticModel model) +{ + if (e is InvocationExpressionSyntax inv + && inv.Expression is MemberAccessExpressionSyntax m + && m.Name.Identifier.Text is "AsSpan" or "AsMemory" + && inv.ArgumentList.Arguments.Count == 0 // no start/length -> whole array + && m.Expression is IdentifierNameSyntax recv + && model.GetSymbolInfo(inv).Symbol is IMethodSymbol { ContainingType: { Name: "MemoryExtensions" } mct } + && IsInNamespace(mct, "System")) + return recv.Identifier.Text; + if (e is BaseObjectCreationExpressionSyntax oc + && oc.ArgumentList is { Arguments.Count: 1 } // only the array -> whole array + && oc.ArgumentList.Arguments[0].Expression is IdentifierNameSyntax arg + && model.GetSymbolInfo(oc).Symbol is IMethodSymbol + { ContainingType: { Name: "Span" or "ReadOnlySpan" or "Memory" or "ReadOnlyMemory" } sct } + && IsInNamespace(sct, "System")) + return arg.Identifier.Text; + return null; +} + // If `idn` references a Span/ReadOnlySpan/Memory/ReadOnlyMemory VIEW local declared from an owner // buffer (`Memory view = owner.AsMemory(…)`), the owner buffer's local name — so a use of the // view (including RETURNING it, an escape) lowers to a use of the owner (the borrow). Resolved diff --git a/ownlang/analysis.py b/ownlang/analysis.py index 256e2cd1..9964b745 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -58,6 +58,7 @@ Invoke, Kind, MoveInto, + Overspan, Release, Return, Symbol, @@ -370,6 +371,18 @@ def step(self, ins: Instr, st: State) -> None: f"region", ins.line) return + if isinstance(ins, Overspan): + # POOL005: a full-length view over the whole pooled array reaches past + # the logical length it was rented for (the oversized [n, Length) tail). + # A property of the view-creation site, not of the owner's flow state — + # so it raises regardless of OWNED/RELEASED and changes no state. + self.err("OWN025", + f"'{ins.sym.name}' is viewed at its full backing length, past " + f"the logical length it was rented for (over-read / " + f"over-clear)", ins.line, subject=ins.sym.origin, + resource_kind=ins.sym.resource_kind) + return + if isinstance(ins, Invoke): for sym, eff in ins.args: if sym is not None: diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index e71fe17d..f3006e1a 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -112,6 +112,18 @@ class Use: line: int +@dataclass(frozen=True) +class Overspan: + """`overspan x;` — a full-length view (`Span`/`Memory`) is taken over the + whole pooled buffer `x`, reaching past the logical length it was rented for. + A pooled array is oversized (`ArrayPool.Rent(n)` returns `Length >= n`), so a + view with no length bound (`buf.AsSpan()`, `new Span(buf)`) exposes — and a + `.Clear()`/`.Fill()` through it overwrites — the stale `[n, Length)` tail. The + over-read / over-clear is POOL005; the fix is a bounded view `buf.AsSpan(0, n)`.""" + var: str + line: int + + @dataclass(frozen=True) class Call: """callee(args); -> a call to a declared extern or local fn""" @@ -164,7 +176,8 @@ class Subscribe: line: int -Stmt = Let | Release | Use | Call | BorrowBlock | If | While | Return | Subscribe +Stmt = (Let | Release | Use | Overspan | Call | BorrowBlock | If | While + | Return | Subscribe) # ---- top level ------------------------------------------------------------ diff --git a/ownlang/cfg.py b/ownlang/cfg.py index 7ee2bca2..ad38e160 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -117,6 +117,15 @@ class Use: line: int +@dataclass +class Overspan: + """A full-length view (`Span`/`Memory`) taken over the whole pooled buffer + `sym`, reaching past the logical length it was rented for (POOL005). Carries + no state transition — the owner stays OWNED; it only raises OWN025 at `line`.""" + sym: Symbol + line: int + + @dataclass class Invoke: """A resolved call. `args` pairs each argument's resolved Symbol (or None @@ -148,7 +157,7 @@ class Return: line: int -Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Invoke +Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Overspan | Invoke | BorrowStart | BorrowEnd | Return) @@ -332,6 +341,17 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: if sym is not None: cur.instrs.append(Use(sym, st.line)) return cur + if isinstance(st, A.Overspan): + sym = self.lookup(st.var, st.line) + if sym is not None: + if sym.kind != Kind.OWNED: + self.diags.append(Diagnostic( + "OWN034", + f"cannot take a full-length view of '{st.var}': it is not " + f"an owned resource ({sym.kind.name.lower()})", st.line)) + else: + cur.instrs.append(Overspan(sym, st.line)) + return cur if isinstance(st, A.Call): return self.lower_call(st, cur) if isinstance(st, A.BorrowBlock): diff --git a/ownlang/codegen.py b/ownlang/codegen.py index 96854f82..4fbf7581 100644 --- a/ownlang/codegen.py +++ b/ownlang/codegen.py @@ -442,6 +442,12 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: return [f"{ind}{self._release_stmt(st.var, rt)}"] if isinstance(st, A.Use): return [f"{ind}Use({st.var});"] + if isinstance(st, A.Overspan): + # POOL005: a full-length view over the whole pooled array (no length + # bound) — reaches past the logical length it was rented for. The + # bounded, correct form is `{st.var}.AsSpan(0, n)`. + return [f"{ind}{st.var}.AsSpan(); " + f"// full-length view over the pooled tail (over-read)"] if isinstance(st, A.Call): return [f"{ind}{st.callee}({', '.join(self._arg(a) for a in st.args)});"] if isinstance(st, A.BorrowBlock): diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 12710994..66d8c4d8 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -56,6 +56,7 @@ class Severity(Enum): "OWN021": "stack allocation requires a statically known bound", "OWN023": "scratch fallback forbidden but the size may exceed the inline limit", "OWN024": "sensitive buffer is not cleared on release", + "OWN025": "full-length view of a pooled buffer reaches past its logical length", # ---- unsupported ---- "OWN020": "unsupported construct (out of scope for the MVP)", # ---- name resolution & structural ---- diff --git a/ownlang/lexer.py b/ownlang/lexer.py index b3f14b3b..4ed3daed 100644 --- a/ownlang/lexer.py +++ b/ownlang/lexer.py @@ -34,6 +34,7 @@ class Tok(Enum): CONSUME = auto() AS = auto() USE = auto() + OVERSPAN = auto() IF = auto() ELSE = auto() WHILE = auto() @@ -80,6 +81,7 @@ class Tok(Enum): "consume": Tok.CONSUME, "as": Tok.AS, "use": Tok.USE, + "overspan": Tok.OVERSPAN, "if": Tok.IF, "else": Tok.ELSE, "while": Tok.WHILE, diff --git a/ownlang/ownir.py b/ownlang/ownir.py index a88b77ee..ce918e4a 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -111,6 +111,7 @@ Let, LifetimeDecl, Module, + Overspan, Param, Release, ResourceDecl, @@ -998,6 +999,13 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str, h = localmap.get(str(n.get("var"))) if h is not None: body.append(Use(h, line)) + elif op == "overspan": + # POOL005: a full-length Span/Memory view of a pooled buffer. The + # extractor emits this only for a Rent'd local viewed with no length + # bound; it routes to the same core op the `.own` `overspan` lowers to. + h = localmap.get(str(n.get("var"))) + if h is not None: + body.append(Overspan(h, line)) elif op == "release": h = localmap.get(str(n.get("var"))) if h is not None: @@ -1102,6 +1110,19 @@ def check_facts(facts: dict[str, Any]) -> list[Finding]: # P-016 B0b/B2: path-sensitive local-IDisposable verdicts. The code is # the core's (OWN001/002/003/009); phrase it for the C# local. name = event + if d.code == "OWN025": + # POOL005: a full-length view of a pooled buffer reaches past its + # logical length. Report at the VIEW site (d.line — where the + # unbounded AsSpan/Memory is taken), not the Rent site, and tag it + # a pooled buffer rather than the generic disposable. + findings.append(Finding( + file=sub["file"], line=d.line, code=d.code, + component=component, event=name, handler="", + message=(f"pooled buffer '{name}' is viewed at its full " + f"length, past the logical length it was rented for " + f"(over-read / over-clear)"), + kind="pooled buffer")) + continue if d.code == "OWN001": # OWN001 spans "released on 0 paths" and "released on some but not all" # — the core's "not on every path". Word it from whether the flow body diff --git a/ownlang/parser.py b/ownlang/parser.py index e05ada1b..1fba3363 100644 --- a/ownlang/parser.py +++ b/ownlang/parser.py @@ -19,8 +19,9 @@ param := IDENT ":" type ("lifetime" IDENT)? type := "&" "mut"? IDENT | IDENT block := "{" stmt* "}" - stmt := let | release | use | call | borrow | if | while | return | subscribe + stmt := let | release | use | overspan | call | borrow | if | while | return | subscribe subscribe := "subscribe" "self" "to" IDENT ";" // self/to contextual + overspan := "overspan" IDENT ";" // full-length pooled view (POOL005) let := "let" IDENT "=" rhs ";" rhs := "acquire" IDENT "(" args? ")" | "move" IDENT | bufferintent | IDENT | INT @@ -300,6 +301,8 @@ def parse_stmt(self) -> A.Stmt: return self.parse_release() if self.at(Tok.USE): return self.parse_use() + if self.at(Tok.OVERSPAN): + return self.parse_overspan() if self.at(Tok.BORROW) or self.at(Tok.BORROW_MUT): return self.parse_borrow() if self.at(Tok.IF): @@ -419,6 +422,12 @@ def parse_use(self) -> A.Use: self.eat(Tok.SEMI) return A.Use(var=v.text, line=kw.line) + def parse_overspan(self) -> A.Overspan: + kw = self.eat(Tok.OVERSPAN) + v = self.eat(Tok.IDENT) + self.eat(Tok.SEMI) + return A.Overspan(var=v.text, line=kw.line) + def parse_call(self) -> A.Call: nm = self.eat(Tok.IDENT) self.eat(Tok.LPAREN) diff --git a/scripts/metamorphic.py b/scripts/metamorphic.py index 0e4c96af..8417e254 100644 --- a/scripts/metamorphic.py +++ b/scripts/metamorphic.py @@ -50,6 +50,7 @@ Let, Module, Move, + Overspan, Release, Return, Subscribe, @@ -131,6 +132,8 @@ def _sub_stmt(s: Stmt, old: str, new: str) -> Stmt: return replace(s, var=new) if s.var == old else s if isinstance(s, Use): return replace(s, var=new) if s.var == old else s + if isinstance(s, Overspan): + return replace(s, var=new) if s.var == old else s if isinstance(s, Call): return replace(s, args=[_sub_expr(a, old, new) for a in s.args]) if isinstance(s, BorrowBlock): @@ -185,7 +188,7 @@ def walk(body: list[Stmt]) -> None: if isinstance(s, Let): names.add(s.name) names.update(_expr_names(s.rhs)) - elif isinstance(s, (Release, Use)): + elif isinstance(s, (Release, Use, Overspan)): names.add(s.var) elif isinstance(s, Call): for a in s.args: @@ -243,7 +246,7 @@ def _touches(s: Stmt) -> set[str] | None: simple, reorderable statement (control flow / borrow blocks are excluded).""" if isinstance(s, Let): return {s.name} | _expr_names(s.rhs) - if isinstance(s, (Release, Use)): + if isinstance(s, (Release, Use, Overspan)): return {s.var} if isinstance(s, Call): return set().union(set(), *(_expr_names(a) for a in s.args)) diff --git a/spec/BufferPolicies.md b/spec/BufferPolicies.md index dc95f949..7b2c720d 100644 --- a/spec/BufferPolicies.md +++ b/spec/BufferPolicies.md @@ -39,6 +39,15 @@ inline = 256)`. The namespace is `Buffer`; the method selects the mode. - **B7 — requested length preserved.** `scratch` lowering preserves the *requested* logical length, independent of whether the stack or pool branch is taken. +- **B9 — full view stays within the logical length.** A pooled buffer is + *oversized*: `ArrayPool.Rent(n)` returns an array of `Length >= n`, not + exactly `n`. A FULL-length view of it — `buf.AsSpan()` / `buf.AsMemory()` / + `new Span(buf)` with **no length bound** — reaches past the requested length + `n` into the stale `[n, Length)` tail (a previous renter's bytes); reading or + copying through it is an over-read / over-copy → **OWN025**. The fix is a bounded + view, `buf.AsSpan(0, n)`. (P-007 POOL005; the OwnLang model op is `overspan b`. + Distinct from B6/OWN024, which is clearing *too little* of a sensitive buffer — + this is reading *too much*.) ## Buffer options and `policy` blocks diff --git a/spec/Diagnostics.md b/spec/Diagnostics.md index 4e7ed015..a3171d58 100644 --- a/spec/Diagnostics.md +++ b/spec/Diagnostics.md @@ -42,6 +42,7 @@ See [BufferPolicies.md](BufferPolicies.md). | OWN021 | stack allocation requires a statically known bound | | OWN023 | scratch fallback forbidden but the size may exceed the inline limit | | OWN024 | sensitive buffer is not cleared on release | +| OWN025 | full-length view of a pooled buffer reaches past its logical length | ## Unsupported diff --git a/tests/run_tests.py b/tests/run_tests.py index cbcde052..ad6af414 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -406,6 +406,30 @@ def codes(src: str) -> list[str]: ("buf_moved_then_used", "fn f(n: int){ let a = Buffer.pooled(n); let b = move a; use a; " "release b; }", ["OWN005"]), + + # ---- POOL005: full-length pooled view reaches past the logical length ---- + # `overspan b` is a FULL-length Span/Memory view of a pooled buffer (no length + # bound) — it over-reads the oversized [n, Length) tail. A property of the + # view-creation site (raises regardless of the buffer's flow state), so it sits + # beside the ordinary leak/use/release checks rather than replacing them. + ("pool_overspan_full_view", + "fn f(n: int){ let b = Buffer.pooled(n); overspan b; release b; }", + ["OWN025"]), + ("pool_overspan_resource_form", + "fn f(n: int){ let b = acquire Buffer(n); overspan b; release b; }", + ["OWN025"]), + ("pool_overspan_then_leak", + "fn f(n: int){ let b = Buffer.pooled(n); overspan b; }", + ["OWN001", "OWN025"]), + ("pool_overspan_in_branch", + "fn f(n: int){ let b = Buffer.pooled(n); if (c) { overspan b; } " + "release b; }", ["OWN025"]), + ("pool_overspan_not_owned", + "fn f(b: &Buffer){ overspan b; }", ["OWN034"]), + ("pool_overspan_undefined", + "fn f(){ overspan ghost; }", ["OWN030"]), + ("pool_bounded_view_use_ok", + "fn f(n: int){ let b = Buffer.pooled(n); use b; release b; }", []), ] diff --git a/tests/test_gallery.py b/tests/test_gallery.py index a12af19a..e984267c 100644 --- a/tests/test_gallery.py +++ b/tests/test_gallery.py @@ -41,6 +41,7 @@ ("08_stack_buffer_escapes.own", "OWN015", "returned a Span over a stackalloc (dangling)"), ("09_untracked_call.own", "OWN040", "ownership laundered through an opaque call"), ("10_leak_in_loop.own", "OWN001", "acquired in a loop, never released (while)"), + ("11_overspan_full_view.own", "OWN025", "full view buf.AsSpan() past the rented length"), ] diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 968d2167..6b043086 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -1042,6 +1042,20 @@ def _sub(source: str | None) -> list[Finding]: if amb: fails.append(f"an ambiguous pass-through param must not be inferred, crash, " f"or false-positive, got {[(x.component, x.code) for x in amb]}") + # POOL005: a full-length view of a pooled buffer (`overspan` flow fact) raises + # OWN025 at the VIEW site (line 12, not the Rent site), tagged a pooled buffer; + # the buffer is still returned, so there is no OWN001 leak. Routes through the + # same core op the `.own` `overspan` statement lowers to. + checks += 1 + osp = check_facts({"module": "M", "functions": [ + {"name": "Framer.Frame", "file": "Framer.cs", + "body": [{"op": "acquire", "var": "buf", "line": 10}, + {"op": "overspan", "var": "buf", "line": 12}, + {"op": "release", "var": "buf", "line": 14}]}]}) + if [(x.code, x.line, x.kind) for x in osp] != [("OWN025", 12, "pooled buffer")]: + fails.append(f"an `overspan` fact should raise OWN025 at the view line (12) " + f"tagged a pooled buffer, got " + f"{[(x.code, x.line, x.kind) for x in osp]}") # --- output surfaces (Уровень 1): the same finding renders for a human, a # GitHub annotation, and an MSBuild/VS Error List line. The format lives diff --git a/tests/test_spec.py b/tests/test_spec.py index ef4bff5d..17eab307 100644 --- a/tests/test_spec.py +++ b/tests/test_spec.py @@ -103,6 +103,9 @@ def _codes(src: str) -> list[str]: "module M\nfn f(flag: bool) { let b = Buffer.stack(flag); }"), ("Buffer-B8", "OWN030", "module M\npolicy P { bogus = 1; }"), + ("Buffer-B9", "OWN025", + f"module M\n{_BUF}\n" + "fn f() { let b = acquire Buf(); overspan b; release b; }"), # structural ("Struct-OWN031", "OWN031", f"module M\n{_BUF}\n"