flow: model explicit throw as an abnormal exit (body-level dispose-not-called-on-throw)

.github/workflows/ci.yml

@@ -639,6 +639,16 @@ jobs:
             || { echo "FAIL: expected OWN001 on the undisposed local in a do-while loop"; exit 1; }
           echo "$out" | grep -qE "OWN001.*'swLeak'" \
             || { echo "FAIL: expected OWN001 on the switch default-branch leak"; exit 1; }
+          # body-level explicit `throw` (no enclosing try) — these methods used to bail the flow
+          # pass entirely (a `throw` hit the unmodelled default). Now an explicit throw is an
+          # abnormal exit, so they are analysed: a top-level validation throw no longer HIDES a
+          # later undisposed local ('vtl', never disposed), and a Dispose skipped by a `throw`
+          # on the guard path leaks on that path ('dotNoTry', partial). Closes the no-try slice
+          # of cs/dispose-not-called-on-throw + un-bails every validation-throw-guarded method.
+          echo "$out" | grep -qE "OWN001.*'vtl' is never disposed" \
+            || { echo "FAIL: expected OWN001 on the local hidden behind a top-level validation throw"; exit 1; }
+          echo "$out" | grep -qE "OWN001.*'dotNoTry' may not be disposed on every path" \
+            || { echo "FAIL: expected OWN001 on the body-level dispose-not-called-on-throw (no try)"; exit 1; }
           # closure-capture escape (precision): a SemaphoreSlim captured by a returned async
           # lambda outlives the method, so it cannot be disposed at method scope -> escaped ->
           # silent ('captured'). A SemaphoreSlim NOT captured and never disposed STILL leaks ->
@@ -699,7 +709,13 @@ jobs:
           # silenced (Codex/CodeRabbit P1; benchmark memorypool-double-dispose parity).
           echo "$out" | grep -qE "OWN002.*'pooled'" \
             || { echo "FAIL: a MemoryPool owner's .Memory used after Dispose must still trip OWN002"; exit 1; }
-          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; do
+          # 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).
+          # 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 @@
     && 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
@@ -911,7 +929,8 @@
             // mutually-exclusive branches: `if(*){ s1 } else { if(*){ s2 } else { … } }` — one
             // per section, value-opaque (we model control flow, not the matched value). A
             // trailing `break` ends a section (stripped); a section doing anything the model
-            // can't place here (a nested `break`, `goto case`, `throw`) bails the method.
+            // can't place here (a nested `break`, `goto case`) bails the method. A bare `throw`
+            // in a section IS modelled now (an abnormal exit) when no enclosing try wraps it.
             List<object>? defaultNodes = null;
             var cases = new List<List<object>>();
             foreach (var section in sw.Sections)
@@ -946,8 +965,33 @@
             nodes.AddRange(chain);
             return true;
         }
+        case ThrowStatementSyntax thr:
+            // An explicit `throw` is an abnormal method exit: control leaves the method
+            // WITHOUT running the statements below it, so a resource owned here and disposed
+            // only LATER leaks on the throw path — dispose-not-called-on-throw with NO
+            // enclosing `try`. Modelled at the method-body level only: `onThrow is null` AND
+            // the throw escapes (`canEscape`) means no enclosing try would run a `finally` or
+            // catch it, so it is a bare CFG exit where a still-owned resource leaks — the same
+            // synthetic exit the injected may-throw edges use. INSIDE a try an explicit throw
+            // may run a finally or be caught (typed / catch-all); modelling that soundly needs
+            // the thrown-type-vs-catch match, which is not threaded here, so an explicit throw
+            // there keeps bailing (return false) exactly as before — no new false escape past a
+            // catch. (`throw;` rethrow only appears in a catch body, never lowered, so this is
+            // 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.
+            // ...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;
+            }
+            return false;
         default:
-            return false;   // unmodelled (goto/labeled/throw/...) -> bail the method
+            // unmodelled (goto / labeled / local function / lock / fixed / a `throw` INSIDE a
+            // try) -> bail the method, honestly skipping rather than guessing.
+            return false;
     }
 }
 
@@ -2044,7 +2088,7 @@
     .Split(Path.PathSeparator, StringSplitOptions.RemoveEmptyEntries)
     .Where(p => p.EndsWith(".dll", StringComparison.OrdinalIgnoreCase))
     .ToList();
 var refNames = new HashSet<string>(tpa.Select(Path.GetFileName), StringComparer.OrdinalIgnoreCase);
 var references = tpa.Select(p => (MetadataReference)MetadataReference.CreateFromFile(p)).ToList();
 // P-004 WPF profile: widen the reference set with assemblies named by the
 // OWN_EXTRA_REF_DIRS env var (colon-separated dirs) — e.g. the WindowsDesktop ref

frontend/roslyn/samples/FlowLocalsSample.cs

@@ -272,6 +272,71 @@
         lamPrior.Dispose();
     }
 
+    // ─── body-level explicit `throw` (no enclosing try) ──────────────────────────────────
+    // An explicit `throw` used to make the flow pass bail the WHOLE method (it hit the
+    // unmodelled `default`). It is now an abnormal method exit, so these methods are analysed
+    // — closing the no-try slice of CodeQL's cs/dispose-not-called-on-throw and, more broadly,
+    // un-bailing every method guarded by a top-level validation throw.
+
+    // recall (the un-bail win): a top-level validation `throw` no longer bails the method, so
+    // `vtl` — acquired after the guard and never disposed — now leaks (OWN001, "is never
+    // disposed"). Before, the throw made the whole method invisible to every detector.
+    public void ValidatedThenLeaks(object arg)
+    {
+        if (arg is null) throw new ArgumentNullException(nameof(arg));
+        var vtl = new MemoryStream();
+        vtl.WriteByte(1);
+    }
+
+    // recall (the body-level dispose-on-throw the in-try model missed): `dotNoTry` is disposed
+    // at the end, but the `throw` on the guard path leaves the method first and skips that
+    // Dispose -> it leaks on the throw path. Disposed on the fall-through path, never on the
+    // throw path -> OWN001 "may not be disposed on every path". The fix is `using`.
+    public void ThrowAfterAcquireLeaks(bool bad)
+    {
+        var dotNoTry = new MemoryStream();
+        if (bad) throw new InvalidOperationException();
+        dotNoTry.Dispose();
+    }
+
+    // NOT a leak (the throw-exit is placed where ownership is exact, not blanket): the Dispose
+    // runs BEFORE the `throw`, so `tdClean` is already released at the abnormal exit -> nothing
+    // owned there -> silent. Proves "the method contains a throw" alone never leaks.
+    public void ThrowAfterDisposeClean()
+    {
+        var tdClean = new MemoryStream();
+        tdClean.WriteByte(1);
+        tdClean.Dispose();
+        throw new InvalidOperationException();
+    }
+
+    // NOT a leak (the un-bail must not over-flag): the same top-level validation `throw`, but
+    // `vtc` is acquired after it AND disposed -> analysed (no longer bailed) and balanced on
+    // every real path -> silent. The guard throw exits before the acquire, owning nothing.
+    public void ValidatedThenClean(object arg)
+    {
+        if (arg is null) throw new ArgumentNullException(nameof(arg));
+        var vtc = new MemoryStream();
+        vtc.WriteByte(1);
+        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