flow: keep throw inside a finally bailing — fix false leak past an outer finally (Codex P2)

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) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED

Author: claude

.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)"

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;

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