From 7f598b0043c2a8600c5a0049aadf3238f93c9575 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 12:46:58 +0000 Subject: [PATCH 1/2] =?UTF-8?q?flow:=20model=20explicit=20`throw`=20as=20a?= =?UTF-8?q?n=20abnormal=20exit=20=E2=80=94=20body-level=20dispose-not-call?= =?UTF-8?q?ed-on-throw=20(no=20try)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An explicit `throw` statement hit the unmodelled `default` and bailed the WHOLE method, so any leak in a method guarded by a top-level validation throw (`if (x is null) throw …;`) was invisible to every flow detector. Model a `throw` with no enclosing try (onThrow null && canEscape) as a bare CFG exit: a resource owned there and disposed only later leaks on the throw path — exactly the synthetic exit the injected may-throw edges already use. Two wins, both sound (a throw with no enclosing try definitely exits, so an owned resource definitely leaks — FP-free): * the no-try slice of CodeQL's cs/dispose-not-called-on-throw: `acquire; if (bad) throw; dispose;` leaks on the throw path (dotNoTry, partial-path); * un-bailing every validation-throw-guarded method, lighting up all detectors on the rest of the body (vtl, a later undisposed local, now caught). Stays conservative inside a try: an explicit throw there may run a finally or be caught (typed/catch-all), which needs the thrown-type-vs-catch match (not threaded here), so it keeps bailing — no new false escape past a catch. Samples (FlowLocalsSample): ValidatedThenLeaks (vtl, never-disposed, recall), ThrowAfterAcquireLeaks (dotNoTry, partial-path), + ThrowAfterDisposeClean (release before throw) and ValidatedThenClean (balanced) as silent controls. Core handling of the {op:return} exit is unchanged (already pinned); the C# lowering is asserted end-to-end in CI. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 15 +++++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 28 ++++++++++- frontend/roslyn/samples/FlowLocalsSample.cs | 49 +++++++++++++++++++ 3 files changed, 89 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 44faa8a0..6961f8c2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -639,6 +639,16 @@ jobs: || { 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; } + # body-level explicit `throw` (no enclosing try) — these methods used to bail the flow + # pass entirely (a `throw` hit the unmodelled default). Now an explicit throw is an + # abnormal exit, so they are analysed: a top-level validation throw no longer HIDES a + # later undisposed local ('vtl', never disposed), and a Dispose skipped by a `throw` + # on the guard path leaks on that path ('dotNoTry', partial). Closes the no-try slice + # of cs/dispose-not-called-on-throw + un-bails every validation-throw-guarded method. + echo "$out" | grep -qE "OWN001.*'vtl' is never disposed" \ + || { echo "FAIL: expected OWN001 on the local hidden behind a top-level validation throw"; exit 1; } + echo "$out" | grep -qE "OWN001.*'dotNoTry' may not be disposed on every path" \ + || { echo "FAIL: expected OWN001 on the body-level dispose-not-called-on-throw (no try)"; exit 1; } # closure-capture escape (precision): a SemaphoreSlim captured by a returned async # lambda outlives the method, so it cannot be disposed at method scope -> escaped -> # silent ('captured'). A SemaphoreSlim NOT captured and never disposed STILL leaks -> @@ -699,7 +709,10 @@ jobs: # silenced (Codex/CodeRabbit P1; benchmark memorypool-double-dispose parity). echo "$out" | grep -qE "OWN002.*'pooled'" \ || { echo "FAIL: a MemoryPool owner's .Memory used after Dispose must still trip OWN002"; exit 1; } - for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf captured shaClean stopped defer ctorMoved handedOwner; do + # tdClean: a Dispose BEFORE an explicit `throw` -> released at the abnormal exit -> + # silent. vtc: a local acquired after a top-level validation throw AND disposed -> + # analysed (no longer bailed) and balanced -> silent (the un-bail must not over-flag). + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf captured shaClean stopped defer ctorMoved handedOwner tdClean vtc; 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/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 0d783b4d..4937fd67 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -911,7 +911,8 @@ or ImplicitObjectCreationExpressionSyntax // mutually-exclusive branches: `if(*){ s1 } else { if(*){ s2 } else { … } }` — one // per section, value-opaque (we model control flow, not the matched value). A // trailing `break` ends a section (stripped); a section doing anything the model - // can't place here (a nested `break`, `goto case`, `throw`) bails the method. + // can't place here (a nested `break`, `goto case`) bails the method. A bare `throw` + // in a section IS modelled now (an abnormal exit) when no enclosing try wraps it. List? defaultNodes = null; var cases = new List>(); foreach (var section in sw.Sections) @@ -946,8 +947,31 @@ or ImplicitObjectCreationExpressionSyntax nodes.AddRange(chain); return true; } + case ThrowStatementSyntax thr: + // An explicit `throw` is an abnormal method exit: control leaves the method + // WITHOUT running the statements below it, so a resource owned here and disposed + // only LATER leaks on the throw path — dispose-not-called-on-throw with NO + // enclosing `try`. Modelled at the method-body level only: `onThrow is null` AND + // the throw escapes (`canEscape`) means no enclosing try would run a `finally` or + // catch it, so it is a bare CFG exit where a still-owned resource leaks — the same + // synthetic exit the injected may-throw edges use. INSIDE a try an explicit throw + // may run a finally or be caught (typed / catch-all); modelling that soundly needs + // the thrown-type-vs-catch match, which is not threaded here, so an explicit throw + // there keeps bailing (return false) exactly as before — no new false escape past a + // catch. (`throw;` rethrow only appears in a catch body, never lowered, so this is + // the `throw expr;` form.) The win is broad: a method whose only unmodelled + // statement was a top-level validation throw (`if (x is null) throw …;`) is now + // analysed instead of skipped, lighting up every detector on the rest of its body. + if (canEscape && onThrow is null) + { + nodes.Add(new { op = "return", var = (string?)null, line = LineOf(thr) }); + return true; + } + return false; default: - return false; // unmodelled (goto/labeled/throw/...) -> bail the method + // unmodelled (goto / labeled / local function / lock / fixed / a `throw` INSIDE a + // try) -> bail the method, honestly skipping rather than guessing. + return false; } } diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index 464f9658..e471e10f 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -272,6 +272,55 @@ public void CtorInLambdaNotThrow() lamPrior.Dispose(); } + // ─── body-level explicit `throw` (no enclosing try) ────────────────────────────────── + // An explicit `throw` used to make the flow pass bail the WHOLE method (it hit the + // unmodelled `default`). It is now an abnormal method exit, so these methods are analysed + // — closing the no-try slice of CodeQL's cs/dispose-not-called-on-throw and, more broadly, + // un-bailing every method guarded by a top-level validation throw. + + // recall (the un-bail win): a top-level validation `throw` no longer bails the method, so + // `vtl` — acquired after the guard and never disposed — now leaks (OWN001, "is never + // disposed"). Before, the throw made the whole method invisible to every detector. + public void ValidatedThenLeaks(object arg) + { + if (arg is null) throw new ArgumentNullException(nameof(arg)); + var vtl = new MemoryStream(); + vtl.WriteByte(1); + } + + // recall (the body-level dispose-on-throw the in-try model missed): `dotNoTry` is disposed + // at the end, but the `throw` on the guard path leaves the method first and skips that + // Dispose -> it leaks on the throw path. Disposed on the fall-through path, never on the + // throw path -> OWN001 "may not be disposed on every path". The fix is `using`. + public void ThrowAfterAcquireLeaks(bool bad) + { + var dotNoTry = new MemoryStream(); + if (bad) throw new InvalidOperationException(); + dotNoTry.Dispose(); + } + + // NOT a leak (the throw-exit is placed where ownership is exact, not blanket): the Dispose + // runs BEFORE the `throw`, so `tdClean` is already released at the abnormal exit -> nothing + // owned there -> silent. Proves "the method contains a throw" alone never leaks. + public void ThrowAfterDisposeClean() + { + var tdClean = new MemoryStream(); + tdClean.WriteByte(1); + tdClean.Dispose(); + throw new InvalidOperationException(); + } + + // NOT a leak (the un-bail must not over-flag): the same top-level validation `throw`, but + // `vtc` is acquired after it AND disposed -> analysed (no longer bailed) and balanced on + // every real path -> silent. The guard throw exits before the acquire, owning nothing. + public void ValidatedThenClean(object arg) + { + if (arg is null) throw new ArgumentNullException(nameof(arg)); + var vtc = new MemoryStream(); + vtc.WriteByte(1); + vtc.Dispose(); + } + // finally-before-return: the early `return` runs the finally (disposing `other`) FIRST, // then exits — so `other` is released on the return path and stays silent. But `earlyRet` // is disposed only AFTER the try, which the early return (and the throw on WriteByte) skip From 09d3365657aa6fad616896742609b18ae1bdfef1 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 13:18:35 +0000 Subject: [PATCH 2/2] =?UTF-8?q?flow:=20keep=20`throw`=20inside=20a=20final?= =?UTF-8?q?ly=20bailing=20=E2=80=94=20fix=20false=20leak=20past=20an=20out?= =?UTF-8?q?er=20finally=20(Codex=20P2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The explicit-throw exit keyed on `onThrow is null && canEscape`, but `finally` bodies are lowered with the default (null) onThrow — so a `throw` INSIDE a finally also took the bare-return branch, terminating before any ENCLOSING finally runs. For `try { try {} finally { throw; } } finally { s.Dispose(); }` that bare exit skips the outer `s.Dispose()` and falsely reports OWN001 on `s`. Guard the body-level throw branch with `!IsInsideFinally(thr)`: a throw lexically inside a finally keeps bailing the whole method (the sound honest-skip it had before this feature), since its real continuation is the OUTER cleanup the bare exit cannot run. Body-level throws (no enclosing try/finally) are unaffected. Sample ThrowInFinallyBails pins the Codex repro as silent; the four body-level throw samples keep their verdicts. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- .github/workflows/ci.yml | 5 ++++- frontend/roslyn/OwnSharp.Extractor/Program.cs | 22 ++++++++++++++++++- frontend/roslyn/samples/FlowLocalsSample.cs | 16 ++++++++++++++ 3 files changed, 41 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6961f8c2..b6c13833 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -712,7 +712,10 @@ jobs: # tdClean: a Dispose BEFORE an explicit `throw` -> released at the abnormal exit -> # silent. vtc: a local acquired after a top-level validation throw AND disposed -> # analysed (no longer bailed) and balanced -> silent (the un-bail must not over-flag). - for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf captured shaClean stopped defer ctorMoved handedOwner tdClean vtc; do + # tif (Codex P2): a `throw` inside an inner finally propagates through the OUTER finally + # that disposes it -> the throw-exit keeps BAILING the method (it can't run the enclosing + # cleanup) rather than emit a false leak -> silent. + for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf captured shaClean stopped defer ctorMoved handedOwner tdClean vtc tif; 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/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index 4937fd67..85cae321 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -564,6 +564,24 @@ st.Parent is BlockSyntax b && b.Statements.Count > 0 && b.Statements[^1] == st && b.Parent is not StatementSyntax; +// True when `node` sits lexically inside a `finally { }` block (walking up to the enclosing +// member / lambda boundary). A `throw` there is NOT a clean method exit: it propagates through +// any ENCLOSING `finally`/`try` cleanup, which a bare-return exit would skip — and `finally` +// bodies are lowered with the default (null) `onThrow`, so the body-level throw branch cannot +// tell them apart from the method body. Such a throw therefore keeps BAILING the method (sound +// honest-skip, as before this feature) rather than emit a false leak that misses the outer +// finally's release (Codex P2: `try { try {} finally { throw; } } finally { s.Dispose(); }`). +static bool IsInsideFinally(SyntaxNode node) +{ + for (var p = node.Parent; p is not null; p = p.Parent) + { + if (p is FinallyClauseSyntax) return true; + if (p is AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax + or BaseMethodDeclarationSyntax or AccessorDeclarationSyntax) return false; + } + return false; +} + // Inject an exceptional-exit edge `if(*){ onThrow }` before a LEAF may-throw statement // (an expression statement or a local declaration) inside a `try` body. `onThrow` is the // continuation a throw here runs to leave the method — this try's `finally`, then any @@ -962,7 +980,9 @@ or ImplicitObjectCreationExpressionSyntax // the `throw expr;` form.) The win is broad: a method whose only unmodelled // statement was a top-level validation throw (`if (x is null) throw …;`) is now // analysed instead of skipped, lighting up every detector on the rest of its body. - if (canEscape && onThrow is null) + // ...and a throw lexically inside a `finally` likewise keeps bailing (IsInsideFinally): + // its real continuation is the OUTER finally/try cleanup, which a bare exit would skip. + if (canEscape && onThrow is null && !IsInsideFinally(thr)) { nodes.Add(new { op = "return", var = (string?)null, line = LineOf(thr) }); return true; diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs index e471e10f..df3afb0e 100644 --- a/frontend/roslyn/samples/FlowLocalsSample.cs +++ b/frontend/roslyn/samples/FlowLocalsSample.cs @@ -321,6 +321,22 @@ public void ValidatedThenClean(object arg) vtc.Dispose(); } + // NOT a false leak (Codex P2): a `throw` inside the INNER finally is not a clean method exit + // — it propagates through the OUTER finally, which disposes `tif`. A bare-return throw-exit + // can't represent "run the enclosing finally first", and finally bodies are lowered with a + // null onThrow, so a throw lexically inside a finally keeps BAILING the whole method (honest + // skip) rather than emit a false OWN001 that misses the outer release -> silent. + public void ThrowInFinallyBails() + { + var tif = new MemoryStream(); + try + { + try { } + finally { throw new InvalidOperationException(); } + } + finally { tif.Dispose(); } + } + // finally-before-return: the early `return` runs the finally (disposing `other`) FIRST, // then exits — so `other` is released on the return path and stays silent. But `earlyRet` // is disposed only AFTER the try, which the early return (and the throw on WriteByte) skip