flow: opt-in --body-throw-edges tier — body-level (no-try) dispose-not-called-on-throw

.github/workflows/ci.yml

@@ -719,6 +719,36 @@ jobs:
  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)"
+ - name: Opt-in body-throw-edges tier (--body-throw-edges, P-016 throw firehose)
+ run: |
+ # The opt-in tier: body-level "any call may throw" dispose-not-called-on-throw (CodeQL
+ # cs/dispose-not-called-on-throw parity on the no-try slice). OFF by default — its own
+ # sample file is run in BOTH modes to prove the flag GATES the firehose (running it over
+ # FlowLocalsSample would flood every acquire/use/dispose sample under the flag).
+ # default (flag off): the may-throw case is SILENT (a body-level call is not a leak point).
+ dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+ frontend/roslyn/samples/BodyThrowEdgesSample.cs --flow-locals -o "$RUNNER_TEMP/bte_off.json"
+ off=$(python -m ownlang ownir "$RUNNER_TEMP/bte_off.json" || true)
+ echo "$off"
+ for s in mtbd mtf adc; do
+ if echo "$off" | grep -q "'$s'"; then echo "FAIL: '$s' must be SILENT without --body-throw-edges"; exit 1; fi
+ done
+ # opt-in (flag on): the may-throw WriteByte between acquire and Dispose is a throw point
+ # that skips the Dispose -> 'mtbd' leaks; 'adc' (adjacent dispose, nothing throws between)
+ # stays silent even under the flag (the edge needs an intervening may-throw statement).
+ dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+ frontend/roslyn/samples/BodyThrowEdgesSample.cs --flow-locals --body-throw-edges -o "$RUNNER_TEMP/bte_on.json"
+ on=$(python -m ownlang ownir "$RUNNER_TEMP/bte_on.json" || true)
+ echo "$on"
+ echo "$on" | grep -qE "OWN001.*'mtbd' may not be disposed on every path" \
+ || { echo "FAIL: expected OWN001 on 'mtbd' under --body-throw-edges"; exit 1; }
+ # adc: nothing throws between acquire and dispose. mtf (Codex P2): a may-throw call inside
+ # a finally must not get a synthetic bare exit — the outer finally disposes it. Both silent
+ # even under the flag.
+ for s in adc mtf; do
+ if echo "$on" | grep -q "'$s'"; then echo "FAIL: '$s' must stay silent even under --body-throw-edges"; exit 1; fi
+ done
+ echo "OK: --body-throw-edges gates the body-level dispose-not-called-on-throw firehose (off by default; fires only with an intervening may-throw; finally-internal throws excluded)"
  - name: Coverage summary (--stats)
  run: |
  # --stats prints a flow-locals coverage line to stderr and stamps the same

docs/proposals/P-016-deep-fact-extraction.md

@@ -119,6 +119,18 @@ a CFG-carrying bridge, and the existing core checks real code.
  the most common .NET resource bug, and the first time the core's flow analysis
  bites real code. B2 (`using`/try-finally → scoped release) is the smallest first
  slice; do it before the general case.
+ - **dispose-not-called-on-throw — two tiers (mined: the oracle's CodeQL
+ `cs/dispose-not-called-on-throw` showed up oracle-only on Serilog + Npgsql).**
+ *Tier 1 (default, sound):* exceptional-exit edges inside a `try` already model it;
+ an explicit `throw` with no enclosing try is modelled as a bare method exit (so
+ `acquire; if (bad) throw; dispose;` leaks on the throw path, and a top-level
+ validation throw no longer bails the whole method). FP-free — a throw with no
+ enclosing try definitely exits. *Tier 2 (opt-in `--body-throw-edges`, off by
+ default):* also treat ANY escaping body-level may-throw call/`new` as a throw point
+ (full CodeQL parity on the no-try slice). This is the CA2000 firehose — it flags
+ even harmless `MemoryStream`/`StringWriter` dispose-on-throw — so it stays off the
+ shipped low-FP default; the oracle enables it to measure full recall. Graduating it
+ to default would need a "managed-only, no OS handle" dispose-optional expansion.
 - **B3 — Move / ownership transfer.** `return disposable`, or passing it to a callee
  that consumes it → move / escape (P-005 D5). Intraprocedural, driven by declared
  signatures, not whole-program tracing. *Landed (consume handoff):* a call to a

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -46,11 +46,22 @@
 // flow-analysed vs honestly skipped for an unmodelled construct) and stamp the
 // same counts into the facts JSON. Turns "0 findings" into "clean vs didn't-reach".
 bool reportStats = false;
+// --body-throw-edges (opt-in, P-016 throw tier): also treat an ESCAPING body-level may-throw
+// call/`new` (not only those inside a `try`) as a dispose-not-called-on-throw point — CodeQL
+// cs/dispose-not-called-on-throw parity. OFF by default: it is the CA2000 firehose (flags even
+// harmless MemoryStream/StringWriter dispose-on-throw), so the shipped posture stays low-FP; the
+// oracle turns it on to measure full recall. Read deep in InjectThrowEdge via the static
+// Program.BodyThrowEdges (declared at end of file) rather than threaded through the flow recursion.
+// Reset the static field up front so a flag from a prior IN-PROCESS invocation can't leak into a
+// run that did not request it (the other config — emitEvents/flowLocals/reportStats — are locals,
+// re-initialized each call, so they need no reset; only this static one does). CodeRabbit.
+BodyThrowEdges = false;
 for (int i = 0; i < args.Length; i++)
 {
  if (args[i] == "-o" && i + 1 < args.Length) outPath = args[++i];
  else if (args[i] == "--no-event-leaks") emitEvents = false;
  else if (args[i] == "--flow-locals") flowLocals = true;
+ else if (args[i] == "--body-throw-edges") BodyThrowEdges = true;
  else if (args[i] == "--stats") reportStats = true;
  else rawInputs.Add(args[i]);
 }
@@ -71,6 +82,11 @@
  return 2;
 }
 
+// --body-throw-edges only injects edges during the --flow-locals pass; without it it is a no-op.
+// Warn (non-fatal) rather than fail — it is an additive recall knob layered on flow, not a mode.
+if (BodyThrowEdges && !flowLocals)
+ Console.Error.WriteLine("ownsharp-extract: --body-throw-edges has no effect without --flow-locals");
+
 // A path segment we never scan: build output, VCS, and vendored trees.
 static bool IsSkippedDir(string seg) =>
  seg is "bin" or "obj" or ".git" or ".vs" or "node_modules" or "packages";
@@ -590,11 +606,25 @@
 // LEAF statements only; a COMPOUND statement (if/loop/block) is recursed into so the edge
 // lands before the nested leaf — at the point the resource's ownership is exact (after any
 // in-branch dispose), which is what makes nesting sound rather than a false leak.
-static void InjectThrowEdge(StatementSyntax st, List<object> nodes, List<object>? onThrow)
+static void InjectThrowEdge(StatementSyntax st, List<object> nodes, List<object>? onThrow, bool canEscape)
 {
- if (onThrow is not null && StatementMayThrow(st))
+ // Inside a `try`, `onThrow` is the finally+exit continuation a throw here runs. At the
+ // method-body level `onThrow` is null — by default no edge is injected (the shipped low-FP
+ // posture: a body-level may-throw call is NOT treated as a leak point). The opt-in
+ // --body-throw-edges tier (Program.BodyThrowEdges) lifts that: an ESCAPING body-level
+ // may-throw statement (`canEscape`, so no enclosing catch-all swallows it) gets a synthetic
+ // bare method exit as its continuation, matching CodeQL's cs/dispose-not-called-on-throw on
+ // the no-try slice. A catch-all-suppressed region (`canEscape` false) still injects nothing.
+ // `!IsInsideFinally`: a may-throw statement lexically inside a `finally` is lowered with a null
+ // onThrow too, but a real exception there runs the ENCLOSING cleanup — a bare exit would skip
+ // it and falsely flag a resource the outer finally/using disposes, so synthesize no edge there
+ // (the symmetric guard the explicit-throw path already uses — Codex P2 on the may-throw tier).
+ var cont = onThrow ?? (BodyThrowEdges && canEscape && !IsInsideFinally(st)
+ ? new List<object> { new { op = "return", var = (string?)null, line = LineOf(st) } }
+ : null);
+ if (cont is not null && StatementMayThrow(st))
  nodes.Add(new { op = "if", line = LineOf(st),
- then = new List<object>(onThrow), @else = new List<object>() });
+ then = new List<object>(cont), @else = new List<object>() });
 }
 
 // A statement that can raise an exception part-way through: it makes a call that is not
@@ -664,7 +694,7 @@
  var uv = usingDecl.Declaration.Variables[0];
  var owner = uv.Identifier.Text;
  var exit = new List<object> { new { op = "return", var = (string?)null, line = LineOf(usingDecl) } };
- InjectThrowEdge(usingDecl, nodes, onThrow); // a throw DURING Rent() runs the OUTER path (owner not yet acquired)
+ InjectThrowEdge(usingDecl, nodes, onThrow, canEscape); // a throw DURING Rent() runs the OUTER path (owner not yet acquired)
  nodes.Add(new { op = "acquire", var = owner, line = LineOf(uv) });
  var release = new { op = "release", var = owner, line = LineOf(uv) };
  // The rest of THIS block is the try-body; the implicit using-dispose is its finally — run
@@ -704,7 +734,7 @@
  case BlockSyntax b:
  return LowerFlowStatements(b.Statements, 0, tracked, model, nodes, canEscape, onThrow, onReturn);
  case LocalDeclarationStatementSyntax ld:
- InjectThrowEdge(ld, nodes, onThrow);
+ InjectThrowEdge(ld, nodes, onThrow, canEscape);
  if (ld.UsingKeyword == default)
  foreach (var v in ld.Declaration.Variables)
  {
@@ -723,7 +753,7 @@
  }
  return true;
  case ExpressionStatementSyntax es:
- InjectThrowEdge(es, nodes, onThrow);
+ InjectThrowEdge(es, nodes, onThrow, canEscape);
  EmitFlowExpr(es.Expression, tracked, model, nodes);
  return true;
  case IfStatementSyntax ifs:
@@ -2088,7 +2118,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
@@ -2944,3 +2974,12 @@
 if (outPath is null) Console.WriteLine(json);
 else File.WriteAllText(outPath, json);
 return 0;
+
+// Opt-in recall knob for the flow pass, read deep in InjectThrowEdge (a static field rather than
+// a bool threaded through the whole LowerFlow* recursion). Set once from --body-throw-edges; see
+// that flag's note above. Default false keeps the shipped low-FP posture; the oracle flips it on
+// to measure CodeQL-parity dispose-not-called-on-throw recall on the no-try slice.
+partial class Program
+{
+ internal static bool BodyThrowEdges;
+}

frontend/roslyn/samples/BodyThrowEdgesSample.cs

@@ -0,0 +1,50 @@
+using System.IO;
+
+namespace Own.Samples;
+
+// P-016 throw tier — the OPT-IN `--body-throw-edges` firehose: body-level "any call may throw"
+// dispose-not-called-on-throw, matching CodeQL's cs/dispose-not-called-on-throw on the no-try
+// slice. OFF by default (it is CA2000-noisy — it flags even harmless MemoryStream dispose-on-
+// throw); the oracle enables it to measure full recall without shifting the shipped low-FP
+// default. The leak verdict below holds ONLY under --body-throw-edges; by default this file is
+// silent. Kept in its own file so CI can run it in BOTH modes — running it against the default
+// FlowLocalsSample would flood every acquire/use/dispose sample under the flag.
+public class BodyThrowEdgesSample
+{
+ // acquire; a may-throw call; dispose — no try. Under --body-throw-edges the WriteByte call is
+ // a throw point that skips the Dispose, so `mtbd` leaks on that exceptional path -> OWN001
+ // "may not be disposed on every path". Default (flag off): SILENT — a body-level call is not
+ // treated as a leak point (the shipped posture stays below CA2000).
+ public void MayThrowLeaks()
+ {
+ var mtbd = new MemoryStream();
+ mtbd.WriteByte(1);
+ mtbd.Dispose();
+ }
+
+ // control: NOTHING between acquire and dispose can throw (adjacent), so even under the flag
+ // there is no throw point to skip the Dispose -> SILENT in both modes. Proves the edge needs
+ // an intervening may-throw statement — the flag is not "flag any undisposed-looking local".
+ public void AdjacentDisposeClean()
+ {
+ var adc = new MemoryStream();
+ adc.Dispose();
+ }
+
+ // Codex P2 (may-throw tier): a may-throw call lexically inside a `finally` must NOT get a
+ // synthetic bare exit even under the flag — a real exception there runs the ENCLOSING cleanup.
+ // `mtf` is disposed by the OUTER finally; the inner finally's `mtf.WriteByte(1)` may throw, but
+ // that throw runs the outer `mtf.Dispose()`, so `mtf` is released on every path. Without the
+ // IsInsideFinally guard on the may-throw path, the bare exit would skip that outer release and
+ // falsely flag `mtf` -> it must stay SILENT in BOTH modes (mirrors FlowLocalsSample's tif).
+ public void MayThrowInFinallyClean()
+ {
+ var mtf = new MemoryStream();
+ try
+ {
+ try { }
+ finally { mtf.WriteByte(1); }
+ }
+ finally { mtf.Dispose(); }
+ }
+}

scripts/own-check.sh

@@ -12,8 +12,8 @@
 #
 # Usage:
 # scripts/own-check.sh [--format human|github|msbuild|sarif] [--severity error|warning]
-# [--fail-on-finding] [--legacy] [--stats] [--root <own.net checkout>]
-# [--] <path|file> [more ...]
+# [--fail-on-finding] [--legacy] [--stats] [--body-throw-edges]
+# [--root <own.net checkout>] [--] <path|file> [more ...]
 #
 # Defaults: --format human, --severity error, scans ".", does not fail the shell
 # on findings, --root is the repo this script lives in. --severity picks how a
@@ -37,6 +37,7 @@ severity="error"
 fail_on_finding=0
 legacy=0
 stats=0
+body_throw_edges=0
 paths=()
 
 while [[ $# -gt 0 ]]; do
@@ -53,6 +54,7 @@ while [[ $# -gt 0 ]]; do
  --fail-on-finding) fail_on_finding=1; shift ;;
  --legacy) legacy=1; shift ;;
  --stats) stats=1; shift ;;
+ --body-throw-edges) body_throw_edges=1; shift ;;
  --) shift; while [[ $# -gt 0 ]]; do paths+=("$1"); shift; done ;;
  -h|--help) sed -n '2,30p' "$0"; exit 0 ;;
  *) paths+=("$1"); shift ;;
@@ -78,6 +80,9 @@ trap 'rm -f "$facts"' EXIT
 extractor_args=("${paths[@]}" -o "$facts")
 [[ "$legacy" -eq 0 ]] && extractor_args+=(--flow-locals)
 [[ "$stats" -eq 1 ]] && extractor_args+=(--stats)
+# Opt-in P-016 throw tier: also flag body-level (no-try) dispose-not-called-on-throw — CodeQL
+# cs/dispose-not-called-on-throw parity. CA2000-noisy, so off by default (oracle recall measurement).
+[[ "$body_throw_edges" -eq 1 ]] && extractor_args+=(--body-throw-edges)
 dotnet run --project "$extractor" -- "${extractor_args[@]}" 1>&2
 
 # Stage 2: the one checker produces the verdict at the C# location.