From fc2192d5e14a3cb10cc60ad7d2390239a59dd5e7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 10:36:39 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(extractor):=20exception-edge=20recall?= =?UTF-8?q?=20slice=20=E2=80=94=20nested=20try,=20ctor=20throw-points,=20t?= =?UTF-8?q?yped=20catches?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lands the deferred exception-edge recall slice from PR #32. Three sound recall gaps (missed leaks, never false positives) in the try exception-edge model close: - Nested compound statements: edges now recurse into if/loop/block bodies and are injected before the nested LEAF statement — where the resource's ownership is exact (after any in-branch dispose). This catches a throw-before-dispose inside a branch while keeping the dispose-before-throw shape silent (DisposeInsideIfWithThrow 'cif' stays silent for this better reason now, not by skipping compounds). The throw continuation is threaded (onThrow) and composes across nested tries (inner finally, then outer, then return); a canEscape flag propagates an enclosing catch-all's swallow so no edge is injected in a region whose throws never reach method exit. - Constructor (new) as a throw point: a throwing ctor skips a PRIOR owned resource's dispose; StatementMayThrow now treats object creation as may-throw. The edge lands before the resource's own acquire (harmless — not yet owned there). - Typed/filtered catches: a non-tail catch no longer blanket-suppresses edges. Only a genuine catch-all (catch {} / catch (Exception), no when-filter) does; a typed catch lets the uncaught exception types propagate past the post-try dispose and really leak. All three match CodeQL's cs/dispose-not-called-on-throw. Validated end-to-end in CI on new samples (nestedLeak, ctorPrior, typedLeak leak; ctorLater stays silent) and on the core IR via the flow_nested_throw ownir fixture (52/52 bridge checks). Every existing try-sample keeps its verdict. Remaining deferred: finally-before-return and switch/do. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 15 +- docs/ROADMAP.md | 3 +- docs/notes/real-world-mining.md | 23 +-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 139 +++++++++++------- frontend/roslyn/samples/FlowLocalsSample.cs | 60 +++++++- .../ownir/flow_nested_throw.facts.json | 51 +++++++ tests/test_ownir.py | 19 +++ 7 files changed, 239 insertions(+), 71 deletions(-) create mode 100644 tests/fixtures/ownir/flow_nested_throw.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6f0a90c5..cfbc5257 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -271,6 +271,17 @@ jobs: # after a may-throw call, so it leaks on the exceptional path (matches CodeQL). echo "$out" | grep -qE "OWN001.*'dot'" \ || { echo "FAIL: expected OWN001 on the dispose-not-called-on-throw local"; exit 1; } + # exception-edge RECALL slice — three sound recall wins, each matching CodeQL's + # cs/dispose-not-called-on-throw: a may-throw in a nested `if` branch BEFORE the + # dispose ('nestedLeak'); a constructor (`new`) as a throw point that skips a PRIOR + # owned resource's dispose ('ctorPrior'); and a TYPED catch whose uncaught exception + # types propagate past a post-try dispose ('typedLeak'). + echo "$out" | grep -qE "OWN001.*'nestedLeak'" \ + || { echo "FAIL: expected OWN001 on the nested-throw leak"; exit 1; } + echo "$out" | grep -qE "OWN001.*'ctorPrior'" \ + || { echo "FAIL: expected OWN001 on the constructor-throw prior-resource leak"; exit 1; } + echo "$out" | grep -qE "OWN001.*'typedLeak'" \ + || { echo "FAIL: expected OWN001 on the typed-catch uncaught-path leak"; exit 1; } # dispose-optional (Task), disposed/escaping locals, a `for` loop whose # disposable is disposed after it (`looped`, balanced), a balanced # acquire+dispose in a loop (`whileClean`), a try/finally dispose (`tfClean`, @@ -282,7 +293,9 @@ jobs: # an `await DisposeAsync().ConfigureAwait(false)` INSIDE a try (daci), and a Dispose # inside both branches of an `if` in a try alongside a may-throw call (cif) — all # disposed on every path, so all must stay silent (were false OWN001 before). - for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif; do + # `ctorLater` is acquired AFTER the constructor-throw edge in CtorThrowLeaksPrior, so + # it is never live at that edge and must stay silent (only `ctorPrior` leaks there). + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater; do if echo "$out" | grep -q "'$ok'"; then echo "FAIL: silent/exempt case '$ok' was reported"; exit 1; fi done echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, beyond flat)" diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index e891db88..a0992929 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -93,7 +93,8 @@ architectural strictness, and the borrow-checker showcase): The oracle also drove down the *other*-class recall gap (Dispose leaks Own.NET missed because the flow detector skipped methods with unmodelled constructs): `for` and `try` are now lowered — sequentially, then with an **exception-edge** model that injects a - throw exit before each may-throw statement in a `try`. That closes the + throw exit before each may-throw leaf in a `try` (including inside nested branches, with a + constructor `new` as a throw point and typed/filtered catches handled). That closes the `dispose-not-called-on-throw` shape, which now lands in cross-tool **Agree** with CodeQL's dedicated query on the fixture. Deferred: `finally`-before-`return`, `switch`/`do`. See [docs/notes/real-world-mining.md](notes/real-world-mining.md). diff --git a/docs/notes/real-world-mining.md b/docs/notes/real-world-mining.md index cc2dbc7e..f2d2b4bc 100644 --- a/docs/notes/real-world-mining.md +++ b/docs/notes/real-world-mining.md @@ -124,16 +124,19 @@ Their leak findings are **nearly disjoint** (file overlap: **1**): `finally`: the throw skips the `Dispose`). Both confirmed on the cross-tool fixture: the plain `try`-method leak and the dispose-on-throw leak both land in **Agree** across all three tools (the latter matching CodeQL's `cs/dispose-not-called-on-throw`). The - edges are injected only where sound — when the caught path's continuation is end-of- - method (no catch, or the `try` is the body's tail); a swallowing catch with a Dispose - *after* the try/catch (continuation disposes the resource) lowers sequentially instead, - to avoid a false leak (PR #32 review). Still deferred — all **sound recall gaps** (missed - leaks, never false ones), to be tackled as a dedicated exception-edge recall slice with - its own oracle re-validation: exception edges inside nested `try` bodies (only top-level - `try` statements get an edge today); object creation (`new`) as a throw point (it can leak - a prior owned resource whose dispose it skips); typed/filtered catches (a non-tail catch - suppresses edges even when it only continues for *some* exception types — the uncaught-type - paths really do leak); `finally`-before-`return` threading (bailed today); and `switch`/`do`. + edges are injected only where sound, and the recall slice has now landed: they reach into + **nested compound statements** (the edge lands before the nested LEAF, where ownership is + exact — after any in-branch dispose — so a nested dispose-before-throw stays silent while a + throw-before-dispose in a branch is caught); a **constructor (`new`) counts as a throw + point** (a throwing ctor skips a prior owned resource's dispose); and a **typed/filtered + catch no longer suppresses the edges** — only a genuine catch-all (`catch {}` / `catch + (Exception)`, no `when`) on a non-tail `try` does, since the uncaught exception types of a + typed catch propagate past the post-try dispose and really do leak. A swallowing catch-all + with a Dispose *after* the try/catch (the caught path disposes the resource) still lowers + sequentially, to avoid a false leak (PR #32 review). The three recall wins are pinned in CI + (`nestedLeak`, `ctorPrior`, `typedLeak`) and on the core's IR (the `flow_nested_throw` + fixture). Still deferred — both **sound recall gaps** (missed leaks, never false ones): + `finally`-before-`return` threading (bailed today) and `switch`/`do`. - **Agree — 1** (`HttpHelper.cs`). So the SystemEvents and VideoSource findings are **differentiated — confirmed by the diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index f1616fb4..637a0400 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -294,23 +294,46 @@ st.Parent is BlockSyntax b && b.Statements.Count > 0 && b.Statements[^1] == st && b.Parent is not StatementSyntax; -// An exceptional exit before a try-body statement is sound only for a LEAF statement whose -// may-throw call sits at the statement's own level — an expression statement (`x.Foo();`) -// or a local declaration (`var x = Foo();`). A COMPOUND statement (if/loop/block/…) may -// dispose a resource in a nested branch before throwing deeper inside; an edge placed before -// the WHOLE statement (where that resource is still owned) would falsely flag it as leaked -// though every real path disposes it. So edges are skipped for compound statements — the -// nested may-throw is the deferred nested-try slice, a sound recall gap rather than an FP. -static bool EdgeEligible(StatementSyntax st) => - st is ExpressionStatementSyntax or LocalDeclarationStatementSyntax; +// Inject an exceptional-exit edge `if(*){ onThrow }` before a LEAF may-throw statement +// (an expression statement or a local declaration) inside a `try` body. `onThrow` is the +// continuation a throw here runs to leave the method — this try's `finally`, then any +// enclosing tries' finallys, then `return` (built in the try lowering). A resource owned +// at this point and not released by that continuation leaks on the throw path. Called for +// LEAF statements only; a COMPOUND statement (if/loop/block) is recursed into so the edge +// lands before the nested leaf — at the point the resource's ownership is exact (after any +// in-branch dispose), which is what makes nesting sound rather than a false leak. +static void InjectThrowEdge(StatementSyntax st, List nodes, List? onThrow) +{ + if (onThrow is not null && StatementMayThrow(st)) + nodes.Add(new { op = "if", line = LineOf(st), + then = new List(onThrow), @else = new List() }); +} // A statement that can raise an exception part-way through: it makes a call that is not -// itself a dispose. (A `new` can throw too — and would leak a PRIOR owned resource whose -// dispose it skips — but modelling object creation as a throw point is a deferred recall -// slice; today only non-dispose CALLS create an exceptional exit. Both omissions are sound: -// a missed leak, never a false one.) +// itself a dispose, OR it creates an object (`new` — a constructor can throw, leaking a +// PRIOR owned resource whose dispose it would then skip). Creating the resource being +// acquired here is harmless: the edge lands before its `acquire`, where it is not yet owned. static bool StatementMayThrow(StatementSyntax st) => - st.DescendantNodes().OfType().Any(i => !IsDisposeShaped(i)); + st.DescendantNodes().Any(n => + (n is InvocationExpressionSyntax i && !IsDisposeShaped(i)) + || n is ObjectCreationExpressionSyntax or ImplicitObjectCreationExpressionSyntax); + +// A catch clause that catches EVERY exception and so always continues to the post-try +// code: `catch { }` (no declaration) or `catch (Exception)` / `catch (System.Exception)` — +// with NO `when` filter (a filter may evaluate false, letting the exception propagate). A +// typed catch (`catch (IOException)`) or any filtered catch continues for only SOME +// exceptions; the rest propagate out, skipping the post-try dispose, so the resource still +// leaks on those paths. Syntax-only (no semantic model): an alias of System.Exception reads +// as typed — a negligible, documented residual recall gap, never a false positive. +static bool IsCatchAll(CatchClauseSyntax cc) => + cc.Filter is null + && (cc.Declaration is not { } decl + || (decl.Type switch + { + IdentifierNameSyntax id => id.Identifier.Text, + QualifiedNameSyntax q => q.Right.Identifier.Text, + _ => (string?)null, + }) is "Exception"); // Lower a method block to OwnIR flow nodes (acquire/use/release/if/return) for the // `tracked` local IDisposables. Returns null on any UNMODELLED statement @@ -324,16 +347,23 @@ static bool StatementMayThrow(StatementSyntax st) => return nodes; } -static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List nodes) +// `canEscape`: can a throw at the current position leave the METHOD (no enclosing +// catch-all swallows it)? `onThrow`: the continuation a throw here runs to leave the +// method (finally-stack + return), or null when no exception edge should be injected +// (method level, or a region an enclosing catch-all swallows). Both default to the +// method-body context: a throw escapes, but no edge is injected until a `try` sets one. +static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List nodes, + bool canEscape = true, List? onThrow = null) { switch (st) { case BlockSyntax b: foreach (var s2 in b.Statements) - if (!LowerFlowStmt(s2, tracked, nodes)) + if (!LowerFlowStmt(s2, tracked, nodes, canEscape, onThrow)) return false; return true; case LocalDeclarationStatementSyntax ld: + InjectThrowEdge(ld, nodes, onThrow); if (ld.UsingKeyword == default) foreach (var v in ld.Declaration.Variables) if (tracked.Contains(v.Identifier.Text) @@ -342,15 +372,16 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List(); - if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes)) + if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes, canEscape, onThrow)) return false; var elseNodes = new List(); - if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes)) + if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes, canEscape, onThrow)) return false; nodes.Add(new { op = "if", line = LineOf(ifs), then = thenNodes, @else = elseNodes }); return true; @@ -358,7 +389,7 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List tracked, List(); - if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes)) + if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes, canEscape, onThrow)) return false; nodes.Add(new { op = "while", line = LineOf(ws), body = bodyNodes }); return true; @@ -385,7 +416,7 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List(); - if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, bodyNodes)) + if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, bodyNodes, canEscape, onThrow)) return false; nodes.Add(new { op = "while", line = LineOf(fes), body = bodyNodes }); return true; @@ -399,21 +430,21 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List(); - if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, bodyNodes)) + if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, bodyNodes, canEscape, onThrow)) return false; nodes.Add(new { op = "while", line = LineOf(fors), body = bodyNodes }); return true; } case TryStatementSyntax trys: { - // try { A } [catch { C }...] [finally { B }] with EXCEPTION EDGES. Any - // statement in A that makes a (non-dispose) call can throw; before each such - // statement we insert an exceptional exit `if(*){ B; return }` — throw here, - // run the finally, leave. A resource owned at that point and NOT released by - // the finally leaks on the exceptional path: dispose-not-called-on-throw (a - // dispose placed in the try, not the finally). A dispose IN the finally runs - // on every exceptional exit, so the safe pattern stays silent; `acquire; - // dispose;` with no call between has no exit, so no false leak. + // try { A } [catch { C }...] [finally { B }] with EXCEPTION EDGES. Any LEAF + // statement in A (at any nesting depth) that can throw gets an exceptional exit + // `if(*){ B; … ; return }` injected before it — throw here, run the finally(s), + // leave. A resource owned at that point and NOT released by the finally leaks on + // the exceptional path: dispose-not-called-on-throw (a dispose placed in the try, + // not the finally). A dispose IN the finally runs on every exceptional exit, so + // the safe pattern stays silent; `acquire; dispose;` with no throw between has no + // live edge, so no false leak. // // Catch bodies are not lowered; to stay SOUND, bail if any catch disposes, so // a release that only happens in a catch is never missed. Matches `x.Dispose()` @@ -431,30 +462,34 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List(); if (trys.Finally is { } fin && !LowerFlowStmt(fin.Block, tracked, finallyNodes)) return false; - // The exceptional exit `if(*){ B; return }` models the exception LEAVING the - // method — sound only when the caught path's continuation IS end-of-method: - // no catch (it propagates out past any post-try code), or the try is the body's - // tail (nothing runs after the catch). With a catch AND post-try code, a - // resource the post-try code disposes runs on the caught path too, so a return - // there would falsely flag it (dispose-after-try). In that case skip the edges - // and lower the try sequentially — a never-disposed local is still caught at - // end-of-function; only dispose-on-throw is forgone for this shape. - // Conservative: ANY non-tail catch suppresses the edges, even a typed/filtered - // catch that only continues for some exception types — the uncaught-type paths - // really do leak, but distinguishing catch-all from typed/filtered is a deferred - // recall slice. Suppressing is sound: a missed leak, never a false one. - var edgesSound = trys.Catches.Count == 0 || IsBodyTail(trys); - foreach (var stmt in trys.Block.Statements) + // Does a throw in THIS body escape to method exit (so the edge — leave running + // only the finally — models a real execution)? Sound when there is no catch (it + // propagates out past any post-try code), the try is the body's tail (nothing + // runs after), OR no catch is a genuine catch-all — a typed/filtered catch lets + // the uncaught exception types propagate, skipping the post-try dispose, so the + // resource still leaks on those paths. The one shape that SUPPRESSES the edges is + // a catch-all on a non-tail try: every throw is caught and continues to (and may + // dispose in) the post-try code, so a return there would falsely flag a resource + // that path disposes. `canEscape` carries the same fact down through ENCLOSING + // tries: a catch-all higher up already swallows these throws, so they never reach + // method exit -> no edges in the region nested under it. + bool escapesThisTry = trys.Catches.Count == 0 + || IsBodyTail(trys) + || !trys.Catches.Any(IsCatchAll); + bool bodyCanEscape = canEscape && escapesThisTry; + // The continuation an escaping throw runs: this finally, then the enclosing + // exceptional path (its finallys, ending in the method `return`), or just a + // `return` when this is the outermost try. Null when suppressed -> no edges. + List? bodyOnThrow = null; + if (bodyCanEscape) { - if (edgesSound && EdgeEligible(stmt) && StatementMayThrow(stmt)) - { - var ex = new List(finallyNodes) - { new { op = "return", var = (string?)null, line = LineOf(stmt) } }; - nodes.Add(new { op = "if", line = LineOf(stmt), then = ex, @else = new List() }); - } - if (!LowerFlowStmt(stmt, tracked, nodes)) - return false; + bodyOnThrow = new List(finallyNodes); + bodyOnThrow.AddRange(onThrow ?? new List + { new { op = "return", var = (string?)null, line = LineOf(trys) } }); } + foreach (var stmt in trys.Block.Statements) + if (!LowerFlowStmt(stmt, tracked, nodes, bodyCanEscape, bodyOnThrow)) + return false; nodes.AddRange(finallyNodes); // normal completion runs the finally return true; } diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index 5162031d..19166d7c 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -173,13 +173,13 @@ public async Task DisposeAsyncConfiguredInTry() catch (Exception) { /* swallowed */ } } - // NOT a leak: `cif` is disposed on every real path (both branches of the `if`). A - // may-throw call sits in one branch after the dispose, but the exception edge must NOT - // be injected before the whole `if` (where `cif` is still owned) — edges go only before - // LEAF statements (expression / local-declaration), never compound ones, else the - // resource is falsely flagged though every path disposes it. Must stay silent (was a - // false OWN001 — PR #32 Codex review). The nested may-throw is the deferred nested-try - // slice (a sound recall gap, not a leak). + // NOT a leak: `cif` is disposed on every real path (both branches of the `if`), with the + // may-throw call AFTER the dispose in its branch. Exception edges now recurse into nested + // compound statements (the nested-try recall slice), but land before the LEAF — so the + // edge sits after `cif.Dispose()`, where `cif` is already released, and nothing is flagged. + // That leaf-level placement is exactly what makes nesting sound: a coarse edge before the + // whole `if` (where `cif` is still owned) would have falsely flagged it. Must stay silent + // (was a false OWN001 before the leaf-level placement — PR #32 Codex review). public void DisposeInsideIfWithThrow(bool c) { var cif = new MemoryStream(); @@ -191,6 +191,52 @@ public void DisposeInsideIfWithThrow(bool c) catch (Exception) { /* swallowed */ } } + // recall (nested-try): the may-throw call sits in a nested `if` branch BEFORE the dispose, + // so `nestedLeak` is still owned when it throws -> it leaks on that path. The exception + // edge is injected before the nested LEAF (`MayThrow()`), where ownership is exact — caught + // now that edges recurse into compound statements (cf. DisposeInsideIfWithThrow, which + // stays silent because there the dispose precedes the throw in every branch). OWN001. + public void NestedThrowLeaks(bool c) + { + var nestedLeak = new MemoryStream(); + try + { + if (c) { MayThrow(); nestedLeak.Dispose(); } + else { nestedLeak.Dispose(); } + } + catch (Exception) { /* swallowed */ } + } + + // recall (constructor-throw): a `new` can throw, and if it does a PRIOR owned resource is + // leaked. `ctorPrior` is owned when `new MemoryStream()` (for `ctorLater`) runs inside the + // try; if that constructor throws, `ctorPrior.Dispose()` is skipped -> `ctorPrior` leaks on + // the exceptional path (OWN001). `ctorLater` is acquired only AFTER that throw point (the + // edge sits before its acquire), so it never leaks and must stay silent. + public void CtorThrowLeaksPrior() + { + var ctorPrior = new MemoryStream(); + try + { + var ctorLater = new MemoryStream(); + ctorPrior.Dispose(); + ctorLater.Dispose(); + } + catch (Exception) { /* swallowed */ } + } + + // recall (typed/filtered catch): a non-tail `try` whose catch is TYPED handles only some + // exceptions; an uncaught type propagates past the post-try `typedLeak.Dispose()`, so the + // resource leaks on that path. Edges used to be suppressed for ANY non-tail catch; they are + // now injected unless a catch is a genuine catch-all -> OWN001 (matches CodeQL's + // cs/dispose-not-called-on-throw on the uncaught-exception path). + public void TypedCatchLeaks() + { + var typedLeak = new MemoryStream(); + try { typedLeak.WriteByte(1); } + catch (IOException) { /* only IO handled; other exceptions propagate */ } + typedLeak.Dispose(); + } + private static void MayThrow() { } // acquire + dispose within the loop body is balanced -> silent (no false diff --git a/tests/fixtures/ownir/flow_nested_throw.facts.json b/tests/fixtures/ownir/flow_nested_throw.facts.json new file mode 100644 index 00000000..644a2b07 --- /dev/null +++ b/tests/fixtures/ownir/flow_nested_throw.facts.json @@ -0,0 +1,51 @@ +{ + "ownir_version": 0, + "module": "Extracted", + "comment": "Exception-edge RECALL slice: the IR the extractor now emits for three try shapes. (1) NestedThrowLeaks: the throw edge recurses into the `if` and lands before MayThrow() (a nested LEAF), where nestedLeak is still owned -> leaks. (2) DisposeInsideIfWithThrow: the same recursion, but the dispose precedes the throw in each branch, so cif is already released at the edge -> silent. (3) CtorThrowLeaksPrior: a `new` is a throw point; the edge before `var ctorLater = new ...` finds ctorPrior owned -> leaks, while ctorLater (acquired after the edge) is silent.", + "components": [], + "functions": [ + { + "name": "FlowLocalsSample.NestedThrowLeaks", + "file": "FlowLocalsSample.cs", + "body": [ + {"op": "acquire", "var": "nestedLeak", "line": 201}, + {"op": "if", "line": 204, "then": [ + {"op": "if", "line": 204, "then": [ + {"op": "return", "var": null, "line": 202} + ], "else": []}, + {"op": "release", "var": "nestedLeak", "line": 204} + ], "else": [ + {"op": "release", "var": "nestedLeak", "line": 205} + ]} + ] + }, + { + "name": "FlowLocalsSample.DisposeInsideIfWithThrow", + "file": "FlowLocalsSample.cs", + "body": [ + {"op": "acquire", "var": "cif", "line": 185}, + {"op": "if", "line": 188, "then": [ + {"op": "release", "var": "cif", "line": 188}, + {"op": "if", "line": 188, "then": [ + {"op": "return", "var": null, "line": 186} + ], "else": []} + ], "else": [ + {"op": "release", "var": "cif", "line": 189} + ]} + ] + }, + { + "name": "FlowLocalsSample.CtorThrowLeaksPrior", + "file": "FlowLocalsSample.cs", + "body": [ + {"op": "acquire", "var": "ctorPrior", "line": 217}, + {"op": "if", "line": 220, "then": [ + {"op": "return", "var": null, "line": 218} + ], "else": []}, + {"op": "acquire", "var": "ctorLater", "line": 220}, + {"op": "release", "var": "ctorPrior", "line": 221}, + {"op": "release", "var": "ctorLater", "line": 222} + ] + } + ] +} diff --git a/tests/test_ownir.py b/tests/test_ownir.py index 060cce00..aca92cbf 100644 --- a/tests/test_ownir.py +++ b/tests/test_ownir.py @@ -56,6 +56,8 @@ "ownir", "flow_while.facts.json") _TWO_EXITS_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "flow_leak_two_exits.facts.json") +_NESTED_THROW_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", + "ownir", "flow_nested_throw.facts.json") _DI_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", "di.facts.json") _UNRESOLVED_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", @@ -356,6 +358,23 @@ def _one(source: str, lambda_: bool = False) -> Finding: fails.append(f"expected exactly one OWN001 on 'tfLeak'@105 (two leaking exits " f"deduped), got {[(x.event, x.code, x.line) for x in tefindings]}") + # --- exception-edge RECALL slice: the edge now recurses into nested compound statements, + # treats a constructor (`new`) as a throw point, and fires under a TYPED catch. The + # core must flag the nested throw-before-dispose ('nestedLeak') and the prior resource + # a throwing constructor skips ('ctorPrior'), while the dispose-before-throw nested + # case ('cif', disposed in every branch before the throw) and the not-yet-acquired + # later resource ('ctorLater', acquired after the edge) stay silent. Pins the verdict + # on the exact IR the new lowering emits (the C# lowering itself is covered in CI). + with open(_NESTED_THROW_FIXTURE, encoding="utf-8") as f: + ntfacts = json.load(f) + ntfindings = check_facts(ntfacts) + checks += 1 + got = sorted((x.event, x.code, x.line) for x in ntfindings) + if got != [("ctorPrior", "OWN001", 217), ("nestedLeak", "OWN001", 201)]: + fails.append(f"expected OWN001 on 'nestedLeak'@201 and 'ctorPrior'@217 only " + f"(nested clean 'cif' and later-acquired 'ctorLater' stay silent), " + f"got {got}") + # --- P-016 A1 reaches the frontend: a `while` flow body (the extractor now # lowers loops instead of skipping the method) routes through the core's # worklist fixpoint. A resource acquired before the loop and released INSIDE From 83a9d3e35e604697540c4e4ee46004573f926217 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 10:53:52 +0000 Subject: [PATCH 2/2] fix(extractor): two review-driven soundness fixes for the exception-edge slice MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - StatementMayThrow: don't descend into lambda / anonymous-method bodies when scanning for throw points. A `new` (or call) inside `() => …` runs when the delegate is invoked, not where it is declared, so the declaring statement is not a throw point; counting it injected a phantom edge that could falsely flag a prior resource disposed after the try (Codex review). An immediately-invoked lambda is still caught via its outer invocation, and this also closes the same latent issue the pre-existing invocation scan had. Pinned by CtorInLambdaNotThrow (lamPrior silent). - IsCatchAll: match the canonical System.Exception spellings by full text instead of the rightmost identifier. `catch (Foo.Exception)` — a domain type whose rightmost name is `Exception` but which is not System.Exception — was misclassified as a catch-all, suppressing edges and missing a real leak (CodeRabbit review). Now only Exception / System.Exception / global::System.Exception are catch-alls; a qualified domain catch is typed and injects edges. Pinned by QualifiedTypedCatchLeaks (qualLeak). Both are no-false-positive-preserving. Tests 52/52; C# end-to-end validated in CI. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 10 ++++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 28 ++++++++------ frontend/roslyn/samples/FlowLocalsSample.cs | 38 +++++++++++++++++++ 3 files changed, 64 insertions(+), 12 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cfbc5257..285e1d57 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -282,6 +282,11 @@ jobs: || { echo "FAIL: expected OWN001 on the constructor-throw prior-resource leak"; exit 1; } echo "$out" | grep -qE "OWN001.*'typedLeak'" \ || { echo "FAIL: expected OWN001 on the typed-catch uncaught-path leak"; exit 1; } + # ...and a qualified DOMAIN catch (`catch (DomainErrors.Exception)` — rightmost name + # `Exception` but NOT System.Exception) is typed too, so its uncaught types leak + # ('qualLeak'); IsCatchAll matches only the canonical spellings (CodeRabbit review). + echo "$out" | grep -qE "OWN001.*'qualLeak'" \ + || { echo "FAIL: expected OWN001 on the qualified-typed-catch leak"; exit 1; } # dispose-optional (Task), disposed/escaping locals, a `for` loop whose # disposable is disposed after it (`looped`, balanced), a balanced # acquire+dispose in a loop (`whileClean`), a try/finally dispose (`tfClean`, @@ -295,7 +300,10 @@ jobs: # disposed on every path, so all must stay silent (were false OWN001 before). # `ctorLater` is acquired AFTER the constructor-throw edge in CtorThrowLeaksPrior, so # it is never live at that edge and must stay silent (only `ctorPrior` leaks there). - for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater; do + # `lamPrior`: a `new` inside a LAMBDA body is deferred (runs on invoke, not at the + # declaration), so the lambda statement is not a throw point -> no phantom edge skips + # its post-try dispose -> silent (Codex review: don't descend into lambda bodies). + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior; do if echo "$out" | grep -q "'$ok'"; then echo "FAIL: silent/exempt case '$ok' was reported"; exit 1; fi done echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, beyond flat)" diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 637a0400..fa4bbca7 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -313,27 +313,33 @@ static void InjectThrowEdge(StatementSyntax st, List nodes, List // itself a dispose, OR it creates an object (`new` — a constructor can throw, leaking a // PRIOR owned resource whose dispose it would then skip). Creating the resource being // acquired here is harmless: the edge lands before its `acquire`, where it is not yet owned. +// Does NOT descend into lambda / anonymous-method bodies: a `new` (or call) inside `() => …` +// runs when the delegate is INVOKED, not where it is declared, so the declaring statement is +// not a throw point — counting it would inject a phantom edge that falsely flags a prior +// resource disposed after the `try`. An immediately-invoked lambda is still caught: the outer +// invocation is itself the throw point. static bool StatementMayThrow(StatementSyntax st) => - st.DescendantNodes().Any(n => + st.DescendantNodes(descendIntoChildren: n => n is not AnonymousFunctionExpressionSyntax) + .Any(n => (n is InvocationExpressionSyntax i && !IsDisposeShaped(i)) || n is ObjectCreationExpressionSyntax or ImplicitObjectCreationExpressionSyntax); // A catch clause that catches EVERY exception and so always continues to the post-try // code: `catch { }` (no declaration) or `catch (Exception)` / `catch (System.Exception)` — // with NO `when` filter (a filter may evaluate false, letting the exception propagate). A -// typed catch (`catch (IOException)`) or any filtered catch continues for only SOME -// exceptions; the rest propagate out, skipping the post-try dispose, so the resource still -// leaks on those paths. Syntax-only (no semantic model): an alias of System.Exception reads -// as typed — a negligible, documented residual recall gap, never a false positive. +// typed catch (`catch (IOException)`, or a qualified DOMAIN type like `catch (Foo.Exception)` +// whose rightmost name is `Exception` but is not System.Exception) or any filtered catch +// continues for only SOME exceptions; the rest propagate out, skipping the post-try dispose, +// so the resource still leaks on those paths. Match the canonical System.Exception spellings +// by full text — a rightmost-name match would misread a domain `Foo.Exception` as catch-all +// and suppress a real leak. Syntax-only (no semantic model): the inverse pathology — an +// exotic alias making a typed-looking name resolve to System.Exception — is never written. static bool IsCatchAll(CatchClauseSyntax cc) => cc.Filter is null && (cc.Declaration is not { } decl - || (decl.Type switch - { - IdentifierNameSyntax id => id.Identifier.Text, - QualifiedNameSyntax q => q.Right.Identifier.Text, - _ => (string?)null, - }) is "Exception"); + || decl.Type.ToString() is "Exception" + or "System.Exception" + or "global::System.Exception"); // Lower a method block to OwnIR flow nodes (acquire/use/release/if/return) for the // `tracked` local IDisposables. Returns null on any UNMODELLED statement diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index 19166d7c..06ccd28f 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -237,6 +237,35 @@ public void TypedCatchLeaks() typedLeak.Dispose(); } + // recall (qualified typed catch): `DomainErrors.Exception` is a DOMAIN exception — its + // rightmost name is `Exception` but it is NOT System.Exception, so it catches only its own + // type and other exceptions propagate past the post-try `qualLeak.Dispose()` and leak. + // IsCatchAll matches the canonical System.Exception spellings by full text (not just the + // rightmost name), so this is treated as typed and the edge is injected -> OWN001 + // (CodeRabbit review on PR #33: a rightmost-name match wrongly suppressed this leak). + public void QualifiedTypedCatchLeaks() + { + var qualLeak = new MemoryStream(); + try { qualLeak.WriteByte(1); } + catch (DomainErrors.Exception) { /* domain type, not System.Exception */ } + qualLeak.Dispose(); + } + + // NOT a leak: the `new` lives in a LAMBDA body, so it runs only when the delegate is + // invoked (never here) — declaring `make` is not a throw point. Without excluding deferred + // bodies, the statement would get a phantom throw edge that skips the post-try + // `lamPrior.Dispose()` and falsely flag it. Must stay silent (Codex review on PR #33). + public void CtorInLambdaNotThrow() + { + var lamPrior = new MemoryStream(); + try + { + Func make = () => new MemoryStream(); + } + finally { } + lamPrior.Dispose(); + } + private static void MayThrow() { } // acquire + dispose within the loop body is balanced -> silent (no false @@ -297,3 +326,12 @@ public async Task DisposedAsyncConfigured() await asyncDisposedCfg.DisposeAsync().ConfigureAwait(false); } } + +// A domain exception type literally named `Exception`, in a non-System namespace — the +// fixture for QualifiedTypedCatchLeaks. `catch (DomainErrors.Exception)` catches only this +// type, so IsCatchAll must classify it as TYPED (not a catch-all) by full-text match, not by +// its rightmost name alone. +namespace DomainErrors +{ + public class Exception : System.Exception { } +}