diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6f0a90c5..285e1d57 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -271,6 +271,22 @@ 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; } + # ...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`, @@ -282,7 +298,12 @@ 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). + # `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/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..fa4bbca7 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -294,23 +294,52 @@ 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. +// 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().OfType().Any(i => !IsDisposeShaped(i)); + 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 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.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 @@ -324,16 +353,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 +378,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 +395,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 +422,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 +436,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 +468,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..06ccd28f 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,81 @@ 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(); + } + + // 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 @@ -251,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 { } +} 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