From 4f6716f3f9a02e4de052b6d0056cfbc376c0729b Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 17:57:00 +0000 Subject: [PATCH 01/10] Add ruff + mypy --strict quality gate with exhaustive node dispatch Python was chosen for prototype speed, but untyped dispatch hid a class of 'forgot a variant' bugs (the kind the old codegen kept reintroducing). Tighten the screws: - pyproject.toml: ruff (E,W,F,I,B,UP,C4,RUF) over the tree; mypy --strict on the ownlang package (tests are dynamic fuzzer code, ruff-only). - typing.assert_never in every node dispatch (lower_stmt / step / _stmt_inline): an unhandled union variant is now a type error. This already surfaced a real gap -- a buffer let falling through the inline emitter. - Fix all 39 strict-mypy findings (type params, untyped defs, union-attr narrowing, None-flow) and ruff findings; no behavior change (suite green: analysis 123/123, codegen content 23/23, fuzz, gallery 10/10, corpus 2/2). - CI: new 'lint' job runs ruff + mypy on every push/PR. - README: document the gate next to the regression net. --- .github/workflows/ci.yml | 18 ++++++++++ README.md | 27 +++++++++++++- examples/golden_arraypool/verify_emit.py | 4 +-- ownlang/__main__.py | 31 +++++++++++----- ownlang/analysis.py | 30 +++++++++++----- ownlang/ast_nodes.py | 18 +++++----- ownlang/buffers.py | 24 +++++++------ ownlang/cfg.py | 19 +++++----- ownlang/codegen.py | 35 ++++++++++++------ ownlang/parser.py | 4 +-- ownlang/report.py | 17 +++++---- pyproject.toml | 23 ++++++++++++ tests/run_tests.py | 46 ++++++++++++------------ tests/test_codegen.py | 21 ++++++----- tests/test_codegen_props.py | 18 +++++----- tests/test_corpus.py | 12 +++---- tests/test_gallery.py | 12 +++---- 17 files changed, 237 insertions(+), 122 deletions(-) create mode 100644 pyproject.toml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56753d8c..64b21fe0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,6 +7,24 @@ on: workflow_dispatch: jobs: + # Quality gate: ruff (style/bugs) on the whole tree, and mypy --strict on the + # ownlang package (tests are dynamic/fuzzer code, covered by ruff only). These + # are the "tighten the screws on Python" guard rails — see README. + lint: + name: lint (ruff + mypy --strict) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.11" + - name: Install linters + run: pip install "ruff==0.15.8" "mypy==1.19.1" + - name: ruff + run: ruff check . + - name: mypy --strict (ownlang) + run: mypy + tests: name: tests (py${{ matrix.python-version }}) runs-on: ubuntu-latest diff --git a/README.md b/README.md index fec9fd7d..d362c81b 100644 --- a/README.md +++ b/README.md @@ -629,6 +629,31 @@ ownlang/ examples/ ok_*.own # проходят bad_*.own # падают с конкретным кодом + gallery/ # «что оно ловит» — narrated примеры, пинятся тестом golden_arraypool/ # buffer.own + Program.cs (host-код; .csproj не входит) - tests/run_tests.py # 42 кейса анализа + codegen smoke + golden smoke + corpus/real-world/ # hand-reduced реальные ArrayPool-баги + expected-коды + tests/ + run_tests.py # кейсы анализа + codegen smoke + golden smoke + test_codegen.py # content-assertions на сгенерённый C# + test_codegen_props.py # property-фаззер с независимым AST-оракулом + test_gallery.py # пинит каждый gallery-пример к его коду + test_corpus.py # пинит каждый corpus-кейс к expected-диагностикам + pyproject.toml # gate: ruff + mypy --strict (см. ниже) ``` + +### Гейт качества (ruff + mypy --strict) + +Python взяли ради скорости прототипа, но без типов он легко скрывает «забыл ветку» +класс багов (ровно такие плодил старый кодоген). Поэтому прикручены гайки, и они +блокируют CI (job `lint`): + +- **ruff** (`E,W,F,I,B,UP,C4,RUF`) — стиль + bugbear-ловушки на всём дереве; +- **mypy `--strict`** на пакете `ownlang` (тесты — динамический фаззер-код, их + держит только ruff); +- **`typing.assert_never`** в каждом разборе по видам узлов (`lower_stmt`, `step`, + `_stmt_inline`): новый невручённый вариант union'а — это **ошибка компиляции + типов**, дешёвая замена exhaustive-match. Включение это уже поймало реальную + дыру — buffer-`let`, незакрытый в inline-эмиттере. + +Локально: `ruff check . && mypy`. Это не заменяет regression-сеть (фаззер/оракул/ +корпус ловят логику, линтер — опечатки и типы), а дополняет её. diff --git a/examples/golden_arraypool/verify_emit.py b/examples/golden_arraypool/verify_emit.py index 2264bbc3..7ee00306 100644 --- a/examples/golden_arraypool/verify_emit.py +++ b/examples/golden_arraypool/verify_emit.py @@ -17,8 +17,8 @@ _HERE = os.path.dirname(os.path.abspath(__file__)) sys.path.insert(0, os.path.join(_HERE, "..", "..")) -from ownlang.parser import parse # noqa: E402 -from ownlang.codegen import generate # noqa: E402 +from ownlang.codegen import generate # noqa: E402 +from ownlang.parser import parse # noqa: E402 def _method_lines(text: str) -> list[str]: diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 9f4febb0..ca6588b9 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -12,15 +12,19 @@ from __future__ import annotations import sys +from typing import TYPE_CHECKING + +if TYPE_CHECKING: + from .cfg import Instr -from .parser import parse, ParseError -from .lexer import LexError -from .cfg import build_cfg, collect_signatures, collect_policies, CFG from .analysis import analyze -from .codegen import generate from .buffers import validate_policies -from .report import build_report, render_report +from .cfg import CFG, build_cfg, collect_policies, collect_signatures +from .codegen import generate from .diagnostics import Diagnostic, Severity +from .lexer import LexError +from .parser import ParseError, parse +from .report import build_report, render_report def _collect(src: str) -> tuple[list[Diagnostic], object | None]: @@ -120,9 +124,18 @@ def _print_cfg(cfg: CFG) -> None: print() -def _fmt_instr(ins) -> str: - from .cfg import (Acquire, AcquireBuffer, MoveInto, Release, Use, Invoke, - BorrowStart, BorrowEnd, Return) +def _fmt_instr(ins: Instr) -> str: + from .cfg import ( + Acquire, + AcquireBuffer, + BorrowEnd, + BorrowStart, + Invoke, + MoveInto, + Release, + Return, + Use, + ) if isinstance(ins, Acquire): return f"acquire {ins.sym.name} : {ins.resource}" if isinstance(ins, AcquireBuffer): @@ -152,7 +165,7 @@ def _fmt_instr(ins) -> str: def _read(path: str) -> str: - with open(path, "r", encoding="utf-8") as f: + with open(path, encoding="utf-8") as f: return f.read() diff --git a/ownlang/analysis.py b/ownlang/analysis.py index b681a75c..c75a5f52 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -35,13 +35,25 @@ from dataclasses import dataclass, field from enum import Enum, auto +from typing import assert_never +from .ast_nodes import Effect from .cfg import ( - CFG, Block, Symbol, Kind, - Acquire, AcquireBuffer, MoveInto, Release, Use, Invoke, - BorrowStart, BorrowEnd, Return, + CFG, + Acquire, + AcquireBuffer, + Block, + BorrowEnd, + BorrowStart, + Instr, + Invoke, + Kind, + MoveInto, + Release, + Return, + Symbol, + Use, ) -from .ast_nodes import Effect from .diagnostics import Diagnostic @@ -70,7 +82,7 @@ class State: var: dict[int, set[VarState]] = field(default_factory=dict) loans: dict[int, Loan] = field(default_factory=dict) - def copy(self) -> "State": + def copy(self) -> State: return State( var={k: set(v) for k, v in self.var.items()}, loans=dict(self.loans), @@ -167,7 +179,7 @@ def topo_order(self) -> list[int]: continue reachable.add(x) stack.extend(self.blocks[x].succ) - local_indeg = {b: 0 for b in reachable} + local_indeg = dict.fromkeys(reachable, 0) for b in reachable: for s in self.blocks[b].succ: if s in reachable: @@ -265,7 +277,7 @@ def transfer(self, blk: Block, st: State) -> State: self.step(ins, st) return st - def step(self, ins, st: State) -> None: + def step(self, ins: Instr, st: State) -> None: if isinstance(ins, Acquire): st.var[id(ins.sym)] = {VarState.OWNED} return @@ -283,7 +295,7 @@ def step(self, ins, st: State) -> None: if isinstance(ins, Release): subj = ins.sym.origin S = st.var.get(id(ins.sym), {VarState.OWNED}) - if S == {VarState.RELEASED}: + if {VarState.RELEASED} == S: self.err("OWN003", f"'{ins.sym.name}' is released twice", ins.line, subject=subj) elif VarState.RELEASED in S: @@ -374,7 +386,7 @@ def step(self, ins, st: State) -> None: st.var[id(ins.sym)] = {VarState.ESCAPED} return - raise AssertionError(f"unknown instr {ins!r}") + assert_never(ins) # -- permission checks -------------------------------------------------- diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index 33110275..d140b71a 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -49,7 +49,7 @@ class VarRef: class Acquire: """acquire Resource(args) -> Owned""" resource: str - args: list["Expr"] + args: list[Expr] line: int @@ -68,12 +68,12 @@ class BufferIntent: named option (inline, max, fallback, clear, trace, counters, policy) to its value expression. `ns` is the namespace as written (must be "Buffer").""" mode: str - size: "Expr | None" - options: dict[str, "Expr"] + size: Expr | None + options: dict[str, Expr] line: int ns: str = "Buffer" col: int = 0 - dups: tuple = () # option names that appeared more than once + dups: tuple[str, ...] = () # option names that appeared more than once Expr = IntLit | VarRef | Acquire | Move | BufferIntent @@ -107,7 +107,7 @@ class Use: class Call: """callee(args); -> a call to a declared extern or local fn""" callee: str - args: list["Expr"] + args: list[Expr] line: int @@ -116,7 +116,7 @@ class BorrowBlock: owner: str binding: str kind: BorrowKind - body: list["Stmt"] + body: list[Stmt] line: int @@ -124,8 +124,8 @@ class BorrowBlock: class If: # condition is intentionally opaque: we model control flow, not values cond_text: str - then_body: list["Stmt"] - else_body: list["Stmt"] + then_body: list[Stmt] + else_body: list[Stmt] line: int @@ -200,7 +200,7 @@ class PolicyDecl: name: str settings: dict[str, object] line: int - dups: tuple = () # setting keys that appeared more than once + dups: tuple[str, ...] = () # setting keys that appeared more than once @dataclass diff --git a/ownlang/buffers.py b/ownlang/buffers.py index 46e82e47..8d0d63f6 100644 --- a/ownlang/buffers.py +++ b/ownlang/buffers.py @@ -113,7 +113,7 @@ def size_is_const(self) -> bool: def escape_policy(self) -> str: return "local-only" if self.stack_backed else "movable" - def branches(self) -> list[dict]: + def branches(self) -> list[dict[str, str]]: """The runtime backend branches, for the compile-time report.""" if self.mode == BufferMode.SCRATCH and self.fallback_pool: return [ @@ -136,7 +136,7 @@ class Policy: name: str settings: dict[str, object] = field(default_factory=dict) line: int = 0 - dups: tuple = () # setting keys that appeared more than once + dups: tuple[str, ...] = () # setting keys that appeared more than once # -------------------------------------------------------------------------- @@ -144,11 +144,11 @@ class Policy: # -------------------------------------------------------------------------- -def _as_int(expr) -> int | None: +def _as_int(expr: object) -> int | None: return expr.value if isinstance(expr, A.IntLit) else None -def _as_ident(expr) -> str | None: +def _as_ident(expr: object) -> str | None: return expr.name if isinstance(expr, A.VarRef) else None @@ -177,7 +177,7 @@ def validate_policies(policies: dict[str, Policy]) -> list[Diagnostic]: return diags -def resolve(intent: "A.BufferIntent", policies: dict[str, Policy] +def resolve(intent: A.BufferIntent, policies: dict[str, Policy] ) -> tuple[BufferInfo, list[Diagnostic]]: """Resolve one buffer intent against the available policies. Returns the metadata plus any policy/bound diagnostics (OWN019/021/023). Always returns @@ -299,8 +299,11 @@ def first_int(sources: list[tuple[bool, str]], label: str, f"invalid 'max' value '{_fallback_token(opts['max'])}'; " f"expected an integer", line)) else: - mx_val = (_as_int(opts["max"]) if "max" in opts + mx_raw = (_as_int(opts["max"]) if "max" in opts else opt_int("max_bytes", -1)) + # the `"max" in opts and _as_int(...) is None` case is handled in + # the branch above, so mx_raw is a concrete int here. + mx_val = mx_raw if mx_raw is not None else -1 if mx_val < 0: diags.append(Diagnostic( "OWN021", @@ -395,7 +398,7 @@ def first_int(sources: list[tuple[bool, str]], label: str, return info, diags -def _fallback_token(v) -> str: +def _fallback_token(v: object) -> str: """Render a fallback value (an AST expr from an inline option, or a Python value from a policy) as a display token for validation/diagnostics.""" if isinstance(v, A.IntLit): @@ -407,8 +410,8 @@ def _fallback_token(v) -> str: return str(v) -def _bool_flag(opt_expr, policy_val, default: bool, label: str, - diags, line: int) -> bool: +def _bool_flag(opt_expr: object, policy_val: object, default: bool, label: str, + diags: list[Diagnostic], line: int) -> bool: # a malformed boolean (a typo like `ture`, or any non-bool) must be rejected, # not silently treated as the default — for a sensitive buffer that would # quietly turn off clear-on-release. @@ -438,7 +441,8 @@ def _bool_flag(opt_expr, policy_val, default: bool, label: str, _TRACE_OFF = ("off", "none", "false") -def _trace_flag(opt_expr, policy_val, default: bool, diags, line: int) -> bool: +def _trace_flag(opt_expr: object, policy_val: object, default: bool, + diags: list[Diagnostic], line: int) -> bool: # `trace = debug` / `trace = off` / `trace = false`; on/off/none/true/false # toggle the (Conditional) hooks. A malformed value is rejected, not assumed # on. An inline option wins over the policy value. diff --git a/ownlang/cfg.py b/ownlang/cfg.py index 4bf92f21..a1de65a8 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -22,12 +22,13 @@ from dataclasses import dataclass, field from enum import Enum, auto +from typing import assert_never from . import ast_nodes as A from .ast_nodes import Effect +from .buffers import MODE_NAMES, BufferInfo, Policy +from .buffers import resolve as resolve_buffer from .diagnostics import Diagnostic -from .buffers import BufferInfo, Policy, resolve as resolve_buffer, MODE_NAMES - # --------------------------------------------------------------------------- # Symbols & kinds @@ -115,7 +116,7 @@ class Invoke: """A resolved call. `args` pairs each argument's resolved Symbol (or None for a literal / unresolved) with the ownership Effect the callee applies.""" callee: str - args: list[tuple["Symbol | None", Effect]] + args: list[tuple[Symbol | None, Effect]] line: int @@ -231,7 +232,8 @@ def pop_scope(self) -> None: self.scopes.pop() def declare(self, name: str, kind: Kind, line: int, *, - is_param_borrow=False, borrow_is_mut=None) -> Symbol: + is_param_borrow: bool = False, + borrow_is_mut: bool | None = None) -> Symbol: for sc in self.scopes: if name in sc: self.diags.append(Diagnostic( @@ -289,11 +291,12 @@ def build(self) -> CFG: ) def lower_seq(self, stmts: list[A.Stmt], cur: Block) -> Block | None: + node: Block | None = cur for st in stmts: - if cur is None: + if node is None: return None - cur = self.lower_stmt(st, cur) - return cur + node = self.lower_stmt(st, node) + return node def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: if isinstance(st, A.Let): @@ -322,7 +325,7 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: return self.lower_if(st, cur) if isinstance(st, A.Return): return self.lower_return(st, cur) - raise AssertionError(f"unknown stmt {st!r}") + assert_never(st) def lower_let(self, st: A.Let, cur: Block) -> Block: rhs = st.rhs diff --git a/ownlang/codegen.py b/ownlang/codegen.py index dc3c263e..0583e2e9 100644 --- a/ownlang/codegen.py +++ b/ownlang/codegen.py @@ -28,8 +28,12 @@ from __future__ import annotations +from collections.abc import Iterator +from typing import assert_never + from . import ast_nodes as A -from .buffers import BufferMode, Policy, resolve as resolve_buffer +from .buffers import BufferInfo, BufferMode, Policy +from .buffers import resolve as resolve_buffer class CodegenError(Exception): @@ -109,7 +113,7 @@ def emit(self) -> str: # -- simple (try/finally hoist) ---------------------------------------- def _emit_simple(self, stmts: list[A.Stmt]) -> str: - return "".join(l + "\n" for l in self._emit_hoist(stmts, " ")) + return "".join(line + "\n" for line in self._emit_hoist(stmts, " ")) def _emit_hoist(self, stmts: list[A.Stmt], base: str) -> list[str]: """Emit a straight-line sequence, nesting each openable resource (an @@ -127,6 +131,7 @@ def _emit_hoist(self, stmts: list[A.Stmt], base: str) -> list[str]: st = stmts[i] scope = self._scope_lowering(st) if scope is not None: + assert isinstance(st, A.Let) # only a Let opens a scope prelude, fin = scope out.extend(base + p for p in prelude) after = stmts[i + 1:] @@ -176,7 +181,7 @@ def _scope_lowering(self, st: A.Stmt) -> tuple[list[str], list[str]] | None: def _emit_inline(self, stmts: list[A.Stmt], indent: int) -> str: ind = " " * indent out = self._emit_block(stmts, ind) - return "".join(l + "\n" for l in out) + return "".join(line + "\n" for line in out) def _emit_block(self, stmts: list[A.Stmt], ind: str) -> list[str]: """Emit a statement list, lowering each buffer let by its lifetime shape. @@ -293,7 +298,8 @@ def _buffer_lowering(self, name: str, intent: A.BufferIntent pre.append(f"if ({size} <= {L})") pre.append("{") if info.trace: - pre.append(f' OwnTrace.ScratchSelected("{fn}", "{name}", {size}, {L}, "stackalloc");') + pre.append(f' OwnTrace.ScratchSelected("{fn}", "{name}", ' + f'{size}, {L}, "stackalloc");') if sc: pre.append(" OwnCounters.StackHit();") pre.append(f" {name} = {name}_backing[..{size}];") @@ -301,7 +307,8 @@ def _buffer_lowering(self, name: str, intent: A.BufferIntent pre.append("else") pre.append("{") if info.trace: - pre.append(f' OwnTrace.ScratchSelected("{fn}", "{name}", {size}, {L}, "ArrayPool");') + pre.append(f' OwnTrace.ScratchSelected("{fn}", "{name}", ' + f'{size}, {L}, "ArrayPool");') if sc: pre.append(f" OwnCounters.PoolFallback({size});") pre.append(f" {name}_rented = ArrayPool.Shared.Rent({size});") @@ -388,7 +395,7 @@ def _emit_buffer_inline(self, name: str, intent: A.BufferIntent, self.buffer_cleanup[name] = fin return [ind + p for p in pre] - def _size_expr(self, info) -> str: + def _size_expr(self, info: BufferInfo) -> str: if info.size_is_const: return str(info.size_const) if info.size_var: @@ -404,7 +411,8 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: rt = st.rhs.resource self.owned_resource[st.name] = rt args_csv = ", ".join(self._arg(x) for x in st.rhs.args) - return [f"{ind}{self._local_type(rt)} {st.name} = {self._acquire_expr(rt, args_csv)};"] + return [f"{ind}{self._local_type(rt)} {st.name} = " + f"{self._acquire_expr(rt, args_csv)};"] if isinstance(st.rhs, A.Move): # a moved buffer carries its identity to the new owner: copy the # pending cleanup to the new name (do NOT remove the original — @@ -421,6 +429,10 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: return [f"{ind}var {st.name} = {st.rhs.value};"] if isinstance(st.rhs, A.VarRef): return [f"{ind}var {st.name} = {st.rhs.name};"] + # a buffer let never reaches the plain inline emitter — buffers are + # lowered by _emit_block / _buffer_lowering before this point. + raise CodegenError( + f"buffer let {st.name!r} reached the plain inline emitter") if isinstance(st, A.Release): if st.var in self.buffer_cleanup: # a branchy buffer release: emit this buffer's real cleanup @@ -452,7 +464,7 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: return out if isinstance(st, A.Return): return [f"{ind}return {st.var};" if st.var else f"{ind}return;"] - raise CodegenError(f"cannot codegen {st!r}") + assert_never(st) # -- template helpers --------------------------------------------------- @@ -511,7 +523,7 @@ def _contains_branch_or_transfer(stmts: list[A.Stmt]) -> bool: return False -def _iter_stmts(stmts: list[A.Stmt]): +def _iter_stmts(stmts: list[A.Stmt]) -> Iterator[A.Stmt]: """Yield every statement in the tree, descending into if-branches and borrow blocks.""" for st in stmts: @@ -573,7 +585,8 @@ def _scope_body_has_plain_let(stmts: list[A.Stmt]) -> bool: if isinstance(st, A.Let) and isinstance(st.rhs, (A.Acquire, A.BufferIntent)): rel = None for k in range(i + 1, len(stmts)): - if isinstance(stmts[k], A.Release) and stmts[k].var == st.name: + s2 = stmts[k] + if isinstance(s2, A.Release) and s2.var == st.name: rel = k break body = stmts[i + 1:rel] if rel is not None else stmts[i + 1:] @@ -632,7 +645,7 @@ def _fn_has_native(stmts: list[A.Stmt]) -> bool: def _buffer_modes(mod: A.Module) -> set[str]: modes: set[str] = set() - def walk(stmts): + def walk(stmts: list[A.Stmt]) -> None: for st in stmts: if isinstance(st, A.Let) and isinstance(st.rhs, A.BufferIntent): modes.add(st.rhs.mode) diff --git a/ownlang/parser.py b/ownlang/parser.py index c279bd56..ab72a8f4 100644 --- a/ownlang/parser.py +++ b/ownlang/parser.py @@ -36,8 +36,8 @@ from __future__ import annotations -from .lexer import Tok, Token, lex from . import ast_nodes as A +from .lexer import Tok, Token, lex class ParseError(Exception): @@ -323,7 +323,7 @@ def parse_buffer_intent(self) -> A.BufferIntent: return A.BufferIntent(mode=mode, size=size, options=options, line=ns.line, ns=ns.text, col=ns.col, dups=dups) - def _buffer_arg(self, options: dict, seen: list, first: bool + def _buffer_arg(self, options: dict[str, A.Expr], seen: list[str], first: bool ) -> tuple[A.Expr | None, bool]: """Parse one buffer argument: a named option, or the leading positional size. Returns (size_expr_or_None, still_first).""" diff --git a/ownlang/report.py b/ownlang/report.py index 1b0871c3..77265ab1 100644 --- a/ownlang/report.py +++ b/ownlang/report.py @@ -15,11 +15,14 @@ from __future__ import annotations +from collections.abc import Iterator +from typing import Any + from . import ast_nodes as A -from .buffers import resolve as resolve_buffer, Policy, MODE_NAMES +from .buffers import MODE_NAMES, Policy +from .buffers import resolve as resolve_buffer from .diagnostics import Diagnostic - # Diagnostics that, if present for a given buffer, mean a specific check failed. _CHECK_CODES = { "noEscape": {"OWN015", "OWN016", "OWN017"}, @@ -29,7 +32,9 @@ } -def _walk_buffers(stmts: list[A.Stmt]): +def _walk_buffers( + stmts: list[A.Stmt], +) -> Iterator[tuple[str, A.BufferIntent]]: """Yield (let_name, BufferIntent) for every buffer intent in a statement tree, descending into if-branches and borrow blocks.""" for st in stmts: @@ -42,7 +47,7 @@ def _walk_buffers(stmts: list[A.Stmt]): yield from _walk_buffers(st.body) -def build_report(mod: A.Module, diags: list[Diagnostic]) -> dict: +def build_report(mod: A.Module, diags: list[Diagnostic]) -> dict[str, Any]: policies: dict[str, Policy] = { p.name: Policy(p.name, dict(p.settings), p.line) for p in mod.policies } @@ -55,7 +60,7 @@ def build_report(mod: A.Module, diags: list[Diagnostic]) -> dict: if d.subject is not None: by_subject.setdefault(d.subject, set()).add(d.code) - entries: list[dict] = [] + entries: list[dict[str, Any]] = [] for fn in mod.functions: for name, intent in _walk_buffers(fn.body): # skip a malformed intent (bad namespace or mode, e.g. Foo.stack / @@ -89,7 +94,7 @@ def build_report(mod: A.Module, diags: list[Diagnostic]) -> dict: return {"module": mod.name, "buffers": entries} -def render_report(report: dict) -> str: +def render_report(report: dict[str, Any]) -> str: lines: list[str] = [f"buffer report for module '{report['module']}'"] if not report["buffers"]: lines.append(" (no buffers)") diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 00000000..c4dbe98a --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,23 @@ +[project] +name = "ownlang" +version = "0.0.0" +description = "A tiny ownership / borrow / lifetime checker for a resource DSL that lowers to C#." +requires-python = ">=3.11" + +[tool.ruff] +line-length = 100 +target-version = "py311" + +[tool.ruff.lint] +# High-signal rules only. SIM (flake8-simplify) is deliberately omitted: its +# nested-if collapsing fights intentional, commented branch structure here. +# E/W pycodestyle · F pyflakes · I import order · B bugbear gotchas +# UP pyupgrade · C4 comprehensions · RUF ruff-native +select = ["E", "W", "F", "I", "B", "UP", "C4", "RUF"] + +[tool.mypy] +# The package is held to --strict. Tests/fuzzers are not (they lean on dynamic +# construction and an AST oracle); ruff still covers them. +python_version = "3.11" +files = ["ownlang"] +strict = true diff --git a/tests/run_tests.py b/tests/run_tests.py index ac1409bb..b5b42422 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -14,15 +14,14 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang.parser import parse, ParseError # noqa: E402 -from ownlang.lexer import LexError # noqa: E402 -from ownlang.cfg import (build_cfg, collect_signatures, # noqa: E402 - collect_policies) -from ownlang.analysis import analyze # noqa: E402 -from ownlang.diagnostics import Severity # noqa: E402 -from ownlang.codegen import generate # noqa: E402 -from ownlang.buffers import validate_policies # noqa: E402 -from ownlang.report import build_report # noqa: E402 +from ownlang.analysis import analyze +from ownlang.buffers import validate_policies +from ownlang.cfg import build_cfg, collect_policies, collect_signatures +from ownlang.codegen import generate +from ownlang.diagnostics import Severity +from ownlang.lexer import LexError +from ownlang.parser import ParseError, parse +from ownlang.report import build_report PRELUDE = ( "module M\n" @@ -523,7 +522,8 @@ def buffer_smoke() -> list[str]: golden_path = os.path.join(os.path.dirname(__file__), "buffer_scratch_program.cs.txt") if os.path.exists(golden_path): - prog = open(golden_path, encoding="utf-8").read() + with open(golden_path, encoding="utf-8") as f: + prog = f.read() for s in ("public static void parse(int size)", "if (size < 0)", "ArrayPool.Shared.Rent(size)", @@ -589,7 +589,8 @@ def escape_and_length_smoke() -> list[str]: rep = build_report(parse(scratch_const), []) e = rep["buffers"][0] if e["fallback"] != "forbidden": - fails.append(f"forbidden scratch report fallback should be 'forbidden', got {e['fallback']}") + fails.append("forbidden scratch report fallback should be " + f"'forbidden', got {e['fallback']}") backends = {b["backend"] for b in e["branches"]} if backends != {"stackalloc"}: fails.append(f"forbidden scratch report should be stack-only, got {backends}") @@ -620,7 +621,7 @@ def branchy_and_malformed_smoke() -> list[str]: bogus = parse("module M\nfn f(n: int){ let b = Buffer.bogus(n); release b; }\n") try: rep = build_report(bogus, []) - except Exception as e: # noqa: BLE001 + except Exception as e: fails.append(f"report crashed on a malformed buffer mode: {type(e).__name__}: {e}") else: if rep["buffers"]: @@ -634,7 +635,7 @@ def branchy_and_malformed_smoke() -> list[str]: fails.append(f"FIFO overlapping buffers should check clean, got {codes(fifo)}") try: out = generate(parse(fifo)) - except Exception as e: # noqa: BLE001 + except Exception as e: fails.append(f"FIFO overlapping buffers crashed codegen: {type(e).__name__}: {e}") else: if out.count("ArrayPool.Shared.Return(a_array)") != 1: @@ -660,8 +661,8 @@ def branchy_and_malformed_smoke() -> list[str]: # a non-identifier fallback (fallback = 0) must likewise fail safe: OWN030 # AND no ArrayPool fallback enabled (it must not silently heap-allocate). - from ownlang.buffers import resolve as _resolve from ownlang.ast_nodes import BufferIntent, IntLit + from ownlang.buffers import resolve as _resolve intent = BufferIntent(mode="scratch", size=IntLit(8, 1), options={"fallback": IntLit(0, 1)}, line=1) info, idiags = _resolve(intent, {}) @@ -684,7 +685,7 @@ def branchy_and_malformed_smoke() -> list[str]: fails.append(f"move-then-release buffer should check clean, got {codes(moved)}") try: out = generate(parse(moved)) - except Exception as e: # noqa: BLE001 + except Exception as e: fails.append(f"move-then-release buffer crashed codegen: {type(e).__name__}: {e}") else: if out.count("ArrayPool.Shared.Return(a_array)") != 1: @@ -707,7 +708,7 @@ def branchy_and_malformed_smoke() -> list[str]: def _report_check(mod, check): """Run the full checker over a parsed module and return the named report check (True/False) for its first buffer.""" - from ownlang.cfg import build_cfg, collect_signatures, collect_policies + from ownlang.cfg import build_cfg, collect_policies, collect_signatures rn = {r.name for r in mod.resources} sg = collect_signatures(mod) pl = collect_policies(mod) @@ -757,8 +758,9 @@ def nesting_native_trace_smoke() -> list[str]: fails.append("native constant size should not emit a negative guard") # Issue 3: a policy trace = false disables tracing - from ownlang.buffers import resolve as _resolve, Policy from ownlang.ast_nodes import BufferIntent, VarRef + from ownlang.buffers import Policy + from ownlang.buffers import resolve as _resolve intent = BufferIntent(mode="scratch", size=VarRef("n", 1), options={"policy": VarRef("Quiet", 1)}, line=1) pol = {"Quiet": Policy("Quiet", {"trace": False, "counters": True})} @@ -976,7 +978,7 @@ def run() -> int: continue try: generate(parse(PRELUDE + body)) - except Exception as e: # noqa: BLE001 + except Exception as e: cg_fail += 1 print(f"CODEGEN FAIL {name}: {type(e).__name__}: {e}") @@ -1022,19 +1024,19 @@ def run() -> int: # Content-level codegen assertions + property fuzzer: these inspect the # generated C# itself (release placement/count, declaration order), catching # lowerings that are silently wrong rather than ones that merely throw. - import test_codegen # noqa: E402 (lives in this directory) + import test_codegen cc_rc = test_codegen.run() - import test_codegen_props # noqa: E402 + import test_codegen_props pf_rc = test_codegen_props.run(iterations=3000, seed=1234) # The "what it catches" gallery: every examples/gallery/ file must still # produce exactly the diagnostic it advertises, so the demo can't drift. - import test_gallery # noqa: E402 + import test_gallery gl_rc = test_gallery.run() # Real-world corpus: each case.own (a reduction of a real ArrayPool/Dispose # bug) must still produce the diagnostics it documents. - import test_corpus # noqa: E402 + import test_corpus co_rc = test_corpus.run() return 1 if (failed or cg_fail or golden_fails or buffer_fails diff --git a/tests/test_codegen.py b/tests/test_codegen.py index e139d069..7de297e1 100644 --- a/tests/test_codegen.py +++ b/tests/test_codegen.py @@ -23,12 +23,11 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang.parser import parse # noqa: E402 -from ownlang.cfg import build_cfg, collect_signatures # noqa: E402 -from ownlang.analysis import analyze # noqa: E402 -from ownlang.diagnostics import Severity # noqa: E402 -from ownlang.codegen import generate # noqa: E402 - +from ownlang.analysis import analyze +from ownlang.cfg import build_cfg, collect_signatures +from ownlang.codegen import generate +from ownlang.diagnostics import Severity +from ownlang.parser import parse # Schematic prelude: resource Buffer renders as Buffer.rent(...) / x.give(). SCHEMATIC = ( @@ -89,23 +88,23 @@ def __init__(self, name: str, prelude: str, fn_src: str): # -- assertions --------------------------------------------------------- - def has(self, needle: str) -> "Check": + def has(self, needle: str) -> Check: if needle not in self.cs: self.fails.append(f"expected to contain {needle!r}") return self - def lacks(self, needle: str) -> "Check": + def lacks(self, needle: str) -> Check: if needle in self.cs: self.fails.append(f"expected NOT to contain {needle!r}") return self - def count(self, needle: str, n: int) -> "Check": + def count(self, needle: str, n: int) -> Check: got = self.cs.count(needle) if got != n: self.fails.append(f"expected {needle!r} x{n}, got x{got}") return self - def before(self, a: str, b: str) -> "Check": + def before(self, a: str, b: str) -> Check: """`a` must appear, and its first occurrence must precede `b`'s.""" ia, ib = self.cs.find(a), self.cs.find(b) if ia < 0: @@ -116,7 +115,7 @@ def before(self, a: str, b: str) -> "Check": self.fails.append(f"ordering: expected {a!r} before {b!r}") return self - def release_is_hoisted(self, give: str) -> "Check": + def release_is_hoisted(self, give: str) -> Check: """`give` (a release call) must sit inside a `finally`, exactly once, and not also be duplicated in the `try` body.""" self.has("try").has("finally").count(give, 1) diff --git a/tests/test_codegen_props.py b/tests/test_codegen_props.py index 0335a110..e52a6dff 100644 --- a/tests/test_codegen_props.py +++ b/tests/test_codegen_props.py @@ -40,13 +40,12 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang import ast_nodes as A # noqa: E402 -from ownlang.parser import parse # noqa: E402 -from ownlang.cfg import build_cfg, collect_signatures # noqa: E402 -from ownlang.analysis import analyze # noqa: E402 -from ownlang.diagnostics import Severity # noqa: E402 -from ownlang.codegen import generate # noqa: E402 - +from ownlang import ast_nodes as A +from ownlang.analysis import analyze +from ownlang.cfg import build_cfg, collect_signatures +from ownlang.codegen import generate +from ownlang.diagnostics import Severity +from ownlang.parser import parse PRELUDE = ( "module M\n" @@ -76,7 +75,6 @@ def fresh(self, p: str) -> str: def fn(self) -> tuple[str, set[str]]: """Return (function source, coverage-tags hit).""" self.coverage = set() - params: list[str] = [] # (name, owned?) owned: list[str] = [] # names of owned values still needing a fate lines: list[str] = [] @@ -282,7 +280,7 @@ def run(iterations: int = 4000, seed: int = 1234) -> int: try: if not _is_clean(src): continue - except Exception: # noqa: BLE001 (malformed draw -> skip) + except Exception: continue clean += 1 coverage |= cov @@ -290,7 +288,7 @@ def run(iterations: int = 4000, seed: int = 1234) -> int: mod = parse(src) try: cs = generate(mod) # P1: must not throw - except Exception as e: # noqa: BLE001 + except Exception as e: failures.append((fn_src, [f"generate threw {type(e).__name__}: {e}"])) continue diff --git a/tests/test_corpus.py b/tests/test_corpus.py index 4f62c0a9..9e836324 100644 --- a/tests/test_corpus.py +++ b/tests/test_corpus.py @@ -26,12 +26,12 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang.parser import parse, ParseError # noqa: E402 -from ownlang.lexer import LexError # noqa: E402 -from ownlang.cfg import build_cfg, collect_signatures, collect_policies # noqa: E402 -from ownlang.analysis import analyze # noqa: E402 -from ownlang.buffers import validate_policies # noqa: E402 -from ownlang.diagnostics import Severity # noqa: E402 +from ownlang.analysis import analyze +from ownlang.buffers import validate_policies +from ownlang.cfg import build_cfg, collect_policies, collect_signatures +from ownlang.diagnostics import Severity +from ownlang.lexer import LexError +from ownlang.parser import ParseError, parse _CORPUS = os.path.join(os.path.dirname(__file__), "..", "corpus", "real-world") diff --git a/tests/test_gallery.py b/tests/test_gallery.py index 0076ce50..b0910441 100644 --- a/tests/test_gallery.py +++ b/tests/test_gallery.py @@ -18,12 +18,12 @@ sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) -from ownlang.parser import parse, ParseError # noqa: E402 -from ownlang.lexer import LexError # noqa: E402 -from ownlang.cfg import build_cfg, collect_signatures, collect_policies # noqa: E402 -from ownlang.analysis import analyze # noqa: E402 -from ownlang.buffers import validate_policies # noqa: E402 -from ownlang.diagnostics import Severity, TITLES # noqa: E402 +from ownlang.analysis import analyze +from ownlang.buffers import validate_policies +from ownlang.cfg import build_cfg, collect_policies, collect_signatures +from ownlang.diagnostics import TITLES, Severity +from ownlang.lexer import LexError +from ownlang.parser import ParseError, parse _GALLERY = os.path.join(os.path.dirname(__file__), "..", "examples", "gallery") From 52fd4c913cde1e70fd0fe778125a9f7ed2a80397 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 18:40:48 +0000 Subject: [PATCH 02/10] Freeze AST node dataclasses (immutable after parse) Make every ast_nodes dataclass frozen=True. Verified no code mutates AST nodes after construction (container fields are only appended to, which frozen still allows), so this is behavior-preserving and now blocks accidental post-parse mutation at runtime. Gate + suite stay green. --- ownlang/ast_nodes.py | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index d140b71a..34f15c54 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -33,19 +33,19 @@ class TypeRef: # ---- expressions (RHS of a let, or argument) ------------------------------ -@dataclass +@dataclass(frozen=True) class IntLit: value: int line: int -@dataclass +@dataclass(frozen=True) class VarRef: name: str line: int -@dataclass +@dataclass(frozen=True) class Acquire: """acquire Resource(args) -> Owned""" resource: str @@ -53,14 +53,14 @@ class Acquire: line: int -@dataclass +@dataclass(frozen=True) class Move: """move x -> transfers ownership, invalidates x""" var: str line: int -@dataclass +@dataclass(frozen=True) class BufferIntent: """Buffer.(size, name = value, ...) -> Owned with a storage policy. `mode` is one of stack/scratch/pooled/native/inline. `size` is the @@ -82,28 +82,28 @@ class BufferIntent: # ---- statements ----------------------------------------------------------- -@dataclass +@dataclass(frozen=True) class Let: name: str rhs: Expr line: int -@dataclass +@dataclass(frozen=True) class Release: """release x; -> consumes x""" var: str line: int -@dataclass +@dataclass(frozen=True) class Use: """use x; -> reads x (owner or live borrow)""" var: str line: int -@dataclass +@dataclass(frozen=True) class Call: """callee(args); -> a call to a declared extern or local fn""" callee: str @@ -111,7 +111,7 @@ class Call: line: int -@dataclass +@dataclass(frozen=True) class BorrowBlock: owner: str binding: str @@ -120,7 +120,7 @@ class BorrowBlock: line: int -@dataclass +@dataclass(frozen=True) class If: # condition is intentionally opaque: we model control flow, not values cond_text: str @@ -129,7 +129,7 @@ class If: line: int -@dataclass +@dataclass(frozen=True) class Return: var: str | None line: int @@ -141,14 +141,14 @@ class Return: # ---- top level ------------------------------------------------------------ -@dataclass +@dataclass(frozen=True) class ResourceMember: role: str # "acquire" | "release" name: str line: int -@dataclass +@dataclass(frozen=True) class ResourceDecl: name: str members: list[ResourceMember] @@ -161,7 +161,7 @@ class ResourceDecl: emit_borrow: str | None = None # e.g. "{0}.AsSpan()" -@dataclass +@dataclass(frozen=True) class EffectParam: """A positional parameter of an extern fn: an effect + a resource/plain type.""" effect: Effect @@ -169,7 +169,7 @@ class EffectParam: line: int -@dataclass +@dataclass(frozen=True) class ExternDecl: name: str params: list[EffectParam] @@ -177,14 +177,14 @@ class ExternDecl: line: int -@dataclass +@dataclass(frozen=True) class Param: name: str type: TypeRef line: int -@dataclass +@dataclass(frozen=True) class FnDecl: name: str params: list[Param] @@ -193,7 +193,7 @@ class FnDecl: line: int -@dataclass +@dataclass(frozen=True) class PolicyDecl: """policy Name { key = value; ... } — a named bundle of buffer defaults (inline_bytes, max_bytes, mode, fallback, trace, counters, clear_on_release).""" @@ -203,7 +203,7 @@ class PolicyDecl: dups: tuple[str, ...] = () # setting keys that appeared more than once -@dataclass +@dataclass(frozen=True) class Module: name: str resources: list[ResourceDecl] = field(default_factory=list) From 537909edd8611d616801894152b7553608f6863a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 19:21:49 +0000 Subject: [PATCH 03/10] docs: design for the lifetimes module (WPF leak / lifetime checker) Captures the direction before touching the parser: reframe reachability as linear ownership (Subscribe returns an Owned token that must be Disposed), proof that the core WPF leak already trips OWN001 today, the lifetime-region syntax for the genuinely-new part, an OWN-WPF code catalogue mapped to slices, and the honesty/scope caveats. Two open forks left for sign-off. --- docs/lifetimes.md | 138 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100644 docs/lifetimes.md diff --git a/docs/lifetimes.md b/docs/lifetimes.md new file mode 100644 index 00000000..efaf0178 --- /dev/null +++ b/docs/lifetimes.md @@ -0,0 +1,138 @@ +# OwnSharp Lifetimes — модуль `lifetimes` (design) + +> Статус: **draft на согласование.** Описывает, куда растёт PoC после ownership/ +> borrow-ядра. Код ещё не написан — это контракт на синтаксис и границы слайсов, +> чтобы не трогать парсер вслепую. + +## 1. Зачем + +Performance-профиль (`stackalloc`/`scratch`/pool) — это «игрушка для +performance-зоопарка». Бизнес-софт чаще умирает не от того, что `Span` на +7 нс медленнее, а от того, что `CustomerWindowViewModel` висит в памяти весь +день: кто-то подписался на singleton-event и не отписался. Окно закрыто, а +ViewModel жива — зомби с `INotifyPropertyChanged`. GC не телепат: объект +достижим из app-lifetime root через `EventBus -> delegate -> VM.OnChanged -> VM`, +значит он не мусор. + +Цель модуля: **статический lifetime/ownership-чекер для .NET-ресурсов**, который +говорит «кто кого держит, кто обязан отпустить, и почему закрытое окно не +умирает» — с фокусом на WPF-утечки (подписки, таймеры, кэши, `IDisposable`). + +Архитектура — **модульный монолит** с platform-agnostic ядром: + +``` +ownlang/ + core states/lattice/dataflow/diagnostics (= нынешние analysis/cfg/diagnostics) + buffers профиль OwnSharp.Performance (есть) + lifetimes профиль OwnSharp.Lifetimes (этот док) + frontend/csharp Roslyn-ингест (далёкая фаза) +``` + +## 2. Ключевая идея: reachability → linear ownership + +«VM стала достижима из AppLifetime через подписку» — это по-честному +escape/reachability-анализ через хранимые ссылки между объектами, тяжелее нашего +intra-procedural flow. Но есть сворачивание, и оно же — в самой модели WPF: + +> `Subscribe` возвращает **`Owned`**, который **обязан быть +> released в `Dispose`**. + +Эта формулировка переводит проблему достижимости обратно в **линейную +ownership-дисциплину**, которую ядро уже делает: «owned-ресурс не released на всех +путях» = `OWN001`. То есть бóльшая часть бизнес-ценности достаётся +**переиспользованием** проверенного движка, а не новой тяжёлой аналитикой. + +## 3. Что УЖЕ выразимо сегодня (без изменений языка) + +Моделируем ViewModel как **scope функции**: «поля» = owned-ресурсы, которые она +держит; «`Dispose`» = конец scope, где всё обязано быть отпущено. Тогда: + +```ownlang +resource Subscription { // токен подписки + acquire Subscribe // bus.Subscribe(handler) -> token + release Dispose // token.Dispose() +} + +fn CustomerViewModel_buggy(bus: int) { + let token = acquire Subscription(bus); + // нет Dispose -> bus держит VM живой +} +``` + +Сегодняшний вывод чекера, дословно: + +```text +$ python -m ownlang check vm.own +vm.own:12:9: error: [OWN001] 'token' is owned but not released at end of function + 12 | let token = acquire Subscription(bus); + ^ +``` + +Симметрично: использование после `Dispose` → `OWN002` (use-after-release), +двойной `Dispose` → `OWN003`. **Главный класс WPF-утечек ядро ловит уже сейчас.** +Это и делает slice #1 дешёвым: его задача — не новый анализ, а *доказать +корпусом*, что ownership-логика ложится на реальные WPF-баги, и дать +WPF-ориентированную подачу. + +## 4. Что НОВОЕ (нужен дизайн): lifetime-регионы + +Чего текущая модель не выражает — **порядок времён жизни** и утечку из короткого +региона в длинный. Предлагаемый синтаксис: + +```ownlang +lifetime App; +lifetime Window < App; // Window строго короче App +lifetime ViewModel < Window; +``` + +`<` задаёт строгий частичный порядок (DAG, без циклов — проверяется в +`__post_init__`/резолвере: вот первый *настоящий* меж-полевой инвариант, ради +которого post_init окупается). Объект из короткого региона, ставший достижимым из +длинного через strong-подписку, — это `WPF010` (lifetime promotion), если нет +owned-токена с гарантированным release. Это **slice #2**: тут появляется +региональная аннотация на параметрах (`[Lifetime("App")] bus`) и проверка +«source_lifetime > listener_lifetime ⇒ нужен токен». + +## 5. Каталог кодов (OWN-WPF) и куда какой слайс + +| Код | Смысл | Сводится к | Слайс | +|-----|-------|-----------|-------| +| WPF004 | `Subscribe` вернул owned-токен, результат проигнорирован → утечёт | `OWN001` | **#1** | +| WPF005 | `IDisposable`-поле требует `VM : IDisposable` + cascade `Dispose` | `OWN001`/`OWN002` | **#1** | +| WPF002 | `DispatcherTimer`/`Timer` в VM требует `Stop`+detach | `OWN001` | #1/#2 | +| WPF008 | `CollectionChanged`/`PropertyChanged` подписка без отписки | `OWN001` | #2 | +| WPF010 | объект ушёл из короткого lifetime в длинный (region escape) | новый region-анализ | **#2** | +| WPF003 | static-подписка запрещена без weak | region + policy | #2 | +| WPF001/006/007/009 | event+= / DataContext / lambda-capture / static cache | region + capture-анализ | позже | + +MVP (slice #1) сознательно сводит WPF004/005/002 к уже-работающим OWN-кодам. +Региональная половина (WPF010 и зависящие) — slice #2. + +## 6. Слайсы + +- **slice #1 (сейчас):** WPF-корпус `corpus/wpf/` (zombie-VM, незакрытый таймер, + disposable-поле) на текущем движке + WPF-галерея + self-checking тест. Опционально + — тонкий WPF-флейвор слой над диагностиками (см. развилку B). +- **slice #2:** lifetime-регионы (`lifetime A < B;`), region-escape-анализ, WPF010. +- **slice #3 (далеко):** узкий Roslyn-frontend — pattern matcher (`event +=`, + `Subscribe`, `DispatcherTimer`, `IDisposable`-поля) → кормит это же ядро. + Не «ингест всего C#» (это человеко-годы), а распознавание известных паттернов. + +## 7. Открытые развилки (на согласование) + +- **A. Синтаксис регионов:** `lifetime Window < App;` (короче-чем). Альтернатива — + `lifetime Window inside App;`. Решает читаемость. +- **B. MVP-подача:** выдавать ли в slice #1 WPF-специфичные коды (`WPF004: + subscription token never disposed`) или переиспользовать `OWN001/002` с + WPF-формулировкой в корпусе/нотах. Первое — лучше UX и «продаваемость», стоит + тонкого слоя «вид ресурса = subscription/timer». Второе — ноль нового кода. + +## 8. Честность / scope + +- `case.own` — **hand reduction** WPF-паттерна, не C#, который чекер съел: фронта + C# нет (slice #3). Корпус показывает, что ownership-логика **ложится** на + реальный баг, а не что инструмент просканировал реальный код. +- Финализаторы тут не лечат причину: объект, удерживаемый event/static-ссылкой, + до финализации не доходит. Полезны только как debug-sentinel — вне scope ядра. +- Weak events — отдельная policy в slice #2, не серебряная пуля (таймеры, + unmanaged, кэши всё равно требуют ownership). From e95e631df5dbf1f44b65c87040d7957fff64e872 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 19:43:39 +0000 Subject: [PATCH 04/10] lifetimes slice #1: WPF leak corpus via resource-kind metadata The core ownership checker already catches the main class of WPF lifetime leaks once a ViewModel is modelled as a scope (constructor = scope start, Dispose = scope end): a subscription/timer that is never disposed is OWN001, touched after dispose is OWN002. Slice #1 makes that usable without inventing WPF-specific codes: - resource declarations gain an optional, contextual 'kind "..."' attribute (no new reserved word). It is domain-neutral metadata threaded onto the owning Symbol and surfaced on diagnostics as a '[resource: ]' suffix -- the seam a later WPF profile / Roslyn front-end keys off, with the core staying generic. - corpus/wpf/: two self-checking real-pattern cases (zombie ViewModel -> OWN001, handler-use-after-dispose -> OWN002) with before/after C#, case.own, expected codes and honesty notes; tests/test_wpf.py pins both the codes AND that the kind tag reaches rendered output. - docs/lifetimes.md captures the full module plan (lifetime regions, OWN-WPF catalogue, slice boundaries); README gains a business-application section. - bonus: assert_never now also guards lower_let's rhs dispatch; the strict gate caught a real 'kind' name collision in analysis.step during this work. Gate + suite green: analysis 123/123, codegen 23/23, fuzz, gallery 10/10, corpus 2/2, wpf 2/2. --- README.md | 34 +++++ corpus/wpf/handler-use-after-dispose/after.cs | 27 ++++ .../wpf/handler-use-after-dispose/before.cs | 29 +++++ corpus/wpf/handler-use-after-dispose/case.own | 17 +++ .../expected-diagnostics.txt | 1 + corpus/wpf/handler-use-after-dispose/notes.md | 24 ++++ corpus/wpf/zombie-viewmodel/after.cs | 19 +++ corpus/wpf/zombie-viewmodel/before.cs | 19 +++ corpus/wpf/zombie-viewmodel/case.own | 18 +++ .../zombie-viewmodel/expected-diagnostics.txt | 1 + corpus/wpf/zombie-viewmodel/notes.md | 36 ++++++ ownlang/__main__.py | 5 +- ownlang/analysis.py | 36 ++++-- ownlang/ast_nodes.py | 5 + ownlang/cfg.py | 24 +++- ownlang/diagnostics.py | 12 +- ownlang/parser.py | 11 +- tests/run_tests.py | 7 +- tests/test_wpf.py | 122 ++++++++++++++++++ 19 files changed, 423 insertions(+), 24 deletions(-) create mode 100644 corpus/wpf/handler-use-after-dispose/after.cs create mode 100644 corpus/wpf/handler-use-after-dispose/before.cs create mode 100644 corpus/wpf/handler-use-after-dispose/case.own create mode 100644 corpus/wpf/handler-use-after-dispose/expected-diagnostics.txt create mode 100644 corpus/wpf/handler-use-after-dispose/notes.md create mode 100644 corpus/wpf/zombie-viewmodel/after.cs create mode 100644 corpus/wpf/zombie-viewmodel/before.cs create mode 100644 corpus/wpf/zombie-viewmodel/case.own create mode 100644 corpus/wpf/zombie-viewmodel/expected-diagnostics.txt create mode 100644 corpus/wpf/zombie-viewmodel/notes.md create mode 100644 tests/test_wpf.py diff --git a/README.md b/README.md index d362c81b..e5c36f61 100644 --- a/README.md +++ b/README.md @@ -93,6 +93,37 @@ examples/gallery/05_dispose_while_view_live.own:9:13: error: [OWN008] cannot rel ^ ``` +### Бизнес-применение: WPF lifetime-утечки (модуль `lifetimes`, slice #1) + +Performance-профиль (`stackalloc`/pool) — это игрушка для performance-зоопарка. +Бизнес-софт чаще умирает не от того, что `Span` на 7 нс медленнее, а от +зомби-ViewModel: кто-то подписался на singleton-event и не отписался — окно +закрыто, а `CustomerViewModel` жива весь день, потому что event bus держит на неё +strong-ссылку. GC не телепат. + +Ключевой разворот: **это уже выразимо текущим ownership-ядром.** Моделируем +ViewModel как scope (конструктор = начало, `Dispose` = конец); подписка = +`acquire` токена, отписка = `release`. Тогда «подписался и не Dispose» — +это обычный **OWN001**, а «тронул после Dispose» — **OWN002**. Новый, доменно- +нейтральный кусок: у `resource` появился тег `kind`, который вешается на +диагностику как `[resource: ...]` — это шов, за который позже зацепится WPF- +профиль/Roslyn-фронт, не зная про WPF в самом ядре. + +```text +$ python -m ownlang check corpus/wpf/zombie-viewmodel/case.own +case.own:16:9: error: [OWN001] 'customerChanged' is owned but not released at + end of function (leaks on at least one path) [resource: subscription token] + 16 | let customerChanged = acquire Subscription(bus); + ^ +``` + +`corpus/wpf/` — self-checking корпус реальных WPF-паттернов (`before.cs`/ +`after.cs`/`case.own`/expected), прибитый тестом `tests/test_wpf.py`. Полный план +модуля (lifetime-регионы, каталог OWN-WPF, границы слайсов, что отложено) — +в [`docs/lifetimes.md`](docs/lifetimes.md). Честно: `case.own` — hand reduction +паттерна, не C#, который чекер съел (C#-фронта нет, это поздний слайс); корпус +показывает, что ownership-**логика** ложится на реальный баг. + ### Golden-пример: настоящий ArrayPool ```bash @@ -632,12 +663,15 @@ ownlang/ gallery/ # «что оно ловит» — narrated примеры, пинятся тестом golden_arraypool/ # buffer.own + Program.cs (host-код; .csproj не входит) corpus/real-world/ # hand-reduced реальные ArrayPool-баги + expected-коды + corpus/wpf/ # WPF lifetime-баги (zombie-VM, use-after-dispose) + docs/lifetimes.md # дизайн модуля lifetimes (WPF, регионы, слайсы) tests/ run_tests.py # кейсы анализа + codegen smoke + golden smoke test_codegen.py # content-assertions на сгенерённый C# test_codegen_props.py # property-фаззер с независимым AST-оракулом test_gallery.py # пинит каждый gallery-пример к его коду test_corpus.py # пинит каждый corpus-кейс к expected-диагностикам + test_wpf.py # WPF-корпус: коды + [resource: kind] метадата pyproject.toml # gate: ruff + mypy --strict (см. ниже) ``` diff --git a/corpus/wpf/handler-use-after-dispose/after.cs b/corpus/wpf/handler-use-after-dispose/after.cs new file mode 100644 index 00000000..bbff6a30 --- /dev/null +++ b/corpus/wpf/handler-use-after-dispose/after.cs @@ -0,0 +1,27 @@ +// FIXED. The callback guards on the disposed flag (and/or the subscription is +// disposed only after the dispatcher queue is drained), so nothing touches the +// subscription-backed state after Dispose(). +public sealed class CustomerViewModel : IDisposable +{ + private readonly IDisposable _sub; + private bool _disposed; + + public CustomerViewModel(IEventBus bus) + { + _sub = bus.Subscribe(OnCustomerChanged); + } + + private void OnCustomerChanged(CustomerChanged e) + { + if (_disposed) return; // do not touch disposed state + Refresh(); + } + + private void Refresh() { /* ... */ } + + public void Dispose() + { + _disposed = true; + _sub.Dispose(); + } +} diff --git a/corpus/wpf/handler-use-after-dispose/before.cs b/corpus/wpf/handler-use-after-dispose/before.cs new file mode 100644 index 00000000..a5df40c3 --- /dev/null +++ b/corpus/wpf/handler-use-after-dispose/before.cs @@ -0,0 +1,29 @@ +// BUGGY (representative WPF pattern, hand-reduced into case.own). +// +// The VM disposes its subscription on close, but a callback that was already +// queued on the dispatcher still runs and touches the (now disposed) state. In +// real code this surfaces as an ObjectDisposedException or a read of torn state. +public sealed class CustomerViewModel : IDisposable +{ + private readonly IDisposable _sub; + private bool _disposed; + + public CustomerViewModel(IEventBus bus) + { + _sub = bus.Subscribe(OnCustomerChanged); + } + + private void OnCustomerChanged(CustomerChanged e) + { + // a late, already-dispatched callback: runs after Dispose() + Refresh(); // touches subscription-backed state after it was disposed + } + + private void Refresh() { /* reads disposed state */ } + + public void Dispose() + { + _disposed = true; + _sub.Dispose(); + } +} diff --git a/corpus/wpf/handler-use-after-dispose/case.own b/corpus/wpf/handler-use-after-dispose/case.own new file mode 100644 index 00000000..637a6e6b --- /dev/null +++ b/corpus/wpf/handler-use-after-dispose/case.own @@ -0,0 +1,17 @@ +module WpfHandlerAfterDispose + +// Same subscription-token protocol, tagged with its kind. +resource Subscription { + acquire Subscribe + release Dispose + kind "subscription token" +} + +// On window close the VM disposes (unsubscribes) its subscription, but a late +// queued callback still touches it. Using a subscription after Dispose is the +// generic use-after-release (OWN002), tagged with the resource kind. +fn CloseHandler(bus: int) { + let sub = acquire Subscription(bus); + release sub; // unsubscribed / disposed on close + use sub; // a late callback still touches it -> OWN002 +} diff --git a/corpus/wpf/handler-use-after-dispose/expected-diagnostics.txt b/corpus/wpf/handler-use-after-dispose/expected-diagnostics.txt new file mode 100644 index 00000000..3a36fa92 --- /dev/null +++ b/corpus/wpf/handler-use-after-dispose/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN002 diff --git a/corpus/wpf/handler-use-after-dispose/notes.md b/corpus/wpf/handler-use-after-dispose/notes.md new file mode 100644 index 00000000..1aad4984 --- /dev/null +++ b/corpus/wpf/handler-use-after-dispose/notes.md @@ -0,0 +1,24 @@ +# WPF subscription used after Dispose + +**Pattern:** a ViewModel unsubscribes / disposes its subscription on close, but a +callback that was already queued on the dispatcher still runs and touches the +disposed, subscription-backed state. In real code this is an +`ObjectDisposedException` or a read of torn state — the use-after-dispose cousin +of the zombie-ViewModel leak. + +**What the checker says:** using a resource after its `release` (Dispose) is the +generic **OWN002** (use after release), carrying the resource-kind tag: + +```text +$ python -m ownlang check corpus/wpf/handler-use-after-dispose/case.own +case.own:16:9: error: [OWN002] use 'sub' after it was released + [resource: subscription token] + 16 | use sub; + ^ +``` + +**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C# +the checker ingested — OwnLang has no C# front-end. It shows the ownership +*logic* maps onto the real bug; it does not model the dispatcher queue or +exception flow. `before.cs` / `after.cs` are representative, not a verbatim copy +of one PR. diff --git a/corpus/wpf/zombie-viewmodel/after.cs b/corpus/wpf/zombie-viewmodel/after.cs new file mode 100644 index 00000000..1f96bb7c --- /dev/null +++ b/corpus/wpf/zombie-viewmodel/after.cs @@ -0,0 +1,19 @@ +// FIXED. The VM stores the subscription token and disposes it, so when the VM +// is itself disposed (e.g. on window close) it drops out of the bus's reference +// set and becomes collectable. +public sealed class CustomerViewModel : IDisposable +{ + private readonly IDisposable _customerChanged; + + public CustomerViewModel(IEventBus bus) + { + _customerChanged = bus.Subscribe(OnCustomerChanged); + } + + private void OnCustomerChanged(CustomerChanged e) { /* ... */ } + + public void Dispose() + { + _customerChanged.Dispose(); // unsubscribe -> VM no longer reachable + } +} diff --git a/corpus/wpf/zombie-viewmodel/before.cs b/corpus/wpf/zombie-viewmodel/before.cs new file mode 100644 index 00000000..e9e4d070 --- /dev/null +++ b/corpus/wpf/zombie-viewmodel/before.cs @@ -0,0 +1,19 @@ +// BUGGY (representative WPF pattern, hand-reduced into corpus/wpf/case.own). +// +// CustomerViewModel subscribes to a long-lived (App-lifetime) event bus in its +// constructor and never unsubscribes. The bus holds a strong reference to the +// VM's handler, so the VM stays reachable from an App-lifetime GC root for the +// whole process: the window closes, but the ViewModel never dies. A classic +// WPF "zombie ViewModel" leak. +public sealed class CustomerViewModel +{ + public CustomerViewModel(IEventBus bus) + { + // Subscribe hands back an IDisposable token, but it is ignored. + bus.Subscribe(OnCustomerChanged); + } + + private void OnCustomerChanged(CustomerChanged e) { /* ... */ } + + // No Dispose, no unsubscribe -> the bus keeps this VM alive forever. +} diff --git a/corpus/wpf/zombie-viewmodel/case.own b/corpus/wpf/zombie-viewmodel/case.own new file mode 100644 index 00000000..385a01db --- /dev/null +++ b/corpus/wpf/zombie-viewmodel/case.own @@ -0,0 +1,18 @@ +module WpfZombieViewModel + +// A subscription token: bus.Subscribe(handler) hands you one; you must +// Dispose it to unsubscribe. `kind` tags this resource so the generic +// ownership finding carries a business-flavoured [resource: ...] note. +resource Subscription { + acquire Subscribe + release Dispose + kind "subscription token" +} + +// The ViewModel modelled as one scope: its "constructor" subscribes to the +// App-lifetime bus; the end of the scope is its Dispose. Acquiring the token +// without releasing it = the bus keeps the VM alive => leak (OWN001). +fn CustomerViewModel(bus: int) { + let customerChanged = acquire Subscription(bus); + // no `release customerChanged;` -> zombie ViewModel +} diff --git a/corpus/wpf/zombie-viewmodel/expected-diagnostics.txt b/corpus/wpf/zombie-viewmodel/expected-diagnostics.txt new file mode 100644 index 00000000..ed2a1929 --- /dev/null +++ b/corpus/wpf/zombie-viewmodel/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN001 diff --git a/corpus/wpf/zombie-viewmodel/notes.md b/corpus/wpf/zombie-viewmodel/notes.md new file mode 100644 index 00000000..d73e94af --- /dev/null +++ b/corpus/wpf/zombie-viewmodel/notes.md @@ -0,0 +1,36 @@ +# WPF zombie ViewModel (strong event subscription never disposed) + +**Pattern:** a ViewModel subscribes to a longer-lived (App-lifetime) event +bus / event aggregator in its constructor and never unsubscribes. WPF +documentation is explicit that an ordinary event subscription creates a *strong* +reference from the event source to the listener; if the source outlives the +listener and the handler is never unregistered, the listener is kept alive — +a memory leak. The window closes, but the ViewModel lives until the process +ends. This is the single most common real WPF leak. + +**What the checker says:** modelling the ViewModel as one scope (constructor = +scope start, `Dispose` = scope end), the unreleased subscription token is the +generic **OWN001** (owned resource not released on all paths), now carrying the +resource-kind tag: + +```text +$ python -m ownlang check corpus/wpf/zombie-viewmodel/case.own +case.own:16:9: error: [OWN001] 'customerChanged' is owned but not released at + end of function (leaks on at least one path) [resource: subscription token] + 16 | let customerChanged = acquire Subscription(bus); + ^ +``` + +The `[resource: subscription token]` suffix is domain-neutral metadata: the core +stays a generic ownership checker, and a later WPF profile/front-end can read the +kind to phrase this as "WPF004: subscription token never disposed" without the +core knowing anything about WPF. + +**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C# +the checker ingested — OwnLang has no C# front-end (that is a later slice). It +shows the ownership *logic* maps onto the real leak: had the VM been written in +OwnLang, the checker would have rejected it. The lifetime-region machinery that +would catch "VM promoted to App-lifetime through the subscription" (the escape +path) is a separate, later slice; here the bug is caught by plain +acquire/release accounting. `before.cs` / `after.cs` capture the pattern; they +are representative, not a verbatim copy of one PR. diff --git a/ownlang/__main__.py b/ownlang/__main__.py index ca6588b9..17496814 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -19,7 +19,7 @@ from .analysis import analyze from .buffers import validate_policies -from .cfg import CFG, build_cfg, collect_policies, collect_signatures +from .cfg import CFG, build_cfg, collect_kinds, collect_policies, collect_signatures from .codegen import generate from .diagnostics import Diagnostic, Severity from .lexer import LexError @@ -36,9 +36,10 @@ def _collect(src: str) -> tuple[list[Diagnostic], object | None]: rnames = {r.name for r in mod.resources} sigs = collect_signatures(mod) pols = collect_policies(mod) + kinds = collect_kinds(mod) diags: list[Diagnostic] = list(validate_policies(pols)) for fn in mod.functions: - cfg, d1 = build_cfg(fn, rnames, sigs, pols) + cfg, d1 = build_cfg(fn, rnames, sigs, pols, kinds) d2 = analyze(cfg) diags.extend(d1) diags.extend(d2) diff --git a/ownlang/analysis.py b/ownlang/analysis.py index c75a5f52..bb6d2027 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -117,8 +117,10 @@ def initial_state(self) -> State: return s def err(self, code: str, msg: str, line: int, - subject: str | None = None) -> None: - self.diags.append(Diagnostic(code, msg, line, subject=subject)) + subject: str | None = None, + resource_kind: str | None = None) -> None: + self.diags.append(Diagnostic(code, msg, line, subject=subject, + resource_kind=resource_kind)) # -- loan / permission helpers ----------------------------------------- @@ -144,27 +146,28 @@ def binding_live(self, st: State, sym: Symbol) -> bool: def _state_problem(self, st: State, sym: Symbol, verb: str, line: int) -> bool: S = st.var.get(id(sym), {VarState.OWNED}) subj = sym.origin + kind = sym.resource_kind if VarState.OWNED not in S: if VarState.MOVED in S: self.err("OWN005", f"{verb} '{sym.name}' after it was moved", - line, subject=subj) + line, subject=subj, resource_kind=kind) elif VarState.ESCAPED in S and VarState.RELEASED not in S: self.err("OWN002", f"{verb} '{sym.name}' after it was consumed", line, - subject=subj) + subject=subj, resource_kind=kind) else: self.err("OWN002", f"{verb} '{sym.name}' after it was released", - line, subject=subj) + line, subject=subj, resource_kind=kind) return True if S & {VarState.RELEASED, VarState.ESCAPED}: self.err("OWN009", f"{verb} '{sym.name}', which may have been released on some " - f"path", line, subject=subj) + f"path", line, subject=subj, resource_kind=kind) return True if VarState.MOVED in S: self.err("OWN010", f"{verb} '{sym.name}', which may have been moved on some " - f"path", line, subject=subj) + f"path", line, subject=subj, resource_kind=kind) return True return False @@ -249,7 +252,8 @@ def leak_check(self, st: State, at_line: int, context: str, self.err("OWN001", f"'{name}' is owned but not released {context} " f"(leaks on at least one path)", at_line, - subject=(sym.origin if sym else None)) + subject=(sym.origin if sym else None), + resource_kind=(sym.resource_kind if sym else None)) def _sym_by_id(self, symid: int) -> Symbol | None: if not hasattr(self, "_symindex"): @@ -294,20 +298,22 @@ def step(self, ins: Instr, st: State) -> None: if isinstance(ins, Release): subj = ins.sym.origin + rkind = ins.sym.resource_kind S = st.var.get(id(ins.sym), {VarState.OWNED}) if {VarState.RELEASED} == S: self.err("OWN003", f"'{ins.sym.name}' is released twice", - ins.line, subject=subj) + ins.line, subject=subj, resource_kind=rkind) elif VarState.RELEASED in S: self.err("OWN003", f"'{ins.sym.name}' may already be released on some path " - f"before this release", ins.line, subject=subj) + f"before this release", ins.line, subject=subj, + resource_kind=rkind) elif not self._state_problem(st, ins.sym, "release", ins.line): shared, mut = self.loans_on(st, ins.sym) if shared or mut: self.err("OWN008", f"cannot release '{ins.sym.name}' while it is borrowed", - ins.line, subject=subj) + ins.line, subject=subj, resource_kind=rkind) st.var[id(ins.sym)] = {VarState.RELEASED} return @@ -353,16 +359,17 @@ def step(self, ins: Instr, st: State) -> None: exclude=ins.sym) if ins.sym is not None: subj = ins.sym.origin + rkind = ins.sym.resource_kind S = st.var.get(id(ins.sym), {VarState.OWNED}) if VarState.OWNED not in S: if VarState.MOVED in S: self.err("OWN005", f"'{ins.sym.name}' returned after it was moved", - ins.line, subject=subj) + ins.line, subject=subj, resource_kind=rkind) else: self.err("OWN002", f"'{ins.sym.name}' returned after it was released", - ins.line, subject=subj) + ins.line, subject=subj, resource_kind=rkind) else: # returning an owner is an escape (consume): it needs Own # permission, so a live loan on it is OWN007, just like move. @@ -370,7 +377,8 @@ def step(self, ins: Instr, st: State) -> None: if shared or mut: self.err("OWN007", f"cannot return '{ins.sym.name}' while it is " - f"borrowed", ins.line, subject=subj) + f"borrowed", ins.line, subject=subj, + resource_kind=rkind) elif ins.sym.buffer is not None and ins.sym.buffer.stack_backed: self.err("OWN015", f"'{ins.sym.name}' is a {ins.sym.buffer.mode.value} " diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index 34f15c54..e7af1329 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -159,6 +159,11 @@ class ResourceDecl: emit_acquire: str | None = None # e.g. "ArrayPool.Shared.Rent({args})" emit_release: str | None = None # e.g. "ArrayPool.Shared.Return({0})" emit_borrow: str | None = None # e.g. "{0}.AsSpan()" + # an optional human "kind" of resource (e.g. "subscription token", "timer"), + # carried onto diagnostics as `[resource: ]`. Domain-neutral metadata: + # a later profile (e.g. WPF) reads it to give the generic OWN finding a + # business-flavoured framing, without the core knowing about any domain. + kind: str | None = None @dataclass(frozen=True) diff --git a/ownlang/cfg.py b/ownlang/cfg.py index a1de65a8..7dc41107 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -60,6 +60,11 @@ class Symbol: # the declared/inferred type name (e.g. "int", "bool", a resource name), so a # buffer size can be required to be an integer. None when unknown. type_name: str | None = None + # the resource's optional human "kind" (e.g. "subscription token"), copied + # from its ResourceDecl at acquire / on an owned parameter. Surfaced on + # diagnostics as `[resource: ]`; None for plain values and untagged + # resources. + resource_kind: str | None = None # a stable identity for the originating buffer (name#line). Set when a buffer # is acquired and inherited across `move`, so a diagnostic about any alias can # be attributed to the right buffer in the report (distinct from a same-named @@ -213,11 +218,13 @@ def collect_signatures(mod: A.Module) -> dict[str, Signature]: class _Builder: def __init__(self, fn: A.FnDecl, resource_names: set[str], signatures: dict[str, Signature], - policies: dict[str, Policy] | None = None): + policies: dict[str, Policy] | None = None, + resource_kinds: dict[str, str] | None = None): self.fn = fn self.resource_names = resource_names self.signatures = signatures self.policies = policies or {} + self.resource_kinds = resource_kinds or {} self.diags: list[Diagnostic] = [] self.blocks: list[Block] = [] self.scopes: list[dict[str, Symbol]] = [] @@ -271,6 +278,7 @@ def build(self) -> CFG: else: sym = self.declare(p.name, Kind.PLAIN, p.line) sym.type_name = p.type.name + sym.resource_kind = self.resource_kinds.get(p.type.name) self.params.append(sym) entry = self.new_block("entry") @@ -335,6 +343,7 @@ def lower_let(self, st: A.Let, cur: Block) -> Block: "OWN030", f"undefined resource '{rhs.resource}'", rhs.line)) sym = self.declare(st.name, Kind.OWNED, st.line) sym.type_name = rhs.resource + sym.resource_kind = self.resource_kinds.get(rhs.resource) cur.instrs.append(Acquire(sym, rhs.resource, st.line)) return cur if isinstance(rhs, A.BufferIntent): @@ -355,6 +364,7 @@ def lower_let(self, st: A.Let, cur: Block) -> Block: dst.buffer = src.buffer dst.origin = src.origin dst.type_name = src.type_name # the moved value keeps its type + dst.resource_kind = src.resource_kind # ...and its kind tag cur.instrs.append(MoveInto(dst, src, st.line)) return cur if isinstance(rhs, A.VarRef): @@ -372,7 +382,7 @@ def lower_let(self, st: A.Let, cur: Block) -> Block: dst = self.declare(st.name, Kind.PLAIN, st.line) dst.type_name = "int" return cur - raise AssertionError(f"unknown rhs {rhs!r}") + assert_never(rhs) def lower_buffer(self, st: A.Let, rhs: A.BufferIntent, cur: Block) -> Block: if rhs.ns != "Buffer": @@ -561,8 +571,14 @@ def collect_policies(mod: A.Module) -> dict[str, Policy]: def build_cfg(fn: A.FnDecl, resource_names: set[str], signatures: dict[str, Signature], - policies: dict[str, Policy] | None = None + policies: dict[str, Policy] | None = None, + resource_kinds: dict[str, str] | None = None ) -> tuple[CFG, list[Diagnostic]]: - b = _Builder(fn, resource_names, signatures, policies) + b = _Builder(fn, resource_names, signatures, policies, resource_kinds) cfg = b.build() return cfg, b.diags + + +def collect_kinds(mod: A.Module) -> dict[str, str]: + """resource name -> its declared `kind` string (only those that set one).""" + return {r.name: r.kind for r in mod.resources if r.kind} diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 1e51d607..80879a84 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -78,11 +78,18 @@ class Diagnostic: # for buffer diagnostics: a stable identity (name#line) of the buffer the # diagnostic is about, so the report attributes it by symbol, not by name. subject: str | None = None + # the resource's human "kind" (e.g. "subscription token"), when the finding + # is about a tagged resource. Rendered as a ` [resource: ]` suffix — + # domain-neutral metadata a later profile (e.g. WPF) keys off. + resource_kind: str | None = None @property def title(self) -> str: return TITLES.get(self.code, "") + def _kind_suffix(self) -> str: + return f" [resource: {self.resource_kind}]" if self.resource_kind else "" + def _caret_col(self, src_line: str) -> int | None: """1-based column of this diagnostic in `src_line`: the position of the identifier it names. None if it cannot be located.""" @@ -104,7 +111,7 @@ def render(self, filename: str = "") -> str: """Plain one-line rendering: `file:line: severity: [code] message`.""" return ( f"{filename}:{self.line}: {self.severity.value}: " - f"[{self.code}] {self.message}" + f"[{self.code}] {self.message}{self._kind_suffix()}" ) def render_pretty(self, filename: str, source: str) -> str: @@ -115,7 +122,8 @@ def render_pretty(self, filename: str, source: str) -> str: src_line = lines[self.line - 1] if 1 <= self.line <= len(lines) else "" col = self._caret_col(src_line) loc = f"{filename}:{self.line}" + (f":{col}" if col else "") - out = [f"{loc}: {self.severity.value}: [{self.code}] {self.message}"] + out = [f"{loc}: {self.severity.value}: [{self.code}] " + f"{self.message}{self._kind_suffix()}"] if src_line.strip(): gutter = f" {self.line} | " out.append(f"{gutter}{src_line}") diff --git a/ownlang/parser.py b/ownlang/parser.py index ab72a8f4..d4b98cf1 100644 --- a/ownlang/parser.py +++ b/ownlang/parser.py @@ -8,6 +8,7 @@ resource := "resource" IDENT "{" rmember* "}" rmember := ("acquire" | "release") IDENT | ("emit_type"|"emit_acquire"|"emit_release"|"emit_borrow") STRING + | "kind" STRING // contextual; not reserved policy := "policy" IDENT "{" (IDENT "=" atom ";")* "}" extern := "extern" "fn" IDENT "(" eparams? ")" ("->" type)? ";" eparams := eparam ("," eparam)* @@ -161,6 +162,7 @@ def parse_resource(self) -> A.ResourceDecl: self.eat(Tok.LBRACE) members: list[A.ResourceMember] = [] emit: dict[str, str] = {} + kind: str | None = None while not self.at(Tok.RBRACE): if self.at(Tok.ACQUIRE): self.eat(Tok.ACQUIRE) @@ -175,8 +177,14 @@ def parse_resource(self) -> A.ResourceDecl: self.pos += 1 val = self.eat(Tok.STRING).text emit[field] = val + elif self.at(Tok.IDENT) and self.cur.text == "kind": + # contextual keyword (not globally reserved): kind "subscription token" + self.pos += 1 + kind = self.eat(Tok.STRING).text else: - raise ParseError("expected 'acquire', 'release' or an emit_* template", self.cur) + raise ParseError( + "expected 'acquire', 'release', 'kind' or an emit_* template", + self.cur) self.eat(Tok.RBRACE) return A.ResourceDecl( name=name, members=members, line=kw.line, @@ -184,6 +192,7 @@ def parse_resource(self) -> A.ResourceDecl: emit_acquire=emit.get("emit_acquire"), emit_release=emit.get("emit_release"), emit_borrow=emit.get("emit_borrow"), + kind=kind, ) # -- externs ------------------------------------------------------------ diff --git a/tests/run_tests.py b/tests/run_tests.py index b5b42422..42a1e86c 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1039,10 +1039,15 @@ def run() -> int: import test_corpus co_rc = test_corpus.run() + # WPF lifetime corpus (lifetimes slice #1): subscription/timer leaks caught + # by the generic ownership checker, carrying the [resource: ] tag. + import test_wpf + wpf_rc = test_wpf.run() + 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) else 0 + or gl_rc or co_rc or wpf_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_wpf.py b/tests/test_wpf.py new file mode 100644 index 00000000..d4ee7a5f --- /dev/null +++ b/tests/test_wpf.py @@ -0,0 +1,122 @@ +#!/usr/bin/env python3 +""" +WPF lifetime corpus, as a self-checking test (slice #1 of the `lifetimes` work). + +Each corpus/wpf// folder holds a real WPF lifetime bug pattern reduced to +OwnLang: before.cs (buggy) / after.cs (fixed) / case.own (a faithful OwnLang +reduction, with a `kind`-tagged resource) / expected-diagnostics.txt (the codes +the checker must produce) / notes.md (the pattern, source, and honesty caveat). + +The point of slice #1 is that the *core ownership checker already catches the +main class of WPF leaks* (a subscription/timer that is never disposed = OWN001; +touched after dispose = OWN002), and that the domain-neutral resource-kind tag +reaches the rendered output as `[resource: ]`. So this test asserts BOTH: + + * the produced error codes match expected-diagnostics.txt, and + * the rendered diagnostic carries the `[resource: ...]` metadata. + +If the checker ever stops catching one of these patterns, or the kind metadata +stops flowing to the output, the suite goes red. + +NOTE: case.own is a hand reduction, not C# the checker ingested -- OwnLang has no +C# front-end (a later slice). The corpus shows the ownership *logic* maps onto +real WPF bugs, not that the tool scanned real C#. + +Run: python tests/test_wpf.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.buffers import validate_policies +from ownlang.cfg import ( + build_cfg, + collect_kinds, + collect_policies, + collect_signatures, +) +from ownlang.diagnostics import Severity +from ownlang.lexer import LexError +from ownlang.parser import ParseError, parse + +_CORPUS = os.path.join(os.path.dirname(__file__), "..", "corpus", "wpf") + + +def _check(src: str) -> tuple[list[str], str]: + """(error codes, rendered-pretty text) the checker produces for one source.""" + try: + mod = parse(src) + except (ParseError, LexError): + return ["OWN020"], "" + rnames = {r.name for r in mod.resources} + sigs = collect_signatures(mod) + kinds = collect_kinds(mod) + diags = list(validate_policies(collect_policies(mod))) + for fn in mod.functions: + cfg, d1 = build_cfg(fn, rnames, sigs, None, kinds) + diags += d1 + analyze(cfg) + errors = [d for d in diags if d.severity == Severity.ERROR] + codes = [d.code for d in errors] + rendered = "\n".join(d.render_pretty("case.own", src) for d in errors) + return codes, rendered + + +def _cases() -> list[str]: + if not os.path.isdir(_CORPUS): + return [] + return sorted(d for d in os.listdir(_CORPUS) + if os.path.isdir(os.path.join(_CORPUS, d))) + + +def run() -> int: + """Check every WPF case against expected codes + kind metadata; return 0/1.""" + fails: list[str] = [] + rows: list[tuple[str, str]] = [] + checked = 0 + matched = 0 + for case in _cases(): + d = os.path.join(_CORPUS, case) + own = os.path.join(d, "case.own") + exp = os.path.join(d, "expected-diagnostics.txt") + for required in (own, exp, os.path.join(d, "before.cs"), + os.path.join(d, "after.cs"), os.path.join(d, "notes.md")): + if not os.path.exists(required): + fails.append(f"{case}: missing {os.path.basename(required)}") + if not (os.path.exists(own) and os.path.exists(exp)): + continue + checked += 1 + with open(exp, encoding="utf-8") as f: + want = sorted(w for w in f.read().split() if w) + with open(own, encoding="utf-8") as f: + codes, rendered = _check(f.read()) + got = sorted(set(codes)) + ok = True + if got != want: + fails.append(f"{case}: expected {want}, got {got}") + ok = False + # the whole point of slice #1: the resource-kind tag must reach output. + if "[resource: " not in rendered: + fails.append(f"{case}: rendered output carries no [resource: ...] tag") + ok = False + if ok: + matched += 1 + rows.append((case, ",".join(want))) + + print("WPF lifetime corpus (corpus/wpf/):") + width = max((len(c) for c, _ in rows), default=0) + for case, codes in rows: + print(f" {case:<{width}} {codes}") + for f in fails: + print(f"WPF FAIL: {f}") + print(f"wpf: {matched}/{checked} cases match expected codes + carry kind metadata") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From 4520868e95025e0bbe5950ddadfeb797f5d6070b Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 20:24:14 +0000 Subject: [PATCH 05/10] lifetimes slice #2: lifetime regions + region-escape theorem (OWN014) The genuinely-new analysis on top of the ownership core: it reasons about region escape (the WPF 'zombie ViewModel promoted to App lifetime' theorem), not just release within a scope. Language: - lifetime declarations with a strict order: 'lifetime Window < App;' (transitive; cycles -> OWN036, undefined refs -> OWN030, redef -> OWN031). - lifetime annotations on the object a function sets up and on its service params: 'fn VM(bus: EventBus lifetime App) lifetime ViewModel'. - a strong-capture statement: 'subscribe self to SOURCE;' ('self'/'to' contextual; only 'lifetime'/'subscribe' are reserved; '<' lexed). Analysis (ownlang/lifetimes.py, check_lifetimes): - region escape OWN014: if SOURCE strictly outlives self, the strong capture promotes self to SOURCE's lifetime and it leaks. The *ordering* is what makes it a leak -- a same/shorter-lived source is clean. Per fork B the code is domain-neutral (OWN014 'escapes to a longer-lived region'), not WPF-branded. - the mitigation (a disposable token released on close) is the slice-#1 acquire/release pattern, so both halves of the theorem now exist. Wiring/tests: - CLI 'check' runs check_lifetimes; the new Subscribe stmt is a no-op for the loans/permissions flow and a schematic emit in codegen (both assert_never dispatchers updated; lower_let rhs got assert_never too). - corpus/wpf/viewmodel-escapes-to-app (before/after C# + notes); test_wpf made tolerant of non-kinded cases. tests/test_lifetimes.py: 10 region cases. - docs/lifetimes.md + README updated to mark slice #2 built. Gate + suite green: mypy --strict, ruff, analysis 123/123, codegen 23/23, fuzz, gallery 10/10, corpus 2/2, wpf 3/3, lifetimes 10/10. --- README.md | 42 ++++- corpus/wpf/viewmodel-escapes-to-app/after.cs | 21 +++ corpus/wpf/viewmodel-escapes-to-app/before.cs | 18 ++ corpus/wpf/viewmodel-escapes-to-app/case.own | 16 ++ .../expected-diagnostics.txt | 1 + corpus/wpf/viewmodel-escapes-to-app/notes.md | 33 ++++ docs/lifetimes.md | 50 ++++- ownlang/__main__.py | 2 + ownlang/ast_nodes.py | 30 ++- ownlang/cfg.py | 6 + ownlang/codegen.py | 4 + ownlang/diagnostics.py | 2 + ownlang/lexer.py | 7 + ownlang/lifetimes.py | 145 +++++++++++++++ ownlang/parser.py | 50 ++++- tests/run_tests.py | 7 +- tests/test_lifetimes.py | 176 ++++++++++++++++++ tests/test_wpf.py | 10 +- 18 files changed, 593 insertions(+), 27 deletions(-) create mode 100644 corpus/wpf/viewmodel-escapes-to-app/after.cs create mode 100644 corpus/wpf/viewmodel-escapes-to-app/before.cs create mode 100644 corpus/wpf/viewmodel-escapes-to-app/case.own create mode 100644 corpus/wpf/viewmodel-escapes-to-app/expected-diagnostics.txt create mode 100644 corpus/wpf/viewmodel-escapes-to-app/notes.md create mode 100644 ownlang/lifetimes.py create mode 100644 tests/test_lifetimes.py diff --git a/README.md b/README.md index e5c36f61..31263fb6 100644 --- a/README.md +++ b/README.md @@ -93,7 +93,7 @@ examples/gallery/05_dispose_while_view_live.own:9:13: error: [OWN008] cannot rel ^ ``` -### Бизнес-применение: WPF lifetime-утечки (модуль `lifetimes`, slice #1) +### Бизнес-применение: WPF lifetime-утечки (модуль `lifetimes`) Performance-профиль (`stackalloc`/pool) — это игрушка для performance-зоопарка. Бизнес-софт чаще умирает не от того, что `Span` на 7 нс медленнее, а от @@ -117,12 +117,34 @@ case.own:16:9: error: [OWN001] 'customerChanged' is owned but not released at ^ ``` +**Slice #2 — lifetime-регионы (region escape).** Это уже *новый* анализ, а не +переиспользование. Объявляем регионы с порядком и вешаем lifetime на объект и +сервисы; сильная подписка на более долгоживущий источник промотит объект до его +lifetime и течёт — `OWN014`. Именно **порядок** делает это утечкой: подписка на +равный-или-более-короткий источник — чисто. + +```text +$ python -m ownlang check corpus/wpf/viewmodel-escapes-to-app/case.own +case.own:15:23: error: [OWN014] 'bus' (lifetime 'App') outlives the captured + object 'CustomerViewModel' (lifetime 'ViewModel'); the strong subscription + promotes 'CustomerViewModel' to 'App' and it leaks (no release path) + 15 | subscribe self to bus; + ^ +``` +```ownlang +lifetime App; lifetime Window < App; lifetime ViewModel < Window; +fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; // App > ViewModel -> промоушн -> OWN014 +} +``` + `corpus/wpf/` — self-checking корпус реальных WPF-паттернов (`before.cs`/ -`after.cs`/`case.own`/expected), прибитый тестом `tests/test_wpf.py`. Полный план -модуля (lifetime-регионы, каталог OWN-WPF, границы слайсов, что отложено) — -в [`docs/lifetimes.md`](docs/lifetimes.md). Честно: `case.own` — hand reduction -паттерна, не C#, который чекер съел (C#-фронта нет, это поздний слайс); корпус -показывает, что ownership-**логика** ложится на реальный баг. +`after.cs`/`case.own`/expected), прибитый `tests/test_wpf.py`; региональная +теорема — `tests/test_lifetimes.py` (10 кейсов). Полный план модуля (каталог +OWN-WPF, границы слайсов, что отложено) — в [`docs/lifetimes.md`](docs/lifetimes.md). +Честно: `case.own` — hand reduction паттерна, не C#, который чекер съел (C#-фронта +нет, это поздний слайс); `self`/`source` — это scope самой функции и её параметры, +без cross-procedural points-to. ### Golden-пример: настоящий ArrayPool @@ -309,9 +331,15 @@ fn process(size: int) { | OWN032 | owned-ресурс скопирован без `move` | | OWN033 | функция с типом возврата может дойти до конца без `return` | | OWN034 | операция применена не к owned-ресурсу | +| OWN035 | несовпадение типа возврата | +| OWN036 | циклический порядок lifetime-регионов | | OWN040 | вызов необъявленной функции (неизвестные вызовы запрещены) | | OWN041 | несовместимость аргумента вызова (арность / kind / plain-vs-resource) | +Lifetime-регионы (модуль `lifetimes`): **OWN014** — объект промотится в более +долгоживущий регион через сильную подписку (region escape); **OWN036** — цикл в +`<`-порядке; ссылки на необъявленный регион — **OWN030**. + Разделение **definite (002/005)** против **maybe (009/010)** — прямо по ревью: ошибка на *всех* путях и ошибка на *каком-то* пути — это разные по резкости сообщения, и это разделение естественно выпадает из решётки множеств состояний. @@ -653,6 +681,7 @@ ownlang/ buffers.py # storage policies: режимы, резолв policy+intent, валидация cfg.py # resolver (Symbol/Kind) + collect_signatures + lowering, Invoke analysis.py # flow-sensitive dataflow: var-states + active loans + permissions + lifetimes.py # lifetime-регионы: region-escape (OWN014) + валидация порядка diagnostics.py # коды OWN0xx в одном месте codegen.py # C# codegen (emit_* шаблоны, try/finally hoist + inline, буферы) report.py # compile-time buffer report -> stdout + .ownreport.json @@ -672,6 +701,7 @@ ownlang/ test_gallery.py # пинит каждый gallery-пример к его коду test_corpus.py # пинит каждый corpus-кейс к expected-диагностикам test_wpf.py # WPF-корпус: коды + [resource: kind] метадата + test_lifetimes.py # region-escape (OWN014) + валидация lifetime-порядка pyproject.toml # gate: ruff + mypy --strict (см. ниже) ``` diff --git a/corpus/wpf/viewmodel-escapes-to-app/after.cs b/corpus/wpf/viewmodel-escapes-to-app/after.cs new file mode 100644 index 00000000..82f57d8b --- /dev/null +++ b/corpus/wpf/viewmodel-escapes-to-app/after.cs @@ -0,0 +1,21 @@ +// FIXED. The subscription is kept as a disposable token and released when the +// VM is disposed (on window close), so the App-lived bus no longer holds the +// Window-lived VM: the VM drops back to its intended Window lifetime and is +// collectable. (In OwnLang terms this is the slice-#1 acquire/release token +// pattern; the region check then sees a release path and stays quiet.) +public sealed class CustomerViewModel : IDisposable +{ + private readonly IDisposable _customerChanged; + + public CustomerViewModel(IEventBus appBus) + { + _customerChanged = appBus.Subscribe(OnCustomerChanged); + } + + private void OnCustomerChanged(CustomerChanged e) { /* ... */ } + + public void Dispose() + { + _customerChanged.Dispose(); // release path -> VM no longer promoted + } +} diff --git a/corpus/wpf/viewmodel-escapes-to-app/before.cs b/corpus/wpf/viewmodel-escapes-to-app/before.cs new file mode 100644 index 00000000..ae52b324 --- /dev/null +++ b/corpus/wpf/viewmodel-escapes-to-app/before.cs @@ -0,0 +1,18 @@ +// BUGGY (representative WPF pattern, hand-reduced into case.own). +// +// A Window-scoped ViewModel subscribes itself to an App-scoped (singleton) event +// bus with a strong handler and keeps no unsubscribe token. The bus is reachable +// from an App-lifetime GC root, and through the strong delegate so is the VM: +// the VM is *promoted* to App lifetime. Close the window all you want -- the VM +// lives until the process exits. The lifetime mismatch (VM expected Window, +// actually App) is the leak. +public sealed class CustomerViewModel +{ + public CustomerViewModel(IEventBus appBus) // appBus: App lifetime (singleton) + { + // strong subscription, no token kept -> VM promoted to App lifetime + appBus.CustomerChanged += OnCustomerChanged; + } + + private void OnCustomerChanged(object? sender, EventArgs e) { /* ... */ } +} diff --git a/corpus/wpf/viewmodel-escapes-to-app/case.own b/corpus/wpf/viewmodel-escapes-to-app/case.own new file mode 100644 index 00000000..8b21611b --- /dev/null +++ b/corpus/wpf/viewmodel-escapes-to-app/case.own @@ -0,0 +1,16 @@ +module WpfRegionEscape + +// Lifetime regions: a Window-lived ViewModel must not outlive its window, and +// the App-lived event bus outlives everything. +lifetime App; +lifetime Window < App; +lifetime ViewModel < Window; + +// The ViewModel (ViewModel-lived) strongly subscribes itself to the App-lived +// bus. Because App strictly outlives ViewModel, the subscription promotes the +// VM to App lifetime -> it can never die while the app runs => OWN014. This is +// the region-escape theorem: the *ordering* is what makes it a leak (subscribing +// to a same/shorter-lived source would be fine). +fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; +} diff --git a/corpus/wpf/viewmodel-escapes-to-app/expected-diagnostics.txt b/corpus/wpf/viewmodel-escapes-to-app/expected-diagnostics.txt new file mode 100644 index 00000000..3fd038d5 --- /dev/null +++ b/corpus/wpf/viewmodel-escapes-to-app/expected-diagnostics.txt @@ -0,0 +1 @@ +OWN014 diff --git a/corpus/wpf/viewmodel-escapes-to-app/notes.md b/corpus/wpf/viewmodel-escapes-to-app/notes.md new file mode 100644 index 00000000..9edb514c --- /dev/null +++ b/corpus/wpf/viewmodel-escapes-to-app/notes.md @@ -0,0 +1,33 @@ +# WPF ViewModel promoted to App lifetime (region escape) + +**Pattern:** a Window-scoped ViewModel strongly subscribes itself to an +App-scoped (singleton) event bus and keeps no unsubscribe token. The strong +delegate makes the VM reachable from an App-lifetime GC root, so the VM is +*promoted* to App lifetime: it outlives its window and lives until the process +exits. The bug is the **lifetime mismatch** — VM expected `Window`, actually +`App` — not any single missing `Dispose` call in isolation. + +**What the checker says:** this is the region-escape theorem (slice #2). With the +regions declared (`ViewModel < Window < App`) and the source tagged App-lived, +the strong `subscribe self to bus` where the source strictly outlives `self` +trips the generic **OWN014**: + +```text +$ python -m ownlang check corpus/wpf/viewmodel-escapes-to-app/case.own +case.own:16:23: error: [OWN014] 'bus' (lifetime 'App') outlives the captured + object 'CustomerViewModel' (lifetime 'ViewModel'); the strong subscription + promotes 'CustomerViewModel' to 'App' and it leaks (no release path) + 16 | subscribe self to bus; + ^ +``` + +The *ordering* is what makes it a leak: subscribing to a same- or shorter-lived +source produces no diagnostic (no promotion possible). The fix (`after.cs`) keeps +a disposable token released on close — the slice-#1 acquire/release pattern — +which gives the VM a release path back to its Window lifetime. + +**Honesty / scope.** `case.own` is a *hand reduction*, not C# the checker +ingested (no C# front-end yet). `self`/`source` are the function's own scope and +its annotated parameters — there is no cross-procedural points-to, and weak-event +policy as an explicit escape hatch is a later slice (see `docs/lifetimes.md`). +`before.cs` / `after.cs` are representative, not a verbatim copy of one PR. diff --git a/docs/lifetimes.md b/docs/lifetimes.md index efaf0178..40436ae2 100644 --- a/docs/lifetimes.md +++ b/docs/lifetimes.md @@ -85,13 +85,42 @@ lifetime Window < App; // Window строго короче App lifetime ViewModel < Window; ``` -`<` задаёт строгий частичный порядок (DAG, без циклов — проверяется в -`__post_init__`/резолвере: вот первый *настоящий* меж-полевой инвариант, ради -которого post_init окупается). Объект из короткого региона, ставший достижимым из -длинного через strong-подписку, — это `WPF010` (lifetime promotion), если нет -owned-токена с гарантированным release. Это **slice #2**: тут появляется -региональная аннотация на параметрах (`[Lifetime("App")] bus`) и проверка -«source_lifetime > listener_lifetime ⇒ нужен токен». +`<` задаёт строгий частичный порядок; циклы и ссылки на необъявленные регионы +отвергаются (`OWN036`/`OWN030`). Объект из короткого региона, ставший достижимым +из длинного через strong-подписку, промотится до длинного lifetime и утечёт. + +### Реализовано (slice #2) + +Синтаксис, который реально собран: + +```ownlang +lifetime App; +lifetime Window < App; // Window строго короче App +lifetime ViewModel < Window; + +fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; // bus сильно держит self +} +``` + +- `fn F(...) lifetime L` — объект, который функция конструирует, живёт в регионе L. +- `param: T lifetime L` — сервис-параметр живёт в регионе L. +- `subscribe self to SOURCE;` — сильный захват: SOURCE держит self. + +**Правило (region escape, `OWN014`):** если `lifetime(SOURCE)` строго длиннее +`lifetime(self)`, self промотится до длинного региона и утечёт. Захват источником +равного-или-более-короткого lifetime — чисто (промоушена нет). Именно **порядок** +делает это утечкой — это и отличает региональный анализ от простого «не released». +Митигация (disposable-токен с release на close) — это slice-#1 паттерн +`acquire`/`release`: если есть release-путь, `subscribe`-формы не пишут. + +Согласно развилке B код **доменно-нейтральный** (`OWN014` «escape в более долгий +регион»), а не `WPF010`: ядро не знает про WPF, бизнес-формулировку даст будущий +профиль/фронт. + +Чего **нет** (отложено): cross-procedural points-to (`self`/`source` — это scope +самой функции и её аннотированные параметры, не произвольный граф объектов), и +weak-reference policy как явный escape-hatch. ## 5. Каталог кодов (OWN-WPF) и куда какой слайс @@ -101,7 +130,7 @@ owned-токена с гарантированным release. Это **slice #2* | WPF005 | `IDisposable`-поле требует `VM : IDisposable` + cascade `Dispose` | `OWN001`/`OWN002` | **#1** | | WPF002 | `DispatcherTimer`/`Timer` в VM требует `Stop`+detach | `OWN001` | #1/#2 | | WPF008 | `CollectionChanged`/`PropertyChanged` подписка без отписки | `OWN001` | #2 | -| WPF010 | объект ушёл из короткого lifetime в длинный (region escape) | новый region-анализ | **#2** | +| ~~WPF010~~ → `OWN014` | объект ушёл из короткого lifetime в длинный (region escape) | новый region-анализ ✅ **готово** | **#2** | | WPF003 | static-подписка запрещена без weak | region + policy | #2 | | WPF001/006/007/009 | event+= / DataContext / lambda-capture / static cache | region + capture-анализ | позже | @@ -113,7 +142,10 @@ MVP (slice #1) сознательно сводит WPF004/005/002 к уже-ра - **slice #1 (сейчас):** WPF-корпус `corpus/wpf/` (zombie-VM, незакрытый таймер, disposable-поле) на текущем движке + WPF-галерея + self-checking тест. Опционально — тонкий WPF-флейвор слой над диагностиками (см. развилку B). -- **slice #2:** lifetime-регионы (`lifetime A < B;`), region-escape-анализ, WPF010. +- **slice #2 ✅ готово:** lifetime-регионы (`lifetime A < B;`, fn/param-аннотации, + `subscribe self to X;`), region-escape-анализ → `OWN014`; структурная валидация + порядка (`OWN030`/`OWN031`/`OWN036`). Корпус `corpus/wpf/viewmodel-escapes-to-app` + + `tests/test_lifetimes.py` (10 кейсов). - **slice #3 (далеко):** узкий Roslyn-frontend — pattern matcher (`event +=`, `Subscribe`, `DispatcherTimer`, `IDisposable`-поля) → кормит это же ядро. Не «ингест всего C#» (это человеко-годы), а распознавание известных паттернов. diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 17496814..1984cd25 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -23,6 +23,7 @@ from .codegen import generate from .diagnostics import Diagnostic, Severity from .lexer import LexError +from .lifetimes import check_lifetimes from .parser import ParseError, parse from .report import build_report, render_report @@ -38,6 +39,7 @@ def _collect(src: str) -> tuple[list[Diagnostic], object | None]: pols = collect_policies(mod) kinds = collect_kinds(mod) diags: list[Diagnostic] = list(validate_policies(pols)) + diags.extend(check_lifetimes(mod)) for fn in mod.functions: cfg, d1 = build_cfg(fn, rnames, sigs, pols, kinds) d2 = analyze(cfg) diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index e7af1329..22dbd80c 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -135,7 +135,17 @@ class Return: line: int -Stmt = Let | Release | Use | Call | BorrowBlock | If | Return +@dataclass(frozen=True) +class Subscribe: + """`subscribe self to SOURCE;` — the current object (the function's scope, + living at the function's lifetime) is strongly captured by `source`. If + `source` outlives `self`, `self` is promoted to the longer lifetime (a + region escape). The heart of the lifetime/region analysis.""" + source: str + line: int + + +Stmt = Let | Release | Use | Call | BorrowBlock | If | Return | Subscribe # ---- top level ------------------------------------------------------------ @@ -187,6 +197,9 @@ class Param: name: str type: TypeRef line: int + # optional lifetime region this parameter (a service / source) lives at, + # e.g. `bus: EventBus lifetime App`. None when unannotated. + lifetime: str | None = None @dataclass(frozen=True) @@ -196,6 +209,20 @@ class FnDecl: ret: TypeRef | None body: list[Stmt] line: int + # optional lifetime region of the object this function sets up (its scope), + # e.g. `fn CustomerViewModel(...) lifetime ViewModel { ... }`. None when + # unannotated (the lifetime analysis then skips this function). + lifetime: str | None = None + + +@dataclass(frozen=True) +class LifetimeDecl: + """`lifetime NAME;` or `lifetime NAME < LONGER;` — declares a region. The + `< LONGER` form states NAME is strictly shorter-lived than LONGER (nested + inside it). The relation is transitive; cycles are rejected.""" + name: str + longer: str | None # the region this one is strictly shorter than, if any + line: int @dataclass(frozen=True) @@ -215,3 +242,4 @@ class Module: externs: list[ExternDecl] = field(default_factory=list) functions: list[FnDecl] = field(default_factory=list) policies: list[PolicyDecl] = field(default_factory=list) + lifetimes: list[LifetimeDecl] = field(default_factory=list) diff --git a/ownlang/cfg.py b/ownlang/cfg.py index 7dc41107..cd7c0ec1 100644 --- a/ownlang/cfg.py +++ b/ownlang/cfg.py @@ -333,6 +333,12 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None: return self.lower_if(st, cur) if isinstance(st, A.Return): return self.lower_return(st, cur) + if isinstance(st, A.Subscribe): + # a `subscribe self to X` is a lifetime-region fact, handled by the + # separate lifetime analysis (ownlang.lifetimes); it does not move, + # release, or borrow anything, so it is a no-op for the loans/ + # permissions flow. + return cur assert_never(st) def lower_let(self, st: A.Let, cur: Block) -> Block: diff --git a/ownlang/codegen.py b/ownlang/codegen.py index 0583e2e9..05cbf750 100644 --- a/ownlang/codegen.py +++ b/ownlang/codegen.py @@ -464,6 +464,10 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]: 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): + # schematic: the real C# would be `source.Subscribe(this.Handler)`. + return [f"{ind}{st.source}.Subscribe(this); " + f"// captures self at {st.source}'s lifetime"] assert_never(st) # -- template helpers --------------------------------------------------- diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py index 80879a84..ad9ebe3e 100644 --- a/ownlang/diagnostics.py +++ b/ownlang/diagnostics.py @@ -45,6 +45,7 @@ class Severity(Enum): "OWN011": "mutable borrow while another mutable borrow is live", "OWN012": "shared borrow while a mutable borrow is live", "OWN013": "owner accessed while it is mutably borrowed", + "OWN014": "value escapes to a longer-lived region (lifetime promotion)", # ---- buffer storage policies (stackalloc / scratch / pool / native) ---- "OWN015": "stack-backed buffer cannot escape the current function", "OWN016": "stack-backed buffer moved to a longer-lived owner", @@ -63,6 +64,7 @@ class Severity(Enum): "OWN033": "function must return a value on all paths", "OWN034": "operation requires an owned resource", "OWN035": "return type mismatch", + "OWN036": "cyclic lifetime ordering", # ---- extern / call boundary ---- "OWN040": "call to an undeclared function (unknown calls are forbidden)", "OWN041": "call argument mismatch", diff --git a/ownlang/lexer.py b/ownlang/lexer.py index a700e63a..4ac673c1 100644 --- a/ownlang/lexer.py +++ b/ownlang/lexer.py @@ -43,6 +43,9 @@ class Tok(Enum): EMIT_ACQUIRE = auto() EMIT_RELEASE = auto() EMIT_BORROW = auto() + # lifetime regions + LIFETIME = auto() + SUBSCRIBE = auto() # explicitly-unsupported keywords (reported, not parsed) REJECTED = auto() # punctuation @@ -57,6 +60,7 @@ class Tok(Enum): EQ = auto() DOT = auto() ARROW = auto() + LT = auto() EOF = auto() @@ -83,6 +87,8 @@ class Tok(Enum): "emit_acquire": Tok.EMIT_ACQUIRE, "emit_release": Tok.EMIT_RELEASE, "emit_borrow": Tok.EMIT_BORROW, + "lifetime": Tok.LIFETIME, + "subscribe": Tok.SUBSCRIBE, } # Things we refuse to analyze in the MVP. Lexed so we can say so plainly. @@ -201,6 +207,7 @@ def advance(k: int = 1) -> None: "&": Tok.AMP, "=": Tok.EQ, ".": Tok.DOT, + "<": Tok.LT, } if c in simple: advance() diff --git a/ownlang/lifetimes.py b/ownlang/lifetimes.py new file mode 100644 index 00000000..9743a8d1 --- /dev/null +++ b/ownlang/lifetimes.py @@ -0,0 +1,145 @@ +""" +Lifetime-region analysis (the `lifetimes` module, slice #2). + +This is the genuinely new analysis on top of the ownership/borrow core: it +reasons about *region escape* — the WPF "zombie ViewModel" theorem — rather than +about resource release within one scope. + +Model +----- +`lifetime` declarations define regions with a strict partial order: + + lifetime App; + lifetime Window < App; // Window is strictly shorter-lived than App + lifetime ViewModel < Window; + +A function carries the lifetime of the object it sets up (`fn F(...) lifetime +ViewModel`), and its parameters carry the lifetime of the service they are +(`bus: EventBus lifetime App`). A `subscribe self to bus;` statement is a strong +capture: `bus` now holds a reference to the object. + +Theorem (region escape) +----------------------- +If `self` has lifetime L_self and is strongly captured by a `source` of lifetime +L_source with **L_source strictly longer than L_self**, then `self` is promoted +to L_source: it stays reachable for the whole of the longer region and leaks. +That is OWN014. A capture by a source of equal-or-shorter lifetime is fine (no +promotion). The mitigation — a disposable subscription *token* released on close +— is the slice-#1 pattern (`acquire`/`release`, caught by OWN001 if dropped); +the tokenless `subscribe` here is exactly the fire-and-forget leak. + +What this is NOT (yet) +---------------------- +No cross-procedural points-to: `self`/`source` are the function's own scope and +its annotated parameters. Weak-reference policy as an explicit escape hatch, and +ingestion of real C#, are later slices (see docs/lifetimes.md). +""" + +from __future__ import annotations + +from collections.abc import Iterator + +from . import ast_nodes as A +from .diagnostics import Diagnostic + + +def _iter_subscribes(stmts: list[A.Stmt]) -> Iterator[A.Subscribe]: + """Yield every `subscribe` statement in a body, descending into branches.""" + for st in stmts: + if isinstance(st, A.Subscribe): + yield st + elif isinstance(st, A.If): + yield from _iter_subscribes(st.then_body) + yield from _iter_subscribes(st.else_body) + elif isinstance(st, A.BorrowBlock): + yield from _iter_subscribes(st.body) + + +def _strictly_longer(decls: list[A.LifetimeDecl]) -> dict[str, set[str]]: + """Map each region to the set of regions strictly longer-lived than it. + + `lifetime X < Y` means X is shorter than Y, i.e. Y is longer than X. We take + the transitive closure so `ViewModel < Window < App` puts both Window and App + in `longer['ViewModel']`.""" + direct: dict[str, set[str]] = {} + for d in decls: + direct.setdefault(d.name, set()) + if d.longer is not None: + direct.setdefault(d.longer, set()) + direct[d.name].add(d.longer) + longer: dict[str, set[str]] = {n: set() for n in direct} + for start in direct: + stack = list(direct[start]) + while stack: + cur = stack.pop() + if cur in longer[start]: + continue + longer[start].add(cur) + stack.extend(direct.get(cur, ())) + return longer + + +def check_lifetimes(mod: A.Module) -> list[Diagnostic]: + """Region diagnostics for a module: structural validation of the lifetime + order plus the per-function escape check. Empty when no lifetimes are used.""" + diags: list[Diagnostic] = [] + if not mod.lifetimes: + return diags + + names: set[str] = set() + for d in mod.lifetimes: + if d.name in names: + diags.append(Diagnostic( + "OWN031", f"lifetime '{d.name}' is already defined", d.line)) + names.add(d.name) + for d in mod.lifetimes: + if d.longer is not None and d.longer not in names: + diags.append(Diagnostic( + "OWN030", f"undefined lifetime '{d.longer}'", d.line)) + + longer = _strictly_longer(mod.lifetimes) + # a cycle shows up as a region being strictly longer than itself. + for d in mod.lifetimes: + if d.name in longer.get(d.name, set()): + diags.append(Diagnostic( + "OWN036", + f"lifetime '{d.name}' is part of a cyclic ordering " + f"(it ends up strictly longer than itself)", d.line)) + + for fn in mod.functions: + diags.extend(_check_fn(fn, names, longer)) + return diags + + +def _check_fn(fn: A.FnDecl, names: set[str], + longer: dict[str, set[str]]) -> list[Diagnostic]: + out: list[Diagnostic] = [] + # validate any annotations on this function, even if it has no subscribes. + if fn.lifetime is not None and fn.lifetime not in names: + out.append(Diagnostic( + "OWN030", f"undefined lifetime '{fn.lifetime}'", fn.line)) + param_lt: dict[str, str] = {} + for p in fn.params: + if p.lifetime is None: + continue + if p.lifetime not in names: + out.append(Diagnostic( + "OWN030", f"undefined lifetime '{p.lifetime}'", p.line)) + else: + param_lt[p.name] = p.lifetime + + self_lt = fn.lifetime if fn.lifetime in names else None + for sub in _iter_subscribes(fn.body): + src_lt = param_lt.get(sub.source) + # skip when we cannot compare (no self lifetime, unknown/untagged source): + # being conservative avoids false positives. + if self_lt is None or src_lt is None: + continue + if src_lt in longer.get(self_lt, set()): + out.append(Diagnostic( + "OWN014", + f"'{sub.source}' (lifetime '{src_lt}') outlives the captured " + f"object '{fn.name}' (lifetime '{self_lt}'); the strong " + f"subscription promotes '{fn.name}' to '{src_lt}' and it leaks " + f"(no release path)", sub.line)) + return out diff --git a/ownlang/parser.py b/ownlang/parser.py index d4b98cf1..c52dda8d 100644 --- a/ownlang/parser.py +++ b/ownlang/parser.py @@ -4,21 +4,23 @@ Grammar (informal): module := "module" IDENT item* - item := resource | extern | fn | policy + item := resource | extern | fn | policy | lifetime resource := "resource" IDENT "{" rmember* "}" rmember := ("acquire" | "release") IDENT | ("emit_type"|"emit_acquire"|"emit_release"|"emit_borrow") STRING | "kind" STRING // contextual; not reserved + lifetime := "lifetime" IDENT ("<" IDENT)? ";" // region; "<" = shorter-than policy := "policy" IDENT "{" (IDENT "=" atom ";")* "}" extern := "extern" "fn" IDENT "(" eparams? ")" ("->" type)? ";" eparams := eparam ("," eparam)* eparam := ("borrow" | "borrow_mut" | "consume")? IDENT // IDENT = type name - fn := "fn" IDENT "(" params? ")" ("->" type)? block + fn := "fn" IDENT "(" params? ")" ("->" type)? ("lifetime" IDENT)? block params := param ("," param)* - param := IDENT ":" type + param := IDENT ":" type ("lifetime" IDENT)? type := "&" "mut"? IDENT | IDENT block := "{" stmt* "}" - stmt := let | release | use | call | borrow | if | return + stmt := let | release | use | call | borrow | if | return | subscribe + subscribe := "subscribe" "self" "to" IDENT ";" // self/to contextual let := "let" IDENT "=" rhs ";" rhs := "acquire" IDENT "(" args? ")" | "move" IDENT | bufferintent | IDENT | INT @@ -119,11 +121,23 @@ def parse_module(self) -> A.Module: mod.functions.append(self.parse_fn()) elif self.at(Tok.POLICY): mod.policies.append(self.parse_policy()) + elif self.at(Tok.LIFETIME): + mod.lifetimes.append(self.parse_lifetime()) else: raise ParseError( - "expected 'resource', 'extern', 'fn' or 'policy'", self.cur) + "expected 'resource', 'extern', 'fn', 'policy' or 'lifetime'", + self.cur) return mod + def parse_lifetime(self) -> A.LifetimeDecl: + kw = self.eat(Tok.LIFETIME) + name = self.eat(Tok.IDENT).text + longer: str | None = None + if self.accept(Tok.LT): # `lifetime Window < App;` + longer = self.eat(Tok.IDENT).text + self.eat(Tok.SEMI) + return A.LifetimeDecl(name=name, longer=longer, line=kw.line) + # -- policies ----------------------------------------------------------- def parse_policy(self) -> A.PolicyDecl: @@ -240,14 +254,21 @@ def parse_fn(self) -> A.FnDecl: ret: A.TypeRef | None = None if self.accept(Tok.ARROW): ret = self.parse_type() + lifetime: str | None = None # `fn F(...) lifetime ViewModel { }` + if self.accept(Tok.LIFETIME): + lifetime = self.eat(Tok.IDENT).text body = self.parse_block() - return A.FnDecl(name=name, params=params, ret=ret, body=body, line=kw.line) + return A.FnDecl(name=name, params=params, ret=ret, body=body, + line=kw.line, lifetime=lifetime) def parse_param(self) -> A.Param: nm = self.eat(Tok.IDENT) self.eat(Tok.COLON) ty = self.parse_type() - return A.Param(name=nm.text, type=ty, line=nm.line) + lifetime: str | None = None # `bus: EventBus lifetime App` + if self.accept(Tok.LIFETIME): + lifetime = self.eat(Tok.IDENT).text + return A.Param(name=nm.text, type=ty, line=nm.line, lifetime=lifetime) def parse_type(self) -> A.TypeRef: line = self.cur.line @@ -283,10 +304,25 @@ def parse_stmt(self) -> A.Stmt: return self.parse_if() if self.at(Tok.RETURN): return self.parse_return() + if self.at(Tok.SUBSCRIBE): + return self.parse_subscribe() if self.at(Tok.IDENT) and self.peek().kind == Tok.LPAREN: return self.parse_call() raise ParseError("expected a statement", self.cur) + def parse_subscribe(self) -> A.Subscribe: + kw = self.eat(Tok.SUBSCRIBE) + # `self` and `to` are contextual here (not globally reserved words). + kw_self = self.eat(Tok.IDENT) + if kw_self.text != "self": + raise ParseError("expected 'self' after 'subscribe'", kw_self) + kw_to = self.eat(Tok.IDENT) + if kw_to.text != "to": + raise ParseError("expected 'to' in 'subscribe self to '", kw_to) + source = self.eat(Tok.IDENT).text + self.eat(Tok.SEMI) + return A.Subscribe(source=source, line=kw.line) + def parse_let(self) -> A.Let: kw = self.eat(Tok.LET) nm = self.eat(Tok.IDENT) diff --git a/tests/run_tests.py b/tests/run_tests.py index 42a1e86c..3a186bd5 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1044,10 +1044,15 @@ def run() -> int: import test_wpf wpf_rc = test_wpf.run() + # Lifetime-region analysis (lifetimes slice #2): the region-escape theorem + # (a short-lived object captured by a longer-lived source -> OWN014). + import test_lifetimes + lt_rc = test_lifetimes.run() + 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) else 0 + or gl_rc or co_rc or wpf_rc or lt_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_lifetimes.py b/tests/test_lifetimes.py new file mode 100644 index 00000000..e8de52aa --- /dev/null +++ b/tests/test_lifetimes.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +""" +Lifetime-region analysis tests (the `lifetimes` module, slice #2). + +Pins the region-escape theorem and the structural validation of the lifetime +order. Each case is a tiny module paired with the exact set of error codes it +must produce, so the WPF "zombie ViewModel" check can never quietly drift. + +The headline case: a ViewModel (short lifetime) strongly subscribed to an +App-lifetime source is promoted to App and leaks -> OWN014; the same subscription +to an equal-or-shorter-lived source is clean (no promotion). + +Run: python tests/test_lifetimes.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.lexer import LexError +from ownlang.lifetimes import check_lifetimes +from ownlang.parser import ParseError, parse + +# (name, source, expected sorted error codes) +CASES: list[tuple[str, str, list[str]]] = [ + ( + "escape_to_app", + """ + module M + lifetime App; + lifetime Window < App; + lifetime ViewModel < Window; + fn VM(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; + } + """, + ["OWN014"], + ), + ( + "escape_transitive", # ViewModel < Window < App, subscribe straight to App + """ + module M + lifetime App; + lifetime Window < App; + lifetime ViewModel < Window; + fn VM(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; + } + """, + ["OWN014"], + ), + ( + "same_lifetime_ok", # capture by an equal-lifetime source -> no promotion + """ + module M + lifetime App; + lifetime ViewModel < App; + fn ParentVM(child: ChildVM lifetime ViewModel) lifetime ViewModel { + subscribe self to child; + } + """, + [], + ), + ( + "shorter_source_ok", # source is shorter-lived than self -> fine + """ + module M + lifetime App; + lifetime Window < App; + fn AppService(view: View lifetime Window) lifetime App { + subscribe self to view; + } + """, + [], + ), + ( + "no_annotations_skipped", # without lifetimes, the analysis is a no-op + """ + module M + fn VM(bus: EventBus) { + subscribe self to bus; + } + """, + [], + ), + ( + "unannotated_self_skipped", # source tagged but self is not -> cannot compare + """ + module M + lifetime App; + fn VM(bus: EventBus lifetime App) { + subscribe self to bus; + } + """, + [], + ), + ( + "cyclic_order", + """ + module M + lifetime A < B; + lifetime B < A; + """, + ["OWN036", "OWN036"], + ), + ( + "undefined_longer", + """ + module M + lifetime A < Nope; + """, + ["OWN030"], + ), + ( + "undefined_param_lifetime", + """ + module M + lifetime App; + fn VM(bus: EventBus lifetime Bogus) lifetime App { + subscribe self to bus; + } + """, + ["OWN030"], + ), + ( + "redefined_lifetime", + """ + module M + lifetime App; + lifetime App; + """, + ["OWN031"], + ), +] + + +def _codes(src: str) -> list[str]: + try: + mod = parse(src) + except (ParseError, LexError): + return ["PARSE_ERROR"] + return sorted(d.code for d in check_lifetimes(mod)) + + +def run() -> int: + """Run every region case against its expected codes; return 0/1.""" + fails: list[str] = [] + matched = 0 + for name, src, want in CASES: + got = _codes(src) + if got == sorted(want): + matched += 1 + else: + fails.append(f"{name}: expected {sorted(want)}, got {got}") + + # the headline OWN014 must name the source, the captured object and BOTH + # lifetimes, and place a caret under the source in the `subscribe` line. + escape_src = CASES[0][1] + diags = check_lifetimes(parse(escape_src)) + pretty = diags[0].render_pretty("m.own", escape_src) + for needed in ("bus", "App", "VM", "ViewModel", "^"): + if needed not in pretty: + fails.append(f"escape message missing {needed!r}") + + for f in fails: + print(f"LIFETIMES FAIL: {f}") + print(f"lifetimes: {matched}/{len(CASES)} region cases match expected codes") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) diff --git a/tests/test_wpf.py b/tests/test_wpf.py index d4ee7a5f..4cf3cdc6 100644 --- a/tests/test_wpf.py +++ b/tests/test_wpf.py @@ -43,6 +43,7 @@ ) from ownlang.diagnostics import Severity from ownlang.lexer import LexError +from ownlang.lifetimes import check_lifetimes from ownlang.parser import ParseError, parse _CORPUS = os.path.join(os.path.dirname(__file__), "..", "corpus", "wpf") @@ -58,6 +59,7 @@ def _check(src: str) -> tuple[list[str], str]: sigs = collect_signatures(mod) kinds = collect_kinds(mod) diags = list(validate_policies(collect_policies(mod))) + diags += check_lifetimes(mod) for fn in mod.functions: cfg, d1 = build_cfg(fn, rnames, sigs, None, kinds) diags += d1 + analyze(cfg) @@ -94,14 +96,16 @@ def run() -> int: with open(exp, encoding="utf-8") as f: want = sorted(w for w in f.read().split() if w) with open(own, encoding="utf-8") as f: - codes, rendered = _check(f.read()) + source = f.read() + codes, rendered = _check(source) got = sorted(set(codes)) ok = True if got != want: fails.append(f"{case}: expected {want}, got {got}") ok = False - # the whole point of slice #1: the resource-kind tag must reach output. - if "[resource: " not in rendered: + # a case that tags a resource kind must surface it as [resource: ...]; + # region-escape cases (no kinded resource) are exempt. + if 'kind "' in source and "[resource: " not in rendered: fails.append(f"{case}: rendered output carries no [resource: ...] tag") ok = False if ok: From 9b1e9d13abafc31d0e8a7d5eb168def950d02a01 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 07:09:22 +0000 Subject: [PATCH 06/10] Add normative spec/ + forward-looking docs/proposals/ + conformance pilot Split the project's design material into two clearly-separated tracks so aspirational docs can never lie about the code: spec/ -- NORMATIVE, descriptive: what OwnLang IS today, derived from the working checker and pinned by tests. - OwnCore.md: affine ownership + borrow permissions; identity, states, loans, numbered rules R1-R12, call boundary. - BufferPolicies.md (B1-B7), Lifetimes.md (L1-L4), Diagnostics.md (every OWN code linked to the rule that raises it), CodegenContract.md (C1-C4: codegen may reject a sound program but must never emit unsafe C#). docs/proposals/ -- FORWARD-LOOKING RFCs for what is NOT built yet, with explicit non-goals (the discipline is refusing the soul-eating version): - P-001 C# -> OwnIR extractor (the WPF leak spike; recommended seam + v0 scope). - P-002 verification backend (Boogie/Dafny, horizon). - P-003 lifetime visualization (RustOwl-style, horizon). Conformance pilot: tests/test_spec.py runs one canonical program per normative rule and asserts its code fires (15/15), so spec and checker cannot drift. Wired into run_tests; README structure updated. Gate + suite green: ruff, mypy --strict, analysis 123/123, codegen 23/23, fuzz, gallery 10/10, corpus 2/2, wpf 3/3, lifetimes 10/10, spec 15/15. --- README.md | 3 + docs/proposals/P-001-csharp-extractor.md | 71 +++++++++ docs/proposals/P-002-verification-backend.md | 55 +++++++ .../proposals/P-003-lifetime-visualization.md | 45 ++++++ docs/proposals/README.md | 41 +++++ spec/BufferPolicies.md | 54 +++++++ spec/CodegenContract.md | 56 +++++++ spec/Diagnostics.md | 76 ++++++++++ spec/Lifetimes.md | 59 ++++++++ spec/OwnCore.md | 142 ++++++++++++++++++ spec/README.md | 34 +++++ tests/run_tests.py | 6 +- tests/test_spec.py | 119 +++++++++++++++ 13 files changed, 760 insertions(+), 1 deletion(-) create mode 100644 docs/proposals/P-001-csharp-extractor.md create mode 100644 docs/proposals/P-002-verification-backend.md create mode 100644 docs/proposals/P-003-lifetime-visualization.md create mode 100644 docs/proposals/README.md create mode 100644 spec/BufferPolicies.md create mode 100644 spec/CodegenContract.md create mode 100644 spec/Diagnostics.md create mode 100644 spec/Lifetimes.md create mode 100644 spec/OwnCore.md create mode 100644 spec/README.md create mode 100644 tests/test_spec.py diff --git a/README.md b/README.md index 31263fb6..73e134c7 100644 --- a/README.md +++ b/README.md @@ -693,6 +693,8 @@ ownlang/ golden_arraypool/ # buffer.own + Program.cs (host-код; .csproj не входит) corpus/real-world/ # hand-reduced реальные ArrayPool-баги + expected-коды corpus/wpf/ # WPF lifetime-баги (zombie-VM, use-after-dispose) + spec/ # НОРМАТИВНАЯ спека: OwnCore/Buffer/Lifetimes/Diag/Codegen + docs/proposals/ # forward-looking RFC: P-001 C#-extractor, P-002 verif, ... docs/lifetimes.md # дизайн модуля lifetimes (WPF, регионы, слайсы) tests/ run_tests.py # кейсы анализа + codegen smoke + golden smoke @@ -702,6 +704,7 @@ ownlang/ test_corpus.py # пинит каждый corpus-кейс к expected-диагностикам test_wpf.py # WPF-корпус: коды + [resource: kind] метадата test_lifetimes.py # region-escape (OWN014) + валидация lifetime-порядка + test_spec.py # conformance: каждое правило spec/ срабатывает на примере pyproject.toml # gate: ruff + mypy --strict (см. ниже) ``` diff --git a/docs/proposals/P-001-csharp-extractor.md b/docs/proposals/P-001-csharp-extractor.md new file mode 100644 index 00000000..3858faa6 --- /dev/null +++ b/docs/proposals/P-001-csharp-extractor.md @@ -0,0 +1,71 @@ +# P-001 — C# → OwnIR extractor (the WPF leak spike) + +- **Status:** draft (decision pending: seam + v0 scope) +- **Depends on:** `spec/OwnCore.md`, `spec/Lifetimes.md` (the fact vocabulary) + +## Motivation + +Today OwnLang catches real bug *patterns*, but only on hand-written `.own`: there +is no C# front-end, so the corpus is hand-reduced. The highest-value next step — +and the one that turns "our DSL correctly rejected release-after-move" into +"Own.NET found a leak in **our real code**" — is ingesting actual C# for the +narrow class of leaks the core already models: event subscriptions, timers, +`IDisposable` fields, ignored `Subscribe` results. + +This is **not** a full C# ownership front-end (generics, async, dataflow — that is +human-years and explicitly rejected). It is a syntactic/local pattern extractor. + +## Scope (v0) + +Recognize, in classes that look like ViewModels/Views (heuristic: name ends +`ViewModel`/`View`, derives `Window`/`UserControl`/`Page`, implements +`INotifyPropertyChanged`): + +- `source.Event += handler` with no matching `-=` in a `Dispose`/`OnClosed`/ + `Unloaded` body; +- `Subscribe(...)` whose `IDisposable` result is ignored; +- (next) `DispatcherTimer` started with no `Stop`/`Tick -=`; +- (next) an `IDisposable` field with no cascade `Dispose`. + +Emit these as **OwnIR facts in the spec's vocabulary** (so DSL, C# and any future +front-end speak one language): + +```text +acquire(Subscription, loc) // event += / Subscribe(...) +release(Subscription, loc) // event -= / token.Dispose() +owner(this, Subscription) +escapes(this, App) // strong capture by a longer-lived source +``` + +The existing core then produces `OWN001` (no release path) / `OWN014` (region +escape), with the `[resource: subscription]` kind tag. + +## Non-goals + +XAML / binding engine / visual tree / routed events / dependency properties / +`WeakEventManager` inference / Rx beyond `IDisposable` / every event-aggregator +library. A `[OwnIgnore("reason")]` suppression attribute is the escape hatch. + +## Sketch / architecture + +**Recommended seam:** Roslyn (C#) extractor → OwnIR facts (JSON) → the existing +Python core checks them and renders diagnostics. Do **not** reimplement the +checker in C# (a second checker drifts from the core — the project's own +meta-irony). The two meet through OwnIR, exactly as `spec/` enables. + +```text +*.cs --[Roslyn extractor (C#)]--> facts.ownir.json --[Python core]--> OWN001/OWN014 +``` + +**Environment note:** this sandbox has `dotnet` only in CI (the `dotnet-golden` +job). So: build and fully test the **Python fact-ingest** locally against +hand-written `facts.ownir.json` fixtures now; the Roslyn extractor is a +CI-validated C# artifact (like the golden). Land **one pattern** first +(`event += without -=`) end-to-end before adding timers/fields. + +## Open questions + +1. **Seam:** confirm `C# extractor → OwnIR → Python core` (vs all-in-C#). +2. **v0 scope:** one pattern first, or the four-rule set in one go. +3. **OwnIR serialization:** JSON schema vs emitting `.own` directly. +4. Heuristic vs annotation for "this class is a lifetime-bound component". diff --git a/docs/proposals/P-002-verification-backend.md b/docs/proposals/P-002-verification-backend.md new file mode 100644 index 00000000..45eaad93 --- /dev/null +++ b/docs/proposals/P-002-verification-backend.md @@ -0,0 +1,55 @@ +# P-002 — Verification backend (Boogie / Dafny) + +- **Status:** draft (horizon — not a near-term commitment) +- **Depends on:** `spec/OwnCore.md` (the soundness theorem to discharge) + +## Motivation + +Today soundness is **argued and tested**, not proven: the property fuzzer + an +independent AST oracle + the spec conformance suite give strong empirical +confidence (the theory advisor's "Level 1"). The honest next rung is exporting +the core soundness obligation to an SMT-backed verifier so we can say more than +"this Python didn't lie on today's random draws". + +The theorem (from `spec/OwnCore.md §6`): + +> If a program is well-typed and the ownership check passes, then it cannot: +> use-after-release, double-release, release-while-borrowed, move-while-borrowed, +> or escape a stack-backed resource. + +## Scope + +- **Level 2 (target):** translate per-function proof obligations to **Boogie** + (→ Z3) — e.g. "at this `release`, no loan of `R` is active and `R` is OWNED". + Boogie is the right backend: it is the intermediate verification language Dafny + itself lowers to, and it maps cleanly onto our CFG + state lattice. +- **Level 3 (stretch):** a **Dafny** model of OwnCore semantics, with the rules + as lemmas. + +## Non-goals + +- Proving the C# **codegen** correct (translation validation is a separate, harder + problem; the `CodegenContract` + golden-compile cover it pragmatically). +- Proving anything about `unsafe` / interop. +- A Level-4 F\* mechanized soundness proof — interesting, far, and only worth it + with a concrete consumer pulling for it. + +## Sketch + +OwnCore already produces exactly the shape Boogie wants: a CFG, per-variable +state sets, and active-loan sets with a join that is *asserted* identical across +predecessors. A backend would emit, per block, `assert`/`assume` for the +permission each operation needs, and let Z3 discharge them. + +```text +CFG + states + loans --[obligation emitter]--> program.bpl --[Boogie/Z3]--> verified | counterexample +``` + +## Open questions + +1. Is empirical (fuzzer + conformance) confidence already "enough" for the PoC's + audience? (Likely yes until a user demands formal proof — this stays a + proposal until then.) +2. Boogie obligations per-function only, or whole-module? +3. How to keep the Boogie model and the Python checker in sync (shared spec rule + IDs as the contract). diff --git a/docs/proposals/P-003-lifetime-visualization.md b/docs/proposals/P-003-lifetime-visualization.md new file mode 100644 index 00000000..1aeffd34 --- /dev/null +++ b/docs/proposals/P-003-lifetime-visualization.md @@ -0,0 +1,45 @@ +# P-003 — Lifetime visualization (RustOwl-style) + +- **Status:** draft (horizon) +- **Depends on:** `spec/OwnCore.md`, `spec/Lifetimes.md` + +## Motivation + +The most compelling existing ownership tools for Rust are *visual*: **RustOwl** +(in-editor ownership/loan highlighting), **RustViz** (timeline of ownership and +borrow events), **BORIS** (borrow visualizer). For .NET there is no equivalent. +A "who holds whom, who must release, and why this object doesn't die" picture is +exactly the killer demo for the business-lifetime story — far more persuasive +than a code listing. + +## Scope + +- A **lifetime graph** per function: owners, their loans (shared/mut) as spans, + and `subscribe` edges, with the region-escape (OWN014) path highlighted + ("expected: Window — actual: App — path: bus → self"). +- A **timeline** per owned resource: acquire → borrows → move/release/escape. +- Output as text/ASCII first (cheap, CI-friendly), then SVG/DOT; IDE integration + much later. + +## Non-goals + +A full IDE extension or LSP server in v0. Runtime heap-graph visualization +(that is a separate runtime-diagnostics track). Anything requiring a GUI toolkit. + +## Sketch + +All the data already exists: the CFG carries instructions with symbols, states, +and loans; the lifetime analysis carries regions and `subscribe` edges. A +visualizer is a *consumer* of these facts — no new analysis. Start by emitting +DOT from the CFG + lifetime facts. + +```text +CFG + lifetime facts --[graph/timeline emitter]--> *.dot / ASCII timeline +``` + +## Open questions + +1. ASCII-only (CI-renderable, in-repo) vs SVG/DOT (needs Graphviz) for v0. +2. Per-function graph vs whole-module lifetime graph. +3. Does this belong before or after P-001? (A visualization of hand-written + `.own` is less compelling than one of *real* extracted C#, so likely after.) diff --git a/docs/proposals/README.md b/docs/proposals/README.md new file mode 100644 index 00000000..9ae14541 --- /dev/null +++ b/docs/proposals/README.md @@ -0,0 +1,41 @@ +# Proposals (`docs/proposals/`) + +**Forward-looking** design proposals for things OwnLang does *not* do yet. The +counterpart to [`spec/`](../../spec/): the spec is normative (what is true today, +pinned by tests); proposals are exploratory (options for tomorrow, no code +commitment). Keeping them apart stops aspirational docs from lying about the +code. + +Each proposal is numbered `P-NNN` and has the same shape: + +- **Status** — `draft` / `accepted` / `in progress` / `done` / `rejected`. +- **Motivation** — the real pain it solves. +- **Scope** and **Non-goals** — what it is *not* (the most important section; the + whole project's discipline is refusing the soul-eating version). +- **Sketch** — enough design to judge feasibility, not a full spec. +- **Open questions** — what must be decided before building. + +When a proposal is built, its behaviour moves into `spec/` (normative) and the +proposal is marked `done` with a pointer. + +## Index + +| # | Title | Status | +|---|-------|--------| +| [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | draft | +| [P-002](P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | draft | +| [P-003](P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | draft | + +## The long-term arc (one paragraph) + +OwnLang today is a sound, tested resource/borrow/lifetime checker for a small +`.own` DSL that lowers to C# (see `spec/`). The arc from here: +**(1)** retro-document and pin behaviour with the spec ✅; +**(2)** ingest *real* C# via a narrow Roslyn extractor that emits OwnIR facts in +the spec's vocabulary (P-001) — the first time the tool bites real code; +**(3)** optionally export proof obligations to a verification backend for the +core soundness theorem (P-002); +**(4)** surface lifetimes/loans visually (P-003). +The core stays the same checker throughout; everything else produces or consumes +OwnIR facts. We resist the boil-the-ocean versions of each (full C# frontend, +proving all of unsafe, XAML engine) — boredom keeps projects alive. diff --git a/spec/BufferPolicies.md b/spec/BufferPolicies.md new file mode 100644 index 00000000..cc5dbcad --- /dev/null +++ b/spec/BufferPolicies.md @@ -0,0 +1,54 @@ +# Buffer Storage Policies + +> **Status: normative, descriptive.** Source of truth: `ownlang/buffers.py`, +> `ownlang/codegen.py`. Buffers are owned resources (OwnCore §1–7 apply) with an +> additional *storage policy* that constrains escape and codegen. + +A buffer is introduced by a buffer-intent let, e.g. `let b = Buffer.scratch(n, +inline = 256)`. The namespace is `Buffer`; the method selects the mode. + +## Modes + +| Mode | Backing | Escape | Release | +|------|---------|--------|---------| +| `stack` | `stackalloc` | **local-only**, cannot escape | none (stack unwinds) | +| `scratch` | stack branch *or* pool branch | local-only | pool branch returns; clear if sensitive | +| `pooled` | `ArrayPool` rented array | owns the array | returns to the pool | +| `native` | `NativeMemory` unmanaged pointer | owns the pointer | frees the pointer | +| `inline` | fixed stack buffer | local-only | none | + +## Rules (normative) + +- **B1 — stack cannot escape.** A stack-backed buffer (`stack`, `inline`, or a + `scratch` whose pool fallback is forbidden) MUST NOT be returned, consumed, + stored in a longer-lived owner, or captured → **OWN015** (return), + **OWN016** (move to longer-lived owner). +- **B2 — movable escape unsupported.** Returning a `pooled`/`native` buffer is + rejected in the MVP because codegen has no handle representation for the caller + to Return/Free → **OWN017**. (Checker-accepts / codegen-rejects, see + [CodegenContract.md](CodegenContract.md).) +- **B3 — static bound for dynamic stack.** A dynamically-sized stack allocation + requires a statically-known bound (`max = N`) → **OWN021** if absent; + → **OWN019** if the inline capacity is too large for the stack. +- **B4 — size is integer.** A non-integer size → **OWN018**. +- **B5 — scratch fallback honesty.** A `scratch` that forbids the pool fallback + but whose size may exceed the inline limit → **OWN023**. Its compile-time + report MUST NOT advertise an ArrayPool branch that cannot occur at runtime. +- **B6 — sensitive must clear.** A `sensitive` buffer that is not cleared on + release → **OWN024** (zeroing before return/free is mandatory). +- **B7 — requested length preserved.** `scratch` lowering preserves the + *requested* logical length, independent of whether the stack or pool branch is + taken. + +## Logging surfaces + +Under `[Conditional]` compilation symbols, codegen may emit `OwnTrace` (which +branch was selected) and `OwnCounters` (stack hits, requested/returned bytes, +forced clears). These are off by default and never change semantics — see +`README.md` for the symbols. + +## Compile-time report + +`ownlang report` emits a per-buffer summary (mode, policy, runtime branches, +checks) to stdout and `*.ownreport.json`, attributed by resource identity +(name#line#col), not by variable name. diff --git a/spec/CodegenContract.md b/spec/CodegenContract.md new file mode 100644 index 00000000..5d8a10b6 --- /dev/null +++ b/spec/CodegenContract.md @@ -0,0 +1,56 @@ +# Codegen Contract + +> **Status: normative, descriptive.** Source of truth: `ownlang/codegen.py`. +> This is the contract between the checker and the C# code generator. It exists +> to stop the class of bug that dominated early development: codegen quietly +> emitting unsafe C# (double-return, leak, use-before-decl). + +## The contract + +- **C1 — separation.** The *checker* decides whether a program is sound. The + *codegen* decides whether it can lower a sound program to faithful C#. +- **C2 — codegen may reject, never lie.** Codegen MAY reject a checker-accepted + program it cannot lower, raising `CodegenError` (the program is sound but the + PoC has no faithful lowering). Codegen MUST NEVER emit semantically unsafe C# + to "make it compile". Honest rejection beats a wrong `Return`. + - Example: an escaping `pooled`/`native` buffer — the checker may model it, but + codegen rejects it (the caller has no handle to Return/Free). See + [BufferPolicies §B2](BufferPolicies.md) / OWN017. +- **C3 — resource identity, not name.** Codegen MUST track resources by identity + (carried across `move`), not by variable name. Looking only for `release x` + after `let y = move x` is forbidden ([OwnCore §1](OwnCore.md#1-resource-identity)). +- **C4 — release on all paths is real.** For a sound program, every owned + resource is released exactly once on every path. Codegen MUST preserve this: + the `finally` makes it hold across C# exceptions too. + +## Two lowering modes + +| Mode | When | Shape | +|------|------|-------| +| **try/finally hoist** | straight-line: no branch, no `move`, no owned `return`, laminar scopes with top-level releases | acquire → `try { ... } finally { release }`, nested for multiple resources | +| **faithful inline** | branches / ownership transfer / non-laminar scopes | releases emitted inline exactly where the source put them | + +The hoist emits **no** runtime "released?" flag: because the release is hoisted +*out* of the `try` (not also in the body), it runs exactly once with no guard. A +flag would only make sense if we did not trust the static result — and if we do +not trust it, we should not ship it. + +## What "faithful" means + +- `resource` emit templates (`emit_type`/`emit_acquire`/`emit_release`/ + `emit_borrow`) produce **real** .NET (e.g. `ArrayPool.Shared.Rent/Return`, + `byte[]`, `.AsSpan()`). Absent templates fall back to the schematic + `Resource.method()` form. +- A borrow binding renders as its C# view (the span / ref); an owned argument as + its variable. +- The generated C# is intentionally **boring**. Boring generated code is the + compiler doing the work instead of pretending to be an artist. + +## Verification + +The golden example (`examples/golden_arraypool/`) is the one place the generated +C# is genuinely compiled and run by the real .NET compiler — the `dotnet-golden` +CI job: it checks the emitted method stays byte-identical to the host +(`verify_emit.py`), then `dotnet run`s it. Elsewhere the property fuzzer asserts +the release-accounting invariant on generated programs via an independent AST +oracle. diff --git a/spec/Diagnostics.md b/spec/Diagnostics.md new file mode 100644 index 00000000..7c875058 --- /dev/null +++ b/spec/Diagnostics.md @@ -0,0 +1,76 @@ +# OwnLang Diagnostics + +> **Status: normative, descriptive.** The single source of truth is +> `ownlang/diagnostics.py` (`TITLES`); this document groups the codes and links +> them to the rule that raises them. All are `error` severity unless noted. + +The split between **definite** (holds on every path) and **maybe** (holds on some +path) codes is deliberate: a fault that holds everywhere is a sharper message +than one behind a branch. It falls out of the set-of-states lattice +([OwnCore §3](OwnCore.md#3-ownership-states)). + +## Flow-sensitive ownership / loans / permissions + +| Code | Title | Rule | +|------|-------|------| +| OWN001 | owned resource not released on all paths (possible leak) | [R1](OwnCore.md#6-rules-normative) | +| OWN002 | use after release | R2 (definite) | +| OWN003 | double release | R3 | +| OWN004 | borrow escapes its scope | R10 | +| OWN005 | use after move | R4 (definite) | +| OWN006 | mutable borrow while a shared borrow is live | R8 | +| OWN007 | move while borrowed | R5 | +| OWN008 | release while borrowed | R6 | +| OWN009 | use after possible release (released on some path) | R2 (maybe) | +| OWN010 | use after possible move (moved on some path) | R4 (maybe) | +| OWN011 | mutable borrow while another mutable borrow is live | R8 | +| OWN012 | shared borrow while a mutable borrow is live | R9 | +| OWN013 | owner accessed while it is mutably borrowed | R7 | +| OWN014 | value escapes to a longer-lived region (lifetime promotion) | [Lifetimes §L3](Lifetimes.md) | + +## Buffer storage policies + +See [BufferPolicies.md](BufferPolicies.md). + +| Code | Title | +|------|-------| +| OWN015 | stack-backed buffer cannot escape the current function | +| OWN016 | stack-backed buffer moved to a longer-lived owner | +| OWN017 | movable buffer escape is not supported by codegen (PoC limitation) | +| OWN018 | buffer size must be an integer | +| OWN019 | inline capacity too large for a stack-backed policy | +| OWN021 | stack allocation requires a statically known bound | +| OWN023 | scratch fallback forbidden but the size may exceed the inline limit | +| OWN024 | sensitive buffer is not cleared on release | + +## Unsupported + +| Code | Title | +|------|-------| +| OWN020 | unsupported construct (loops / async — out of scope for the MVP) | + +## Name resolution & structural + +| Code | Title | +|------|-------| +| OWN030 | undefined name (incl. undefined resource / lifetime) | +| OWN031 | name already defined in this scope (incl. redefined lifetime) | +| OWN032 | owned resource copied without 'move' | +| OWN033 | function must return a value on all paths | +| OWN034 | operation requires an owned resource | +| OWN035 | return type mismatch | +| OWN036 | cyclic lifetime ordering | + +## Extern / call boundary + +| Code | Title | +|------|-------| +| OWN040 | call to an undeclared function (unknown calls are forbidden) | +| OWN041 | call argument mismatch (arity / effect / plain-vs-resource) | + +## Rendering + +The CLI renders rustc-style: `file:line:col`, the source line, and a caret under +the named identifier (the first single-quoted name in the message). A finding +about a kind-tagged resource carries a `[resource: ]` suffix +([Lifetimes §L4](Lifetimes.md)). diff --git a/spec/Lifetimes.md b/spec/Lifetimes.md new file mode 100644 index 00000000..bd661115 --- /dev/null +++ b/spec/Lifetimes.md @@ -0,0 +1,59 @@ +# Lifetime Regions + +> **Status: normative, descriptive.** Source of truth: `ownlang/lifetimes.py`. +> This layer adds region reasoning on top of OwnCore — the "object escapes to a +> longer-lived region" theorem (the WPF zombie-ViewModel leak). + +## Model + +`lifetime` declarations define regions with a strict partial order: + +```ownlang +lifetime App; +lifetime Window < App; // Window is strictly shorter-lived than App +lifetime ViewModel < Window; // order is transitive +``` + +A function carries the lifetime of the object it sets up; its parameters carry +the lifetime of the service they are: + +```ownlang +fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel { + subscribe self to bus; // strong capture: bus now holds self +} +``` + +## Rules (normative) + +- **L1 — order is a strict partial order.** `<` is transitive. A region that + ends up strictly longer than itself is a cycle → **OWN036**. A reference to an + undeclared region → **OWN030**; a redeclared region → **OWN031**. +- **L2 — annotations resolve.** A function/parameter lifetime that names an + undeclared region → **OWN030**. +- **L3 — region escape.** `subscribe self to SOURCE` where `lifetime(SOURCE)` is + **strictly longer** than `lifetime(self)` promotes `self` to the longer region: + it stays reachable for the whole longer region and leaks → **OWN014**. A + capture by a source of equal-or-shorter lifetime is clean (no promotion). The + *ordering* is what makes it a leak. + +## L4 — resource kind metadata + +A `resource` may declare `kind "subscription token"`. The kind is domain-neutral +metadata threaded onto the owning symbol and surfaced on diagnostics as a +`[resource: ]` suffix. The core stays generic; a later WPF profile / C# +front-end keys off the kind to phrase findings in business terms — without the +core knowing about any domain. + +## Mitigation + +The safe counterpart to a leaking `subscribe` is the OwnCore token pattern: +`let t = acquire Subscription(bus); ... release t;`. A released token gives a +release path, so OWN001 stays quiet — i.e. both halves of the theorem reuse the +same machinery. + +## Out of scope (see proposals) + +No cross-procedural points-to: `self`/`source` are the function's own scope and +its annotated parameters, not an arbitrary object graph. Weak-reference policy as +an explicit escape hatch, and C# ingestion that would produce these facts from +real code, are tracked in [`docs/proposals/`](../docs/proposals/). diff --git a/spec/OwnCore.md b/spec/OwnCore.md new file mode 100644 index 00000000..8299c00e --- /dev/null +++ b/spec/OwnCore.md @@ -0,0 +1,142 @@ +# OwnCore Specification + +> **Status: normative, descriptive.** This document specifies what OwnLang *is +> today*, derived from the working checker — not a wish list. Every rule here is +> backed by the implementation (`ownlang/`) and pinned by a test (see +> [§9 Conformance](#9-conformance)). Forward-looking ideas live in +> [`docs/proposals/`](../docs/proposals/), never here. + +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, +no higher-ranked anything. Buffers and lifetime regions are layered on top and +specified separately ([BufferPolicies.md](BufferPolicies.md), +[Lifetimes.md](Lifetimes.md)). + +## 1. Resource identity + +A **variable name is not a resource.** A resource has a stable identity `R`, +created at `acquire`. `let y = move x` transfers ownership of `R` from `x` to +`y`; both names refer to the same `R`, and `R`'s cleanup identity (its +release/return action) travels with the move. Diagnostics and codegen MUST work +through resource identity, not variable name — checking only `release x` after +`let y = move x` would be a bug. + +## 2. Kinds and types + +```text +Owned resource a value that owns a resource R (acquired, moved, or an owned param) +&T (borrow) a shared, read-only loan of an owner +&mut T (borrow_mut) an exclusive, mutable loan of an owner +int / bool plain values (no ownership) +``` + +`Moved` and `Released` are **analyzer states, not user-facing types** (§3). + +## 3. Ownership states + +Each owned symbol carries a *set* of states — "what could be true here across all +paths". Merges at control-flow joins take the **union**. + +```text +OWNED owns its resource R +MOVED ownership transferred away (move / consumed by a call) +RELEASED released / disposed +ESCAPED ownership left the function: returned, or consumed by a callee +``` + +A *definite* fault holds on every path (`OWNED ∉ S`); a *maybe* fault holds on +some path (`OWNED ∈ S` but a gone-state is also present). The two get different, +sharper codes (§6). + +## 4. Loans and permissions + +A borrow is a first-class **Loan(owner, binding, kind)**, kind ∈ {SHARED, MUT}, +*added* when the borrow opens and *removed* when it closes. Loans live beside the +states, not inside them: **the owner stays OWNED while borrowed.** Permissions are +derived on demand: + +| Owner state | Active loans | Permissions | +|---|---|---| +| OWNED | none | Own + Read + Write + Drop | +| OWNED | shared | Read (Own/Write/Drop suspended) | +| 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 +invariant rather than assuming it. + +## 5. Operations + +```text +let x = acquire T(args) x: OWNED, identity R created +let y = move x y: OWNED(R), x: MOVED +borrow x as b { ... } opens a SHARED loan of x for the block +borrow_mut x as b { ... } opens a MUT loan of x for the block +use x reads x (needs Read) +release x needs Own + Drop (no live loan); x: RELEASED +call f(args) f must resolve; args carry effects (§8) +return x x escapes: needs Own (no live loan); x: ESCAPED +``` + +## 6. Rules (normative) + +Each rule names the diagnostic it raises. Codes are catalogued in +[Diagnostics.md](Diagnostics.md). + +- **R1 — release on all paths.** An OWNED resource live at scope exit (function + end or `return`) is a leak → **OWN001**. +- **R2 — no use after release.** Using a RELEASED (or consumed/ESCAPED) resource + on every path → **OWN002**; on only some path → **OWN009**. +- **R3 — no double release.** `release` of an already-RELEASED resource → + **OWN003**. +- **R4 — no use after move.** Using a MOVED resource on every path → **OWN005**; + on only some path → **OWN010**. +- **R5 — move needs Own.** `move`/`return` of a resource with a live loan → + **OWN007**. +- **R6 — release needs Drop.** `release` while a loan is live → **OWN008**. +- **R7 — owner read needs Read.** `use` of an owner that is mutably borrowed → + **OWN013**. +- **R8 — exclusive borrow.** `borrow_mut` while a shared loan is live → + **OWN006**; while another mutable loan is live → **OWN011**. +- **R9 — shared excludes mutable.** `borrow` while a mutable loan is live → + **OWN012**. +- **R10 — borrow cannot escape.** A borrow binding used outside its live block → + **OWN004**. +- **R11 — no implicit copy.** Binding an owned resource to a new name without + `move` → **OWN032**. +- **R12 — release needs an owner.** `release`/`move` of a non-owned value → + **OWN034**. + +## 7. Resource protocol (summary) + +```text +acquire R ==> exactly one release of R on every path, + OR R moved out, OR R returned as Owned. +No use after release. No double release. No release while borrowed. +``` + +## 8. Call boundary + +Every call MUST resolve to a declared `extern fn` or a local `fn`; an unknown +call is **OWN040** (no laundering ownership through opaque calls). Each parameter +carries an effect: `borrow` (temporary shared loan), `borrow_mut` (temporary +exclusive loan), `consume` (takes ownership → owner becomes ESCAPED), or plain. +`borrow`/`borrow_mut` parameters are **noescape** by definition; the only way a +value leaves is `consume`/return. Argument/effect mismatch → **OWN041**. + +## 9. Conformance + +Rules are not prose-only: each is pinned by an executable example. +`tests/test_spec.py` runs one canonical program per rule and asserts the exact +code, so the spec and the checker cannot drift. The broader gallery +(`tests/test_gallery.py`), region (`tests/test_lifetimes.py`) and corpus suites +extend this. A spec change 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, +and formal soundness proofs are explicitly **not** part of OwnCore today. They +are tracked in [`docs/proposals/`](../docs/proposals/). diff --git a/spec/README.md b/spec/README.md new file mode 100644 index 00000000..6603a494 --- /dev/null +++ b/spec/README.md @@ -0,0 +1,34 @@ +# OwnLang specification (`spec/`) + +This directory is the **normative, descriptive** specification of OwnLang: what +the language *is today*, derived from the working checker and pinned by tests. It +is not a wish list. Anything not yet built lives in +[`docs/proposals/`](../docs/proposals/) instead — keeping the two apart is how we +stop aspirational docs from lying about the code. + +| File | Covers | +|------|--------| +| [OwnCore.md](OwnCore.md) | the affine-ownership + borrow-permission core: identity, states, loans, rules R1–R12, call boundary | +| [BufferPolicies.md](BufferPolicies.md) | storage policies (stack/scratch/pooled/native/inline), rules B1–B7 | +| [Lifetimes.md](Lifetimes.md) | lifetime regions and the region-escape theorem, rules L1–L4 | +| [Diagnostics.md](Diagnostics.md) | every OWN code, grouped, linked to the rule that raises it | +| [CodegenContract.md](CodegenContract.md) | the checker↔codegen contract C1–C4, lowering modes | + +## Spec ↔ tests (conformance) + +Each normative rule is backed by an executable example, so the spec and the +checker cannot silently drift: + +- `tests/test_spec.py` — one canonical program per OwnCore/Lifetimes rule, + asserting the exact code. The conformance pilot. +- `tests/test_gallery.py`, `tests/test_lifetimes.py`, `tests/test_wpf.py`, + `tests/test_corpus.py` — broader pinned examples. + +A spec change without a matching test change (or vice-versa) is a red build. To +add a rule: write it here with an ID, add its example to `test_spec.py`, and add +the code to `Diagnostics.md`. + +## Reading order + +Start with [OwnCore.md](OwnCore.md). Buffers and lifetimes layer on top of it and +reuse its identity/states/loans machinery. diff --git a/tests/run_tests.py b/tests/run_tests.py index 3a186bd5..eaf21d4e 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1049,10 +1049,14 @@ def run() -> int: import test_lifetimes lt_rc = test_lifetimes.run() + # Spec conformance pilot: every normative spec/ rule fires on its example. + import test_spec + spec_rc = test_spec.run() + 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) else 0 + or gl_rc or co_rc or wpf_rc or lt_rc or spec_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_spec.py b/tests/test_spec.py new file mode 100644 index 00000000..7cab90fd --- /dev/null +++ b/tests/test_spec.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +""" +Spec conformance pilot (spec/OwnCore.md, spec/Lifetimes.md). + +One canonical program per normative rule, asserting that the rule's diagnostic +fires. This is the seam that keeps the written spec and the checker from +drifting: if a rule stops firing on its example, the build goes red. + +Membership, not exact-set: each case asserts the rule's code is *among* the +produced codes (a minimal program that isolates exactly one code is often +awkward; firing is what conformance needs). The broader suites +(test_gallery / test_lifetimes / test_wpf / run_tests CASES) pin exact behaviour. + +Run: python tests/test_spec.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.buffers import validate_policies +from ownlang.cfg import ( + build_cfg, + collect_kinds, + collect_policies, + collect_signatures, +) +from ownlang.lexer import LexError +from ownlang.lifetimes import check_lifetimes +from ownlang.parser import ParseError, parse + +_BUF = "resource Buf { acquire rent release give }" + + +def _codes(src: str) -> list[str]: + """All error codes the full checker produces for one source string.""" + try: + mod = parse(src) + except (ParseError, LexError): + return ["PARSE_ERROR"] + rnames = {r.name for r in mod.resources} + sigs = collect_signatures(mod) + kinds = collect_kinds(mod) + out = [d.code for d in validate_policies(collect_policies(mod))] + out += [d.code for d in check_lifetimes(mod)] + for fn in mod.functions: + cfg, d1 = build_cfg(fn, rnames, sigs, None, kinds) + out += [d.code for d in (d1 + analyze(cfg))] + return out + + +# (rule id, code that must fire, program) +CASES: list[tuple[str, str, str]] = [ + ("OwnCore-R1", "OWN001", + f"module M\n{_BUF}\nfn f() {{ let a = acquire Buf(); }}"), + ("OwnCore-R2", "OWN002", + f"module M\n{_BUF}\nfn f() {{ let a = acquire Buf(); release a; use a; }}"), + ("OwnCore-R3", "OWN003", + f"module M\n{_BUF}\nfn f() {{ let a = acquire Buf(); release a; release a; }}"), + ("OwnCore-R4", "OWN005", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); let b = move a; use a; release b; }"), + ("OwnCore-R5", "OWN007", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); borrow a as x { let b = move a; release b; } }"), + ("OwnCore-R6", "OWN008", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); borrow a as x { release a; } }"), + ("OwnCore-R7", "OWN013", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); borrow_mut a as x { use a; } release a; }"), + ("OwnCore-R8", "OWN006", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); borrow a as x { borrow_mut a as y { } } " + "release a; }"), + ("OwnCore-R9", "OWN012", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); borrow_mut a as x { borrow a as y { } } " + "release a; }"), + ("OwnCore-R11", "OWN032", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); let b = a; release a; }"), + ("OwnCore-R12", "OWN034", + f"module M\n{_BUF}\nfn f(x: int) {{ release x; }}"), + ("OwnCore-S8", "OWN040", + f"module M\n{_BUF}\nfn f() {{ let a = acquire Buf(); Unknown(a); release a; }}"), + ("Lifetimes-L1", "OWN036", + "module M\nlifetime A < B;\nlifetime B < A;"), + ("Lifetimes-L2", "OWN030", + "module M\nlifetime App;\nfn f() lifetime Bogus { }"), + ("Lifetimes-L3", "OWN014", + "module M\nlifetime App;\nlifetime ViewModel < App;\n" + "fn VM(bus: EventBus lifetime App) lifetime ViewModel { subscribe self to bus; }"), +] + + +def run() -> int: + """Check every spec rule fires on its canonical example; return 0/1.""" + fails: list[str] = [] + matched = 0 + for rule, code, src in CASES: + got = _codes(src) + if code in got: + matched += 1 + else: + fails.append(f"{rule}: expected {code} to fire, got {sorted(set(got))}") + for f in fails: + print(f"SPEC FAIL: {f}") + print(f"spec: {matched}/{len(CASES)} normative rules fire on their example") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From 69a536aa0d1148bec9bd0a246028d716e753aec3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 07:24:13 +0000 Subject: [PATCH 07/10] spec: complete the coverage map (Grammar, CLI, policy blocks); broaden conformance Round out the normative spec so every existing surface has a reference point for future changes: - spec/Grammar.md: the full surface syntax -- tokens (reserved vs contextual vs rejected), EBNF, and a construct->spec map. Was only in a parser docstring. - spec/CLI.md: check / emit / cfg / report and their exit semantics. - spec/BufferPolicies.md: add the 'policy {}' block + options spec (rule B8: unknown/malformed keys -> OWN030). - spec/README.md index + reading order updated. Conformance pilot broadened to 22 rules pinning ~21 distinct codes (added Buffer B1/B4/B8 and structural OWN031/033/035/041); the remaining codes (maybe-variants, buffer specifics) stay covered by the buffer/analysis suites. Gate + suite green; markdown cross-links validated. --- spec/BufferPolicies.md | 12 ++++++++ spec/CLI.md | 18 +++++++++++ spec/Grammar.md | 69 ++++++++++++++++++++++++++++++++++++++++++ spec/README.md | 10 ++++-- tests/test_spec.py | 17 +++++++++++ 5 files changed, 123 insertions(+), 3 deletions(-) create mode 100644 spec/CLI.md create mode 100644 spec/Grammar.md diff --git a/spec/BufferPolicies.md b/spec/BufferPolicies.md index cc5dbcad..dc95f949 100644 --- a/spec/BufferPolicies.md +++ b/spec/BufferPolicies.md @@ -40,6 +40,18 @@ inline = 256)`. The namespace is `Buffer`; the method selects the mode. *requested* logical length, independent of whether the stack or pool branch is taken. +## Buffer options and `policy` blocks + +A buffer-intent takes a positional `size` plus named options; a `policy P { ... }` +block is a **reusable bundle of the same defaults**, applied by `policy = P`. +Inline options win over the policy. Recognised keys: `inline`/`inline_bytes`, +`max`/`max_bytes`, `fallback` (`pool`/`forbidden`), `trace`, `counters`, +`clear`/`clear_on_release`, `sensitive`, `mode`, `policy`. + +- **B8 — keys are validated.** An unknown key in a `policy` block, or a malformed + value (e.g. `clear = ture`, `fallback = bogus`), is **OWN030** — never a silent + default. A duplicate key is reported too. + ## Logging surfaces Under `[Conditional]` compilation symbols, codegen may emit `OwnTrace` (which diff --git a/spec/CLI.md b/spec/CLI.md new file mode 100644 index 00000000..727c7c0d --- /dev/null +++ b/spec/CLI.md @@ -0,0 +1,18 @@ +# CLI + +> **Status: normative, descriptive.** Source of truth: `ownlang/__main__.py`. +> Run as `python -m ownlang `. + +| Command | Does | Exit | +|---|---|---| +| `check` | runs the full checker (policies + lifetimes + per-fn loans/permissions), prints rustc-style diagnostics | non-zero if any **error** | +| `emit` | prints the generated C# (or an honest `CodegenError` if unsupported, see [CodegenContract §C2](CodegenContract.md)) | non-zero on error | +| `cfg` | prints the control-flow graph (blocks + instructions) for inspection | — | +| `report`| prints the compile-time buffer report and writes `*.ownreport.json` | — | + +Notes: +- `check`'s non-zero exit on errors is what makes it usable as a CI gate. +- Diagnostics are sorted by `(line, code)`; rendering is rustc-style + (`file:line:col`, source line, caret) with a `[resource: ]` suffix when + the finding is about a kind-tagged resource. +- A parse/lex failure surfaces as a single **OWN020** at the offending line. diff --git a/spec/Grammar.md b/spec/Grammar.md new file mode 100644 index 00000000..d7b6e10e --- /dev/null +++ b/spec/Grammar.md @@ -0,0 +1,69 @@ +# Grammar + +> **Status: normative, descriptive.** Source of truth: `ownlang/lexer.py`, +> `ownlang/parser.py`. The surface syntax of OwnLang — what can be written. +> Semantics of each construct live in the other `spec/` files (linked inline). + +## Tokens + +- **Reserved keywords:** `module resource acquire release extern fn let move + borrow borrow_mut consume as use if else return mut policy lifetime subscribe` + and the emit templates `emit_type emit_acquire emit_release emit_borrow`. +- **Contextual keywords** (plain identifiers except in their one position, *not* + reserved): `kind` (in a resource body), `self`/`to` (in `subscribe`). +- **Rejected keywords** (lexed only to refuse them, → OWN020): `while for loop + async await yield spawn`. +- **Punctuation:** `( ) { } , : ; & = . -> <` +- **Literals:** `INT` (digits), `STRING` (`"..."` with `\n \t \" \\`), `IDENT`. +- Line comments `// ...`. No block comments. + +## Grammar (EBNF-ish) + +```text +module := "module" IDENT item* +item := resource | extern | fn | policy | lifetime + +resource := "resource" IDENT "{" rmember* "}" +rmember := ("acquire" | "release") IDENT + | ("emit_type"|"emit_acquire"|"emit_release"|"emit_borrow") STRING + | "kind" STRING +extern := "extern" "fn" IDENT "(" eparams? ")" ("->" type)? ";" +eparam := ("borrow" | "borrow_mut" | "consume")? IDENT // IDENT = type name +policy := "policy" IDENT "{" (IDENT "=" atom ";")* "}" +lifetime := "lifetime" IDENT ("<" IDENT)? ";" // "<" = shorter-than + +fn := "fn" IDENT "(" params? ")" ("->" type)? ("lifetime" IDENT)? block +param := IDENT ":" type ("lifetime" IDENT)? +type := "&" "mut"? IDENT | IDENT // "&" = borrow view + +block := "{" stmt* "}" +stmt := let | release | use | call | borrow | if | return | subscribe +let := "let" IDENT "=" rhs ";" +rhs := "acquire" IDENT "(" args? ")" | "move" IDENT | bufferintent | IDENT | INT +bufferintent:= IDENT "." IDENT "(" bargs? ")" // e.g. Buffer.scratch(...) +barg := IDENT "=" atom | atom // named option | positional size +release := "release" IDENT ";" +use := "use" IDENT ";" +call := IDENT "(" args? ")" ";" +borrow := ("borrow" | "borrow_mut") IDENT "as" IDENT block +if := "if" "(" cond ")" block ("else" block)? // cond is opaque text +return := "return" IDENT? ";" +subscribe := "subscribe" "self" "to" IDENT ";" +args := atom ("," atom)* +atom := INT | IDENT +``` + +## Construct → spec map + +| Construct | Declares / does | Spec | +|---|---|---| +| `resource { acquire/release }` | a resource protocol (one acquire verb, one release verb) | [OwnCore §1,§7](OwnCore.md) | +| `resource { emit_* "..." }` | real-.NET lowering templates | [CodegenContract](CodegenContract.md) | +| `resource { kind "..." }` | domain-neutral metadata tag | [Lifetimes §L4](Lifetimes.md) | +| `Buffer.(size, opts)` | a storage-policy buffer | [BufferPolicies](BufferPolicies.md) | +| `policy P { k = v; }` | reusable buffer defaults | [BufferPolicies §Policies](BufferPolicies.md) | +| `extern fn` / param effects | the call boundary | [OwnCore §8](OwnCore.md) | +| `lifetime` / `subscribe` | regions + strong capture | [Lifetimes](Lifetimes.md) | +| `if` | control flow only — the condition is opaque text, values are not modelled | [OwnCore §10](OwnCore.md) | + +Loops and `async` are out of scope and refused at lex time (**OWN020**). diff --git a/spec/README.md b/spec/README.md index 6603a494..6e26e54f 100644 --- a/spec/README.md +++ b/spec/README.md @@ -8,19 +8,23 @@ stop aspirational docs from lying about the code. | File | Covers | |------|--------| +| [Grammar.md](Grammar.md) | the surface syntax: tokens, EBNF, construct→spec map | | [OwnCore.md](OwnCore.md) | the affine-ownership + borrow-permission core: identity, states, loans, rules R1–R12, call boundary | -| [BufferPolicies.md](BufferPolicies.md) | storage policies (stack/scratch/pooled/native/inline), rules B1–B7 | +| [BufferPolicies.md](BufferPolicies.md) | storage policies (stack/scratch/pooled/native/inline), rules B1–B8, `policy` blocks | | [Lifetimes.md](Lifetimes.md) | lifetime regions and the region-escape theorem, rules L1–L4 | | [Diagnostics.md](Diagnostics.md) | every OWN code, grouped, linked to the rule that raises it | | [CodegenContract.md](CodegenContract.md) | the checker↔codegen contract C1–C4, lowering modes | +| [CLI.md](CLI.md) | the `check` / `emit` / `cfg` / `report` commands | ## Spec ↔ tests (conformance) Each normative rule is backed by an executable example, so the spec and the checker cannot silently drift: -- `tests/test_spec.py` — one canonical program per OwnCore/Lifetimes rule, - asserting the exact code. The conformance pilot. +- `tests/test_spec.py` — one canonical program per normative rule + (OwnCore R1–R12/S8, Lifetimes L1–L3, Buffer B1/B4/B8, structural), asserting + the rule's code fires. ~21 distinct codes pinned; the rest (maybe-variants, + buffer specifics) are covered by the suites below. - `tests/test_gallery.py`, `tests/test_lifetimes.py`, `tests/test_wpf.py`, `tests/test_corpus.py` — broader pinned examples. diff --git a/tests/test_spec.py b/tests/test_spec.py index 7cab90fd..ef4bff5d 100644 --- a/tests/test_spec.py +++ b/tests/test_spec.py @@ -96,6 +96,23 @@ def _codes(src: str) -> list[str]: ("Lifetimes-L3", "OWN014", "module M\nlifetime App;\nlifetime ViewModel < App;\n" "fn VM(bus: EventBus lifetime App) lifetime ViewModel { subscribe self to bus; }"), + # buffers + ("Buffer-B1", "OWN015", + "module M\nfn f() -> Buffer { let b = Buffer.stack(16); return b; }"), + ("Buffer-B4", "OWN018", + "module M\nfn f(flag: bool) { let b = Buffer.stack(flag); }"), + ("Buffer-B8", "OWN030", + "module M\npolicy P { bogus = 1; }"), + # structural + ("Struct-OWN031", "OWN031", + f"module M\n{_BUF}\n" + "fn f() { let a = acquire Buf(); let a = acquire Buf(); release a; }"), + ("Struct-OWN033", "OWN033", + f"module M\n{_BUF}\nfn f() -> Buf {{ }}"), + ("Struct-OWN035", "OWN035", + f"module M\n{_BUF}\nfn f(n: int) -> Buf {{ return n; }}"), + ("Struct-OWN041", "OWN041", + f"module M\n{_BUF}\nextern fn Need(consume Buf);\nfn f(x: int) {{ Need(x); }}"), ] From 375fa70973f66a0a82d92c164b62520bc5906d94 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 07:53:14 +0000 Subject: [PATCH 08/10] P-001 v0: C# -> OwnIR -> core leak pipeline (event += without -=) First time the tool bites real C#, along the recommended seam: a Roslyn extractor produces facts, the existing Python core renders the verdict -- one checker, not two. - ownlang/ownir.py + 'python -m ownlang ownir facts.json': ingests OwnIR facts, lowers them to a synthetic .own sketch (subscription = owned resource, += = acquire, -= = release), runs the core, and maps OWN001 back to the C# location with the [resource: subscription token] tag. - frontend/roslyn/OwnSharp.Extractor: syntax-only Roslyn that scans .cs for 'target += handler' with no matching '-=' and emits OwnIR JSON. CI-only (no local dotnet). - CI job 'wpf-extractor': real .cs -> extractor -> facts -> core -> leak at the C# line; the disposed sample stays silent. - tests/test_ownir.py (5 checks) pins the bridge locally against hand-written facts; wired into run_tests. docs/proposals/P-001 -> in progress (v0 built). Scope v0 is exactly the event-subscription leak; timers / IDisposable fields / region facts are next. Gate + suite green (ownir 5/5). --- .github/workflows/ci.yml | 34 +++++ README.md | 18 +++ docs/proposals/P-001-csharp-extractor.md | 19 ++- docs/proposals/README.md | 2 +- .../OwnSharp.Extractor.csproj | 16 +++ frontend/roslyn/OwnSharp.Extractor/Program.cs | 82 ++++++++++++ frontend/roslyn/README.md | 33 +++++ frontend/roslyn/samples/CustomerViewModel.cs | 14 ++ frontend/roslyn/samples/OrdersViewModel.cs | 21 +++ ownlang/__main__.py | 19 ++- ownlang/ownir.py | 124 ++++++++++++++++++ tests/fixtures/ownir/sample.facts.json | 19 +++ tests/run_tests.py | 8 +- tests/test_ownir.py | 83 ++++++++++++ 14 files changed, 487 insertions(+), 5 deletions(-) create mode 100644 frontend/roslyn/OwnSharp.Extractor/OwnSharp.Extractor.csproj create mode 100644 frontend/roslyn/OwnSharp.Extractor/Program.cs create mode 100644 frontend/roslyn/README.md create mode 100644 frontend/roslyn/samples/CustomerViewModel.cs create mode 100644 frontend/roslyn/samples/OrdersViewModel.cs create mode 100644 ownlang/ownir.py create mode 100644 tests/fixtures/ownir/sample.facts.json create mode 100644 tests/test_ownir.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 64b21fe0..aee8b065 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -84,3 +84,37 @@ jobs: cp examples/golden_arraypool/Program.cs "$RUNNER_TEMP/golden_app/Program.cs" dotnet run --project "$RUNNER_TEMP/golden_app" + # P-001: prove the C# leak pipeline end-to-end on real C# — the Roslyn + # extractor turns sample .cs into OwnIR facts, and the core surfaces the + # subscription leak at its C# location (and stays silent on the disposed one). + wpf-extractor: + name: C# leak extractor (Roslyn) -> OwnIR -> core + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.13" + - uses: actions/setup-dotnet@v4 + with: + dotnet-version: "8.0.x" + - name: Extract OwnIR facts from sample C# + run: | + dotnet run --project frontend/roslyn/OwnSharp.Extractor -- \ + frontend/roslyn/samples/CustomerViewModel.cs \ + frontend/roslyn/samples/OrdersViewModel.cs \ + -o "$RUNNER_TEMP/facts.json" + cat "$RUNNER_TEMP/facts.json" + - name: Check facts through the core + run: | + out=$(python -m ownlang ownir "$RUNNER_TEMP/facts.json" || true) + echo "$out" + echo "$out" | grep -q "CustomerViewModel.cs" \ + || { echo "FAIL: expected the CustomerViewModel leak"; exit 1; } + echo "$out" | grep -q "OWN001" \ + || { echo "FAIL: expected OWN001"; exit 1; } + if echo "$out" | grep -q "OrdersViewModel.cs"; then + echo "FAIL: disposed subscription wrongly reported"; exit 1 + fi + echo "OK: real C# -> facts -> OWN001 at the C# location" + diff --git a/README.md b/README.md index 73e134c7..9b85ad08 100644 --- a/README.md +++ b/README.md @@ -138,6 +138,21 @@ fn CustomerViewModel(bus: EventBus lifetime App) lifetime ViewModel { } ``` +**P-001 — настоящий C# (а не hand-reduced).** Узкий Roslyn-экстрактор +(`frontend/roslyn/`, syntax-only) находит `event += без -=` в реальном `.cs` и +эмитит OwnIR-факты; Python-мост (`python -m ownlang ownir facts.json`) прогоняет +их через **то же ядро** и выдаёт OWN001 **на месте C#**: + +```text +CustomerViewModel.cs:9: error: [OWN001] event 'bus.CustomerChanged' is subscribed + (handler 'OnCustomerChanged') but never unsubscribed — ... (leak) + [resource: subscription token] +``` +Ядро одно (не второй чекер на C#): экстрактор только производит факты. dotnet +есть лишь в CI (job `wpf-extractor` гоняет экстрактор на сэмплах сквозняком); +Python-мост тестируется локально (`tests/test_ownir.py`) на рукописных фактах. +Объём v0 и не-цели — в [`docs/proposals/P-001`](docs/proposals/P-001-csharp-extractor.md). + `corpus/wpf/` — self-checking корпус реальных WPF-паттернов (`before.cs`/ `after.cs`/`case.own`/expected), прибитый `tests/test_wpf.py`; региональная теорема — `tests/test_lifetimes.py` (10 кейсов). Полный план модуля (каталог @@ -682,6 +697,7 @@ ownlang/ cfg.py # resolver (Symbol/Kind) + collect_signatures + lowering, Invoke analysis.py # flow-sensitive dataflow: var-states + active loans + permissions lifetimes.py # lifetime-регионы: region-escape (OWN014) + валидация порядка + ownir.py # C#-факты (OwnIR) -> ядро -> диагностика на месте C# (P-001) diagnostics.py # коды OWN0xx в одном месте codegen.py # C# codegen (emit_* шаблоны, try/finally hoist + inline, буферы) report.py # compile-time buffer report -> stdout + .ownreport.json @@ -705,6 +721,8 @@ ownlang/ test_wpf.py # WPF-корпус: коды + [resource: kind] метадата test_lifetimes.py # region-escape (OWN014) + валидация lifetime-порядка test_spec.py # conformance: каждое правило spec/ срабатывает на примере + test_ownir.py # OwnIR-мост: C#-факты -> ядро -> OWN001 на месте C# + frontend/roslyn/ # C#-экстрактор (Roslyn, CI-only) + сэмплы .cs (P-001) pyproject.toml # gate: ruff + mypy --strict (см. ниже) ``` diff --git a/docs/proposals/P-001-csharp-extractor.md b/docs/proposals/P-001-csharp-extractor.md index 3858faa6..cb1cb52d 100644 --- a/docs/proposals/P-001-csharp-extractor.md +++ b/docs/proposals/P-001-csharp-extractor.md @@ -1,8 +1,25 @@ # P-001 — C# → OwnIR extractor (the WPF leak spike) -- **Status:** draft (decision pending: seam + v0 scope) +- **Status:** in progress — **v0 built** (`event += without -=`). Seam and v0 + scope decided as recommended below. - **Depends on:** `spec/OwnCore.md`, `spec/Lifetimes.md` (the fact vocabulary) +## What is built (v0) + +The `event += without -=` pattern, end-to-end, exactly along the recommended +seam: + +- **Roslyn extractor** (`frontend/roslyn/OwnSharp.Extractor`, C#, syntax-only): + scans `.cs`, emits OwnIR facts (JSON) — built & run in CI (`wpf-extractor`). +- **Python fact bridge** (`ownlang/ownir.py`, `python -m ownlang ownir`): lowers + facts to a synthetic `.own` sketch, runs the **existing core**, and maps the + OWN001 verdict back to the C# location with the `[resource: subscription + token]` tag. Tested locally against hand-written facts (`tests/test_ownir.py`). +- **CI** (`wpf-extractor` job): real `.cs` → extractor → facts → core → leak at + its C# line; the disposed sample stays silent. + +Next: timers, `IDisposable` fields, and feeding region facts to OWN014. + ## Motivation Today OwnLang catches real bug *patterns*, but only on hand-written `.own`: there diff --git a/docs/proposals/README.md b/docs/proposals/README.md index 9ae14541..94fcde3c 100644 --- a/docs/proposals/README.md +++ b/docs/proposals/README.md @@ -22,7 +22,7 @@ proposal is marked `done` with a pointer. | # | Title | Status | |---|-------|--------| -| [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | draft | +| [P-001](P-001-csharp-extractor.md) | C# → OwnIR extractor (the WPF leak spike) | in progress (v0 built) | | [P-002](P-002-verification-backend.md) | Verification backend (Boogie/Dafny) | draft | | [P-003](P-003-lifetime-visualization.md) | Lifetime visualization (RustOwl-style) | draft | diff --git a/frontend/roslyn/OwnSharp.Extractor/OwnSharp.Extractor.csproj b/frontend/roslyn/OwnSharp.Extractor/OwnSharp.Extractor.csproj new file mode 100644 index 00000000..8b95e816 --- /dev/null +++ b/frontend/roslyn/OwnSharp.Extractor/OwnSharp.Extractor.csproj @@ -0,0 +1,16 @@ + + + + Exe + net8.0 + enable + enable + ownsharp-extract + + + + + + + + diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs new file mode 100644 index 00000000..3d70b221 --- /dev/null +++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs @@ -0,0 +1,82 @@ +// OwnSharp OwnIR extractor (P-001 v0). +// +// Scans C# *source text* (syntax only — no compilation, no references) for the +// event-subscription leak pattern and emits OwnIR facts (JSON) in the OwnLang +// spec's vocabulary. The Python core (`python -m ownlang ownir facts.json`) then +// produces the verdict (OWN001 leak) at the C# location. +// +// v0 heuristic (documented in docs/proposals/P-001): a subscription is +// `target += handler` where the right side is a method group (identifier or +// member access), not e.g. `count += 1`. It is "released" if a matching +// `target -= handler` (same text on both sides) exists anywhere in the class. +// +// Usage: ownsharp-extract [more.cs ...] [-o facts.json] + +using System.Text.Json; +using Microsoft.CodeAnalysis; +using Microsoft.CodeAnalysis.CSharp; +using Microsoft.CodeAnalysis.CSharp.Syntax; + +var inputs = new List(); +string? outPath = null; +for (int i = 0; i < args.Length; i++) +{ + if (args[i] == "-o" && i + 1 < args.Length) outPath = args[++i]; + else inputs.Add(args[i]); +} + +if (inputs.Count == 0) +{ + Console.Error.WriteLine("usage: ownsharp-extract [...] [-o facts.json]"); + return 2; +} + +static bool IsHandler(ExpressionSyntax rhs) => + rhs is IdentifierNameSyntax || rhs is MemberAccessExpressionSyntax; + +static int LineOf(SyntaxNode node) => + node.GetLocation().GetLineSpan().StartLinePosition.Line + 1; + +var components = new List(); + +foreach (var path in inputs) +{ + var text = File.ReadAllText(path); + var file = Path.GetFileName(path); + var root = CSharpSyntaxTree.ParseText(text, path: path).GetRoot(); + + foreach (var cls in root.DescendantNodes().OfType()) + { + var assigns = cls.DescendantNodes().OfType().ToList(); + + // every `target -= handler` in this class, keyed by "left|right". + var unsub = new HashSet(); + foreach (var a in assigns) + if (a.IsKind(SyntaxKind.SubtractAssignmentExpression) && IsHandler(a.Right)) + unsub.Add($"{a.Left}|{a.Right}"); + + var subs = new List(); + foreach (var a in assigns) + { + if (!a.IsKind(SyntaxKind.AddAssignmentExpression) || !IsHandler(a.Right)) + continue; + subs.Add(new + { + @event = a.Left.ToString(), + handler = a.Right.ToString(), + line = LineOf(a.Left), + released = unsub.Contains($"{a.Left}|{a.Right}"), + }); + } + + if (subs.Count > 0) + components.Add(new { name = cls.Identifier.Text, file, subscriptions = subs }); + } +} + +var facts = new { module = "Extracted", components }; +var json = JsonSerializer.Serialize(facts, new JsonSerializerOptions { WriteIndented = true }); + +if (outPath is null) Console.WriteLine(json); +else File.WriteAllText(outPath, json); +return 0; diff --git a/frontend/roslyn/README.md b/frontend/roslyn/README.md new file mode 100644 index 00000000..5b2423f3 --- /dev/null +++ b/frontend/roslyn/README.md @@ -0,0 +1,33 @@ +# OwnSharp Roslyn extractor (P-001 v0) + +The C# half of the [P-001](../../docs/proposals/P-001-csharp-extractor.md) +pipeline: scan **real C#** and emit OwnIR facts that the existing Python core +checks. + +```text +*.cs --[OwnSharp.Extractor (Roslyn)]--> facts.json --[python -m ownlang ownir]--> OWN001 @ C# location +``` + +## What it does (v0) + +Syntax-only (no compilation, no references): finds `target += handler` event +subscriptions and marks each `released` iff a matching `target -= handler` exists +in the same class. Exactly the `event += without -=` leak pattern. The verdict +(OWN001) comes from the core, not from here — there is one checker, not two. + +## Run + +```bash +dotnet run --project OwnSharp.Extractor -- samples/CustomerViewModel.cs samples/OrdersViewModel.cs -o facts.json +python -m ownlang ownir facts.json +# -> CustomerViewModel.cs:9: error: [OWN001] event 'bus.CustomerChanged' ... (leak) +# (OrdersViewModel unsubscribes in Dispose -> nothing reported) +``` + +## Scope / honesty + +This sandbox has no local `dotnet`, so the extractor is built and run only in CI +(the `wpf-extractor` job); the Python bridge + core are tested locally +(`tests/test_ownir.py`) against hand-written facts. The heuristic (RHS is a +method group) and non-goals (XAML, timers, IDisposable fields, semantic event +resolution) are tracked in the proposal. diff --git a/frontend/roslyn/samples/CustomerViewModel.cs b/frontend/roslyn/samples/CustomerViewModel.cs new file mode 100644 index 00000000..2eaeb737 --- /dev/null +++ b/frontend/roslyn/samples/CustomerViewModel.cs @@ -0,0 +1,14 @@ +using System; + +// LEAK: subscribes to a (longer-lived) event bus in its constructor and never +// unsubscribes. The extractor emits a subscription with released=false, and the +// core reports OWN001 at the `+=` line. +public sealed class CustomerViewModel +{ + public CustomerViewModel(IEventBus bus) + { + bus.CustomerChanged += OnCustomerChanged; // no matching -= anywhere -> leak + } + + private void OnCustomerChanged(object? sender, EventArgs e) { } +} diff --git a/frontend/roslyn/samples/OrdersViewModel.cs b/frontend/roslyn/samples/OrdersViewModel.cs new file mode 100644 index 00000000..8c78b853 --- /dev/null +++ b/frontend/roslyn/samples/OrdersViewModel.cs @@ -0,0 +1,21 @@ +using System; + +// OK: subscribes in the constructor and unsubscribes in Dispose. The extractor +// finds a matching -= (released=true), so the core reports nothing. +public sealed class OrdersViewModel : IDisposable +{ + private readonly IEventBus _bus; + + public OrdersViewModel(IEventBus bus) + { + _bus = bus; + _bus.OrdersChanged += OnOrdersChanged; + } + + public void Dispose() + { + _bus.OrdersChanged -= OnOrdersChanged; // matching unsubscribe + } + + private void OnOrdersChanged(object? sender, EventArgs e) { } +} diff --git a/ownlang/__main__.py b/ownlang/__main__.py index 1984cd25..5dd8a7c9 100644 --- a/ownlang/__main__.py +++ b/ownlang/__main__.py @@ -5,6 +5,7 @@ python -m ownlang emit file.own # check, then print generated C# python -m ownlang cfg file.own # dump the control-flow graph python -m ownlang report file.own # buffer storage report + .ownreport.json + python -m ownlang ownir facts.json # check OwnIR facts extracted from C# (P-001) Exit code is non-zero if any error-level diagnostic was produced. """ @@ -172,13 +173,27 @@ def _read(path: str) -> str: return f.read() +def cmd_ownir(path: str) -> int: + """Check OwnIR facts (extracted from real C# by the Roslyn frontend) through + the same core, surfacing findings at their C# locations (P-001).""" + from .ownir import check_facts, load + findings = check_facts(load(path)) + for f in findings: + print(f.render()) + if not findings: + print(f"{path}: ok — no subscription leaks found") + n = len(findings) + print(f"\n{n} finding{'s' if n != 1 else ''}.") + return 1 if findings else 0 + + def main(argv: list[str]) -> int: - if len(argv) < 2 or argv[0] not in {"check", "emit", "cfg", "report"}: + if len(argv) < 2 or argv[0] not in {"check", "emit", "cfg", "report", "ownir"}: print(__doc__) return 2 cmd, path = argv[0], argv[1] return {"check": cmd_check, "emit": cmd_emit, "cfg": cmd_cfg, - "report": cmd_report}[cmd](path) + "report": cmd_report, "ownir": cmd_ownir}[cmd](path) if __name__ == "__main__": diff --git a/ownlang/ownir.py b/ownlang/ownir.py new file mode 100644 index 00000000..820cdd97 --- /dev/null +++ b/ownlang/ownir.py @@ -0,0 +1,124 @@ +""" +OwnIR fact bridge (P-001 v0): C# leak facts -> the existing OwnLang core. + +A Roslyn extractor (frontend/roslyn/, CI-only) scans real C# and emits *facts* in +the spec's vocabulary; this module ingests them, routes them through the proven +checker, and maps the verdict back to the original C# location. The core stays a +single checker — we do not reimplement it in C# (a second checker would drift). + +OwnIR v0 schema (JSON):: + + { + "module": "WpfApp", + "components": [ + { + "name": "CustomerViewModel", + "file": "CustomerViewModel.cs", + "subscriptions": [ + {"event": "bus.CustomerChanged", "handler": "OnCustomerChanged", + "line": 12, "released": false} + ] + } + ] + } + +A subscription is modelled as an owned `Subscription` resource: `event +=` is an +`acquire`, a matching `-=` / Dispose is a `release`. An unreleased subscription +is therefore the core's OWN001 (owned-but-not-released), carrying the +`[resource: subscription token]` kind tag — surfaced at the C# `line`. + +v0 covers exactly the `event += without -=` pattern (released == false -> leak). +Timers, IDisposable fields and region escape are later (see docs/proposals/P-001). +""" + +from __future__ import annotations + +import json +from dataclasses import dataclass +from typing import Any + +from .diagnostics import _SUBJECT_RE, Severity + +_PRELUDE = ( + 'resource Subscription {\n' + ' acquire Subscribe\n' + ' release Dispose\n' + ' kind "subscription token"\n' + '}\n' +) + + +@dataclass(frozen=True) +class Finding: + file: str + line: int + code: str + component: str + event: str + handler: str + message: str + + def render(self) -> str: + return (f"{self.file}:{self.line}: error: [{self.code}] " + f"{self.message} [resource: subscription token]") + + +def load(path: str) -> dict[str, Any]: + """Load an OwnIR facts file.""" + with open(path, encoding="utf-8") as f: + result: dict[str, Any] = json.load(f) + return result + + +def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: + """Lower OwnIR facts to a synthetic `.own` module (a readable ownership + sketch of the C#) plus a map from each synthetic handle to its source fact. + + Each subscription becomes `let = acquire Subscription();`, with a + `release` iff the extractor found a matching unsubscribe. Handles are globally + unique so a diagnostic naming one maps straight back to its C# location.""" + handles: dict[str, dict[str, Any]] = {} + lines = [f"module {facts.get('module', 'Extracted')}", "", _PRELUDE] + gid = 0 + for comp in facts.get("components", []): + cname = comp.get("name", f"Component{gid}") + lines.append(f"fn {cname}() {{") + for sub in comp.get("subscriptions", []): + handle = f"sub_{gid}" + gid += 1 + handles[handle] = {**sub, "component": cname, + "file": comp.get("file", "?")} + lines.append(f" let {handle} = acquire Subscription();") + if sub.get("released"): + lines.append(f" release {handle};") + lines.append("}") + lines.append("") + return "\n".join(lines), handles + + +def check_facts(facts: dict[str, Any]) -> list[Finding]: + """Run the core checker over the lowered facts and return findings mapped + back to their original C# locations (v0: the `event += without -=` leak).""" + # imported here to avoid a module-level cycle (ownir is a leaf consumer) + from .__main__ import _collect + + src, handles = to_own(facts) + diags, _ = _collect(src) + findings: list[Finding] = [] + for d in diags: + if d.severity != Severity.ERROR: + continue + m = _SUBJECT_RE.search(d.message) + sub = handles.get(m.group(1)) if m else None + if sub is None: + continue + findings.append(Finding( + file=sub["file"], line=int(sub.get("line", 0)), code=d.code, + component=sub["component"], event=sub.get("event", "?"), + handler=sub.get("handler", "?"), + message=(f"event '{sub.get('event', '?')}' is subscribed " + f"(handler '{sub.get('handler', '?')}') but never " + f"unsubscribed — the source keeps " + f"'{sub['component']}' alive (leak)"))) + findings.sort(key=lambda f: (f.file, f.line, f.code)) + return findings diff --git a/tests/fixtures/ownir/sample.facts.json b/tests/fixtures/ownir/sample.facts.json new file mode 100644 index 00000000..c92a4d69 --- /dev/null +++ b/tests/fixtures/ownir/sample.facts.json @@ -0,0 +1,19 @@ +{ + "module": "WpfApp", + "components": [ + { + "name": "CustomerViewModel", + "file": "CustomerViewModel.cs", + "subscriptions": [ + {"event": "bus.CustomerChanged", "handler": "OnCustomerChanged", "line": 12, "released": false} + ] + }, + { + "name": "OrdersViewModel", + "file": "OrdersViewModel.cs", + "subscriptions": [ + {"event": "bus.OrdersChanged", "handler": "OnOrdersChanged", "line": 20, "released": true} + ] + } + ] +} diff --git a/tests/run_tests.py b/tests/run_tests.py index eaf21d4e..30b99b88 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1053,10 +1053,16 @@ def run() -> int: import test_spec spec_rc = test_spec.run() + # OwnIR fact bridge (P-001): C#-extracted facts route through the core and + # surface a subscription leak at its C# location. + import test_ownir + ownir_rc = test_ownir.run() + 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) else 0 + or gl_rc or co_rc or wpf_rc or lt_rc or spec_rc + or ownir_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_ownir.py b/tests/test_ownir.py new file mode 100644 index 00000000..0893577f --- /dev/null +++ b/tests/test_ownir.py @@ -0,0 +1,83 @@ +#!/usr/bin/env python3 +""" +OwnIR fact-bridge tests (P-001 v0). + +The locally-testable half of the C#-extraction pipeline: given OwnIR facts (as a +Roslyn extractor would emit), the bridge must route them through the existing +core and surface a finding at the original C# location for an unreleased +subscription — and stay silent for a released one. + +The Roslyn extractor itself (frontend/roslyn/) needs dotnet and is validated in +CI; here we feed hand-written facts so the bridge + core path is pinned with no +dotnet dependency. + +Run: python tests/test_ownir.py + python tests/run_tests.py (runs it as part of the suite) +""" + +from __future__ import annotations + +import json +import os +import sys + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) + +from ownlang.ownir import check_facts, to_own +from ownlang.parser import parse + +_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures", "ownir", + "sample.facts.json") + + +def run() -> int: + """Pin the OwnIR bridge on the canonical leak/ok facts; return 0/1.""" + fails: list[str] = [] + checks = 0 + + with open(_FIXTURE, encoding="utf-8") as f: + facts = json.load(f) + + # the lowered sketch must be valid .own (it goes through the real parser). + src, _ = to_own(facts) + checks += 1 + try: + parse(src) + except Exception as e: + fails.append(f"lowered facts do not parse: {e}") + + findings = check_facts(facts) + + # exactly one finding: the unreleased CustomerViewModel subscription. + checks += 1 + if len(findings) != 1: + fails.append(f"expected 1 finding, got {len(findings)}: " + f"{[ (x.file, x.line, x.code) for x in findings ]}") + else: + f0 = findings[0] + checks += 1 + if (f0.file, f0.line, f0.code) != ("CustomerViewModel.cs", 12, "OWN001"): + fails.append(f"wrong location/code: {f0.file}:{f0.line} {f0.code}") + if "CustomerChanged" not in f0.message or "leak" not in f0.message: + fails.append(f"message missing event/leak: {f0.message!r}") + if "[resource: subscription token]" not in f0.render(): + fails.append("rendered finding missing kind tag") + + # a released subscription (OrdersViewModel) must NOT be reported. + checks += 1 + if any(x.component == "OrdersViewModel" for x in findings): + fails.append("released subscription was wrongly reported") + + # an empty facts set yields nothing and does not crash. + checks += 1 + if check_facts({"module": "Empty", "components": []}): + fails.append("empty facts produced findings") + + for f in fails: + print(f"OWNIR FAIL: {f}") + print(f"ownir: {checks - len(fails)}/{checks} bridge checks passed") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run()) From 26b868a9ba651cc4062153fd51154d8ec0f986d1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 09:22:37 +0000 Subject: [PATCH 09/10] Address CodeRabbit review (9 of 11 findings) Code / correctness: - lifetimes.py: drop the early-return on empty mod.lifetimes so a 'fn/param lifetime X' annotation referencing an undeclared region still emits OWN030 (was silently accepted with no declarations). Real soundness gap. - ownir.py: shape-check OwnIR facts (root/components/subscriptions) in load() AND to_own(), raising a clear ValueError on malformed input instead of a deep traceback. Tests: - test_lifetimes.py: guard the headline render check against empty diags (pick the OWN014 diagnostic explicitly). - test_wpf.py: compare sorted(codes), not sorted(set(...)), so a duplicate diagnostic is a regression, not masked. CI hardening: - ci.yml: add least-privilege 'permissions: contents: read' (action SHA-pinning stays deferred per README #7). Docs (stale-claim cleanup now that the P-001 extractor exists): - corpus notes + P-001: reword 'no C# front-end' to 'not direct extractor output; the P-001 extractor is narrow (event subscriptions)'. - P-001: v0 produces OWN001 with [resource: subscription token]; OWN014 is the next increment, not v0. - spec/OwnCore.md: conformance asserts the code is *among* produced codes (membership), matching test_spec. - docs/lifetimes.md: add 'text' language to the directory-tree fence (MD040). Gate + suite green (analysis 123/123, spec 22/22, wpf 3/3, lifetimes 10/10, ownir 5/5). --- .github/workflows/ci.yml | 6 ++++ .../arraypool-use-after-return/notes.md | 5 ++-- corpus/wpf/handler-use-after-dispose/notes.md | 5 ++-- corpus/wpf/viewmodel-escapes-to-app/notes.md | 5 ++-- corpus/wpf/zombie-viewmodel/notes.md | 7 +++-- docs/lifetimes.md | 2 +- docs/proposals/P-001-csharp-extractor.md | 6 ++-- ownlang/lifetimes.py | 9 ++++-- ownlang/ownir.py | 28 ++++++++++++++++--- spec/OwnCore.md | 9 +++--- tests/test_lifetimes.py | 12 +++++--- tests/test_wpf.py | 2 +- 12 files changed, 68 insertions(+), 28 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index aee8b065..4c0fc8aa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,11 @@ name: CI +# Least privilege: every job only reads the repo (no job pushes or needs write). +# Action SHA-pinning / persist-credentials hardening is deliberately deferred to +# a Dependabot/hardening pass — see README "где оно жульничает" item #7. +permissions: + contents: read + on: push: branches: ["**"] diff --git a/corpus/real-world/arraypool-use-after-return/notes.md b/corpus/real-world/arraypool-use-after-return/notes.md index 2a0e3dcb..4cc5ca45 100644 --- a/corpus/real-world/arraypool-use-after-return/notes.md +++ b/corpus/real-world/arraypool-use-after-return/notes.md @@ -18,8 +18,9 @@ case.own:14:14: error: [OWN002] borrow 'quotient' after it was released ^ ``` -**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C# -the checker ingested — OwnLang has no C# front-end. It demonstrates that the +**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not +direct C# extractor output (the narrow P-001 extractor covers event-subscription +leaks, not ArrayPool). It demonstrates that the ownership *logic* maps onto the real bug: had the code been written in OwnLang, the checker would have rejected it. The real-world specifics (the division math, the exact slice bounds) are abstracted to `acquire`/`release`/`borrow`. diff --git a/corpus/wpf/handler-use-after-dispose/notes.md b/corpus/wpf/handler-use-after-dispose/notes.md index 1aad4984..75f9a811 100644 --- a/corpus/wpf/handler-use-after-dispose/notes.md +++ b/corpus/wpf/handler-use-after-dispose/notes.md @@ -17,8 +17,9 @@ case.own:16:9: error: [OWN002] use 'sub' after it was released ^ ``` -**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C# -the checker ingested — OwnLang has no C# front-end. It shows the ownership +**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not +direct C# extractor output (the C# extractor in P-001 is narrow — event +subscriptions only). It shows the ownership *logic* maps onto the real bug; it does not model the dispatcher queue or exception flow. `before.cs` / `after.cs` are representative, not a verbatim copy of one PR. diff --git a/corpus/wpf/viewmodel-escapes-to-app/notes.md b/corpus/wpf/viewmodel-escapes-to-app/notes.md index 9edb514c..638ef478 100644 --- a/corpus/wpf/viewmodel-escapes-to-app/notes.md +++ b/corpus/wpf/viewmodel-escapes-to-app/notes.md @@ -26,8 +26,9 @@ source produces no diagnostic (no promotion possible). The fix (`after.cs`) keep a disposable token released on close — the slice-#1 acquire/release pattern — which gives the VM a release path back to its Window lifetime. -**Honesty / scope.** `case.own` is a *hand reduction*, not C# the checker -ingested (no C# front-end yet). `self`/`source` are the function's own scope and +**Honesty / scope.** `case.own` is a *hand reduction*, not direct C# extractor +output (the narrow P-001 extractor does not yet emit region facts). `self`/ +`source` are the function's own scope and its annotated parameters — there is no cross-procedural points-to, and weak-event policy as an explicit escape hatch is a later slice (see `docs/lifetimes.md`). `before.cs` / `after.cs` are representative, not a verbatim copy of one PR. diff --git a/corpus/wpf/zombie-viewmodel/notes.md b/corpus/wpf/zombie-viewmodel/notes.md index d73e94af..d7511d4d 100644 --- a/corpus/wpf/zombie-viewmodel/notes.md +++ b/corpus/wpf/zombie-viewmodel/notes.md @@ -26,9 +26,10 @@ stays a generic ownership checker, and a later WPF profile/front-end can read th kind to phrase this as "WPF004: subscription token never disposed" without the core knowing anything about WPF. -**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not C# -the checker ingested — OwnLang has no C# front-end (that is a later slice). It -shows the ownership *logic* maps onto the real leak: had the VM been written in +**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not +direct C# extractor output for this case. A narrow C# extractor now exists +(P-001, event subscriptions), but this example is curated to spotlight the +ownership logic: had the VM been written in OwnLang, the checker would have rejected it. The lifetime-region machinery that would catch "VM promoted to App-lifetime through the subscription" (the escape path) is a separate, later slice; here the bug is caught by plain diff --git a/docs/lifetimes.md b/docs/lifetimes.md index 40436ae2..d07e2178 100644 --- a/docs/lifetimes.md +++ b/docs/lifetimes.md @@ -20,7 +20,7 @@ ViewModel жива — зомби с `INotifyPropertyChanged`. GC не теле Архитектура — **модульный монолит** с platform-agnostic ядром: -``` +```text ownlang/ core states/lattice/dataflow/diagnostics (= нынешние analysis/cfg/diagnostics) buffers профиль OwnSharp.Performance (есть) diff --git a/docs/proposals/P-001-csharp-extractor.md b/docs/proposals/P-001-csharp-extractor.md index cb1cb52d..b7cd1792 100644 --- a/docs/proposals/P-001-csharp-extractor.md +++ b/docs/proposals/P-001-csharp-extractor.md @@ -54,8 +54,10 @@ owner(this, Subscription) escapes(this, App) // strong capture by a longer-lived source ``` -The existing core then produces `OWN001` (no release path) / `OWN014` (region -escape), with the `[resource: subscription]` kind tag. +In v0 the existing core produces `OWN001` (no release path) with the +`[resource: subscription token]` kind tag. `OWN014` (region escape) is enabled +once the extractor emits the `escapes(...)`/lifetime facts above — that is the +next increment, not v0. ## Non-goals diff --git a/ownlang/lifetimes.py b/ownlang/lifetimes.py index 9743a8d1..f6df898d 100644 --- a/ownlang/lifetimes.py +++ b/ownlang/lifetimes.py @@ -81,10 +81,13 @@ def _strictly_longer(decls: list[A.LifetimeDecl]) -> dict[str, set[str]]: def check_lifetimes(mod: A.Module) -> list[Diagnostic]: """Region diagnostics for a module: structural validation of the lifetime - order plus the per-function escape check. Empty when no lifetimes are used.""" + order plus the per-function escape check. Empty when no lifetimes are used. + + Note: we do NOT early-return on an empty `mod.lifetimes` — a function or + parameter may still carry a `lifetime X` annotation referencing an undeclared + region, which must be flagged (OWN030). With no declarations, `names` is empty + and any annotation is therefore undefined.""" diags: list[Diagnostic] = [] - if not mod.lifetimes: - return diags names: set[str] = set() for d in mod.lifetimes: diff --git a/ownlang/ownir.py b/ownlang/ownir.py index 820cdd97..e3ef5446 100644 --- a/ownlang/ownir.py +++ b/ownlang/ownir.py @@ -64,9 +64,19 @@ def render(self) -> str: def load(path: str) -> dict[str, Any]: - """Load an OwnIR facts file.""" + """Load and shape-check an OwnIR facts file (it is external input — a + malformed file should fail with a clear error, not a deep traceback).""" with open(path, encoding="utf-8") as f: - result: dict[str, Any] = json.load(f) + result: Any = json.load(f) + if not isinstance(result, dict): + raise ValueError("OwnIR root must be a JSON object") + comps = result.get("components", []) + if not isinstance(comps, list) or not all(isinstance(c, dict) for c in comps): + raise ValueError("OwnIR 'components' must be a JSON array of objects") + for c in comps: + subs = c.get("subscriptions", []) + if not isinstance(subs, list) or not all(isinstance(s, dict) for s in subs): + raise ValueError("each component's 'subscriptions' must be objects") return result @@ -80,10 +90,20 @@ def to_own(facts: dict[str, Any]) -> tuple[str, dict[str, dict[str, Any]]]: handles: dict[str, dict[str, Any]] = {} lines = [f"module {facts.get('module', 'Extracted')}", "", _PRELUDE] gid = 0 - for comp in facts.get("components", []): + components = facts.get("components", []) + if not isinstance(components, list): + raise ValueError("OwnIR 'components' must be a JSON array") + for comp in components: + if not isinstance(comp, dict): + raise ValueError("each OwnIR component must be a JSON object") cname = comp.get("name", f"Component{gid}") lines.append(f"fn {cname}() {{") - for sub in comp.get("subscriptions", []): + subscriptions = comp.get("subscriptions", []) + if not isinstance(subscriptions, list): + raise ValueError("component 'subscriptions' must be a JSON array") + for sub in subscriptions: + if not isinstance(sub, dict): + raise ValueError("each subscription must be a JSON object") handle = f"sub_{gid}" gid += 1 handles[handle] = {**sub, "component": cname, diff --git a/spec/OwnCore.md b/spec/OwnCore.md index 8299c00e..f43dc79e 100644 --- a/spec/OwnCore.md +++ b/spec/OwnCore.md @@ -129,10 +129,11 @@ value leaves is `consume`/return. Argument/effect mismatch → **OWN041**. ## 9. Conformance Rules are not prose-only: each is pinned by an executable example. -`tests/test_spec.py` runs one canonical program per rule and asserts the exact -code, so the spec and the checker cannot drift. The broader gallery -(`tests/test_gallery.py`), region (`tests/test_lifetimes.py`) and corpus suites -extend this. A spec change without a test change (or vice-versa) is a red build. +`tests/test_spec.py` runs one canonical program per rule and asserts the rule's +diagnostic code is among the produced codes, so the spec and the checker cannot +drift. The broader gallery (`tests/test_gallery.py`), region +(`tests/test_lifetimes.py`) and corpus suites pin exact behaviour. A spec change +without a test change (or vice-versa) is a red build. ## 10. Out of scope (see proposals, not here) diff --git a/tests/test_lifetimes.py b/tests/test_lifetimes.py index e8de52aa..c971fdcf 100644 --- a/tests/test_lifetimes.py +++ b/tests/test_lifetimes.py @@ -161,10 +161,14 @@ def run() -> int: # lifetimes, and place a caret under the source in the `subscribe` line. escape_src = CASES[0][1] diags = check_lifetimes(parse(escape_src)) - pretty = diags[0].render_pretty("m.own", escape_src) - for needed in ("bus", "App", "VM", "ViewModel", "^"): - if needed not in pretty: - fails.append(f"escape message missing {needed!r}") + headline = next((d for d in diags if d.code == "OWN014"), None) + if headline is None: + fails.append("escape_to_app: expected an OWN014 headline diagnostic") + else: + pretty = headline.render_pretty("m.own", escape_src) + for needed in ("bus", "App", "VM", "ViewModel", "^"): + if needed not in pretty: + fails.append(f"escape message missing {needed!r}") for f in fails: print(f"LIFETIMES FAIL: {f}") diff --git a/tests/test_wpf.py b/tests/test_wpf.py index 4cf3cdc6..135bdbbb 100644 --- a/tests/test_wpf.py +++ b/tests/test_wpf.py @@ -98,7 +98,7 @@ def run() -> int: with open(own, encoding="utf-8") as f: source = f.read() codes, rendered = _check(source) - got = sorted(set(codes)) + got = sorted(codes) # keep multiplicity: a duplicate code is a regression ok = True if got != want: fails.append(f"{case}: expected {want}, got {got}") From ef5b9ff8e92179e9ffcbac33c2970dc681f4bf09 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 09:29:48 +0000 Subject: [PATCH 10/10] ast_nodes: document that frozen=True is shallow by design (CodeRabbit #6) --- ownlang/ast_nodes.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/ownlang/ast_nodes.py b/ownlang/ast_nodes.py index 22dbd80c..9542aa34 100644 --- a/ownlang/ast_nodes.py +++ b/ownlang/ast_nodes.py @@ -1,4 +1,13 @@ -"""AST for OwnLang. Plain dataclasses; every node carries a source line.""" +"""AST for OwnLang. Plain dataclasses; every node carries a source line. + +Nodes are `@dataclass(frozen=True)`. The freeze is **shallow by design**: it +blocks attribute *rebinding* (`node.rhs = ...`), which is the realistic accident +we want to catch, but not mutation of a nested container (`node.args.append(...)` +still works). We rely on this plus a verified convention that no pass mutates AST +containers after parsing — `Module`'s collections are in fact filled by the +parser via `.append` during construction. Deep immutability (tuples / +MappingProxyType) was considered and deferred as low-value churn for the PoC. +""" from __future__ import annotations