Model exception edges in try lowering for dispose-not-called-on-throw

.github/workflows/ci.yml

@@ -263,18 +263,26 @@ jobs:
             || { echo "FAIL: expected OWN001 on the undisposed local in a foreach loop"; exit 1; }
           echo "$out" | grep -qE "OWN001.*'forLeak'" \
             || { echo "FAIL: expected OWN001 on the undisposed local in a for loop"; exit 1; }
-          # `try`/`finally` lowered sequentially (try-methods no longer skipped): a
-          # local never disposed inside a try is now caught.
+          # `try`/`finally` lowered with exception edges (try-methods no longer skipped):
+          # a local never disposed inside a try is caught...
           echo "$out" | grep -qE "OWN001.*'tfLeak'" \
             || { echo "FAIL: expected OWN001 on the undisposed local in a try-method"; exit 1; }
+          # ...and so is dispose-not-called-on-throw: `dot` is disposed inside the try
+          # 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; }
           # 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`,
           # balanced) and a catch-disposes method (`tfCatch`, soundly skipped) must
           # stay silent:
           # released via `await x.DisposeAsync()` (asyncDisposed) and the chained
           # `.ConfigureAwait(false)` form (asyncDisposedCfg) -> both must stay silent.
-          for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull; do
+          # PR #32 FP fixes: a swallowing catch with a Dispose AFTER the try/catch (cda),
+          # 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
             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)"

corpus/fixtures/systemevents-console/Program.cs

@@ -31,6 +31,7 @@ public static void Main()
         _ = new DisplayWatcher();
         LeakAFile();
         LeakInTry();
+        DisposeOnThrow();
     }
 
     // (2) DISPOSE leak — CodeQL's / Infer#'s class, and the control: a local
@@ -55,4 +56,26 @@ private static void LeakInTry()
         catch (Exception) { /* logged, not disposed */ }
         // ...no Dispose()/using -> resource leak, now seen despite the `try`
     }
+
+    // (4) DISPOSE-NOT-CALLED-ON-THROW — the exception-edge slice. Unlike (2)/(3), this
+    // stream IS disposed; but the Dispose() sits INSIDE the try, after a may-throw call
+    // (WriteByte). On the normal path it's disposed; if WriteByte throws, control jumps
+    // to the catch and the Dispose is skipped -> the stream leaks on the exceptional
+    // path. CodeQL has a dedicated query for exactly this (cs/dispose-not-called-on-throw,
+    // and cs/local-not-disposed also models exceptional flow). Own.NET used to miss it —
+    // disposed-somewhere looked balanced — until the exception-edge model put a throw
+    // edge before each may-throw statement; it now flags it too -> should join (2)/(3)
+    // in "Agree".
+    //
+    // The try is kept a ONE-LINER (like LeakInTry) on purpose: the three tools anchor
+    // this one leak at different points — Own.NET at the acquire, CodeQL at the Dispose,
+    // Infer# at last-access — so a spread-out method puts them >3 lines apart and the
+    // oracle's ±3 line window splits one leak into own-only + oracle-only. Keeping the
+    // acquire and the try adjacent pulls the anchors back inside the window.
+    private static void DisposeOnThrow()
+    {
+        var onThrow = new FileStream("scratch3.bin", FileMode.Create);
+        try { onThrow.WriteByte(0x42); onThrow.Dispose(); }
+        catch (Exception) { /* swallowed, no dispose */ }
+    }
 }

corpus/fixtures/systemevents-console/README.md

@@ -13,12 +13,29 @@ The leaks (`Program.cs`):
 | 1 | `SystemEvents.DisplaySettingsChanged += …`, never `-=` | subscription / lifetime | **Own.NET only** |
 | 2 | `new FileStream(…)` local, never disposed | Dispose / RAII | **all three** (the control) |
 | 3 | `new FileStream(…)` never disposed, inside a `try`-method | Dispose / RAII | **all three** (closed by `try`-lowering) |
+| 4 | `Dispose()` inside `try` after a may-throw call (skipped on the throw path) | Dispose-on-throw | **all three** (exception-edge slice) |
 
 Leak `#2` is the agreement that proves the RAII oracles ran on the fixture; `#1` is
 the differentiator — Own.NET flags it, CodeQL / Infer# have no query for the
-subscription-leak class. #3 is the recall slice: before `try`/`finally` was lowered,
-Own.NET skipped any method containing a `try`, so this leak was *Oracle only*; now it
-joins #2 in **Agree** across all three tools.
+subscription-leak class. #3 is the `try`-lowering recall slice: before `try`/`finally`
+was lowered, Own.NET skipped any method containing a `try`, so this leak was *Oracle
+only*; now it joins #2 in **Agree** across all three tools.
+
+#4 is the **exception-edge** slice. The stream *is* disposed, but the `Dispose()` sits
+inside the `try` after a may-throw call, so it's skipped if the call throws — a leak only
+on the exceptional path. CodeQL has a dedicated query for this (`cs/dispose-not-called-on-throw`;
+`cs/local-not-disposed` also models exceptional flow) and Infer#'s Pulse engine models
+exceptional paths too. Own.NET used to miss it (disposed *somewhere* looked balanced)
+until the exception-edge model inserted a throw edge before each may-throw statement in a
+`try`; it now flags it too, so #4 joins #2/#3 in **Agree** across all three.
+
+One wrinkle worth recording: the three tools anchor this leak at *different* program
+points — Own.NET at the acquire, CodeQL at the `Dispose()` call, Infer# at the last
+access — so a spread-out method puts them >3 lines apart and the oracle's ±3 line window
+splits one leak into "Own.NET only" + "Oracle only". Keeping the `try` a one-liner (as
+`LeakInTry` already is) pulls the anchors back within the window so the agreement is
+visible. The line window is intentionally conservative; this is a property of the
+*comparison*, not of the detections.
 
 Run via the oracle's local-fixture mode — set `corpus/oracle-target.txt` to:
 

corpus/oracle-target.txt

@@ -4,8 +4,12 @@
 # Optional lines: ref=, paths=, build=, include_tests=. Dev-branch only.
 #
 # Cross-tool oracle on a Linux-buildable fixture, so ALL THREE tools run (Infer#
-# included — ScreenToGif's WPF won't build on Linux). Re-run after aligning the
-# codeql-action analyze@v4 with init@v4 (the v3/v4 mismatch broke CodeQL last run);
-# expect the 3rd leak (try-method) in "Agree" across all THREE now. See the README.
+# included — ScreenToGif's WPF won't build on Linux). Re-run #2 of the EXCEPTION-EDGE
+# slice after the first run surfaced two artifacts: (a) #3 (tfLeak) was double-reported
+# — a never-disposed local in a try leaks on BOTH the injected exceptional exit and the
+# normal end; now deduped in the bridge; (b) #4's anchors were >3 lines apart (Own.NET
+# acquire / CodeQL Dispose / Infer# last-access) so the ±3 window split it — the try is
+# now a one-liner adjacent to the acquire. Expect #2/#3/#4 in "Agree" (no dup), #1
+# Own.NET-only, 0 oracle-only. See the README.
 local:corpus/fixtures/systemevents-console
 build=SystemEventsLeak.csproj

docs/ROADMAP.md

@@ -90,7 +90,13 @@ architectural strictness, and the borrow-checker showcase):
    The cross-tool oracle confirms the differentiation: CodeQL *and* Infer# (the latter
    via a buildable fixture) cover the Dispose/RAII class and flag none of these
    subscription leaks — agreeing with Own.NET only on a Dispose leak, never a subscription.
-   See [docs/notes/real-world-mining.md](notes/real-world-mining.md).
+   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
+   `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).
 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

@@ -116,33 +116,56 @@ Their leak findings are **nearly disjoint** (file overlap: **1**):
   coverage, not type recognition**: the `--flow-locals` detector skips any method with
   an unmodelled construct (`for`/`try`/`switch`), and these disposables live in such
   methods (tell: the `StringReader`/`XmlReader` cases are a *recognised* disposable
-  type, yet still missed). `for` **and** `try`/`finally` are now lowered (sequential
-  `A; B`, catch-disposes bailed for soundness), so a plain undisposed local inside a
-  try-method is caught — confirmed on the cross-tool fixture, where a `try`-method
-  `FileStream` leak moved from *Oracle only* into **Agree** (Own.NET + Infer#). Still
-  deferred: the true `dispose-not-called-on-throw` shape (disposed in `try`, not
-  `finally`) needs per-statement exceptional exits, and `switch`/`do` are unmodelled.
+  type, yet still missed). `for` **and** `try` are now lowered, in two slices: first
+  sequential `A; B` (catch-disposes bailed for soundness), so a plain undisposed local
+  inside a try-method is caught; then the **exception-edge** model — before each
+  may-throw statement in a `try`, inject an exceptional exit (`if(*){ <finally>; return }`)
+  — which catches the true `dispose-not-called-on-throw` shape (disposed in `try`, not
+  `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`.
 - **Agree — 1** (`HttpHelper.cs`).
 
 So the SystemEvents and VideoSource findings are **differentiated — confirmed by the
 oracle, not just argued**: the tools are complementary (Own.NET on subscription/
 lifetime, CodeQL on Dispose/RAII), overlapping on a single file.
 
 **Infer#, via a buildable fixture.** ScreenToGif can't build on Linux, so to get the
-third tool in, a minimal `net8.0` console reproduces both leak classes
+third tool in, a minimal `net8.0` console reproduces the leak classes
 (`corpus/fixtures/systemevents-console/`, fed to the oracle via a `local:` target).
-All three tools run; the diff is a clean 2×2:
-
-| `Program.cs` | leak | Own.NET | CodeQL | Infer# |
-|---|---|:-:|:-:|:-:|
-| `:41` | `new FileStream(…)` never disposed — Dispose/RAII | ✓ | ✓ | ✓ |
-| `:20` | `SystemEvents.DisplaySettingsChanged +=` never `-=` — subscription | ✓ | — | — |
-
-The FileStream leak is **Agree** across all three — the control that proves CodeQL
-*and* Infer# actually run and detect resource leaks on this code. The SystemEvents
-subscription is **Own.NET only**: **Infer# misses it too.** Both mature oracles cover
-the Dispose/RAII class and neither has the subscription-leak class — the
-differentiation, nailed with all three tools.
+All three tools run; the diff (latest run) is:
+
+| `Program.cs` | leak | class | Own.NET | CodeQL | Infer# |
+|---|---|---|:-:|:-:|:-:|
+| `:43` | `new FileStream(…)` never disposed | Dispose/RAII | ✓ | ✓ | ✓ |
+| `:54` | undisposed local inside a `try`-method | Dispose/RAII (try-lowering) | ✓ | ✓ | ✓ |
+| `:77` | `Dispose()` in `try` after a may-throw call — skipped on the throw path | dispose-on-throw (exception-edge) | ✓ | ✓ | ✓ |
+| `:20` | `SystemEvents.DisplaySettingsChanged +=` never `-=` | subscription | ✓ | — | — |
+
+The three Dispose/RAII leaks are **Agree** across all three tools — the controls that
+prove CodeQL *and* Infer# actually run and detect resource leaks on this code — and the
+bottom two are the recall slices: the plain `try`-method leak (sequential lowering) and
+the dispose-on-throw leak (exception-edge), the latter matching CodeQL's dedicated
+`cs/dispose-not-called-on-throw` query. **Oracle-only is empty** — no Dispose/RAII leak
+on this fixture is missed. The `SystemEvents` subscription is **Own.NET only**: **Infer#
+misses it too.** Both mature oracles cover the Dispose/RAII class and neither has the
+subscription-leak class — the differentiation, nailed with all three tools.
+
+> The exception-edge slice also surfaced a hygiene bug it then fixed: a local that
+> leaks on *both* the injected exceptional exit *and* the normal end produced two
+> identical OWN001s (every flow-local diagnostic remaps to the acquire line, so they
+> collapse). The bridge now drops byte-identical findings (`ownir.py`), pinned by
+> `tests/fixtures/ownir/flow_leak_two_exits.facts.json`. One leak, one finding.
 
 > Getting a trustworthy diff took fixing two oracle bugs: the comparator dropped
 > multi-line / untagged own-check findings (`scripts/mine_report.py` parser drift —