extractor: sound throw-routing for using/finally-only-try bodies (onThrowDefinite)

Follow-up to PR #159's deferred item. An explicit throw inside a
using (existingLocal) body previously had to bail the whole method (the
ThrowStatementSyntax case refuses a non-null onThrow, since a throw inside a
try might be caught), losing detection of unrelated leaks; #159 worked around
it by gating the using-release out when the body threw.

This threads an `onThrowDefinite` flag alongside `onThrow` through the lowering
(LowerFlowStmt / LowerFlowStatements / LowerSwitchSection). 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, a match this lowering does not model). The
throw case then routes the throw through the release continuation when definite,
and still bails otherwise. Throws inside a `finally` keep bailing (IsInsideFinally
guard, unchanged).

Net: the using-local release no longer needs the explicit-throw gate (removed);
finally-only `try` bodies with an explicit throw are now analysed instead of
bailed (sound bonus). try-with-catch is unchanged (still conservative). No
existing golden sample has an explicit throw in a using/finally-only-try body,
so no expected-output changes.

Fixture: using-statement-throw-releases (before.cs: an unrelated leak is still
caught despite a throw in the using body — a direct no-bail regression test;
after.cs clean). Selftests: corpus 30/30, oracle 31/31, ruff clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019846YSZ35c7CdkWQ1qX5gm

Author: claude

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`.

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();
+        }
+    }
+}

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();
+        }
+    }
+}

corpus/real-world/using-statement-throw-releases/case.own

@@ -0,0 +1,18 @@
+// OwnLang model: a method with an explicit throw inside a `using (guard)` body must still
+// report an UNRELATED undisposed local (`conn`). The extractor routes the using-body throw
+// through guard's release (onThrowDefinite) instead of bailing the whole method, so conn's
+// leak is not hidden. Modelled here as conn acquired with no release -> OWN001. (The throw
+// routing and guard's release are extractor-level; the benchmark before.cs/after.cs exercise
+// them end-to-end — see notes.md.)
+module Corpus
+resource Res {
+  acquire create
+  release dispose
+  kind "disposable"
+  emit_type    "Res"
+  emit_acquire "new Res()"
+  emit_release "{0}.Dispose()"
+}
+fn Run(bad: int) {
+  let conn = acquire Res();   // var conn = new Res(); never disposed -> OWN001
+}

corpus/real-world/using-statement-throw-releases/expected-diagnostics.txt

@@ -0,0 +1 @@
+OWN001

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.