Model exception edges in try lowering for dispose-not-called-on-throw#32
Conversation
…lled-on-throw
The try-lowering now inserts an exceptional exit before each try-body statement that
makes a (non-dispose) call: `if(*){ <finally>; return }` — throw here, run the finally,
leave. A resource owned there and not released by the finally leaks on the exceptional
path = dispose-not-called-on-throw (a dispose placed in the try, not the finally):
* dispose in finally -> released on every exceptional exit -> silent (safe pattern);
* dispose inside the try after a may-throw call -> leaks (now caught, matching
CodeQL's cs/dispose-not-called-on-throw);
* `acquire; dispose;` with no call between -> no exit -> no false leak.
Helpers IsDisposeShaped (member access + binding) and StatementMayThrow (a non-dispose
call) drive it; the catch-dispose bail reuses IsDisposeShaped. A try-with-finally that
contains a return still bails (finally-before-return not threaded through the exits yet).
FlowLocalsSample gains DisposeOnThrow (now flagged); existing try cases stay correct.
CI asserts `dot` is flagged.
… re-validation Leak #4 in the SystemEvents fixture: a FileStream that IS disposed, but the Dispose() sits inside the try after a may-throw call (WriteByte), so it's skipped on the exceptional path. This is CodeQL's cs/dispose-not-called-on-throw (cs/local-not-disposed also models it). Own.NET used to miss it — disposed somewhere looked balanced — until the exception-edge model (77b2edd) inserted a throw edge before each may-throw statement in a try. Re-running the oracle on this fixture should land #4 in "Agree" with CodeQL, joining #2/#3, with #1 (subscription) staying Own.NET-only. Bumps the oracle sentinel to trigger the push-run.
…oracle fixture
The exception-edge try-lowering injects an exceptional exit (a bare return while
the local is live) before each may-throw statement. A local never disposed then
leaks on BOTH that exit and the normal fall-through, so the core emits OWN001
once per exit. Every flow-local diagnostic remaps to the acquire line, so the two
collapse to byte-identical findings. The first oracle run surfaced this as
Program.cs:54 appearing twice in "Agree".
- ownir.py: drop byte-identical findings (same file/line/code/component/event/
handler/message/kind/severity) before sorting. Native-OwnLang leaks at distinct
lines stay distinct — the key includes line; only the bridge's line-collapse
makes them identical, so deduping is exactly right.
- test_ownir.py + flow_leak_two_exits fixture: a two-leaking-exits flow body
(acquire; if(*){return}; use) must yield exactly one OWN001 (TryNeverDisposed
'tfLeak'@105). Without the dedup it returns two.
Also tighten the SystemEvents fixture's dispose-on-throw case (#4): the three
tools anchor the same leak at different points (Own.NET acquire / CodeQL Dispose /
Infer# last-access), so a spread-out method puts them >3 lines apart and the
oracle's ±3 window splits one leak into own-only + oracle-only. Keep the try a
one-liner adjacent to the acquire so the anchors fall inside the window -> #4
joins #2/#3 in "Agree" across all three. Bumps the oracle sentinel.
…esult The dispose-not-called-on-throw shape (disposed in `try`, not `finally`) is no longer deferred: the exception-edge model closes it, and the latest oracle run on the SystemEvents fixture lands it in Agree across all three tools, matching CodeQL's cs/dispose-not-called-on-throw. Updates the recall-gap paragraph, the fixture results table (now 4 leaks: 3 Dispose/RAII in Agree, subscription Own.NET-only, oracle-only empty), and the milestone-1 ROADMAP entry. Also notes the one-leak-one-finding dedup the slice surfaced and fixed.
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Repository UI Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
✅ Files skipped from review due to trivial changes (1)
🚧 Files skipped from review as they are similar to previous changes (1)
📝 WalkthroughWalkthroughThe PR upgrades the flow-locals ChangesException-edge try-lowering, deduplication, and validation
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
![chatgpt-codex-connector[bot]](https://cdn.github.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 994dde660b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if (StatementMayThrow(stmt)) | ||
| { | ||
| var ex = new List<object>(finallyNodes) | ||
| { new { op = "return", var = (string?)null, line = LineOf(stmt) } }; |
There was a problem hiding this comment.
When the try has a catch that handles the exception, this synthetic return makes the exceptional path leave the method before any statements after the try/catch run. Safe code such as var s = new MemoryStream(); try { MayThrow(); } catch { } s.Dispose(); is therefore reported as an OWN001 even though the catch completes and the subsequent dispose executes on the thrown path; the guard above only bails when the catch itself disposes, so this false positive is reachable for ordinary logging/empty catches.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Good catch — fixed in f9563ef. You're right: with a swallowing catch the exceptional path rejoins normal flow, so a Dispose() after the try/catch runs on the thrown path too, and the synthetic return was a false leak. The exception edges are now injected only when the caught path's continuation is end-of-method — no catch (the exception propagates out past any post-try code), or the try is the method body's tail statement. Otherwise the try is lowered sequentially (a never-disposed local is still caught at end-of-function; only dispose-on-throw is forgone for that shape, which is sound). Locked with a CatchThenDisposeAfter sample that must stay silent (CI asserts it).
Generated by Claude Code
| foreach (var stmt in trys.Block.Statements) | ||
| { | ||
| if (StatementMayThrow(stmt)) |
There was a problem hiding this comment.
Because this loop only injects an edge for each top-level statement in trys.Block.Statements, a may-throw call nested inside an if, loop, or inner block gets a synthetic exit before the outer statement, before locals acquired inside that branch are live, and LowerFlowStmt then lowers the nested body without any exception edge at the actual call. A shape like try { if (c) { var s = new MemoryStream(); s.WriteByte(1); s.Dispose(); } } catch {} is missed even though WriteByte can skip the dispose, so the new dispose-not-called-on-throw coverage does not work inside common nested control flow.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed — and deferred as the next slice rather than fixed now. This one is a recall gap (a missed detection), not a false positive: the injection only walks the try's top-level statements, so a may-throw nested in an if/loop/inner block inside the try doesn't get an exit at the call site. Recursing the edges into nested bodies — with the right finally threading and the same continuation/tail soundness as the sibling fix in f9563ef — is a real modelling step I'd rather land deliberately than rush into this PR. Tracked alongside finally-before-return and switch/do in the deferred list (docs/notes/real-world-mining.md).
Generated by Claude Code
![coderabbitai[bot]](https://cdn.github.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@frontend/roslyn/OwnSharp.Extractor/Program.cs`:
- Around line 270-283: The IsDisposeShaped method does not unwrap ConfigureAwait
calls, causing it to misidentify dispose calls wrapped in ConfigureAwait(false)
as non-dispose invocations. This leads StatementMayThrow to incorrectly classify
such statements as potentially throwing. Update IsDisposeShaped to unwrap
ConfigureAwait(false) invocations before checking the method name, similar to
how EmitFlowExpr already handles this unwrapping on lines 431-435. When the
expression is an invocation where the invoked member is ConfigureAwait and its
expression is another invocation, unwrap to check that inner invocation instead.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 6b815273-0ca7-4d8f-9157-d2bd68553a50
📒 Files selected for processing (11)
.github/workflows/ci.ymlcorpus/fixtures/systemevents-console/Program.cscorpus/fixtures/systemevents-console/README.mdcorpus/oracle-target.txtdocs/ROADMAP.mddocs/notes/real-world-mining.mdfrontend/roslyn/OwnSharp.Extractor/Program.csfrontend/roslyn/samples/FlowLocalsSample.csownlang/ownir.pytests/fixtures/ownir/flow_leak_two_exits.facts.jsontests/test_ownir.py
Both are dispose-on-throw FPs where the resource is actually disposed on every
path; the synthetic exceptional exit mismodelled the continuation.
1. Swallowing catch + post-try Dispose (Codex): `try { MayThrow(); } catch {}
s.Dispose();` — the synthetic `return` models the exception leaving the method,
but a swallowing catch continues to the post-try Dispose, so s IS disposed on
the thrown path. The exception edges are sound only when the caught path's
continuation is end-of-method: no catch (it propagates out), or the try is the
body's tail statement. Otherwise inject no edges and lower the try sequentially
— a never-disposed local is still caught at end-of-function; only dispose-on-
throw is forgone for that shape. New IsBodyTail helper; regression
CatchThenDisposeAfter (silent).
2. ConfigureAwait-wrapped async dispose (CodeRabbit): `await x.DisposeAsync()
.ConfigureAwait(false)` inside a try read as a non-dispose ConfigureAwait call,
so StatementMayThrow injected a false exceptional-leak edge before the release.
IsDisposeShaped now unwraps `.ConfigureAwait(false)`, mirroring EmitFlowExpr.
Regression DisposeAsyncConfiguredInTry (silent).
CI silent list gains cda + daci. Existing try cases unchanged (DisposeOnThrow,
LeakInTry stay flagged; tfClean/tfCatch/tfRet/tfNull stay silent). Deferred
(sound recall gap, Codex): recurse exception edges into nested try bodies.
Note the soundness condition on the exception edges (only injected when the caught path's continuation is end-of-method) and add nested try bodies to the deferred list, matching the PR #32 review replies.
|
@codex review The two false positives you flagged are fixed in
The nested- Generated by Claude Code |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2110e64f5f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if (edgesSound && StatementMayThrow(stmt)) | ||
| { | ||
| var ex = new List<object>(finallyNodes) | ||
| { new { op = "return", var = (string?)null, line = LineOf(stmt) } }; | ||
| nodes.Add(new { op = "if", line = LineOf(stmt), then = ex, @else = new List<object>() }); |
There was a problem hiding this comment.
When the try-body stmt is an if/loop/block, StatementMayThrow(stmt) looks through all descendants but the synthetic exceptional return is inserted before the entire parent statement. For example, try { var s = ...; if (c) { s.Dispose(); MayThrow(); } else { s.Dispose(); } } catch {} is disposed on every real path, but this edge runs before the if while s is still owned and produces a false OWN001. Exception edges need to be placed inside lowered nested bodies, or skipped for compound statements until that is supported.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Good catch — fixed in be778d9. You're right: StatementMayThrow looks through all descendants, so for a compound statement (if/loop/block) the edge landed before the whole statement, where a resource disposed inside a nested branch is still owned — a false OWN001 on try { var s=...; if (c) { s.Dispose(); MayThrow(); } else { s.Dispose(); } } catch {}. Exception edges are now injected only before leaf statements whose may-throw is at the statement's own level — expression statements and local declarations (new EdgeEligible helper); compound statements get no edge. Every real dispose-on-throw is an expression-statement may-throw, so detection is unchanged (DisposeOnThrow/LeakInTry still flagged). The nested may-throw inside a compound is the same deferred nested-try slice (a sound recall gap, not an FP). Locked with a DisposeInsideIfWithThrow regression that must stay silent (CI asserts it).
Generated by Claude Code
…ements A third exception-edge false positive (PR #32 Codex review). StatementMayThrow looks through ALL descendants of a statement, so for a compound statement (if/loop/block) it returns true when any nested call may throw — but the synthetic exit was inserted before the WHOLE statement, where resources disposed INSIDE a nested branch are still owned. e.g. `try { var s=...; if (c) { s.Dispose(); MayThrow(); } else { s.Dispose(); } } catch {}` is disposed on every real path, yet the edge before the `if` flagged a false OWN001. Edges are now injected only before LEAF statements whose may-throw call is at the statement's own level — expression statements and local declarations (new EdgeEligible helper). Compound statements get no edge; their nested may-throw is the already-deferred nested-try slice (a sound recall gap, not an FP). Every true positive is an expression-statement may-throw, so detection is unchanged (DisposeOnThrow/LeakInTry still flagged). Regression DisposeInsideIfWithThrow (silent); CI silent list gains cif.
PhysShell
changed the title
|
@codex review
Generated by Claude Code |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: be778d9d0e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| // it is not a leak point — only non-dispose CALLS create an exceptional exit worth | ||
| // modelling for dispose-not-called-on-throw.) | ||
| static bool StatementMayThrow(StatementSyntax st) => | ||
| st.DescendantNodes().OfType<InvocationExpressionSyntax>().Any(i => !IsDisposeShaped(i)); |
There was a problem hiding this comment.
When a try already owns a local and a later constructor runs before cleanup, e.g. var r = ...; try { var f = new FileStream(path, FileMode.Open); r.Dispose(); }, the constructor can throw and skip r.Dispose(). StatementMayThrow only looks for InvocationExpressionSyntax, so object creations produce no synthetic exceptional edge; the flow lowers sequentially and reports no leak even though r is undisposed on that path.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
You're right, and thanks — the comment there was incomplete (it only considered the resource being created, not a prior one). A throwing constructor does leak a PRIOR owned resource whose dispose it skips. This is a sound recall gap (a missed leak, not a false positive), so rather than rush it into this FP-fix PR I'm deferring it to a dedicated exception-edge recall slice — alongside the nested-try gap and the typed/filtered-catch one — to be modelled deliberately and re-validated against the oracle. Corrected the misleading comment in 118d08e and recorded it in the deferred list (docs/notes/real-world-mining.md).
Generated by Claude Code
| // there would falsely flag it (dispose-after-try). In that case skip the edges | ||
| // and lower the try sequentially — a never-disposed local is still caught at | ||
| // end-of-function; only dispose-on-throw is forgone for this shape. | ||
| var edgesSound = trys.Catches.Count == 0 || IsBodyTail(trys); |
There was a problem hiding this comment.
When a try has a typed or filtered catch plus cleanup after it, e.g. try { MayThrow(); } catch (InvalidOperationException) { } r.Dispose();, exceptions not handled by that catch still leave the method and skip the post-try dispose. This condition disables all exception edges for any catch that is not the method tail, so those uncaught exceptional paths are lowered as if the cleanup always runs and dispose-not-called-on-throw leaks are missed; the suppression should only apply when the catch guarantees continuation.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Good point — you're right the guard is over-broad: it suppresses edges for ANY non-tail catch, but a typed/filtered catch lets other exception types propagate, and those paths really do skip the post-try dispose. The precise condition would suppress only for a genuine catch-all (catch {} / catch (Exception), no when filter). This is a sound recall gap (a missed leak, not a false positive) introduced by the swallowing-catch fix, so I'm deferring the precise distinction to the dedicated exception-edge recall slice with the constructor and nested-try gaps — to land deliberately with oracle re-validation. Documented the conservatism in-code (118d08e) and in the deferred list.
Generated by Claude Code
…ecall gaps Codex's re-review surfaced two more dispose-on-throw cases the model misses. Both are sound RECALL gaps (missed leaks, not false positives), deferred to a dedicated exception-edge recall slice (with the nested-try gap) per review decision — no behavior change here, only corrected comments + the deferred list: - StatementMayThrow comment claimed a `new` "is not a leak point" because the created resource is never acquired — incomplete: a throwing constructor DOES leak a PRIOR owned resource whose dispose it skips. Corrected, marked deferred. - edgesSound: noted that suppressing edges for ANY non-tail catch is conservative — a typed/filtered catch lets other exception types propagate (those paths leak); distinguishing catch-all is deferred. Suppressing stays sound. - docs/notes/real-world-mining.md: deferred list now groups nested-try, constructor-throw, and typed/filtered-catch as the recall slice.
…-points, typed catches Lands the deferred exception-edge recall slice from PR #32. Three sound recall gaps (missed leaks, never false positives) in the try exception-edge model close: - Nested compound statements: edges now recurse into if/loop/block bodies and are injected before the nested LEAF statement — where the resource's ownership is exact (after any in-branch dispose). This catches a throw-before-dispose inside a branch while keeping the dispose-before-throw shape silent (DisposeInsideIfWithThrow 'cif' stays silent for this better reason now, not by skipping compounds). The throw continuation is threaded (onThrow) and composes across nested tries (inner finally, then outer, then return); a canEscape flag propagates an enclosing catch-all's swallow so no edge is injected in a region whose throws never reach method exit. - Constructor (new) as a throw point: a throwing ctor skips a PRIOR owned resource's dispose; StatementMayThrow now treats object creation as may-throw. The edge lands before the resource's own acquire (harmless — not yet owned there). - Typed/filtered catches: a non-tail catch no longer blanket-suppresses edges. Only a genuine catch-all (catch {} / catch (Exception), no when-filter) does; a typed catch lets the uncaught exception types propagate past the post-try dispose and really leak. All three match CodeQL's cs/dispose-not-called-on-throw. Validated end-to-end in CI on new samples (nestedLeak, ctorPrior, typedLeak leak; ctorLater stays silent) and on the core IR via the flow_nested_throw ownir fixture (52/52 bridge checks). Every existing try-sample keeps its verdict. Remaining deferred: finally-before-return and switch/do. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
2 participants
Summary by CodeRabbit
Release Notes
New Features
tryexception paths, including dispose/close and configured async disposal patterns.Bug Fixes
Tests
trylowering and multi-exit leak behavior.Documentation