feat(extractor): exception-edge recall slice — nested try, ctor throw-points, typed catches

.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)"

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).

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