diff --git a/corpus/real-world/local-dispose-via-using-statement/notes.md b/corpus/real-world/local-dispose-via-using-statement/notes.md index d5a7de57..11324e8d 100644 --- a/corpus/real-world/local-dispose-via-using-statement/notes.md +++ b/corpus/real-world/local-dispose-via-using-statement/notes.md @@ -34,11 +34,10 @@ Scoped to a `using (identifier)` whose identifier is a **tracked local**. A identifier and is not threaded — that resource is the callee's to dispose and is not a tracked local here. The declaration forms are unchanged. -Also gated on the body having **no explicit escaping `throw`**. Threading a release onto -the throw path requires a non-null `bodyOnThrow`, which makes the lowering's -`ThrowStatementSyntax` case bail the whole method (it refuses a non-null `onThrow` because -a throw inside a `try` might be caught — a distinction a `using` doesn't need but the -lowering can't tell apart without invasive threading). So when the body throws explicitly -we fall through to the plain lowering rather than bail — the method stays analysed (no lost -recall on unrelated locals), at the cost of leaving `r` itself possibly shown as undisposed -on the throw path (no worse than before this fix). Caught by Codex P2 on the first cut. +An explicit `throw` in the body is now handled soundly. The lowering threads an +`onThrowDefinite` flag alongside `onThrow`: for a `using` (no catch) a throw runs the +release then propagates, so the `ThrowStatementSyntax` case routes it through the release +continuation instead of bailing the method. A `try` with a `catch` keeps `onThrowDefinite` +false and still bails (the catch-vs-thrown-type match is not modelled). See the companion +fixture [`using-statement-throw-releases`](../using-statement-throw-releases/notes.md) and +the `onThrowDefinite` contract on `LowerFlowStmt`. diff --git a/corpus/real-world/using-statement-throw-releases/after.cs b/corpus/real-world/using-statement-throw-releases/after.cs new file mode 100644 index 00000000..b54a2b87 --- /dev/null +++ b/corpus/real-world/using-statement-throw-releases/after.cs @@ -0,0 +1,21 @@ +using System; + +sealed class Guard : IDisposable { public void Dispose() { } } +sealed class Res : IDisposable { public void Work() { } public void Dispose() { } } + +static class Demo +{ + // FIX: `conn` is disposed (using-declared). The `using (guard)` body still throws, and the + // extractor routes that throw through guard's release — the method stays analysed (the throw + // does not bail it) and is clean: `guard` released on every path, `conn` auto-disposed. + public static void Run(bool bad) + { + var guard = new Guard(); + using var conn = new Res(); + using (guard) + { + if (bad) throw new InvalidOperationException(); + conn.Work(); + } + } +} diff --git a/corpus/real-world/using-statement-throw-releases/before.cs b/corpus/real-world/using-statement-throw-releases/before.cs new file mode 100644 index 00000000..acc415dd --- /dev/null +++ b/corpus/real-world/using-statement-throw-releases/before.cs @@ -0,0 +1,22 @@ +using System; + +sealed class Guard : IDisposable { public void Dispose() { } } +sealed class Res : IDisposable { public void Work() { } public void Dispose() { } } + +static class Demo +{ + // The `using (guard)` body contains an explicit `throw`. The extractor must NOT bail the + // whole method on that throw (which would hide the UNRELATED `conn` leak) — it routes the + // throw through the using's release instead (onThrowDefinite). So `conn`, never disposed + // on any path, is still caught → OWN001; `guard` is released on every path and is silent. + public static void Run(bool bad) + { + var guard = new Guard(); + var conn = new Res(); // BUG: never disposed -> OWN001 + using (guard) + { + if (bad) throw new InvalidOperationException(); + conn.Work(); + } + } +} diff --git a/corpus/real-world/using-statement-throw-releases/case.own b/corpus/real-world/using-statement-throw-releases/case.own new file mode 100644 index 00000000..336c2699 --- /dev/null +++ b/corpus/real-world/using-statement-throw-releases/case.own @@ -0,0 +1,29 @@ +// OwnLang model: a method with an explicit throw inside a `using (guard)` body must still +// report an UNRELATED undisposed local (`conn`). `guard` is acquired and released (the using's +// scope-exit dispose); `conn` is acquired and never released -> OWN001. The throw-routing +// itself — release on the throw path, no whole-method bail — is an EXTRACTOR-level concern +// (the onThrowDefinite flag) exercised end-to-end by before.cs/after.cs in the dotnet +// benchmark; this pure-OwnLang reduction pins the ownership OUTCOME the extractor must produce: +// guard balanced, conn leaked. See notes.md. +module Corpus +resource Guard { + acquire create + release dispose + kind "disposable" + emit_type "Guard" + emit_acquire "new Guard()" + emit_release "{0}.Dispose()" +} +resource Res { + acquire create + release dispose + kind "disposable" + emit_type "Res" + emit_acquire "new Res()" + emit_release "{0}.Dispose()" +} +fn Run(bad: int) { + let guard = acquire Guard(); // var guard = new Guard(); + let conn = acquire Res(); // var conn = new Res(); never disposed -> OWN001 + release guard; // using (guard) { ... } disposes guard on every exit +} diff --git a/corpus/real-world/using-statement-throw-releases/expected-diagnostics.txt b/corpus/real-world/using-statement-throw-releases/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/real-world/using-statement-throw-releases/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/real-world/using-statement-throw-releases/notes.md b/corpus/real-world/using-statement-throw-releases/notes.md new file mode 100644 index 00000000..168bdad5 --- /dev/null +++ b/corpus/real-world/using-statement-throw-releases/notes.md @@ -0,0 +1,37 @@ +# using-statement-throw-releases + +The sound handling of an **explicit `throw` inside a `using (existingLocal)` body** — the +follow-up to [`local-dispose-via-using-statement`](../local-dispose-via-using-statement/notes.md), +which first deferred this case (Codex P2 on PR #159). + +When the `using`-local release was threaded as a non-null `bodyOnThrow`, the +`ThrowStatementSyntax` lowering bailed the **whole method** (it refuses a non-null `onThrow` +because a throw inside a `try` might be caught). That lost detection of UNRELATED leaks in +any method with such a body. This fixture pins the fixed behaviour. + +- **before.cs** — an unrelated local `conn` is never disposed → `OWN001`. Crucially, the + `using (guard)` body contains `if (bad) throw …;`. The bug is only caught if the throw + does **not** bail the method — so this fixture is a direct regression test for the + no-bail fix. `guard` is released on every path (normal, throw, return) and stays silent. +- **after.cs** — `conn` is `using`-declared (auto-disposed); the body still throws, and the + method stays analysed and **clean**. + +## Recognition rule + +`LowerFlowStmt`/`LowerFlowStatements`/`LowerSwitchSection` thread an `onThrowDefinite` flag +beside `onThrow`. It is true when a throw that runs `onThrow` **definitely** leaves the +method uncaught — a `using` or a finally-only `try` (neither has a catch) — and false for a +`try` with any `catch` (the throw may be caught). The `ThrowStatementSyntax` case: + +- `onThrow is null` (method level) → bare exit, as before; +- `onThrow` non-null **and** `onThrowDefinite` → route the throw through `onThrow` (the + release continuation, ending in exit), so the cleanup's resource is released on the throw + path and the method stays analysed; +- `onThrow` non-null and **not** definite (try-with-catch) → still bail. + +## Honesty caveat + +The definite routing covers `using` statements and finally-only `try`s. A `try` with a +`catch` still bails an explicit throw in its body — modelling that soundly needs matching +the thrown type against each catch clause, which the lowering does not do. That is the same +conservative posture as before; this change only *adds* the provably-uncaught cases. diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs index dd29aa29..bc4baca3 100644 --- a/frontend/roslyn/OwnSharp.Extractor/Program.cs +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -1307,7 +1307,8 @@ cc.Filter is null // statement in turn, so non-pooled `using` locals and every existing shape are unaffected. static bool LowerFlowStatements(IReadOnlyList stmts, int start, HashSet tracked, SemanticModel model, List nodes, - bool canEscape, List? onThrow, List? onReturn) + bool canEscape, List? onThrow, List? onReturn, + bool onThrowDefinite = false) { for (var i = start; i < stmts.Count; i++) { @@ -1329,17 +1330,22 @@ static bool LowerFlowStatements(IReadOnlyList stmts, int start, var restOnReturn = new List { release }; restOnReturn.AddRange(onReturn ?? exit); List? restOnThrow = null; + // The implicit using-dispose has no catch, so a throw running it then propagates; + // it reaches method exit uncaught iff the enclosing path does (true at body level + // where onThrow is null). See the `onThrowDefinite` contract on the throw case. + bool restDefinite = onThrow is null || onThrowDefinite; if (canEscape) { restOnThrow = new List { release }; restOnThrow.AddRange(onThrow ?? exit); } - if (!LowerFlowStatements(stmts, i + 1, tracked, model, nodes, canEscape, restOnThrow, restOnReturn)) + if (!LowerFlowStatements(stmts, i + 1, tracked, model, nodes, canEscape, restOnThrow, restOnReturn, + onThrowDefinite: restDefinite)) return false; nodes.Add(release); // normal completion (no return) disposes at scope exit too return true; } - if (!LowerFlowStmt(st, tracked, model, nodes, canEscape, onThrow, onReturn)) + if (!LowerFlowStmt(st, tracked, model, nodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; } return true; @@ -1351,15 +1357,20 @@ static bool LowerFlowStatements(IReadOnlyList stmts, int start, // (method level, or a region an enclosing catch-all swallows). `onReturn`: the continuation // a `return` here runs FIRST — the enclosing `finally`(s), then the exit — so a resource a // finally disposes is released on the return path; null = a bare return (outside any try). +// `onThrowDefinite`: when `onThrow` is non-null, does a throw that runs it DEFINITELY leave +// the method (no enclosing `catch` can intercept and resume normal flow)? True for a `using` +// or a finally-only `try` (neither has a catch); false for a `try` with any `catch` (the +// throw may be caught). An explicit `throw` routes through `onThrow` only when this holds — +// otherwise it bails (the catch-match is not modelled). Irrelevant when `onThrow` is null. // Defaults are the method-body context: throws escape, nothing is injected, returns are bare. static bool LowerFlowStmt(StatementSyntax st, HashSet tracked, SemanticModel model, List nodes, bool canEscape = true, List? onThrow = null, - List? onReturn = null) + List? onReturn = null, bool onThrowDefinite = false) { switch (st) { case BlockSyntax b: - return LowerFlowStatements(b.Statements, 0, tracked, model, nodes, canEscape, onThrow, onReturn); + return LowerFlowStatements(b.Statements, 0, tracked, model, nodes, canEscape, onThrow, onReturn, onThrowDefinite); case LocalDeclarationStatementSyntax ld: InjectThrowEdge(ld, nodes, onThrow, canEscape); if (ld.UsingKeyword == default) @@ -1427,10 +1438,10 @@ or ImplicitObjectCreationExpressionSyntax case IfStatementSyntax ifs: { var thenNodes = new List(); - if (!LowerFlowStmt(ifs.Statement, tracked, model, thenNodes, canEscape, onThrow, onReturn)) + if (!LowerFlowStmt(ifs.Statement, tracked, model, thenNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; var elseNodes = new List(); - if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, model, elseNodes, canEscape, onThrow, onReturn)) + if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, model, elseNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; nodes.Add(new { op = "if", line = LineOf(ifs), then = thenNodes, @else = elseNodes }); return true; @@ -1454,13 +1465,17 @@ or ImplicitObjectCreationExpressionSyntax var bodyOnReturn = new List { release }; bodyOnReturn.AddRange(onReturn ?? exit); List? bodyOnThrow = null; + // A using has no catch: a throw runs the release then propagates, reaching + // method exit uncaught iff the enclosing path does (true at body level). + bool bodyDefinite = onThrow is null || onThrowDefinite; if (canEscape) { bodyOnThrow = new List { release }; bodyOnThrow.AddRange(onThrow ?? exit); } if (us.Statement is not null - && !LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, bodyOnThrow, bodyOnReturn)) + && !LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, bodyOnThrow, bodyOnReturn, + onThrowDefinite: bodyDefinite)) return false; nodes.Add(release); // normal completion disposes at scope exit too return true; @@ -1475,21 +1490,14 @@ or ImplicitObjectCreationExpressionSyntax // (var x = ...)` declaration form needs nothing: `x` is auto-disposed and never // tracked as a leak candidate. // - // GATED on the body having no EXPLICIT escaping `throw`: threading a non-null - // bodyOnThrow makes the `ThrowStatementSyntax` case bail the whole method (it - // refuses a non-null onThrow — a throw inside a `try` might be caught, which a bare - // exit can't model). A `using` has no catch, so routing a throw through the release - // IS sound, but the lowering can't tell using-onThrow from try-onThrow without - // invasive threading. Rather than regress recall (bailing every method with an - // explicit throw in such a body, losing UNRELATED leaks too — Codex P2), fall - // through to the plain body lowering when the body throws explicitly; that keeps the - // method analysed (status quo for this rare expression form — `r` itself may still - // show as undisposed on the throw path, no worse than before this fix). + // An EXPLICIT throw in the body is handled soundly: the body is lowered with + // `onThrowDefinite` set (a using has no catch, so a throw runs the release then + // propagates — definite iff the enclosing path is), and the `ThrowStatementSyntax` + // case routes the throw through that release continuation instead of bailing the + // whole method. So `var leaked = new ...; using (r) { if (bad) throw; }` still + // reports `leaked` and releases `r` on every exit (Codex P2). if (us.Expression is IdentifierNameSyntax usingId - && tracked.Contains(usingId.Identifier.Text) - && !(us.Statement?.DescendantNodes(n => - n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) - .OfType().Any() ?? false)) + && tracked.Contains(usingId.Identifier.Text)) { var owner = usingId.Identifier.Text; var exit = new List { new { op = "return", var = (string?)null, line = LineOf(us) } }; @@ -1497,18 +1505,20 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) var bodyOnReturn = new List { release }; bodyOnReturn.AddRange(onReturn ?? exit); List? bodyOnThrow = null; + bool bodyDefinite = onThrow is null || onThrowDefinite; if (canEscape) { bodyOnThrow = new List { release }; bodyOnThrow.AddRange(onThrow ?? exit); } if (us.Statement is not null - && !LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, bodyOnThrow, bodyOnReturn)) + && !LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, bodyOnThrow, bodyOnReturn, + onThrowDefinite: bodyDefinite)) return false; nodes.Add(release); // normal completion disposes at scope exit return true; } - return us.Statement is null || LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, onThrow, onReturn); + return us.Statement is null || LowerFlowStmt(us.Statement, tracked, model, nodes, canEscape, onThrow, onReturn, onThrowDefinite); } case ReturnStatementSyntax rs: { @@ -1567,7 +1577,7 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // double-release). The condition is opaque (we model control flow, not // values). If the body has an unmodelled statement, bail the method. var bodyNodes = new List(); - if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn)) + if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; nodes.Add(new { op = "while", line = LineOf(ws), body = bodyNodes }); return true; @@ -1580,7 +1590,7 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // body as a `while` is sound. (`for` and `do` are handled below; `do` runs 1+ // times, so it is desugared rather than modelled as a bare 0+-trip `while`.) var bodyNodes = new List(); - if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn)) + if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; nodes.Add(new { op = "while", line = LineOf(fes), body = bodyNodes }); return true; @@ -1594,7 +1604,7 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // method-body local, so it is never a tracked candidate — no soundness // concern, just a separate (rare) recall gap. var bodyNodes = new List(); - if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn)) + if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; nodes.Add(new { op = "while", line = LineOf(fors), body = bodyNodes }); return true; @@ -1644,6 +1654,12 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) bodyOnThrow.AddRange(onThrow ?? new List { new { op = "return", var = (string?)null, line = LineOf(trys) } }); } + // Is a throw in the body DEFINITELY uncaught (so an explicit throw may route through + // `bodyOnThrow` instead of bailing)? Only a finally-only try (no catches): the throw + // runs the finally then propagates, reaching method exit iff the enclosing path does. + // ANY catch makes it false — the throw might be caught, which this lowering can't + // match against the thrown type, so an explicit throw there keeps bailing. + bool bodyOnThrowDefinite = trys.Catches.Count == 0 && (onThrow is null || onThrowDefinite); // A `return` inside the body runs THIS finally, then the enclosing return path // (its finallys), then exits — independent of catches (a `return` is never caught, // unlike a throw), so it is threaded even where the throw edges are suppressed. The @@ -1652,7 +1668,8 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) var bodyOnReturn = new List(finallyNodes); bodyOnReturn.AddRange(onReturn ?? new List { new { op = "return", var = (string?)null, line = LineOf(trys) } }); - if (!LowerFlowStatements(trys.Block.Statements, 0, tracked, model, nodes, bodyCanEscape, bodyOnThrow, bodyOnReturn)) + if (!LowerFlowStatements(trys.Block.Statements, 0, tracked, model, nodes, bodyCanEscape, bodyOnThrow, bodyOnReturn, + onThrowDefinite: bodyOnThrowDefinite)) return false; nodes.AddRange(finallyNodes); // normal completion runs the finally return true; @@ -1665,10 +1682,10 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // only in the body but acquired before the loop would falsely leak on the phantom // 0-trip path. Bail (like the loops) if the body has an unmodelled statement. if (dos.Statement is null - || !LowerFlowStmt(dos.Statement, tracked, model, nodes, canEscape, onThrow, onReturn)) + || !LowerFlowStmt(dos.Statement, tracked, model, nodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; var bodyNodes = new List(); - if (!LowerFlowStmt(dos.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn)) + if (!LowerFlowStmt(dos.Statement, tracked, model, bodyNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; nodes.Add(new { op = "while", line = LineOf(dos), body = bodyNodes }); return true; @@ -1686,7 +1703,7 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) foreach (var section in sw.Sections) { var secNodes = new List(); - if (!LowerSwitchSection(section, tracked, model, secNodes, canEscape, onThrow, onReturn)) + if (!LowerSwitchSection(section, tracked, model, secNodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; if (section.Labels.Any(l => l is DefaultSwitchLabelSyntax)) defaultNodes = secNodes; @@ -1732,10 +1749,24 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // analysed instead of skipped, lighting up every detector on the rest of its body. // ...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)) + if (!IsInsideFinally(thr) && canEscape) { - nodes.Add(new { op = "return", var = (string?)null, line = LineOf(thr) }); - return true; + if (onThrow is null) + { + nodes.Add(new { op = "return", var = (string?)null, line = LineOf(thr) }); + return true; + } + // A non-null onThrow that DEFINITELY reaches method exit uncaught (a `using` or a + // finally-only `try` — no catch can intercept) routes the throw through its + // cleanup continuation (release(s) then exit), so the resource the cleanup + // disposes is released on the throw path instead of the whole method bailing. A + // catchable onThrow (try-with-catch) leaves onThrowDefinite false and still bails: + // the catch-vs-thrown-type match is not modelled, so guessing would be unsound. + if (onThrowDefinite) + { + nodes.AddRange(onThrow); + return true; + } } return false; default: @@ -1751,13 +1782,14 @@ n is not (AnonymousFunctionExpressionSyntax or LocalFunctionStatementSyntax)) // the unmodelled default and conservatively skips the whole method. static bool LowerSwitchSection(SwitchSectionSyntax section, HashSet tracked, SemanticModel model, List nodes, bool canEscape, - List? onThrow, List? onReturn) + List? onThrow, List? onReturn, + bool onThrowDefinite = false) { foreach (var stmt in section.Statements) { if (stmt is BreakStatementSyntax) break; - if (!LowerFlowStmt(stmt, tracked, model, nodes, canEscape, onThrow, onReturn)) + if (!LowerFlowStmt(stmt, tracked, model, nodes, canEscape, onThrow, onReturn, onThrowDefinite)) return false; } return true;