feat: PoC oficially proven?

.github/workflows/ci.yml

@@ -187,6 +187,57 @@ jobs:
             echo "FAIL: a static-handler subscription was wrongly reported"; exit 1
           fi
           echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) at the C# location"
+      - name: Flow-sensitive local IDisposables (--flow-locals, P-016 B0b/B2)
+        run: |
+          # Path-sensitive flow analysis of local IDisposables — bugs the flat D1
+          # detector cannot catch (use-after-dispose, double-dispose, leak-on-path).
+          dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+            frontend/roslyn/samples/FlowLocalsSample.cs --flow-locals -o "$RUNNER_TEMP/flow.json"
+          out=$(python -m ownlang ownir "$RUNNER_TEMP/flow.json" || true)
+          echo "$out"
+          echo "$out" | grep -q "OWN002" || { echo "FAIL: expected OWN002 (use-after-dispose)"; exit 1; }
+          echo "$out" | grep -q "OWN001" || { echo "FAIL: expected OWN001 (leak on a path)"; exit 1; }
+          echo "$out" | grep -q "OWN003" || { echo "FAIL: expected OWN003 (double-dispose)"; exit 1; }
+          # a real Timer leak the flat curated allowlist misses but the semantic path catches:
+          echo "$out" | grep -q "OWN001.*'realTimer'" || { echo "FAIL: expected OWN001 on the leaked Timer"; exit 1; }
+          # the OWN001 wording splits on whether the local was released anywhere: the
+          # Timer is released on no path -> "is never disposed"; LeakOnElse's `leak` is
+          # released on the then-branch only -> "may not be disposed on every path".
+          echo "$out" | grep -qE "'realTimer' is never disposed" \
+            || { echo "FAIL: expected the never-disposed wording for the 0-release Timer"; exit 1; }
+          echo "$out" | grep -qE "'leak' may not be disposed on every path" \
+            || { echo "FAIL: expected the partial-path wording for LeakOnElse"; exit 1; }
+          # dispose-optional (Task) and disposed/loopy/escaping locals must stay silent:
+          for ok in clean looped esc exemptTask; 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, never-vs-every-path wording, dispose-optional exempt, beyond flat)"
+      - name: Escape-via-projection leak — GTM UnitOfWork (--flow-locals, P-016 B0b/B2)
+        run: |
+          # A real GTM leak the flat detector misses: a UnitOfWork (IDisposable) used
+          # ONLY through member access to build a returned DEFERRED IQueryable. The
+          # bare `uow` never escapes, so it stays tracked and is disposed on no path
+          # -> OWN001. Crucially NOT fixable by a naive `using` (the deferred query
+          # would run after dispose) — the `using var`+materialize fix (uowFixed) is
+          # the one that must stay silent.
+          dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \
+            frontend/roslyn/samples/UnitOfWorkFlowSample.cs --flow-locals -o "$RUNNER_TEMP/uow.json"
+          out=$(python -m ownlang ownir "$RUNNER_TEMP/uow.json" || true)
+          echo "$out"
+          # `uow` is released on no path, so the OWN001 reads "is never disposed".
+          echo "$out" | grep -qE "OWN001.*'uow' is never disposed" \
+            || { echo "FAIL: expected OWN001 'is never disposed' on UnitOfWork 'uow'"; exit 1; }
+          echo "$out" | grep -q "UnitOfWorkFlowSample.cs" \
+            || { echo "FAIL: expected the finding at the C# sample location"; exit 1; }
+          # the three correct fixes must stay silent: materialize inside `using`
+          # (uowFixed), and ownership TRANSFERRED to the caller — returned (uowOwned)
+          # or moved out as an argument (uowMoved).
+          for ok in uowFixed uowOwned uowMoved; do
+            if echo "$out" | grep -q "'$ok'"; then
+              echo "FAIL: a correct fix ('$ok') was wrongly reported as a leak"; exit 1
+            fi
+          done
+          echo "OK: escape-via-projection UnitOfWork leak -> OWN001 'never disposed'; materialize + ownership-transfer fixes stay silent"
 
   # The distribution surface (Уровень 1): the own-check.sh orchestrator walks a
   # directory of real C# and prints findings in the host-parseable formats the

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

@@ -1,6 +1,16 @@
 # P-016 — Deep C# fact extraction: CFG + flow lowering
 
-- **Status:** draft (P1 — the "make the core actually bite real C#" track)
+- **Status:** draft (P1 — the "make the core actually bite real C#" track). **B0a
+  done** (direct `Module`, no re-parse). **B0b+B2 spike landed** (experimental
+  `--flow-locals`): real C# → CFG flow facts → core → path-sensitive OWN001/002/003
+  on local IDisposables — proven on `samples/FlowLocalsSample.cs`, run clean over
+  GTM. **GTM findings triaged:** 9 real leaks the flat name-based detector misses
+  (UnitOfWork, `System.Threading.Timer`, StreamReader/Writer) + 14 dispose-optional
+  FPs (Task/DataTable) now excluded by a CA2000-style exemption → 100% precision on
+  the sample. The own-check wrappers (`own-check.ps1`/`.sh`) now **default to
+  `--flow-locals`** (`-Legacy`/`--legacy` opts back to the flat detector); the raw
+  extractor flag stays default-off pending A1 + an `OWNIR_VERSION` bump. Next: A1
+  (loops), escape-via-projection hardening, then full graduation.
 - **Depends on:**
   - [P-014](P-014-semantic-resolution.md) Tier A — the `SemanticModel` (**DONE**).
     The hard prerequisite: typed ownership facts are impossible without binding.

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -35,10 +35,16 @@
 // (e.g. to run only the disposable/pool detectors); it is the first instance of
 // the broader check-selection surface tracked in P-015.
 bool emitEvents = true;
+// --flow-locals (P-016 B0b/B2, EXPERIMENTAL, default off): emit per-method flow
+// facts for non-escaping local IDisposables (acquire/use/release/if/return over a
+// CFG) so the core checks them path-sensitively (OWN001/002/003). Supersedes the
+// flat D1 local-disposable detector when on. Default off keeps the shipped surface.
+bool flowLocals = 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 rawInputs.Add(args[i]);
 }
 
@@ -144,6 +150,114 @@ static bool IsStaticHandler(ExpressionSyntax right, SemanticModel model) =>
     IsHandler(right)
         && model.GetSymbolInfo(right).Symbol is IMethodSymbol { IsStatic: true };
 
+// --- P-016 B0b/B2: flow lowering for local IDisposables (experimental) ---
+
+// A type that implements System.IDisposable (semantic) — the flow lowering tracks
+// locals of such types.
+static bool ImplementsIDisposable(ITypeSymbol? t) =>
+    t is not null
+    && ((t.Name == "IDisposable" && t.ContainingNamespace?.ToString() == "System")
+        || t.AllInterfaces.Any(i => i.Name == "IDisposable"
+                                    && i.ContainingNamespace?.ToString() == "System"));
+
+// Types that implement IDisposable but whose disposal is conventionally OPTIONAL —
+// the .NET guidance / Roslyn CA2000 exempt them: Task/ValueTask only hold a
+// lazily-allocated wait handle, and the System.Data containers' Dispose() is a
+// no-op. The flow detector must not flag an undisposed local of these (this is the
+// curated exemption the flat D1 detector gets for free via IsDisposableType, which
+// is exactly why D1 never flagged Task/DataTable and the semantic path did).
+static bool IsDisposeOptional(ITypeSymbol t)
+{
+    var ns = t.ContainingNamespace?.ToString();
+    return (ns == "System.Threading.Tasks" && t.Name is "Task" or "ValueTask")
+        || (ns == "System.Data" && t.Name is "DataTable" or "DataSet" or "DataView");
+}
+
+static string MethodName(BaseMethodDeclarationSyntax m) => m switch
+{
+    MethodDeclarationSyntax md => md.Identifier.Text,
+    ConstructorDeclarationSyntax => ".ctor",
+    _ => "?",
+};
+
+// Lower a method block to OwnIR flow nodes (acquire/use/release/if/return) for the
+// `tracked` local IDisposables. Returns null on any UNMODELLED statement
+// (loop/try/switch/...): the method is then honestly skipped, not guessed.
+static List<object>? LowerFlowBody(BlockSyntax block, HashSet<string> tracked)
+{
+    var nodes = new List<object>();
+    foreach (var st in block.Statements)
+        if (!LowerFlowStmt(st, tracked, nodes))
+            return null;
+    return nodes;
+}
+
+static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<object> nodes)
+{
+    switch (st)
+    {
+        case BlockSyntax b:
+            foreach (var s2 in b.Statements)
+                if (!LowerFlowStmt(s2, tracked, nodes))
+                    return false;
+            return true;
+        case LocalDeclarationStatementSyntax ld:
+            if (ld.UsingKeyword == default)
+                foreach (var v in ld.Declaration.Variables)
+                    if (tracked.Contains(v.Identifier.Text)
+                        && v.Initializer?.Value is ObjectCreationExpressionSyntax
+                                                or ImplicitObjectCreationExpressionSyntax)
+                        nodes.Add(new { op = "acquire", var = v.Identifier.Text, line = LineOf(v) });
+            return true;
+        case ExpressionStatementSyntax es:
+            EmitFlowExpr(es.Expression, tracked, nodes);
+            return true;
+        case IfStatementSyntax ifs:
+        {
+            var thenNodes = new List<object>();
+            if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes))
+                return false;
+            var elseNodes = new List<object>();
+            if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes))
+                return false;
+            nodes.Add(new { op = "if", line = LineOf(ifs), then = thenNodes, @else = elseNodes });
+            return true;
+        }
+        case UsingStatementSyntax us:
+            // using(...) {body}: the using local is auto-disposed (untracked); still
+            // lower the body so a tracked plain local used inside is seen.
+            return us.Statement is null || LowerFlowStmt(us.Statement, tracked, nodes);
+        case ReturnStatementSyntax rs:
+            // a tracked local never escapes (excluded), so a returned value is not a
+            // tracked resource — model it as a bare return (a CFG exit edge).
+            nodes.Add(new { op = "return", var = (string?)null, line = LineOf(rs) });
+            return true;
+        default:
+            return false;   // unmodelled (loop/try/switch/...) -> bail the method
+    }
+}
+
+static void EmitFlowExpr(ExpressionSyntax expr, HashSet<string> tracked, List<object> nodes)
+{
+    // x.Dispose()/x.Close() on a tracked local -> release.
+    if (expr is InvocationExpressionSyntax inv
+        && inv.Expression is MemberAccessExpressionSyntax ma
+        && ma.Name.Identifier.Text is "Dispose" or "Close"
+        && ma.Expression is IdentifierNameSyntax rid
+        && tracked.Contains(rid.Identifier.Text))
+    {
+        nodes.Add(new { op = "release", var = rid.Identifier.Text, line = LineOf(inv) });
+        return;
+    }
+    // any other reference to a tracked local -> use (once per local in this expr).
+    var used = new SortedSet<string>(StringComparer.Ordinal);
+    foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
+        if (tracked.Contains(idn.Identifier.Text))
+            used.Add(idn.Identifier.Text);
+    foreach (var u in used)
+        nodes.Add(new { op = "use", var = u, line = LineOf(expr) });
+}
+
 // The field name an expression refers to: "_f" for `_f` or `this._f`, else null.
 static string? FieldName(ExpressionSyntax expr) => expr switch
 {
@@ -165,6 +279,8 @@ t is "IDisposable" or "IAsyncDisposable" or "CancellationTokenSource"
     || t.EndsWith("Subscription");
 
 var components = new List<object>();
+// P-016 B0b/B2: per-method flow bodies (only when --flow-locals).
+var flowFunctions = new List<object>();
 
 // Parse every input into a syntax tree first (keeping the file path we report
 // it under), then build ONE compilation over all of them so the SemanticModel
@@ -385,7 +501,9 @@ or ImplicitObjectCreationExpressionSyntax
         // D1 (P-005): a local IDisposable the method `new`s but never disposes,
         // not guarded by `using`, and not handed out (returned / passed as an
         // argument / assigned out) — ownership transfer is ambiguous syntactically
-        // (P-005 D5), so those are conservatively excluded. Per member.
+        // (P-005 D5), so those are conservatively excluded. Per member. Suppressed
+        // under --flow-locals, where the path-sensitive flow detector supersedes it.
+        if (!flowLocals)
         foreach (var member in cls.Members)
         {
             var usingGuarded = new HashSet<string>();
@@ -436,14 +554,59 @@ or ImplicitObjectCreationExpressionSyntax
             }
         }
 
+        // P-016 B0b/B2 (--flow-locals): per-method flow facts for non-escaping local
+        // IDisposables. The core checks them path-sensitively (OWN001/002/003).
+        // Methods with an unmodelled construct (loop/try/switch) are honestly skipped.
+        if (flowLocals)
+            foreach (var method in cls.Members.OfType<BaseMethodDeclarationSyntax>())
+            {
+                if (method.Body is not { } mbody)
+                    continue;
+                var candidates = new HashSet<string>();
+                foreach (var ld in mbody.DescendantNodes().OfType<LocalDeclarationStatementSyntax>())
+                {
+                    if (ld.UsingKeyword != default)
+                        continue;
+                    foreach (var v in ld.Declaration.Variables)
+                        if (v.Initializer is { Value: ObjectCreationExpressionSyntax
+                                                   or ImplicitObjectCreationExpressionSyntax } init
+                            && model.GetTypeInfo(init.Value).Type is { } dt
+                            && ImplementsIDisposable(dt) && !IsDisposeOptional(dt))
+                            candidates.Add(v.Identifier.Text);
+                }
+                if (candidates.Count == 0)
+                    continue;
+                // a local that escapes (returned / passed as arg / assigned out) is
+                // conservatively not tracked — its disposal may be the callee's job.
+                var escapedLocals = new HashSet<string>();
+                foreach (var idn in mbody.DescendantNodes().OfType<IdentifierNameSyntax>())
+                    if (candidates.Contains(idn.Identifier.Text)
+                        && (idn.Parent is ReturnStatementSyntax or ArgumentSyntax
+                            || (idn.Parent is AssignmentExpressionSyntax asg && asg.Right == idn)))
+                        escapedLocals.Add(idn.Identifier.Text);
+                var tracked = new HashSet<string>(candidates);
+                tracked.ExceptWith(escapedLocals);
+                if (tracked.Count == 0)
+                    continue;
+                var fbody = LowerFlowBody(mbody, tracked);
+                if (fbody is null || fbody.Count == 0)
+                    continue;
+                flowFunctions.Add(new
+                {
+                    name = $"{cls.Identifier.Text}.{MethodName(method)}",
+                    file,
+                    body = fbody,
+                });
+            }
+
         if (subs.Count > 0)
             components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs });
     }
 }
 
 // ownir_version stamps the fact-schema vocabulary; the Python core rejects a
 // mismatch loudly (ownlang/ownir.py OWNIR_VERSION) rather than mis-reading facts.
-var facts = new { ownir_version = 0, module = "Extracted", components };
+var facts = new { ownir_version = 0, module = "Extracted", components, functions = flowFunctions };
 var json = JsonSerializer.Serialize(facts, new JsonSerializerOptions { WriteIndented = true });
 
 if (outPath is null) Console.WriteLine(json);

frontend/roslyn/samples/FlowLocalsSample.cs

@@ -0,0 +1,78 @@
+using System;
+using System.IO;
+using System.Threading;
+using System.Threading.Tasks;
+
+// P-016 B0b/B2 (experimental, --flow-locals): path-sensitive flow analysis of
+// local IDisposables. These are bugs the flat D1 detector cannot catch (it only
+// asks "disposed anywhere?"). Distinct local names let CI assert each verdict.
+public class FlowLocalsSample
+{
+    // OWN002: used after Dispose()
+    public void UseAfterDispose()
+    {
+        var uad = new MemoryStream();
+        uad.WriteByte(1);
+        uad.Dispose();
+        uad.WriteByte(2);
+    }
+
+    // OWN001: disposed only on the `then` path -> leaks on the else path
+    public void LeakOnElse(bool c)
+    {
+        var leak = new MemoryStream();
+        if (c)
+        {
+            leak.Dispose();
+        }
+    }
+
+    // OWN003: disposed twice
+    public void DoubleDispose()
+    {
+        var dbl = new MemoryStream();
+        dbl.Dispose();
+        dbl.Dispose();
+    }
+
+    // clean: disposed on all paths -> silent
+    public void Clean()
+    {
+        var clean = new MemoryStream();
+        clean.WriteByte(1);
+        clean.Dispose();
+    }
+
+    // has a loop -> method honestly skipped (no flow finding)
+    public void HasLoop()
+    {
+        var looped = new MemoryStream();
+        for (int i = 0; i < 3; i++) { looped.WriteByte((byte)i); }
+        looped.Dispose();
+    }
+
+    // escapes (returned) -> not tracked
+    public Stream Escapes()
+    {
+        var esc = new MemoryStream();
+        return esc;
+    }
+
+    // dispose-optional: Task is IDisposable but disposing it is unnecessary
+    // (CA2000-exempt) -> silent, not a leak.
+    public void TaskIsExempt()
+    {
+        var exemptTask = new Task(() => { });
+        exemptTask.Start();
+    }
+
+    // real leak: System.Threading.Timer owns an unmanaged timer-queue handle and
+    // MUST be disposed (not dispose-optional) -> OWN001. The flat detector misses
+    // this (Timer is absent from its curated allowlist); the semantic flow path
+    // catches it.
+    public void TimerLeaks()
+    {
+        var realTimer = new Timer(_ => { });
+        realTimer.Change(0, 1000);
+    }
+}