diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 52533551..9169b430 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 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, 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/.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/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..4d08f97c 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. +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. 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..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). 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 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 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 diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 6dc735de..01c979c1 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -357,8 +357,45 @@ 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). + // + // 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 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; + 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..dd8c1866 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -88,6 +88,54 @@ 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(); } + } + + // 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)