P-016: extractor lowers while/foreach to flow facts (A1 reaches real C#)

.github/workflows/ci.yml

@@ -207,11 +207,19 @@ jobs:
             || { 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
+          # P-016 A1 reached the frontend: `while`/`foreach` bodies are now lowered
+          # (not skipped), so a per-iteration leak in one is caught.
+          echo "$out" | grep -qE "OWN001.*'whileLeak' is never disposed" \
+            || { echo "FAIL: expected OWN001 on the undisposed local in a while loop"; exit 1; }
+          echo "$out" | grep -qE "OWN001.*'foreachLeak'" \
+            || { echo "FAIL: expected OWN001 on the undisposed local in a foreach loop"; exit 1; }
+          # dispose-optional (Task), disposed/escaping locals, a `for` loop (still
+          # skipped: `looped`), and a balanced acquire+dispose in a loop (`whileClean`)
+          # must stay silent:
+          for ok in clean looped esc exemptTask whileClean; 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)"
+          echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach, 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

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

@@ -13,9 +13,14 @@
   support) landed:** `while` is analysed with a worklist+fixpoint over the back-edge
   (cross-iteration leak / use-after-release / double-release), replacing the single
   topological pass; `for`/`loop`/async stay `OWN020`. Pinned by `tests/test_loops.py`
-  + gallery `10_leak_in_loop.own`. Next: have the flow extractor lower `while` to
-  back-edge flow facts (it currently bails on loop bodies), escape-via-projection
-  hardening, then full graduation.
+  + gallery `10_leak_in_loop.own`. **A1 reached the frontend:** the flow extractor now
+  lowers `while` and `foreach` bodies to a `while` back-edge flow op (0+ iterations,
+  opaque condition) instead of skipping the whole method — so loopy C# is analysed
+  end-to-end (cross-iteration leak/double-release through the bridge). `for` (can
+  declare a resource in its initializer) and `do` (runs 1+ times) still bail honestly.
+  Pinned by `samples/FlowLocalsSample.cs` (`whileLeak`/`foreachLeak`/`whileClean`) +
+  `tests/fixtures/ownir/flow_while.facts.json`. Next: `for`/`foreach`-with-disposable-
+  iterator lowering, 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.
@@ -81,9 +86,12 @@ a CFG-carrying bridge, and the existing core checks real code.
   second pass on the converged in-states (never during fixpoint iteration). Removed
   the `OWN020` "loops" clause for `while` (`for`/`loop`/async still `OWN020`). Fully
   independent of the frontend; pinned by `tests/test_loops.py` (cross-iteration
-  OWN001/003/009) + gallery `10_leak_in_loop.own`. Remaining: the flow **extractor**
-  still bails on loop bodies — lowering `while` to back-edge flow facts is a Track-B
-  follow-on (so loopy C# methods stop being honestly skipped).
+  OWN001/003/009) + gallery `10_leak_in_loop.own`. **Frontend follow-on landed:** the
+  flow extractor (`LowerFlowStmt`) now lowers `while` and `foreach` bodies to a `while`
+  back-edge flow op (both are the 0+-iteration, opaque-condition shape), and the bridge
+  (`ownir._lower_flow`) maps it to the core `While` node — so loopy C# is analysed
+  end-to-end instead of the whole method being skipped. `for`/`do` still bail honestly.
+  Pinned by `FlowLocalsSample.cs` + `tests/fixtures/ownir/flow_while.facts.json`.
 
 ### Track B — frontend depth (needs the `SemanticModel`, now present)
 

frontend/roslyn/OwnSharp.Extractor/Program.cs

@@ -232,8 +232,34 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
             // 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;
+        case WhileStatementSyntax ws:
+        {
+            // P-016 A1 reached the frontend: a `while` lowers to a `while` flow op
+            // (a body that runs 0+ times with a back-edge); the core analyses it with
+            // its worklist fixpoint (cross-iteration leak / use-after-release /
+            // double-release). The condition is opaque (we model control flow, not
+            // values). If the body has an unmodelled statement, bail the method.
+            var bodyNodes = new List<object>();
+            if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes))
+                return false;
+            nodes.Add(new { op = "while", line = LineOf(ws), body = bodyNodes });
+            return true;
+        }
+        case ForEachStatementSyntax fes:
+        {
+            // `foreach` runs its body 0+ times over an (opaque) collection — the same
+            // ownership shape as `while`. The loop variable is never a `new`'d
+            // candidate and the hidden enumerator is auto-disposed, so modelling the
+            // body as a `while` is sound. (`for`/`do` stay unmodelled below: `for`
+            // can declare a resource in its initializer and `do` runs 1+ times.)
+            var bodyNodes = new List<object>();
+            if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, bodyNodes))
+                return false;
+            nodes.Add(new { op = "while", line = LineOf(fes), body = bodyNodes });
+            return true;
+        }
         default:
-            return false;   // unmodelled (loop/try/switch/...) -> bail the method
+            return false;   // unmodelled (for/do/try/switch/...) -> bail the method
     }
 }
 

frontend/roslyn/samples/FlowLocalsSample.cs

@@ -11,7 +11,7 @@
     // OWN002: used after Dispose()
     public void UseAfterDispose()
     {
         var uad = new MemoryStream();
         uad.WriteByte(1);
         uad.Dispose();
         uad.WriteByte(2);
@@ -20,7 +20,7 @@
     // 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();
@@ -30,7 +30,7 @@
     // OWN003: disposed twice
     public void DoubleDispose()
     {
         var dbl = new MemoryStream();
         dbl.Dispose();
         dbl.Dispose();
     }
@@ -43,14 +43,52 @@
         clean.Dispose();
     }
 
-    // has a loop -> method honestly skipped (no flow finding)
+    // has a `for` loop (not yet lowered: `for` can declare a resource in its
+    // initializer) -> method honestly skipped, no flow finding. `while`/`foreach`
+    // ARE lowered now (see below).
     public void HasLoop()
     {
         var looped = new MemoryStream();
         for (int i = 0; i < 3; i++) { looped.WriteByte((byte)i); }
         looped.Dispose();
     }
 
+    // P-016 A1 reached the frontend: a `while` body is lowered to a back-edge the
+    // core's worklist fixpoint analyses. A stream acquired each iteration and never
+    // disposed leaks -> OWN001 (per iteration).
+    public void WhileLeak(int n)
+    {
+        while (n > 0)
+        {
+            var whileLeak = new MemoryStream();
+            whileLeak.WriteByte(1);
+            n = n - 1;
+        }
+    }
+
+    // `foreach` is the same 0+-iteration shape -> the undisposed local leaks too.
+    public void ForeachLeak(int[] items)
+    {
+        foreach (var it in items)
+        {
+            var foreachLeak = new MemoryStream();
+            foreachLeak.WriteByte((byte)it);
+        }
+    }
+
+    // acquire + dispose within the loop body is balanced -> silent (no false
+    // positive now that loops are analysed rather than skipped).
+    public void WhileClean(int n)
+    {
+        while (n > 0)
+        {
+            var whileClean = new MemoryStream();
+            whileClean.WriteByte(1);
+            whileClean.Dispose();
+            n = n - 1;
+        }
+    }
+
     // escapes (returned) -> not tracked
     public Stream Escapes()
     {
@@ -72,7 +110,7 @@
     // catches it.
     public void TimerLeaks()
     {
         var realTimer = new Timer(_ => { });
         realTimer.Change(0, 1000);
     }
 }

ownlang/ownir.py

@@ -86,6 +86,7 @@
     Return,
     Stmt,
     Use,
+    While,
 )
 from .di import LIFETIMES as DI_LIFETIMES
 from .di import Service, find_captive_dependencies
@@ -407,9 +408,9 @@ def to_module(facts: dict[str, Any]) -> tuple[Module, dict[str, dict[str, Any]]]
 
 def _released_vars(nodes: list[Any]) -> set[str]:
     """The set of local names with at least one `release` op anywhere in a flow body
-    (recursing into `if` branches). Used to word an OWN001 as "never disposed" (the
-    name is absent here, so it was released on no path) vs "not on every path" (the
-    name is present, but the core still found a leaking path)."""
+    (recursing into `if` branches and `while` bodies). Used to word an OWN001 as
+    "never disposed" (the name is absent here, so it was released on no path) vs "not
+    on every path" (the name is present, but the core still found a leaking path)."""
     out: set[str] = set()
     for n in nodes:
         if not isinstance(n, dict):
@@ -424,6 +425,10 @@ def _released_vars(nodes: list[Any]) -> set[str]:
                 b = n.get(branch, [])
                 if isinstance(b, list):
                     out |= _released_vars(b)
+        elif op == "while":
+            b = n.get("body", [])
+            if isinstance(b, list):
+                out |= _released_vars(b)
     return out
 
 
@@ -433,9 +438,10 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str,
                 released_vars: set[str]) -> list[Stmt]:
     """Lower one OwnIR flow body (B0b/B2) into core statements. acquire/use/release/
     return reference a C# local by name (`var`); `if` carries `then`/`else`
-    sub-bodies. Each acquire gets a globally-unique handle `loc_<n>` (so a finding
-    maps back to the C# local); `localmap` resolves later references within the same
-    function and its branches."""
+    sub-bodies; `while` carries a `body` (a back-edge — the core's worklist fixpoint
+    checks it, P-016 A1). Each acquire gets a globally-unique handle `loc_<n>` (so a
+    finding maps back to the C# local); `localmap` resolves later references within
+    the same function and its branches/loops."""
     body: list[Stmt] = []
     for n in nodes:
         if not isinstance(n, dict):
@@ -471,6 +477,11 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str,
             else_b = _lower_flow(en if isinstance(en, list) else [],
                                  ffile, fname, handles, loc, localmap, released_vars)
             body.append(If("?", then_b, else_b, line))
+        elif op == "while":
+            bn = n.get("body", [])
+            body_b = _lower_flow(bn if isinstance(bn, list) else [],
+                                 ffile, fname, handles, loc, localmap, released_vars)
+            body.append(While("?", body_b, line))
     return body
 
 

tests/fixtures/ownir/flow_while.facts.json

@@ -0,0 +1,17 @@
+{
+  "ownir_version": 0,
+  "module": "Extracted",
+  "components": [],
+  "functions": [
+    {
+      "name": "FlowLocalsSample.WhileXIter",
+      "file": "FlowLocalsSample.cs",
+      "body": [
+        {"op": "acquire", "var": "c", "line": 20},
+        {"op": "while", "line": 21, "body": [
+          {"op": "release", "var": "c", "line": 22}
+        ]}
+      ]
+    }
+  ]
+}

tests/test_ownir.py

@@ -52,6 +52,8 @@
                                  "ownir", "unitofwork_flow.facts.json")
 _LEAK_ON_ELSE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
                                      "ownir", "flow_leak_on_else.facts.json")
+_WHILE_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
+                              "ownir", "flow_while.facts.json")
 _DI_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
                            "ownir", "di.facts.json")
 _UNRESOLVED_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
@@ -298,6 +300,29 @@ def run() -> int:
             fails.append(f"partial-release leak wrongly used the never-disposed "
                          f"wording: {e0.message!r}")
 
+    # --- P-016 A1 reaches the frontend: a `while` flow body (the extractor now
+    #     lowers loops instead of skipping the method) routes through the core's
+    #     worklist fixpoint. A resource acquired before the loop and released INSIDE
+    #     it double-releases on the 2nd turn (OWN003) and leaks on the 0-trip path
+    #     (OWN001) — both on the same local, proving the loop op reaches the fixpoint
+    #     end-to-end through the bridge (not just on the `.own` DSL).
+    with open(_WHILE_FIXTURE, encoding="utf-8") as f:
+        wlfacts = json.load(f)
+    wlfindings = check_facts(wlfacts)
+    checks += 1
+    codes = sorted({x.code for x in wlfindings})
+    if len(wlfindings) != 2 or codes != ["OWN001", "OWN003"] \
+            or any(x.event != "c" for x in wlfindings):
+        fails.append(f"expected cross-iteration OWN001+OWN003 on 'c', got "
+                     f"{[(x.event, x.code) for x in wlfindings]}")
+    else:
+        checks += 1
+        if any(x.file != "FlowLocalsSample.cs" or x.line != 20 for x in wlfindings):
+            fails.append(f"wrong while-xiter location: "
+                         f"{[(x.file, x.line) for x in wlfindings]}")
+        if not all(x.kind == "disposable" for x in wlfindings):
+            fails.append("while-xiter findings missing [resource: disposable] kind")
+
     # --- DI001 captive dependency (P-006): a singleton capturing a scoped
     #     service (directly or through a transient) is flagged at its
     #     registration site; safe registrations stay silent.