From 518ab13e92651584eb3aac1a980cc5d4719291c3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 03:09:30 +0000 Subject: [PATCH 1/5] feat(extractor): lower try/finally in the flow detector (close the try-method recall slice) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The oracle's "Oracle only" Dispose-class bucket included plain undisposed locals the --flow-locals detector skipped only because their method had a `try`. Lower `try { A } [catch...] [finally { B }]` as sequential `A; B`: a local acquired in try and disposed in finally stays balanced (silent), one never disposed leaks (now caught), and try-methods are no longer skipped wholesale. Catch bodies aren't lowered; to stay sound, bail (skip the method) if a catch disposes, so a release that only happens in a catch is never missed -> no false leak. Not yet modelled (documented next step): dispose-not-called-on-throw (disposed in try, not finally) reads as released here — needs per-statement exceptional exits; switch/do likewise stay skipped. FlowLocalsSample gains TryFinallyClean (silent), TryNeverDisposed (flagged), and CatchDisposesSkipped (soundly skipped -> silent); CI asserts each + the coverage invariant still holds. --- .github/workflows/ci.yml | 14 +++++++--- frontend/roslyn/OwnSharp.Extractor/Program.cs | 24 +++++++++++++++- frontend/roslyn/samples/FlowLocalsSample.cs | 28 +++++++++++++++++++ 3 files changed, 61 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 52533551..2147aeab 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -263,15 +263,21 @@ 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. + echo "$out" | grep -qE "OWN001.*'tfLeak'" \ + || { echo "FAIL: expected OWN001 on the undisposed local in a try-method"; exit 1; } # dispose-optional (Task), disposed/escaping locals, a `for` loop whose - # disposable is disposed after it (`looped`, balanced), and a balanced - # acquire+dispose in a loop (`whileClean`) must stay silent: + # 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; do + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch; 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, never-vs-every-path wording, dispose-optional exempt, beyond flat)" + 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)" - name: Coverage summary (--stats) run: | # --stats prints a flow-locals coverage line to stderr and stamps the same diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 6dc735de..985e6ced 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -357,8 +357,30 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List silent (the safe dispose pattern); one never + // released anywhere leaks -> caught. This un-skips try-methods, the big + // recall slice (a plain undisposed local living inside a try). NOT modelled + // yet: dispose-on-throw (released in `try`, not `finally`) reads as released + // here — that needs per-statement exceptional exits (a later slice). 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 (no false leak). + foreach (var cc in trys.Catches) + if (cc.Block.DescendantNodes().OfType() + .Any(i => i.Expression is MemberAccessExpressionSyntax cm + && cm.Name.Identifier.Text is "Dispose" or "Close" or "DisposeAsync")) + return false; + if (!LowerFlowStmt(trys.Block, tracked, nodes)) + return false; + if (trys.Finally is { } fin && !LowerFlowStmt(fin.Block, tracked, nodes)) + return false; + return true; + } default: - return false; // unmodelled (do/try/switch/...) -> bail the method + return false; // unmodelled (do/switch/...) -> bail the method } } diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index 56484fee..ca26ad4c 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -88,6 +88,34 @@ public void ForLeak(int n) } } + // `try`/`finally` lowered sequentially: a stream acquired in `try` and disposed in + // `finally` is balanced -> silent (the safe dispose pattern). Before, the `try` + // made the whole method skip. + public void TryFinallyClean() + { + var tfClean = new MemoryStream(); + try { tfClean.WriteByte(1); } + finally { tfClean.Dispose(); } + } + + // the recall win: a local never disposed, sitting in a try-method whose catch only + // logs -> now caught (OWN001), where the `try` used to make the method skip. + public void TryNeverDisposed() + { + var tfLeak = new MemoryStream(); + try { tfLeak.WriteByte(1); } + catch (Exception) { /* logged, not disposed */ } + } + + // sound bail: a `catch` that disposes a local is not lowered (we'd lose that + // release), so the method is skipped rather than risk a false leak -> silent. + public void CatchDisposesSkipped() + { + var tfCatch = new MemoryStream(); + try { tfCatch.WriteByte(1); } + catch (Exception) { tfCatch.Dispose(); } + } + // acquire + dispose within the loop body is balanced -> silent (no false // positive now that loops are analysed rather than skipped). public void WhileClean(int n) From 3e4ce4cdf72e2d3171dcbba392c324d33431b3e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 03:15:24 +0000 Subject: [PATCH 2/5] test(oracle): add a try-method leak to the fixture to validate the try-lowering slice Third leak in the cross-tool fixture: a FileStream never disposed, inside a try-method. Before try/finally lowering it was "Oracle only" (Own.NET skipped any method with a `try`); now Own.NET lowers it and should join the FileStream control in "Agree" across Own.NET + CodeQL + Infer#. Bump the oracle sentinel to re-run. --- corpus/fixtures/systemevents-console/Program.cs | 13 +++++++++++++ corpus/fixtures/systemevents-console/README.md | 7 +++++-- corpus/oracle-target.txt | 6 +++--- 3 files changed, 21 insertions(+), 5 deletions(-) diff --git a/corpus/fixtures/systemevents-console/Program.cs b/corpus/fixtures/systemevents-console/Program.cs index fcd43504..40e1d82e 100644 --- a/corpus/fixtures/systemevents-console/Program.cs +++ b/corpus/fixtures/systemevents-console/Program.cs @@ -30,6 +30,7 @@ public static void Main() { _ = new DisplayWatcher(); LeakAFile(); + LeakInTry(); } // (2) DISPOSE leak — CodeQL's / Infer#'s class, and the control: a local @@ -42,4 +43,16 @@ private static void LeakAFile() stream.WriteByte(0x42); // ...no Dispose()/using -> resource leak } + + // (3) DISPOSE leak inside a TRY-METHOD — the `try`-lowering recall slice. Before + // try/finally was lowered, Own.NET skipped any method containing a `try`, so this + // leak was "Oracle only" (only CodeQL / Infer# caught it). Now Own.NET lowers + // try/finally and catches it too -> it should land in "Agree" across all three. + private static void LeakInTry() + { + var tried = new FileStream("scratch2.bin", FileMode.Create); + try { tried.WriteByte(0x42); } + catch (Exception) { /* logged, not disposed */ } + // ...no Dispose()/using -> resource leak, now seen despite the `try` + } } diff --git a/corpus/fixtures/systemevents-console/README.md b/corpus/fixtures/systemevents-console/README.md index 6cddeaee..8d4d8f8e 100644 --- a/corpus/fixtures/systemevents-console/README.md +++ b/corpus/fixtures/systemevents-console/README.md @@ -6,16 +6,19 @@ same code. ScreenToGif (the real finding) is WPF and does not `dotnet build` on Linux oracle runner, so Infer# was skipped there; this fixture builds on Linux, so Infer# runs and the cross-tool picture is complete. -The two leaks (`Program.cs`): +The leaks (`Program.cs`): | # | leak | class | expected to flag | |---|------|-------|------------------| | 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) | #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. A clean 2×2 for the differentiation thesis. +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. Run via the oracle's local-fixture mode — set `corpus/oracle-target.txt` to: diff --git a/corpus/oracle-target.txt b/corpus/oracle-target.txt index 2557be31..b25c6134 100644 --- a/corpus/oracle-target.txt +++ b/corpus/oracle-target.txt @@ -4,8 +4,8 @@ # 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). Expected 2x2: the FileStream -# Dispose leak agrees across tools; the SystemEvents subscription leak is Own.NET -# only. See corpus/fixtures/systemevents-console/README.md. +# included — ScreenToGif's WPF won't build on Linux). Re-run after the try-lowering: +# the fixture now has a 3rd leak inside a try-method, which should move from "Oracle +# only" into "Agree" now that Own.NET catches try-method leaks. See the fixture README. local:corpus/fixtures/systemevents-console build=SystemEventsLeak.csproj From f01dcdc9e0d0e4d35f220223e69b5b2a1af92651 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 03:22:03 +0000 Subject: [PATCH 3/5] docs(p-004): record the try-lowering slice + its oracle re-validation The flow detector now lowers try/finally (sequential A;B, catch-disposes bailed for soundness), so a plain undisposed local in a try-method is caught. The cross-tool fixture's try-method FileStream leak moved from "Oracle only" into "Agree" (Own.NET + Infer#), validating the slice. Note the still-deferred dispose-not-called-on-throw (try-not-finally) + switch/do. --- docs/notes/real-world-mining.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/notes/real-world-mining.md b/docs/notes/real-world-mining.md index f48915d8..7f01306e 100644 --- a/docs/notes/real-world-mining.md +++ b/docs/notes/real-world-mining.md @@ -116,8 +116,12 @@ 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` is now lowered too (closing that slice, CI-checked); - the `try`-shaped `dispose-not-called-on-throw` cases are the high-value next step. + 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. - **Agree — 1** (`HttpHelper.cs`). So the SystemEvents and VideoSource findings are **differentiated — confirmed by the From 14708341922c442e0bd25cbab060e772275ebaa2 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 03:23:04 +0000 Subject: [PATCH 4/5] fix(oracle): align codeql-action analyze@v4 with init@v4 (restore the CodeQL arm) The cross-tool re-run lost CodeQL to JOB_STATUS_CONFIGURATION_ERROR ("Loaded a configuration file for version '4.36.2', but running version '3.36.2'"): init was github/codeql-action/init@v4 but analyze was still @v3, so init wrote a v4 config the v3 analyze couldn't read. Bump analyze to @v4 to match. Bump the sentinel to re-run and confirm all three tools (incl. CodeQL) return on the fixture. --- .github/workflows/oracle.yml | 2 +- corpus/oracle-target.txt | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/oracle.yml b/.github/workflows/oracle.yml index 53fb3012..52b081fb 100644 --- a/.github/workflows/oracle.yml +++ b/.github/workflows/oracle.yml @@ -187,7 +187,7 @@ jobs: source-root: target queries: security-and-quality - name: CodeQL analyze - uses: github/codeql-action/analyze@v3 + uses: github/codeql-action/analyze@v4 continue-on-error: true with: category: ownnet-oracle diff --git a/corpus/oracle-target.txt b/corpus/oracle-target.txt index b25c6134..dccfb21d 100644 --- a/corpus/oracle-target.txt +++ b/corpus/oracle-target.txt @@ -4,8 +4,8 @@ # 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 the try-lowering: -# the fixture now has a 3rd leak inside a try-method, which should move from "Oracle -# only" into "Agree" now that Own.NET catches try-method leaks. See the fixture README. +# 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. local:corpus/fixtures/systemevents-console build=SystemEventsLeak.csproj From dc983a6431978bbb68b61fd75de17ef564ffa352 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 05:10:22 +0000 Subject: [PATCH 5/5] fix(extractor): try-lowering FP fixes from PR #31 review (early-return finally + ?.Dispose catch) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two false positives in the try/finally lowering, caught in review: * Codex (P2): a `return` inside a try-with-finally made the finally's release unreachable after the terminal `return` op, so the model falsely flagged a resource the finally disposes (the common `try { …; return x; } finally { r.Dispose(); }`). Until finally-before-return is modelled, bail when a try-with-finally contains a return — that shape is safe anyway, so skipping it is sound. * CodeRabbit: the catch-dispose bail only matched `x.Dispose()` (member access), not `x?.Dispose()` (member binding), so a catch-only conditional dispose got lowered and could false-flag. Match both expression shapes. FlowLocalsSample gains TryFinallyReturn and CatchNullCondDispose (both must stay silent); CI asserts them. Also reword the fixture README to avoid MD018 (CodeRabbit). --- .github/workflows/ci.yml | 2 +- .../fixtures/systemevents-console/README.md | 4 +-- frontend/roslyn/OwnSharp.Extractor/Program.cs | 25 +++++++++++++++---- frontend/roslyn/samples/FlowLocalsSample.cs | 20 +++++++++++++++ 4 files changed, 43 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2147aeab..9169b430 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -274,7 +274,7 @@ jobs: # 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; do + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull; 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/corpus/fixtures/systemevents-console/README.md b/corpus/fixtures/systemevents-console/README.md index 8d4d8f8e..4d08f97c 100644 --- a/corpus/fixtures/systemevents-console/README.md +++ b/corpus/fixtures/systemevents-console/README.md @@ -14,8 +14,8 @@ The leaks (`Program.cs`): | 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) | -#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 +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. diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 985e6ced..01c979c1 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -365,13 +365,28 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, List caught. This un-skips try-methods, the big // recall slice (a plain undisposed local living inside a try). NOT modelled // yet: dispose-on-throw (released in `try`, not `finally`) reads as released - // here — that needs per-statement exceptional exits (a later slice). 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 (no false leak). + // here — that needs per-statement exceptional exits (a later slice). + // + // A `return` inside the try makes a finally's release UNREACHABLE in this + // sequential model (the core treats `return` as terminal), which would + // FALSELY flag a resource the finally disposes. Until finally-before-return + // is modelled, bail when a try-with-finally contains a return: the common + // `try { …; return x; } finally { r.Dispose(); }` is safe anyway, so skipping + // it is sound (a real leak in that shape is rare). + if (trys.Finally is not null + && trys.Block.DescendantNodes().OfType().Any()) + return false; + // 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 (no false leak). Match + // both `x.Dispose()` (member access) and `x?.Dispose()` (member binding). foreach (var cc in trys.Catches) if (cc.Block.DescendantNodes().OfType() - .Any(i => i.Expression is MemberAccessExpressionSyntax cm - && cm.Name.Identifier.Text is "Dispose" or "Close" or "DisposeAsync")) + .Any(i => (i.Expression switch + { + MemberAccessExpressionSyntax ma => ma.Name.Identifier.Text, + MemberBindingExpressionSyntax mb => mb.Name.Identifier.Text, + _ => (string?)null, + }) is "Dispose" or "Close" or "DisposeAsync")) return false; if (!LowerFlowStmt(trys.Block, tracked, nodes)) return false; diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index ca26ad4c..dd8c1866 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -116,6 +116,26 @@ public void CatchDisposesSkipped() catch (Exception) { tfCatch.Dispose(); } } + // a `return` inside a try-with-finally: the finally still disposes (SAFE), but the + // model can't yet place the finally before the return — so it bails rather than + // falsely flag the resource as leaked on the return path -> silent. + public void TryFinallyReturn(bool c) + { + var tfRet = new MemoryStream(); + try { tfRet.WriteByte(1); if (c) return; tfRet.WriteByte(2); } + finally { tfRet.Dispose(); } + } + + // the catch-dispose bail also covers conditional access: `catch { x?.Dispose(); }` + // (a member-binding, not member-access) is still recognised, so the method is + // skipped rather than risk a false leak -> silent. + public void CatchNullCondDispose() + { + var tfNull = new MemoryStream(); + try { tfNull.WriteByte(1); } + catch (Exception) { tfNull?.Dispose(); } + } + // acquire + dispose within the loop body is balanced -> silent (no false // positive now that loops are analysed rather than skipped). public void WhileClean(int n)