From d733ee2c8ea91304c86424063ef73fefa8824715 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Jun 2026 14:18:05 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat:=20P-016=20A1=20=E2=80=94=20loop=20sup?= =?UTF-8?q?port=20in=20the=20core=20(worklist=20fixpoint=20over=20back-edg?= =?UTF-8?q?es)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the single topological pass (which excluded any block in a cycle) with a forward worklist to a fixpoint, so the core analyses `while` loops instead of rejecting them as OWN020. The per-symbol lattice {OWNED,MOVED,RELEASED,ESCAPED} is finite and union-merged, the transfer is monotone, so it converges without widening. On a loop-free CFG it reduces to one pass per block — behaviour is identical to the old walk (and __main__ sorts diagnostics by (line, code), so emission order is unchanged). Key pieces: - lexer/AST/parser: `while (cond) { body }` (cond opaque like `if`); `while` graduates out of REJECTED_KEYWORDS (`for`/`loop`/async stay OWN020). - cfg: `lower_while` emits a header block with a back-edge from the body exit. - analysis: two-phase run — a SILENT fixpoint converges the in-states (a looped block is transferred many times), then ONE emitting pass reports diagnostics on the converged state (so no per-iteration duplicates). Borrows stay block-scoped, so the loan-set-equal-at-merge invariant holds across back-edges too. - codegen/report/lifetimes: handle/descend into `While` (keeps mypy --strict exhaustive and avoids dropping moves/buffers/subscribes inside a loop body). This catches cross-iteration faults a single pass cannot see: a resource released in a loop is double-released on the next turn (OWN003) and used after release (OWN009); one acquired each turn and not released leaks (OWN001). Balanced acquire/release — and a borrow that opens and closes within the body — stay clean. Pinned by tests/test_loops.py (exact code sets, incl. nested loops), gallery 10_leak_in_loop.own, and run_tests CASES. Spec/README/P-016 updated. https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- README.md | 34 +++-- docs/proposals/P-016-deep-fact-extraction.md | 25 +++- examples/gallery/10_leak_in_loop.own | 12 ++ ownlang/analysis.py | 124 +++++++++++------- ownlang/ast_nodes.py | 12 +- ownlang/cfg.py | 28 +++- ownlang/codegen.py | 15 ++- ownlang/lexer.py | 12 +- ownlang/lifetimes.py | 2 +- ownlang/parser.py | 30 ++++- ownlang/report.py | 2 +- spec/OwnCore.md | 14 +- tests/run_tests.py | 24 +++- tests/test_gallery.py | 1 + tests/test_loops.py | 128 +++++++++++++++++++ 15 files changed, 375 insertions(+), 88 deletions(-) create mode 100644 examples/gallery/10_leak_in_loop.own create mode 100644 tests/test_loops.py diff --git a/README.md b/README.md index cfeb134b..d29255b8 100644 --- a/README.md +++ b/README.md @@ -276,8 +276,9 @@ fn process(size: int) { `borrow_mut` требует эксклюзива (живой shared → OWN006, живой mut → OWN011), `borrow` несовместим с живым mut (→ OWN012). -Поскольку язык без циклов и borrow'ы блок-скоупные, множество активных loans -**одинаково** на всех предшественниках любого merge. Это инвариант, который +Поскольку borrow'ы блок-скоупные (loan, открытый в теле `while`, закрывается там +же, в той же итерации), множество активных loans **одинаково** на всех +предшественниках любого merge — включая back-edge цикла. Это инвариант, который `join()` **проверяет ассертом**, а не предполагает (см. ниже про OWN010-ревьюера). --- @@ -341,7 +342,7 @@ fn process(size: int) { | Код | Что ловит | |-----|-----------| -| OWN020 | неподдерживаемая конструкция (цикл/async) | +| OWN020 | неподдерживаемая конструкция (`for`/`loop`-итерация, async; `while` поддержан) | | OWN030 | неизвестное имя | | OWN031 | переопределение в области видимости | | OWN032 | owned-ресурс скопирован без `move` | @@ -387,7 +388,12 @@ if (flag) { release c; } // then: c -> {RELEASED} - `OWNED ∈`, но рядом `MOVED` → **maybe** (OWN010); - на выходе `OWNED ∈` → OWN001. -Обход — один топологический проход по DAG (циклов нет → fixpoint не нужен). +Обход — worklist до fixpoint: `while` даёт back-edge, и блок переоценивается, пока +его in-состояние не перестанет расти (решётка `{OWNED,MOVED,RELEASED,ESCAPED}` +конечна, merge = объединение, transfer монотонен → сходится без widening). На CFG +без циклов это вырождается в один проход на блок — как прежний топологический обход. +Диагностики печатаются вторым проходом, по сошедшимся состояниям (один раз, не на +каждой итерации fixpoint). ### Важный разворот про false positives @@ -620,12 +626,14 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща | OWN013 (missing-return) | OWN033 | | | — | OWN040 / OWN041 | новая граница вызовов | -Про **OWN010-ревьюера «incompatible-state-at-join»**: в блок-скоупном языке без -циклов несовместимых loans на merge быть не может (borrow всегда сбалансирован -внутри ветки). Поэтому это не user-facing код, а **ассерт-инвариант** в `join()`. +Про **OWN010-ревьюера «incompatible-state-at-join»**: в блок-скоупном языке +несовместимых loans на merge быть не может (borrow всегда сбалансирован внутри +ветки — и внутри тела `while`, так что back-edge цикла тоже несёт тот же набор +loans). Поэтому это не user-facing код, а **ассерт-инвариант** в `join()`. Добавлять диагностику, которая структурно никогда не сработает, — это та самая -декорация, против которой вся затея. Когда появятся циклы/ранний выход из borrow'а, -ассерт превратится в реальный код. (Номер OWN010 в новой схеме занят «maybe-move».) +декорация, против которой вся затея. Если появится ранний выход из borrow'а +(`break` из тела с открытым loan), ассерт превратится в реальный код. (Номер +OWN010 в новой схеме занят «maybe-move».) --- @@ -644,8 +652,10 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща Soundness не доказан — он аргументирован и протестирован. Трансляция в Dafny/F\* и доказательство — **следующий слой**, не этот. -3. **Циклы и async отвергаются, а не анализируются** (OWN020). Нужен worklist с - fixpoint и loop-инварианты владения; CFG к этому готов (DAG-проход → worklist). +3. **`while` анализируется** (worklist + fixpoint по back-edge: cross-iteration + leak/use-after-release/double-release, см. `tests/test_loops.py`). А вот + `for`/`loop`-итерация и async пока отвергаются (OWN020) — для них нужна + десугаризация в `while` либо отдельная модель; CFG и worklist к этому готовы. 4. **В песочнице PoC нет .NET** — golden проверен *по построению* и чекером. Но **CI его реально компилирует и запускает** настоящим компилятором (job @@ -691,7 +701,7 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща ``` ownlang/ ownlang/ - lexer.py # токенизатор; цикл/async лексятся как REJECTED; строки для emit_* + lexer.py # токенизатор; for/loop/async лексятся как REJECTED (while — нет); строки для emit_* ast_nodes.py # dataclass-узлы AST (resource, extern, call, эффекты, buffer, policy) parser.py # recursive descent; грамматика в docstring buffers.py # storage policies: режимы, резолв policy+intent, валидация diff --git a/docs/proposals/P-016-deep-fact-extraction.md b/docs/proposals/P-016-deep-fact-extraction.md index 98199ca5..0e0c6a80 100644 --- a/docs/proposals/P-016-deep-fact-extraction.md +++ b/docs/proposals/P-016-deep-fact-extraction.md @@ -9,8 +9,13 @@ 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. + extractor flag stays default-off pending an `OWNIR_VERSION` bump. **A1 (core loop + 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. - **Depends on:** - [P-014](P-014-semantic-resolution.md) Tier A — the `SemanticModel` (**DONE**). The hard prerequisite: typed ownership facts are impossible without binding. @@ -68,11 +73,17 @@ a CFG-carrying bridge, and the existing core checks real code. ### Track A — core only (pure DSL, no frontend, `.own`-tested) -- **A1 — Loops.** Replace the single topological pass over the DAG (`cfg.py`, - `analysis.py`) with a worklist + fixpoint over back-edges. The lattice is the - finite set-of-states (OwnCore §3, union at merges) → monotone → it converges - (confirm whether widening is even needed). Removes the `OWN020` "loops" clause. - Fully independent of the frontend; pinned by new `.own` loop cases + the gallery. +- **A1 — Loops. ✅ DONE.** Replaced the single topological pass over the DAG + (`cfg.py`, `analysis.py`) with a worklist + fixpoint over back-edges. The lattice + is the finite set-of-states (OwnCore §3, union at merges) → monotone → it converges + (widening was **not** needed — the per-symbol lattice has height 4). `while` lowers + to a header block with a back-edge from the body exit; diagnostics are emitted in a + 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). ### Track B — frontend depth (needs the `SemanticModel`, now present) diff --git a/examples/gallery/10_leak_in_loop.own b/examples/gallery/10_leak_in_loop.own new file mode 100644 index 00000000..e2191431 --- /dev/null +++ b/examples/gallery/10_leak_in_loop.own @@ -0,0 +1,12 @@ +// OWN001 — a resource acquired every iteration but never released: leaks each pass. +// Real C#: `while (reader.Read()) { var conn = Open(...); Use(conn); }` with no +// Dispose() — a fresh handle leaks on every loop turn. The checker analyses the +// loop (worklist fixpoint over the back-edge) rather than skipping it. +module Gallery +resource Conn { acquire open release close } +fn drain(n: int) { + while (n) { + let c = acquire Conn(n); // opened every iteration ... + use c; + } // ... never closed -> leak +} diff --git a/ownlang/analysis.py b/ownlang/analysis.py index bb6d2027..256e2cd1 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -26,13 +26,22 @@ a move needs Own (suspended by *any* loan -> OWN007), a release needs Drop (-> OWN008), `use` needs Read (suspended by a mutable loan -> OWN013), and so on. -The traversal is a single topological pass over the loop-free DAG. Because every -borrow is block-scoped, the set of active loans is identical on all predecessors -of a merge, so joining loans is trivial; this invariant is asserted, not assumed. +The traversal is a forward worklist to a fixpoint, so it handles loops (`while`): +a block is re-evaluated until its in-state stops growing. The per-symbol lattice +is the finite set {OWNED,MOVED,RELEASED,ESCAPED} merged by union, and the transfer +is monotone, so the iteration converges (no widening needed). On a loop-free CFG +this reduces to one pass per block — identical to the previous topological walk. +Because every borrow is block-scoped, the active loans are identical on all +predecessors of a merge (back-edges included), so joining loans is trivial; this +invariant is asserted, not assumed. + +Diagnostics are emitted in a second pass, once, on the converged in-states — never +during the fixpoint iteration (a looped block is transferred many times). """ from __future__ import annotations +from collections import deque from dataclasses import dataclass, field from enum import Enum, auto from typing import assert_never @@ -93,11 +102,13 @@ def join(a: State, b: State) -> State: out = State() for k in set(a.var) | set(b.var): out.var[k] = set(a.var.get(k, set())) | set(b.var.get(k, set())) - # Block-scoped borrows => identical active loans on both predecessors. - # Assert the invariant rather than silently papering over a builder bug. + # Block-scoped borrows => identical active loans on both predecessors. This + # holds across loop back-edges too: a borrow opened inside a loop body closes + # within the same iteration, so the loan set at the body exit equals the one on + # the entry edge. Assert the invariant rather than paper over a builder bug. assert set(a.loans) == set(b.loans), ( "active loans differ at a control-flow merge; this should be impossible " - "for block-scoped borrows in a loop-free language" + "for block-scoped borrows (they close within the scope that opened them)" ) out.loans = dict(a.loans) return out @@ -108,6 +119,11 @@ def __init__(self, cfg: CFG): self.cfg = cfg self.diags: list[Diagnostic] = [] self.blocks = {b.id: b for b in cfg.blocks} + # During the fixpoint pass (phase 1) the transfer runs repeatedly to + # converge the per-block in-states; diagnostics must NOT be emitted then + # (a block in a loop is visited many times). `silent` gates `err`; phase 2 + # re-runs the transfer once per block, emitting on the converged state. + self.silent = False def initial_state(self) -> State: s = State() @@ -119,6 +135,8 @@ def initial_state(self) -> State: def err(self, code: str, msg: str, line: int, subject: str | None = None, resource_kind: str | None = None) -> None: + if self.silent: + return self.diags.append(Diagnostic(code, msg, line, subject=subject, resource_kind=resource_kind)) @@ -171,55 +189,75 @@ def _state_problem(self, st: State, sym: Symbol, verb: str, line: int) -> bool: return True return False - # -- topological order over the DAG ------------------------------------ + # -- reachability + dataflow fixpoint ---------------------------------- - def topo_order(self) -> list[int]: - reachable: set[int] = set() + def reachable(self) -> set[int]: + seen: set[int] = set() stack = [self.cfg.entry] while stack: x = stack.pop() - if x in reachable: + if x in seen: continue - reachable.add(x) + seen.add(x) stack.extend(self.blocks[x].succ) - local_indeg = dict.fromkeys(reachable, 0) - for b in reachable: - for s in self.blocks[b].succ: - if s in reachable: - local_indeg[s] += 1 - ready = [b for b in reachable if local_indeg[b] == 0] - order: list[int] = [] - while ready: - b = ready.pop() - order.append(b) - for s in self.blocks[b].succ: - if s in reachable: - local_indeg[s] -= 1 - if local_indeg[s] == 0: - ready.append(s) - return order + return seen + + def in_state_of(self, bid: int, preds: dict[int, list[int]], + reachable: set[int], out_states: dict[int, State]) -> State: + """The in-state of a block = the join (union) of its already-computed + predecessors' out-states; the entry block starts from `initial_state`.""" + if bid == self.cfg.entry: + return self.initial_state() + ps = [p for p in preds[bid] if p in reachable and p in out_states] + if not ps: + return State() + st = out_states[ps[0]].copy() + for p in ps[1:]: + st = join(st, out_states[p]) + return st + + def fixpoint(self, reachable: set[int]) -> dict[int, State]: + """Forward worklist to a fixpoint over a (possibly cyclic) CFG. The + per-symbol lattice is the finite set {OWNED,MOVED,RELEASED,ESCAPED}, merged + by union at joins; the transfer is monotone, so iterating until no out-state + changes converges (a block's out can only grow up the finite lattice). A + block is re-queued only when one of its predecessors' out-state changed. + Runs silently — phase 2 emits the diagnostics on the converged in-states.""" + preds = self.cfg.preds() + in_states: dict[int, State] = {} + out_states: dict[int, State] = {} + work: deque[int] = deque(sorted(reachable)) + queued: set[int] = set(reachable) + while work: + bid = work.popleft() + queued.discard(bid) + in_states[bid] = self.in_state_of(bid, preds, reachable, out_states) + new_out = self.transfer(self.blocks[bid], in_states[bid]) + if bid not in out_states or new_out != out_states[bid]: + out_states[bid] = new_out + for s in self.blocks[bid].succ: + if s in reachable and s not in queued: + work.append(s) + queued.add(s) + return in_states # -- main -------------------------------------------------------------- def run(self) -> list[Diagnostic]: - order = self.topo_order() - preds = self.cfg.preds() + reachable = self.reachable() + # Phase 1: converge the in-states silently (no diagnostics — a looped block + # is transferred many times before it stabilises). + self.silent = True + in_states = self.fixpoint(reachable) + self.silent = False + # Phase 2: one emitting transfer per block, on its converged in-state, so + # every diagnostic is reported exactly once at the fixpoint. Block order is + # irrelevant — __main__ sorts the diagnostics by (line, code). out_states: dict[int, State] = {} - reachable = set(order) - - for bid in order: - ps = [p for p in preds[bid] if p in reachable and p in out_states] - if bid == self.cfg.entry: - in_state = self.initial_state() - elif ps: - in_state = out_states[ps[0]].copy() - for p in ps[1:]: - in_state = join(in_state, out_states[p]) - else: - in_state = State() - out_states[bid] = self.transfer(self.blocks[bid], in_state) + for bid in sorted(reachable): + out_states[bid] = self.transfer(self.blocks[bid], in_states[bid]) - for bid in order: + for bid in sorted(reachable): blk = self.blocks[bid] if blk.succ: continue diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index 9542aa34..e71fe17d 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -138,6 +138,16 @@ class If: line: int +@dataclass(frozen=True) +class While: + # like If, the condition is opaque: we model the loop's control flow (a body + # that may run zero or more times, with a back-edge to the test), not the + # values. The analysis reaches a fixpoint over the back-edge (analysis.py). + cond_text: str + body: list[Stmt] + line: int + + @dataclass(frozen=True) class Return: var: str | None @@ -154,7 +164,7 @@ class Subscribe: line: int -Stmt = Let | Release | Use | Call | BorrowBlock | If | Return | Subscribe +Stmt = Let | Release | Use | Call | BorrowBlock | If | While | Return | Subscribe # ---- top level ------------------------------------------------------------ diff --git a/ownlang/cfg.py b/ownlang/cfg.py index e072e6d7..cd42d657 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -13,9 +13,10 @@ 2. A control-flow graph: real basic blocks with successor edges, branches at `if`, merge nodes, and terminal blocks at `return`. Borrow scopes lower to explicit BORROW_START / BORROW_END instructions; calls lower to an Invoke - instruction carrying the resolved per-argument ownership effect. There are - no loops, so the CFG is a DAG and a single topological pass suffices — this - is exactly where loop support (worklist + fixpoint) would later plug in. + instruction carrying the resolved per-argument ownership effect. A `while` + lowers to a header block (the test) with a back-edge from the body exit, so + the CFG may contain cycles; the analysis converges over them with a worklist + fixpoint (analysis.py) instead of a single topological pass. """ from __future__ import annotations @@ -331,6 +332,8 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: return self.lower_borrow(st, cur) if isinstance(st, A.If): return self.lower_if(st, cur) + if isinstance(st, A.While): + return self.lower_while(st, cur) if isinstance(st, A.Return): return self.lower_return(st, cur) if isinstance(st, A.Subscribe): @@ -517,6 +520,25 @@ def lower_if(self, st: A.If, cur: Block) -> Block | None: else_exit.succ = [merge.id] return merge + def lower_while(self, st: A.While, cur: Block) -> Block | None: + # while (cond) { body }: a header block tests the (opaque) condition with + # two successors — the body and the after-block. The body's exit loops back + # to the header (the back-edge), so the header is a merge of the entry edge + # and the back-edge. The analysis reaches a fixpoint over that back-edge + # (analysis.py worklist); a borrow opened in the body closes within the same + # iteration, so the loan set is identical on both header predecessors. + header = self.new_block("while.header") + cur.succ = [header.id] + body_entry = self.new_block("while.body") + after = self.new_block("while.after") + header.succ = [body_entry.id, after.id] + self.push_scope() + body_exit = self.lower_seq(st.body, body_entry) + self.pop_scope() + if body_exit is not None: + body_exit.succ = [header.id] # back-edge: end of body -> re-test + return after + def lower_return(self, st: A.Return, cur: Block) -> Block | None: ret = self.fn.ret sym: Symbol | None = None diff --git a/ownlang/codegen.py b/ownlang/codegen.py index 05cbf750..96854f82 100644 --- a/ownlang/codegen.py +++ b/ownlang/codegen.py @@ -462,6 +462,11 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: out.extend(self._emit_block(st.else_body, ind + " ")) out.append(f"{ind}}}") return out + if isinstance(st, A.While): + out = [f"{ind}while ({st.cond_text or 'cond'})", f"{ind}{{"] + out.extend(self._emit_block(st.body, ind + " ")) + out.append(f"{ind}}}") + return out if isinstance(st, A.Return): return [f"{ind}return {st.var};" if st.var else f"{ind}return;"] if isinstance(st, A.Subscribe): @@ -515,7 +520,7 @@ def _member(r: A.ResourceDecl, role: str) -> str: def _contains_branch_or_transfer(stmts: list[A.Stmt]) -> bool: for st in stmts: - if isinstance(st, A.If): + if isinstance(st, (A.If, A.While)): return True if isinstance(st, A.Return) and st.var is not None: return True @@ -535,7 +540,7 @@ def _iter_stmts(stmts: list[A.Stmt]) -> Iterator[A.Stmt]: if isinstance(st, A.If): yield from _iter_stmts(st.then_body) yield from _iter_stmts(st.else_body) - elif isinstance(st, A.BorrowBlock): + elif isinstance(st, (A.While, A.BorrowBlock)): yield from _iter_stmts(st.body) @@ -568,7 +573,7 @@ def _fn_has_buffer(stmts: list[A.Stmt]) -> bool: if isinstance(st, A.If): if _fn_has_buffer(st.then_body) or _fn_has_buffer(st.else_body): return True - if isinstance(st, A.BorrowBlock): + if isinstance(st, (A.While, A.BorrowBlock)): if _fn_has_buffer(st.body): return True return False @@ -640,7 +645,7 @@ def _fn_has_native(stmts: list[A.Stmt]) -> bool: if isinstance(st, A.If): if _fn_has_native(st.then_body) or _fn_has_native(st.else_body): return True - if isinstance(st, A.BorrowBlock): + if isinstance(st, (A.While, A.BorrowBlock)): if _fn_has_native(st.body): return True return False @@ -656,7 +661,7 @@ def walk(stmts: list[A.Stmt]) -> None: elif isinstance(st, A.If): walk(st.then_body) walk(st.else_body) - elif isinstance(st, A.BorrowBlock): + elif isinstance(st, (A.While, A.BorrowBlock)): walk(st.body) for fn in mod.functions: diff --git a/ownlang/lexer.py b/ownlang/lexer.py index 4ac673c1..b3f14b3b 100644 --- a/ownlang/lexer.py +++ b/ownlang/lexer.py @@ -3,9 +3,10 @@ Deliberately small. We tokenize keywords, identifiers, integer literals, string literals (used only for C#-emit templates on a resource), and a handful of -punctuation. The features we explicitly DON'T support (loops, async) are lexed -as their own token class so the parser can emit an honest "out of scope" -diagnostic instead of a confusing parse error. +punctuation. The features we explicitly DON'T support (for/loop-style iteration, +async) are lexed as their own token class so the parser can emit an honest "out +of scope" diagnostic instead of a confusing parse error. (`while` IS supported — +the core analyses loops via a worklist fixpoint; see analysis.py.) """ from __future__ import annotations @@ -35,6 +36,7 @@ class Tok(Enum): USE = auto() IF = auto() ELSE = auto() + WHILE = auto() RETURN = auto() MUT = auto() POLICY = auto() @@ -80,6 +82,7 @@ class Tok(Enum): "use": Tok.USE, "if": Tok.IF, "else": Tok.ELSE, + "while": Tok.WHILE, "return": Tok.RETURN, "mut": Tok.MUT, "policy": Tok.POLICY, @@ -92,7 +95,8 @@ class Tok(Enum): } # Things we refuse to analyze in the MVP. Lexed so we can say so plainly. -REJECTED_KEYWORDS = {"while", "for", "loop", "async", "await", "yield", "spawn"} +# (`while` graduated out of this set — the core now analyses it; see analysis.py.) +REJECTED_KEYWORDS = {"for", "loop", "async", "await", "yield", "spawn"} @dataclass(frozen=True) diff --git a/ownlang/lifetimes.py b/ownlang/lifetimes.py index f6df898d..1df6c719 100644 --- a/ownlang/lifetimes.py +++ b/ownlang/lifetimes.py @@ -51,7 +51,7 @@ def _iter_subscribes(stmts: list[A.Stmt]) -> Iterator[A.Subscribe]: elif isinstance(st, A.If): yield from _iter_subscribes(st.then_body) yield from _iter_subscribes(st.else_body) - elif isinstance(st, A.BorrowBlock): + elif isinstance(st, (A.While, A.BorrowBlock)): yield from _iter_subscribes(st.body) diff --git a/ownlang/parser.py b/ownlang/parser.py index c52dda8d..e05ada1b 100644 --- a/ownlang/parser.py +++ b/ownlang/parser.py @@ -19,7 +19,7 @@ param := IDENT ":" type ("lifetime" IDENT)? type := "&" "mut"? IDENT | IDENT block := "{" stmt* "}" - stmt := let | release | use | call | borrow | if | return | subscribe + stmt := let | release | use | call | borrow | if | while | return | subscribe subscribe := "subscribe" "self" "to" IDENT ";" // self/to contextual let := "let" IDENT "=" rhs ";" rhs := "acquire" IDENT "(" args? ")" | "move" IDENT @@ -32,6 +32,7 @@ call := IDENT "(" args? ")" ";" borrow := ("borrow" | "borrow_mut") IDENT "as" IDENT block if := "if" "(" cond ")" block ("else" block)? + while := "while" "(" cond ")" block return := "return" IDENT? ";" args := atom ("," atom)* atom := INT | IDENT @@ -100,8 +101,9 @@ def _reject_guard(self) -> None: if self.at(Tok.REJECTED): t = self.cur raise ParseError( - f"'{t.text}' is out of scope for the MVP — loops and async are " - f"deliberately unsupported (see README, 'Where it cheats')", + f"'{t.text}' is out of scope for the MVP — for/loop-style " + f"iteration and async are deliberately unsupported ('while' is " + f"supported; see README, 'Where it cheats')", t, ) @@ -302,6 +304,8 @@ def parse_stmt(self) -> A.Stmt: return self.parse_borrow() if self.at(Tok.IF): return self.parse_if() + if self.at(Tok.WHILE): + return self.parse_while() if self.at(Tok.RETURN): return self.parse_return() if self.at(Tok.SUBSCRIBE): @@ -460,6 +464,26 @@ def parse_if(self) -> A.If: return A.If(cond_text=" ".join(cond_parts), then_body=then_body, else_body=else_body, line=kw.line) + def parse_while(self) -> A.While: + kw = self.eat(Tok.WHILE) + self.eat(Tok.LPAREN) + cond_parts: list[str] = [] + depth = 1 + while True: + if self.at(Tok.EOF): + raise ParseError("unterminated while-condition", self.cur) + if self.at(Tok.LPAREN): + depth += 1 + elif self.at(Tok.RPAREN): + depth -= 1 + if depth == 0: + self.eat(Tok.RPAREN) + break + cond_parts.append(self.cur.text) + self.pos += 1 + body = self.parse_block() + return A.While(cond_text=" ".join(cond_parts), body=body, line=kw.line) + def parse_return(self) -> A.Return: kw = self.eat(Tok.RETURN) var: str | None = None diff --git a/ownlang/report.py b/ownlang/report.py index 77265ab1..a889bfd6 100644 --- a/ownlang/report.py +++ b/ownlang/report.py @@ -43,7 +43,7 @@ def _walk_buffers( elif isinstance(st, A.If): yield from _walk_buffers(st.then_body) yield from _walk_buffers(st.else_body) - elif isinstance(st, A.BorrowBlock): + elif isinstance(st, (A.While, A.BorrowBlock)): yield from _walk_buffers(st.body) diff --git a/spec/OwnCore.md b/spec/OwnCore.md index f43dc79e..6c70f031 100644 --- a/spec/OwnCore.md +++ b/spec/OwnCore.md @@ -8,7 +8,8 @@ OwnCore is the small affine-ownership + borrow-permission core of OwnLang. It is deliberately boring: a linear resource protocol with block-scoped loans, checked -flow-sensitively over a loop-free CFG. No generic lifetimes, no async borrowing, +flow-sensitively over a CFG (a `while` loop is a back-edge the analysis converges +over with a worklist fixpoint). No generic lifetimes, no async borrowing, no higher-ranked anything. Buffers and lifetime regions are layered on top and specified separately ([BufferPolicies.md](BufferPolicies.md), [Lifetimes.md](Lifetimes.md)). @@ -63,8 +64,9 @@ derived on demand: | OWNED | mutable | — (exclusive: owner unusable) | | MOVED / RELEASED / ESCAPED | — | — | -Because the language is loop-free and borrows are block-scoped, the set of active -loans is identical on all predecessors of a merge; the checker **asserts** this +Because borrows are block-scoped (a loan opened inside a `while` body also closes +inside it, within the same iteration), the set of active loans is identical on all +predecessors of a merge — back-edges included; the checker **asserts** this invariant rather than assuming it. ## 5. Operations @@ -137,7 +139,9 @@ without a test change (or vice-versa) is a red build. ## 10. Out of scope (see proposals, not here) -Loops/async (**OWN020**), a real type system, value-level reasoning (an `if` -condition is opaque text — control flow is modelled, not values), C# ingestion, +`for`/`loop`-style iteration and async (**OWN020**) — but **not** `while`, which is +analysed via a worklist fixpoint — a real type system, value-level reasoning (an +`if`/`while` condition is opaque text — control flow is modelled, not values), C# +ingestion, and formal soundness proofs are explicitly **not** part of OwnCore today. They are tracked in [`docs/proposals/`](../docs/proposals/). diff --git a/tests/run_tests.py b/tests/run_tests.py index 30b99b88..cbcde052 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -150,7 +150,20 @@ def codes(src: str) -> list[str]: "fn f() -> Conn { let c = acquire Conn(1); return c; }", []), ("ok_bare_return_void", "fn f(){ let b = acquire Buffer(1); release b; return; }", []), - ("loop_rejected", "fn f(){ while (x) { use x; } }", ["OWN020"]), + # ---- loops (while): analysed via a worklist fixpoint, not rejected ---- + # acquire + release each iteration is balanced -> clean (also codegens). + ("loop_clean_balanced", + "fn f(n: int){ while (n) { let c = acquire Conn(1); release c; } }", []), + # acquired each iteration but never released -> leaks. + ("loop_leak_each_iter", + "fn f(n: int){ while (n) { let c = acquire Conn(1); use c; } }", ["OWN001"]), + # released inside the loop with no re-acquire: the 2nd iteration double-releases + # (OWN003, only visible once the back-edge state is folded in) and the 0-trip + # path leaks (OWN001). A single topological pass would miss the OWN003. + ("loop_double_release_xiter", + "fn f(n: int){ let c = acquire Conn(1); while (n) { release c; } }", + ["OWN001", "OWN003"]), + # for/loop-style iteration and async stay out of scope -> OWN020. ("async_rejected", "fn f(){ async { use x; } }", ["OWN020"]), # ---- extern boundary ---- @@ -1049,6 +1062,11 @@ def run() -> int: import test_lifetimes lt_rc = test_lifetimes.run() + # Loop support (P-016 A1): `while` is analysed via a worklist fixpoint over the + # back-edge — cross-iteration leak/use-after-release/double-release, not OWN020. + import test_loops + loops_rc = test_loops.run() + # Spec conformance pilot: every normative spec/ rule fires on its example. import test_spec spec_rc = test_spec.run() @@ -1061,8 +1079,8 @@ def run() -> int: return 1 if (failed or cg_fail or golden_fails or buffer_fails or escape_fails or branchy_fails or nest_fails or order_fails or helper_fails or cc_rc or pf_rc - or gl_rc or co_rc or wpf_rc or lt_rc or spec_rc - or ownir_rc) else 0 + or gl_rc or co_rc or wpf_rc or lt_rc or loops_rc + or spec_rc or ownir_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_gallery.py b/tests/test_gallery.py index b0910441..a12af19a 100644 --- a/tests/test_gallery.py +++ b/tests/test_gallery.py @@ -40,6 +40,7 @@ ("07_use_after_handoff.own", "OWN002", "used a buffer after a callee took ownership"), ("08_stack_buffer_escapes.own", "OWN015", "returned a Span over a stackalloc (dangling)"), ("09_untracked_call.own", "OWN040", "ownership laundered through an opaque call"), + ("10_leak_in_loop.own", "OWN001", "acquired in a loop, never released (while)"), ] diff --git a/tests/test_loops.py b/tests/test_loops.py new file mode 100644 index 00000000..f2a3558e --- /dev/null +++ b/tests/test_loops.py @@ -0,0 +1,128 @@ +#!/usr/bin/env python3 +""" +Loop support (P-016 A1): the core analyses `while` via a worklist fixpoint over +the back-edge, instead of skipping it as OWN020. + +The point of these cases is the *cross-iteration* facts a single topological pass +cannot see: a resource released inside the loop is, on the second turn, released +again (OWN003) and used after release (OWN009); a resource acquired each turn and +not released leaks (OWN001). Balanced acquire/release — and a borrow that opens +and closes within the body — stay clean (no false positive). Each case pins the +exact set of error codes, so the fixpoint can't silently regress to the old +loop-free behavior. + +Run: python tests/test_loops.py + python tests/run_tests.py (runs it as part of the suite) +""" + +from __future__ import annotations + +import os +import sys + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) + +from ownlang.analysis import analyze +from ownlang.cfg import build_cfg, collect_signatures +from ownlang.diagnostics import Severity +from ownlang.lexer import LexError +from ownlang.parser import ParseError, parse + +_PRELUDE = ( + "module Loops\n" + "resource Conn { acquire open release close }\n" +) + + +def _codes(body: str) -> set[str]: + """The set of error codes the checker produces for one function body (the + Conn prelude is prepended). A parse/lex rejection surfaces as OWN020, matching + the driver.""" + try: + mod = parse(_PRELUDE + body) + except (ParseError, LexError): + return {"OWN020"} + rnames = {r.name for r in mod.resources} + sigs = collect_signatures(mod) + out: set[str] = set() + for fn in mod.functions: + cfg, d1 = build_cfg(fn, rnames, sigs) + d2 = analyze(cfg) + out |= {d.code for d in (d1 + d2) if d.severity == Severity.ERROR} + return out + + +# (name, body, expected error-code set, note) +CASES: list[tuple[str, str, set[str], str]] = [ + ("clean_balanced", + "fn f(n: int){ while (n) { let c = acquire Conn(1); release c; } }", + set(), "acquire+release each turn is balanced"), + ("clean_use_in_loop_release_after", + "fn f(n: int){ let c = acquire Conn(1); while (n) { use c; } release c; }", + set(), "used across iterations, released once after the loop"), + ("clean_borrow_in_loop", + "fn f(n: int){ let c = acquire Conn(1); " + "while (n) { borrow c as r { use r; } } release c; }", + set(), "a borrow opens and closes within the body -> loans match at the back-edge"), + ("clean_nested_balanced", + "fn f(n: int){ while (n) { while (n) { let c = acquire Conn(1); release c; } } }", + set(), "nested loops converge; inner acquire/release balanced"), + ("leak_each_iter", + "fn f(n: int){ while (n) { let c = acquire Conn(1); use c; } }", + {"OWN001"}, "acquired each turn, never released -> leak"), + ("leak_nested", + "fn f(n: int){ while (n) { while (n) { let c = acquire Conn(1); use c; } } }", + {"OWN001"}, "leak inside a nested loop still surfaces"), + ("xiter_double_release", + "fn f(n: int){ let c = acquire Conn(1); while (n) { release c; } }", + {"OWN001", "OWN003"}, + "2nd turn double-releases (OWN003, fixpoint-only); 0-trip path leaks (OWN001)"), + ("xiter_use_after_release", + "fn f(n: int){ let c = acquire Conn(1); while (n) { use c; release c; } }", + {"OWN001", "OWN003", "OWN009"}, + "2nd turn uses c after last turn released it (OWN009, fixpoint-only)"), +] + + +def run() -> int: + fails: list[str] = [] + checks = 0 + + for name, body, want, _note in CASES: + checks += 1 + got = _codes(body) + if got != want: + fails.append(f"{name}: expected {sorted(want)}, got {sorted(got)}") + # loops must never be reported as unsupported any more. + checks += 1 + if "OWN020" in got: + fails.append(f"{name}: a `while` loop was wrongly rejected as OWN020") + + # the fixpoint's headline wins: cross-iteration faults a single pass misses. + checks += 1 + if "OWN003" not in _codes( + "fn f(n: int){ let c = acquire Conn(1); while (n) { release c; } }"): + fails.append("cross-iteration double-release (OWN003) was not detected") + checks += 1 + if "OWN009" not in _codes( + "fn f(n: int){ let c = acquire Conn(1); while (n) { use c; release c; } }"): + fails.append("cross-iteration use-after-release (OWN009) was not detected") + + # regression guard: the reject path still works for the constructs that ARE + # out of scope (async/for/loop) -> OWN020, so graduating `while` didn't open + # the gate for everything. + checks += 1 + if _codes("fn f(){ async { use x; } }") != {"OWN020"}: + fails.append("async should still be rejected as OWN020") + checks += 1 + if _codes("fn f(){ for (n) { use x; } }") != {"OWN020"}: + fails.append("for-loops should still be rejected as OWN020") + + for f in fails: + print(f"LOOPS FAIL: {f}") + print(f"loops: {checks - len(fails)}/{checks} loop (while) cases pass") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From 8f6163ec226b7982b72d67bea3a961d2a9a2a5ec Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 16 Jun 2026 14:39:19 +0000 Subject: [PATCH 2/2] docs: clarify the loop-leak gallery comment (leak is independent of the loop condition) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The C# analog cited `while (reader.Read())` (which terminates) while the .own code is `while (n)` with an opaque condition — address a review nitpick by noting the condition is opaque to the checker and the per-iteration leak holds regardless of what ends the loop. Comment-only; the OWN001 verdict is unchanged. https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED --- examples/gallery/10_leak_in_loop.own | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/examples/gallery/10_leak_in_loop.own b/examples/gallery/10_leak_in_loop.own index e2191431..7fd72e07 100644 --- a/examples/gallery/10_leak_in_loop.own +++ b/examples/gallery/10_leak_in_loop.own @@ -1,7 +1,8 @@ // OWN001 — a resource acquired every iteration but never released: leaks each pass. -// Real C#: `while (reader.Read()) { var conn = Open(...); Use(conn); }` with no -// Dispose() — a fresh handle leaks on every loop turn. The checker analyses the -// loop (worklist fixpoint over the back-edge) rather than skipping it. +// Real C#: `while (cond) { var conn = Open(...); Use(conn); }` with no Dispose() — +// a fresh handle leaks on every loop turn, regardless of what ends the loop. The +// condition is opaque to the checker (control flow is modelled, not values); what +// matters is the back-edge, which the worklist fixpoint analyses rather than skips. module Gallery resource Conn { acquire open release close } fn drain(n: int) {