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

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,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
+}

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.