From 95af05cfc5ab3257ebc391c786a44a351272d978 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 11:49:39 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(extractor):=20close=20remaining=20flow?= =?UTF-8?q?-lowering=20gaps=20=E2=80=94=20finally-before-return,=20do,=20s?= =?UTF-8?q?witch?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the last deferred control-flow recall gaps in the --flow-locals lowering, so the flow detector now models every common construct (only goto/labeled statements and a few exotic forms still honestly bail). - finally-before-return: an `onReturn` continuation is threaded alongside `onThrow` (the finally-stack + return), so a `return` inside a try-with-finally runs the finally FIRST — a finally-disposed resource is released on the return path. Unlike `onThrow`, `onReturn` is never suppressed by catches (a return is never caught). The old "bail the whole method if a try-with-finally has a return" is removed; such methods are analysed, and an early return that skips a later dispose is now caught. - do-while: desugared `do { B } while(c)` -> `B; while(c){ B }` (the body runs 1+ times). Modelling it as a bare 0+-trip `while` would be unsound — a resource released only in the body but acquired outside would falsely leak on the phantom 0-trip path. - switch: lowered to a chain of opaque, mutually-exclusive `if(*)` branches, one per section, trailing `break` stripped (anything else — nested break, goto case, throw — bails). With NO default the LAST case becomes the tail rather than an empty no-match branch: that avoids a FALSE POSITIVE on an exhaustive switch (e.g. over an enum) where every case disposes; the cost is a sound recall gap (a non-exhaustive no-match leak is only missed when every case disposes). All no-false-positive-preserving. Validated on the core IR via a new flow_finally_switch fixture (silent: finally-before-return clean, switch-all-dispose; leak: early-return, switch-else) — tests 53/53 — and end-to-end in CI on new samples (earlyRet/doLeak/swLeak leak; other/doClean/swAll/tfRet silent). Existing samples keep their verdicts. 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 | 6 +- docs/notes/real-world-mining.md | 10 +- frontend/roslyn/OwnSharp.Extractor/Program.cs | 139 ++++++++++++++---- frontend/roslyn/samples/FlowLocalsSample.cs | 73 ++++++++- .../ownir/flow_finally_switch.facts.json | 55 +++++++ tests/test_ownir.py | 19 +++ 7 files changed, 282 insertions(+), 35 deletions(-) create mode 100644 tests/fixtures/ownir/flow_finally_switch.facts.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 285e1d57..98e0adc7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -287,6 +287,16 @@ jobs: # ('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; } + # remaining flow-lowering gaps closed: finally-before-return threading (an early + # return that skips a later dispose leaks -> 'earlyRet'), `do` desugar (a body-local + # never disposed leaks per iteration -> 'doLeak'), and `switch` lowering (a default + # branch that does not dispose leaks -> 'swLeak'). + echo "$out" | grep -qE "OWN001.*'earlyRet'" \ + || { echo "FAIL: expected OWN001 on the early-return-skips-dispose leak"; exit 1; } + echo "$out" | grep -qE "OWN001.*'doLeak'" \ + || { echo "FAIL: expected OWN001 on the undisposed local in a do-while loop"; exit 1; } + echo "$out" | grep -qE "OWN001.*'swLeak'" \ + || { echo "FAIL: expected OWN001 on the switch default-branch 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`, @@ -303,7 +313,10 @@ jobs: # `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 + # `other`: disposed by the finally, so threaded before the early return -> silent. + # `doClean`: acquire+dispose balanced each `do` iteration. `swAll`: every `switch` + # case disposes (no default) -> last case is the tail, no phantom no-match leak. + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll; 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 a0992929..1f8a2b65 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -96,8 +96,10 @@ architectural strictness, and the borrow-checker showcase): 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). + CodeQL's dedicated query on the fixture. `finally`-before-`return`, `do` and `switch` are + lowered too, so the flow detector covers every common control-flow construct (only + `goto`/labeled statements and a few exotic forms still bail). See + [docs/notes/real-world-mining.md](notes/real-world-mining.md). 2. **Resource core** — generalise WPF subscriptions + `IDisposable` into one acquire/release/owner/release-region model (P-004 ∪ P-005), so WPF is a *profile*, not a one-off. diff --git a/docs/notes/real-world-mining.md b/docs/notes/real-world-mining.md index f2d2b4bc..8765387b 100644 --- a/docs/notes/real-world-mining.md +++ b/docs/notes/real-world-mining.md @@ -135,8 +135,14 @@ Their leak findings are **nearly disjoint** (file overlap: **1**): 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`. + fixture). The remaining control-flow gaps are now closed too: `finally`-before-`return` + (the finally is threaded BEFORE the return instead of bailing the method), `do` (desugared + to `B; while(c){B}` — the body runs 1+ times, so a plain 0+-trip `while` would falsely leak + a body-released resource), and `switch` (opaque mutually-exclusive branches; with no + `default` the last case is the tail rather than an empty no-match path, so an *exhaustive* + switch is never falsely flagged — a non-exhaustive no-match leak is only missed when every + case disposes, a sound recall gap). The flow detector now models every common control-flow + construct; only `goto`/labeled statements and a few exotic forms still honestly bail. - **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 fa4bbca7..f05c4a78 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -342,8 +342,9 @@ cc.Filter is null 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 -// (loop/try/switch/...): the method is then honestly skipped, not guessed. +// `tracked` local IDisposables. Returns null on any UNMODELLED statement (a `goto`, labeled +// statement, local function, `lock`/`fixed`, …): the method is then honestly skipped, not +// guessed. Loops, `try`, `do` and `switch` ARE modelled below. static List? LowerFlowBody(BlockSyntax block, HashSet tracked) { var nodes = new List(); @@ -356,16 +357,19 @@ cc.Filter is null // `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. +// (method level, or a region an enclosing catch-all swallows). `onReturn`: the continuation +// a `return` here runs FIRST — the enclosing `finally`(s), then the exit — so a resource a +// finally disposes is released on the return path; null = a bare return (outside any try). +// Defaults are the method-body context: throws escape, nothing is injected, returns are bare. static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List nodes, - bool canEscape = true, List? onThrow = null) + bool canEscape = true, List? onThrow = null, + List? onReturn = null) { switch (st) { case BlockSyntax b: foreach (var s2 in b.Statements) - if (!LowerFlowStmt(s2, tracked, nodes, canEscape, onThrow)) + if (!LowerFlowStmt(s2, tracked, nodes, canEscape, onThrow, onReturn)) return false; return true; case LocalDeclarationStatementSyntax ld: @@ -384,10 +388,10 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List(); - if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes, canEscape, onThrow)) + if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes, canEscape, onThrow, onReturn)) return false; var elseNodes = new List(); - if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes, canEscape, onThrow)) + if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes, canEscape, onThrow, onReturn)) return false; nodes.Add(new { op = "if", line = LineOf(ifs), then = thenNodes, @else = elseNodes }); return true; @@ -395,11 +399,16 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List tracked, List(); - if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes, canEscape, onThrow)) + if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes, canEscape, onThrow, onReturn)) return false; nodes.Add(new { op = "while", line = LineOf(ws), body = bodyNodes }); return true; @@ -419,10 +428,10 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List