feat(extractor): close remaining flow-lowering gaps — finally-before-return, do, switch

.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,12 @@ 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.
+          # `ncf`: `ncf?.Dispose()` (null-conditional) in a threaded finally IS a release
+          # (member-binding form), so it is disposed on the return path -> silent (Codex review).
+          for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf; 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)"

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.

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