diff --git a/AGENTS.execution-surfaces.md b/AGENTS.execution-surfaces.md new file mode 100644 index 00000000..31964004 --- /dev/null +++ b/AGENTS.execution-surfaces.md @@ -0,0 +1,365 @@ +# AGENTS.execution-surfaces.md + +> ADR + task spec. Итог аудита идеи «Forth-like stack VM как внутренний IR» +> для Own.NET. +> +> Документ агентно-ориентированный: можно скармливать Claude Code / Codex как +> контекст задачи целиком или по секциям. + +--- + +## 0. Решение (ADR) + +Статус: **accepted**. + +**REJECT** — Forth-like stack VM как внутренний IR для Own.NET: + +- universal stack bytecode как центральная модель исполнения; +- сырой stack-DSL (`DUP` / `SWAP` / `ROT`) для написания людьми; +- VM «на вырост» под спекулятивные workload'ы, которых сейчас нет; +- отдельный интерпретатор правил поверх уже существующего dataflow-ядра. + +**ADOPT** — problem-oriented execution surface для Own.NET: + +- typed operation/primitive registry; +- explicit typed signatures + композиционная проверка pipeline'ов через существующий mypy gate, не через runtime-VM; +- structured evidence/provenance как расширение существующего `diagnostics.Evidence`; +- small composable primitives; +- registry операций/детекторов вместо нового DSL; +- per-finding explain surface — отдельно и позже, после покрытия diagnostics evidence. + +**RECONSIDER LATER** — generated stack bytecode допустим только при появлении +workload'а профиля AwkwardForth: + +- машинно-генерируемые программы; +- линейная потоковая обработка; +- высокочастотное исполнение; +- нужен portable bytecode; +- человек этот язык руками не пишет. + +Такого workload'а в Own.NET сейчас нет. + +--- + +## 1. Обоснование + +Ядро Own.NET — это не линейный pipeline вида: + +``` +input -> transform -> transform -> output +``` + +Текущая модель Own.NET: + +``` +parser + -> CFG + -> flow-sensitive dataflow + -> worklist-fixpoint + -> ActiveLoans + -> union на merge + -> diagnostics +``` + +Это graph/fixpoint-задача, а не задача для стекового байткода. + +Стековая VM хорошо ложится на straight-line обработку потока данных. Own.NET же решает задачу распространения состояний по CFG: + +- состояние owned-символа — множество `{OWNED, MOVED, RELEASED, ESCAPED}`; +- borrow — first-class `Loan`; +- active loans живут рядом с variable state; +- на merge происходит union состояний; +- циклы обрабатываются worklist-fixpoint; +- diagnostics эмитятся после схождения. + +Стековый IR здесь создаст лишний слой, поверх которого всё равно придётся писать fixpoint-driver. То есть VM не заменит ядро анализа, а станет дополнительной accidental complexity. + +Естественный декларативный target при росте — Datalog / реляционная модель / Ascent / Soufflé-подобный подход, но не сейчас. Текущий Python worklist остаётся рабочей моделью PoC. + +Хорошие идеи Forth отделимы от стека: + +``` +dictionary -> registry операций +stack effects -> typed signatures +trace -> structured evidence +REPL -> query shell поверх registry +small words -> small composable primitives +``` + +--- + +## 2. Target design: typed rule primitive registry + +### 2.1 PrimitiveSpec + +Каждый детектор-примитив регистрируется с метаданными. + +```python +from dataclasses import dataclass +from enum import Enum + +class Effect(Enum): + PURE = "pure" # только читит факты + REPORTS = "reports" # эмитит диагностику + +@dataclass(frozen=True) +class PrimitiveSpec: + name: str # "loan_active_at" + input_types: tuple[type, ...] # conceptual: (Loan, Location) + output_type: type # conceptual: bool / Sequence[Loan] / state enum + effect: Effect + required_facts: frozenset[str] # {"loans", "cfg"} + doc: str +``` + +Примитивы — обычные типизированные функции. + +Registry: + +``` +dict name -> (PrimitiveSpec, function) +``` + +Композиционная корректность pipeline'ов проверяется существующим mypy gate репы: + +``` +ruff check . +mypy ownlang +``` + +Никакого runtime-bytecode, VM, отдельного parser DSL или Forth-like исполнения. + +### 2.2 Концептуальный стартовый набор примитивов + +Стартовый набор вытаскивается из текущего `analysis.py`, не меняя семантику: + +``` +state_at(Symbol, Location) -> OwnershipState +loan_active_at(Loan, Location) -> bool +loans_of(Symbol, Location) -> Sequence[Loan] +escapes_at(Symbol, Location) -> bool +moved_between(Symbol, Location, Location) -> bool +``` + +Важно: сигнатуры выше — целевая концептуальная форма API, не требование вводить новые доменные типы. + +`Location` / `OwnershipState` в текущем коде не существуют. Текущая модель — это: + +``` +CFG +State +VarState +Loan +Block +Instr +line +RID +handle_rid +``` + +При реализации маппить концептуальные сигнатуры на существующие типы. Не плодить параллельную ownership-модель. Новые доменные типы — только отдельным PR с тестами и явным обоснованием. + +--- + +## 3. Structured evidence: расширить существующий Evidence + +В Own.NET уже есть каноническая модель structured evidence: + +``` +diagnostics.Evidence +Diagnostic.evidence +ownlang/evidence.py +``` + +`diagnostics.Evidence` / `Diagnostic.evidence` — structured successor текстовых riders: location, role, rendering. + +`ownlang/evidence.py` — проекция reachability-slice evidence в SARIF: + +``` +relatedLocations +codeFlows +``` + +Это общий shape для OwnIR DI checker, ownership checker и будущих frontends. + +### 3.1 Что делать + +Расширить покрытие evidence, не заменять модель: + +- `Evidence` остаётся каноническим per-diagnostic shape вторичных локаций; +- добавить недостающие evidence-продьюсеры в `analysis.py` для выбранных flow-диагностик; +- OwnIR/SARIF `codeFlows` потребляют тот же evidence-словарь; +- render evidence — только в presentation слоях: CLI / SARIF / human output; +- задокументировать, где merge-point evidence остаётся частичным. + +### 3.2 Какие события покрывать evidence + +Приоритетные события: + +``` +resource assigned/acquired +loan issued +loan killed +resource moved +resource released +resource consumed/escaped +return escape +merge-point union +``` + +Для merge-point evidence честно указывать ограничения. Не изображать точность, которой нет. Это статанализатор, а не гадалка в халате. + +### 3.3 Что запрещено + +Запрещено вводить параллельный provenance type: + +``` +ProvenanceFact +FactKind +FlowFact +Evidence2 +``` + +Два стандарта provenance для борьбы с одним — это не архитектура, это «Utils2». + +--- + +## 4. Per-finding explain: не перегружать существующую команду explain + +Текущая команда: + +``` +python -m ownlang explain OWN001 +python -m ownlang explain --json findings.json +``` + +— это каталог кодов диагностик: what / why / fix для diagnostic code. + +Она не является трассой конкретного finding. Семантику не менять, provenance на неё не вешать. + +Per-finding объяснение строится на `Diagnostic.evidence` и выносится в отдельную поверхность после появления покрытия evidence. + +Кандидаты: + +``` +check --show-evidence +ownir --format human --show-evidence +trace +``` + +В рамках текущей задачи обязательна только структурная часть: diagnostics должны нести evidence. Presentation surface едет следом. + +--- + +## 5. Acceptance criteria + +- [ ] Весь существующий тест-сьют зелёный. +- [ ] Семантика текущих проверок не менялась. +- [ ] Минимум 3 flow-диагностики несут непустой `Diagnostic.evidence`. +- [ ] Среди этих диагностик есть минимум одна из класса escape / lifetime / resource-leak. +- [ ] Среди этих диагностик есть минимум одна из класса use-after-move / use-after-release. +- [ ] Конкретные коды указаны в PR-описании, не спрятаны за словом «escape». +- [ ] Golden test на evidence в SARIF/codeFlows или human-render snapshot. +- [ ] `.ownreport.json` не перегружен. +- [ ] Новые/изменённые модули `ownlang` проходят существующий gate: `ruff check .` + `mypy ownlang`. +- [ ] Не добавлены новые `# type: ignore` ради прохождения gate. +- [ ] README обновлён: в «Where it cheats» честно описано, где merge-point evidence остаётся неполным. + +### 5.1 Что считать escape / lifetime / resource-leak классом + +В текущей модели слово «escape» многозначно. В PR-описании указывать конкретные коды. + +Примеры: + +``` +OWN001 resource leak +OWN014 lifetime / region escape +OWN015 stack-backed buffer escapes current function +OWN016 stack-backed buffer moved to longer-lived owner +OWN017 movable buffer escape unsupported by codegen +ESCAPED internal state +consume call-boundary escape +return return escape +``` + +--- + +## 6. Что НЕ делать + +- НЕ переписывать worklist/dataflow на Datalog сейчас. +- НЕ строить stack VM. +- НЕ строить интерпретатор правил. +- НЕ делать свой parser rule-DSL. +- НЕ вводить второй provenance-тип параллельно `diagnostics.Evidence`. +- НЕ вводить строковые provenance-факты вместо structured evidence. +- НЕ перегружать существующую команду `explain`. +- НЕ перегружать `.ownreport.json`. +- НЕ материализовать `Location` / `OwnershipState` из conceptual signatures как новые типы. +- НЕ менять mypy-конфиг всего репозитория ради галочки. +- НЕ упрощать branches в `analysis.py` ради эстетики, если это ухудшает читаемость dataflow. + +--- + +## 7. Лестница развития + +Текущий порядок: + +1. Python worklist жив, пока жив PoC. +2. Добавить evidence coverage. +3. Выделить facts/relations явно. +4. Только потом смотреть Datalog / Ascent / Soufflé. + +Datalog пересматривать только при реальной боли: + +- больше 30–50 правил с болезненными interdependencies; +- императивный код правил стал неуправляемым; +- есть измеримые проблемы с поддерживаемостью; +- ядро реально переезжает на Rust. + +Не пересматривать потому что «было бы красиво». Это не критерий, это источник техдолга с поэтическим уклоном. + +--- + +## 8. Trigger table + +| Решение отклонено | Пересмотреть, если | Кандидат | +| --- | --- | --- | +| Datalog-ядро | >30–50 правил с болезненными interdependencies, либо переезд ядра на Rust | Ascent / Soufflé | +| Stack bytecode | Появился workload: машинно-генерируемые, линейные, высокочастотные программы, потоковая обработка, portable bytecode, человек язык не пишет | маленькая typed stack VM | +| Per-finding explain UI | У diagnostics уже есть стабильное evidence coverage | `check --show-evidence`, `ownir --format human --show-evidence`, `trace` | +| REPL/query shell | Registry уже существует и полезен вручную | `ownnet repl` | + +Правило: + +``` +trigger = цифры из профилировщика или реальная боль в коде +``` + +Не: + +``` +trigger = красиво звучит в ADR +``` + +--- + +## 9. Порядок работ + +1. Добавить evidence coverage для 3 flow-диагностик. +2. Добавить golden/snapshot test на evidence. +3. Убедиться, что SARIF/codeFlows или human-render поверхность показывает evidence. +4. Обновить README: «Where it cheats». +5. Только после этого думать про registry/query shell. +6. Никаких VM, Datalog rewrite и rule DSL в этом этапе. + +--- + +## 10. Placement + +Канонический файл: + +``` +PhysShell/Own.NET/AGENTS.execution-surfaces.md +``` + +Этот документ относится к Own.NET. Не добавлять сюда графу 47, 007 или другие проекты. diff --git a/README.md b/README.md index 456dde6d..903b7bd1 100644 --- a/README.md +++ b/README.md @@ -625,6 +625,19 @@ justification" sets the discipline, but running the benchmarks is outside the sa Unsafe contracts (`UNS0xx`) are not yet implemented: `native` lowers into `NativeMemory.Alloc/Free` in an `unsafe` block, but pointer-escape checks are on the roadmap. +Diagnostic **evidence** (the structured `note:` reachability steps some findings +carry — acquire→escape for a stack buffer that returns/consumes at OWN015/OWN016, +move→use for OWN005, and the acquire site of a leaked resource at OWN001) is exact +on a straight-line path, and on a control-flow merge when all incoming paths agree +on the same move line. The analysis keeps the **union** of per-path state, so only +when branches *disagree* on where a resource was moved does the merge keep a +representative site and label the step "moved here (on one of several paths)" +rather than naming a line only one branch took — a static merge cannot say which +path ran. (An acquire site is almost always exact: a resource is minted at one +`acquire`, so its RID has a single source line; a leaked owned *parameter* is +minted with no in-body site and so carries no acquire step.) Evidence coverage is +also partial by design: most findings still carry no slice yet (they render +exactly as before), and only the four producers above are wired so far. --- diff --git a/docs/tasks/evidence-coverage.md b/docs/tasks/evidence-coverage.md new file mode 100644 index 00000000..80dc224d --- /dev/null +++ b/docs/tasks/evidence-coverage.md @@ -0,0 +1,186 @@ +# Task — evidence coverage for flow diagnostics + +Status: **spec, ready to implement** + +Derived from the ADR `AGENTS.execution-surfaces.md` (§3 «Structured evidence» +and §5 «Acceptance criteria»). This is the executable task spec for the first +rung of that document's ladder: wire the already-built-but-idle evidence +machinery so flow diagnostics carry a structured reachability slice. It extends, +and does not replace, `docs/proposals/P-015-reachability-evidence.md`. + +## 0. Goal + +Make at least 3 flow diagnostics carry a non-empty `Diagnostic.evidence` +(a structured acquire→escape / move→use reachability slice), with a golden test +on the human render. Do **not** change analyzer semantics. + +## 1. Scope + +**In scope** +- Thread `evidence=` through `_Analyzer.err()`. +- Evidence for 3 concrete codes (see §3). +- A minimal per-RID provenance addition to `State`, solely for the move site + (§3.3). +- A golden/snapshot test on the human render of evidence. +- README «Where it cheats»: an honest note on merge-point evidence being partial. + +**Out of scope (explicitly do not do)** +- A SARIF bridge for `Diagnostic`. Today `build_sarif` exists only for + `ownir.Finding`; building `Diagnostic → SARIF` is a separate PR. The golden + test rides the human render — the ADR allows «SARIF **or** human-render». +- `check --show-evidence` / `trace` / query shell / registry — later per the ADR. +- New domain types (`Location`, `OwnershipState`), a second provenance type, or + string facts — forbidden by the ADR. +- Any refactor of `analysis.py` branching for aesthetics. + +## 2. The emit-site change (mandatory foundation) + +`analysis.py` — `_Analyzer.err()` gains an optional parameter: + +```python +def err(self, code: str, msg: str, line: int, + subject: str | None = None, + resource_kind: str | None = None, + evidence: tuple[Evidence, ...] = ()) -> None: + if self.silent: + return + self.diags.append(Diagnostic(code, msg, line, subject=subject, + resource_kind=resource_kind, evidence=evidence)) +``` + +`evidence` is declared last, so the positional constructor contract +`Diagnostic(code, msg, line, severity, subject, resource_kind)` is preserved +(`evidence` is already the last field of the dataclass). Import `Evidence` into +`analysis.py`. The evidence branch must not do work before the `self.silent` +early-return. + +## 3. The target diagnostics + +Class coverage required by acceptance: two from escape/lifetime, one from +use-after-move. OWN001 (§3.4) adds the leak acquire site on top of the mandatory +minimum. + +### 3.1 OWN015 — stack-backed buffer escapes function *(escape / lifetime)* + +Data is already available; no new bookkeeping. Acquire site is the buffer's +allocation line (`sym.buffer.line`); escape site is the return line. + +```python +self.err("OWN015", , ins.line, subject=subj, evidence=( + Evidence(line=ins.sym.buffer.line, + label=f"'{ins.sym.name}' allocated here", role="acquired"), + Evidence(line=ins.line, + label="escapes the function by return here", role="escaped"), +)) +``` + +### 3.2 OWN016 — stack-backed buffer moved to longer-lived owner *(escape / lifetime)* + +Emitted in `_apply_effect` (`eff == CONSUME`). Same shape: acquire +`sym.buffer.line`, escape `line`, label «consumed by `'{callee}'` here», +`role="consumed"`. + +### 3.3 OWN005 — use / return after move *(use-after-move)* + +Emitted from `_state_problem` and the return branch. This one needs the **move +site**, which `State` does not currently record. Minimal addition (the only new +state): + +- In `State`: `moved_at: dict[int, tuple[int, bool]] = field(default_factory=dict)` + — RID → `(line, exact)`. `exact` is True when every path that moved this RID + moved it at the same line (a single precise site); False once merged paths + disagree, so the label cannot name a line only one branch took. +- Record it on a **real ownership transfer** in `MoveInto` — only when the source + is still `OWNED` before the move: `st.moved_at[src_rid] = (ins.line, True)`. A + second move of an already-moved handle is itself an OWN005; overwriting there + would later blame that failed move instead of the move that actually consumed + the resource, so keep the first site. +- Thread it through `State.copy()`. +- In `join()`: union the map via a `_join_moved_at` helper. When a RID is moved on + both paths at the **same** line, keep it exact; at **different** lines, keep a + deterministic representative (the earliest) and set `exact=False`. Do **not** + add an invariant `assert` like the `loans` one: multiple move paths are + legitimate here. +- On the OWN005 emit, build the step from `(line, exact)`: + `label = "moved here" if exact else "moved here (on one of several paths)"`; + `evidence=(Evidence(line=line, label=label, role="moved"),)` when a site is + present. + +### 3.4 OWN001 — resource leak *(acquire site)* — done + +Built as the symmetric counterpart to `moved_at`: an `acquired_at: +dict[int, tuple[int, bool]]` recorded when a resource is minted (`Acquire`, +`AcquireBuffer`, and a `MoveInto` destination), threaded through `copy()` and the +same `_join_sites` merge helper. `leak_check` attaches an "acquired here" step so +the leak — reported at the function exit / a return — points at the actionable +open site. A leaked owned *parameter* is minted with no in-body site, so it +carries no step. In practice the acquire site is always exact: a RID is minted at +a single `acquire`, so unlike a move it cannot disagree across paths (the inexact +branch stays defensively available but is unreachable in normal code). + +## 4. Presentation + +Nothing to change: `Diagnostic.human()` / `render_pretty()` already print one +`note:` line per step. The default CLI text output surfaces evidence +automatically. Do **not** introduce a `--show-evidence` flag here. + +## 5. Merge-point honesty (README) + +In README «Where it cheats» (and near the merge-union discussion): add 2–4 +sentences — evidence for move/escape is exact on straight-line paths and on +merges where all incoming paths agree on the same move line; only when branches +disagree does the merge keep a representative site and mark it one-of-N. «Do not +depict precision that isn't there» (ADR §3.2). + +## 6. Tests + +New standalone `tests/test_evidence_coverage.py` (repo convention — not pytest), +folded into `tests/run_tests.py` (like `test_gallery` / `test_corpus`): + +1. `.own` fixtures triggering OWN015, OWN016, OWN005, OWN001; run `analyze`; assert each + `Diagnostic.evidence` is non-empty and that roles/lines match the + acquire/escape/move sites. +2. Golden human-render snapshot: `Diagnostic.render_pretty()` contains the + expected `note:` lines in order. The pattern already exists in + `tests/test_diagnostics.py`. +3. Do not break the «empty-evidence invariant» in `test_diagnostics.py` + (diagnostics with no evidence still render byte-for-byte as before). + +## 7. Gate (hard) + +- `python tests/run_tests.py` green; `ruff check .` + `mypy ownlang` clean. +- **No new `# type: ignore`**; do not touch the repo mypy config. +- Do not «simplify» `analysis.py` branches. +- Do not add a second provenance type / string facts / new domain types. + +## 8. Acceptance mapping (from ADR §5) + +| ADR criterion | How it is met | +| --- | --- | +| ≥3 flow diagnostics with non-empty evidence | OWN015, OWN016, OWN005, OWN001 | +| ≥1 escape / lifetime / leak | OWN015 (§5.1: lifetime/region escape) + OWN016 | +| ≥1 use-after-move / use-after-release | OWN005 | +| Codes named in the PR body, not «escape» | listed explicitly | +| Golden test on evidence | `test_evidence_coverage.py` human-render snapshot | +| `.ownreport.json` not overloaded | `build_report` untouched | +| gate green, no new ignores | §7 | +| README «Where it cheats» on merge | §5 | + +## 9. PR shape + +- Type: `feat` (new structured information on diagnostics), or `docs+feat`; name + the codes **OWN015 / OWN016 / OWN005** explicitly in the PR body. +- Branch: the same feature branch, or a fresh follow-up branch off `main` if the + ADR PR is already merged (per repo rules a merged PR is not reused). + +## 10. Risks / pitfalls + +- **`join()` invariant.** The `moved_at` union must not trip the existing + `loans` / `handle_rid` asserts — it is a separate map added alongside, not + inside that check. +- **`_sym_by_id` / RID resolution.** Evidence labels take the name via the + existing `_sym_by_id` index — do not stand up a parallel index. +- **Positional `Diagnostic` constructor.** Only `evidence` goes last; do not + reorder anything. +- **`silent` mode.** `err()` accumulates nothing when `self.silent` — the + evidence branch must not do work before that check. diff --git a/ownlang/analysis.py b/ownlang/analysis.py index d6f5b09a..7ae63d68 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -65,7 +65,7 @@ Symbol, Use, ) -from .diagnostics import Diagnostic +from .diagnostics import Diagnostic, Evidence class VarState(Enum): @@ -100,12 +100,28 @@ class State: var: dict[int, set[VarState]] = field(default_factory=dict) loans: dict[int, Loan] = field(default_factory=dict) handle_rid: dict[int, int] = field(default_factory=dict) + # Provenance for the move site of a RID: RID -> (line, exact). `exact` is True + # when every path that moved this resource moved it at the same source line + # (a single, precise move to point evidence at); False when it was moved at + # different lines on different paths and merged — an honest "one of several + # paths" marker, since a static merge cannot say which path was taken. Feeds + # OWN005 evidence only; it carries no lattice state and changes no verdict. + moved_at: dict[int, tuple[int, bool]] = field(default_factory=dict) + # Provenance for the acquire site of a RID: RID -> (line, exact), same shape and + # merge rule as `moved_at`. Recorded when a resource is minted (acquire / buffer + # alloc / move destination). Feeds OWN001 evidence — the actionable "you opened + # it here" site the leak diagnostic itself (reported at function exit / a return) + # cannot name. An owned *parameter* is minted with no in-body site, so a leaked + # param carries no acquire step. Carries no lattice state and changes no verdict. + acquired_at: dict[int, tuple[int, bool]] = field(default_factory=dict) def copy(self) -> State: return State( var={k: set(v) for k, v in self.var.items()}, loans=dict(self.loans), handle_rid=dict(self.handle_rid), + moved_at=dict(self.moved_at), + acquired_at=dict(self.acquired_at), ) def rid_of(self, sym: Symbol) -> int: @@ -150,6 +166,29 @@ def _join_handle_rid(a: dict[int, int], b: dict[int, int]) -> dict[int, int]: return out +def _join_sites( + a: dict[int, tuple[int, bool]], b: dict[int, tuple[int, bool]] +) -> dict[int, tuple[int, bool]]: + """Merge two RID->(line, exact) provenance maps (acquire / move sites) of two + merging paths. Unlike the loan/handle joins this carries NO invariant: a + resource legitimately acquires or moves at different lines on different paths. + When the two agree on the line the site stays exact; when they disagree we keep + the earliest line deterministically and mark it inexact, so downstream evidence + says "one of several paths" instead of naming a line that only one path took. + Only ever used to *label* evidence (OWN001 acquire site / OWN005 move site).""" + out = dict(a) + for rid, (line_b, exact_b) in b.items(): + if rid in out: + line_a, exact_a = out[rid] + if line_a == line_b: + out[rid] = (line_a, exact_a and exact_b) + else: + out[rid] = (min(line_a, line_b), False) + else: + out[rid] = (line_b, exact_b) + return out + + def join(a: State, b: State) -> State: out = State() for k in set(a.var) | set(b.var): @@ -164,6 +203,8 @@ def join(a: State, b: State) -> State: ) out.loans = dict(a.loans) out.handle_rid = _join_handle_rid(a.handle_rid, b.handle_rid) + out.moved_at = _join_sites(a.moved_at, b.moved_at) + out.acquired_at = _join_sites(a.acquired_at, b.acquired_at) return out @@ -187,11 +228,39 @@ def initial_state(self) -> State: def err(self, code: str, msg: str, line: int, subject: str | None = None, - resource_kind: str | None = None) -> None: + resource_kind: str | None = None, + evidence: tuple[Evidence, ...] = ()) -> None: if self.silent: return self.diags.append(Diagnostic(code, msg, line, subject=subject, - resource_kind=resource_kind)) + resource_kind=resource_kind, + evidence=evidence)) + + def _moved_evidence(self, st: State, rid: int) -> tuple[Evidence, ...]: + """The move-site reachability step for an OWN005 finding, or empty when the + move site was not recorded. An inexact site (moved at different lines on + different merged paths) is labelled honestly rather than naming one path.""" + site = st.moved_at.get(rid) + if site is None: + return () + line, exact = site + label = "moved here" if exact else "moved here (on one of several paths)" + return (Evidence(line=line, label=label, role="moved"),) + + def _acquired_evidence(self, st: State, rid: int) -> tuple[Evidence, ...]: + """The acquire-site reachability step for an OWN001 leak, or empty when no + site was recorded (e.g. a leaked owned parameter, minted with no in-body + site). An inexact site (acquired at different lines on different merged + paths) is labelled honestly rather than naming one path.""" + site = st.acquired_at.get(rid) + if site is None: + return () + line, exact = site + sym = self._sym_by_id(rid) + who = f"'{sym.name}' " if sym else "" + suffix = "" if exact else " (on one of several paths)" + return (Evidence(line=line, label=f"{who}acquired here{suffix}", + role="acquired"),) # -- loan / permission helpers ----------------------------------------- @@ -227,7 +296,8 @@ def _state_problem(self, st: State, sym: Symbol, verb: str, line: int) -> bool: 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, resource_kind=kind) + line, subject=subj, resource_kind=kind, + evidence=self._moved_evidence(st, st.rid_of(sym))) elif VarState.ESCAPED in S and VarState.RELEASED not in S: self.err("OWN002", f"{verb} '{sym.name}' after it was consumed", line, @@ -350,7 +420,8 @@ def leak_check(self, st: State, at_line: int, context: str, f"'{name}' is owned but not released {context} " f"(leaks on at least one path)", at_line, subject=(sym.origin if sym else None), - resource_kind=(sym.resource_kind if sym else None)) + resource_kind=(sym.resource_kind if sym else None), + evidence=self._acquired_evidence(st, rid)) def _sym_by_id(self, symid: int) -> Symbol | None: if not hasattr(self, "_symindex"): @@ -380,17 +451,37 @@ def transfer(self, blk: Block, st: State) -> State: def step(self, ins: Instr, st: State) -> None: if isinstance(ins, Acquire): - st.var[st.mint(ins.sym)] = {VarState.OWNED} + rid = st.mint(ins.sym) + st.var[rid] = {VarState.OWNED} + # remember where the resource was acquired, so a later leak (OWN001) + # can point evidence at the acquire site instead of the function exit. + st.acquired_at[rid] = (ins.line, True) return if isinstance(ins, AcquireBuffer): - st.var[st.mint(ins.sym)] = {VarState.OWNED} + rid = st.mint(ins.sym) + st.var[rid] = {VarState.OWNED} + st.acquired_at[rid] = (ins.line, True) return if isinstance(ins, MoveInto): self._consume_like(st, ins.src, "move", ins.line, code_borrowed="OWN007") - st.var[st.rid_of(ins.src)] = {VarState.MOVED} - st.var[st.mint(ins.dst)] = {VarState.OWNED} + src_rid = st.rid_of(ins.src) + # remember where the move happened, so a later use/return-after-move + # (OWN005) can point evidence at the move site. Record ONLY a real + # ownership transfer — a move of a handle that is already gone is + # itself an OWN005 error, and overwriting here would later blame that + # failed move instead of the move that actually consumed the resource + # (Codex P2). `_consume_like` only reports; it does not change state, + # so `var` still holds the pre-move state here. A single move is exact. + if VarState.OWNED in st.var.get(src_rid, {VarState.OWNED}): + st.moved_at[src_rid] = (ins.line, True) + st.var[src_rid] = {VarState.MOVED} + dst_rid = st.mint(ins.dst) + st.var[dst_rid] = {VarState.OWNED} + # the move destination is a freshly-owned obligation: if it later leaks, + # its acquire site is the move that produced it. + st.acquired_at[dst_rid] = (ins.line, True) return if isinstance(ins, AliasJoin): @@ -489,7 +580,9 @@ def step(self, ins: Instr, st: State) -> None: if VarState.MOVED in S: self.err("OWN005", f"'{ins.sym.name}' returned after it was moved", - ins.line, subject=subj, resource_kind=rkind) + ins.line, subject=subj, resource_kind=rkind, + evidence=self._moved_evidence( + st, st.rid_of(ins.sym))) else: self.err("OWN002", f"'{ins.sym.name}' returned after it was released", @@ -507,7 +600,15 @@ def step(self, ins: Instr, st: State) -> None: self.err("OWN015", f"'{ins.sym.name}' is a {ins.sym.buffer.mode.value} " f"buffer and may be stack-backed; it cannot escape " - f"the current function", ins.line, subject=subj) + f"the current function", ins.line, subject=subj, + evidence=( + Evidence(line=ins.sym.buffer.line, + label=f"'{ins.sym.name}' allocated here", + role="acquired"), + Evidence(line=ins.line, + label="escapes the function by return " + "here", role="escaped"), + )) elif ins.sym.buffer is not None: self.err("OWN017", f"'{ins.sym.name}' is a {ins.sym.buffer.mode.value} " @@ -564,7 +665,15 @@ def _apply_effect(self, st: State, sym: Symbol, eff: Effect, f"'{sym.name}' is a {sym.buffer.mode.value} buffer " f"and may be stack-backed; it cannot be moved to a " f"longer-lived owner by consuming it in '{callee}'", - line, subject=sym.origin) + line, subject=sym.origin, + evidence=( + Evidence(line=sym.buffer.line, + label=f"'{sym.name}' allocated here", + role="acquired"), + Evidence(line=line, + label=f"consumed by '{callee}' here", + role="consumed"), + )) elif sym.buffer is not None: self.err("OWN017", f"'{sym.name}' is a {sym.buffer.mode.value} buffer; " diff --git a/tests/run_tests.py b/tests/run_tests.py index 9c9d01fe..b422e952 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -1122,6 +1122,12 @@ def run() -> int: import test_explain explain_rc = test_explain.run() + # Evidence coverage (execution-surfaces ADR §3/§5): OWN015/OWN016/OWN005 carry + # a structured acquire->escape / move->use reachability slice, rendered as + # ordered `note:` lines, with the merge-point move site labelled honestly. + import test_evidence_coverage + evid_rc = test_evidence_coverage.run() + # Reactive-effect stability (P-020): the EFF001 effect-storm analysis — the # identity lattice, reference propagation, cycle safety, and the OwnIR bridge # mapping the optional `effects` block to an EFF001 finding (a new core @@ -1134,7 +1140,7 @@ def run() -> int: 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 loops_rc or spec_rc or ownir_rc or own5_rc or rid_rc or diag_rc - or explain_rc or effects_rc) else 0 + or explain_rc or effects_rc or evid_rc) else 0 if __name__ == "__main__": diff --git a/tests/test_evidence_coverage.py b/tests/test_evidence_coverage.py new file mode 100644 index 00000000..e2ab5718 --- /dev/null +++ b/tests/test_evidence_coverage.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +""" +Evidence coverage for flow diagnostics (execution-surfaces ADR §3/§5). + +The `diagnostics.Evidence` machinery (structured secondary locations rendered as +`note:` lines / SARIF codeFlows) existed but no flow diagnostic populated it — +every finding shipped `evidence == ()`. This pins the producers wired into +`ownlang/analysis.py`, one per acceptance class: + + * OWN015 — a stack-backed buffer escapes by return (escape / lifetime) + * OWN016 — a stack-backed buffer consumed into a longer-lived owner (escape) + * OWN005 — use / return after move (use-after-move) + * OWN001 — resource leak (acquire site of the leak) + +Two contracts per code: + 1. the structured slice: `Diagnostic.evidence` carries the exact + (line, role, label) steps for the acquire->escape / move->use path; + 2. the human render: `Diagnostic.render()` appends those steps as ordered + `note:` lines after the header (the presentation the CLI already emits). + +Plus the merge-point honesty check: a resource moved at different lines on +different paths and used after the merge is labelled "one of several paths", +never a single line only one path took — and the empty-evidence invariant still +holds for a finding with no slice (OWN001 leak). + +Run: python tests/test_evidence_coverage.py + python tests/run_tests.py (as part of the suite) +""" + +from __future__ import annotations + +import os +import sys + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), "..")) + +from ownlang.analysis import analyze +from ownlang.cfg import build_cfg, collect_policies, collect_signatures +from ownlang.diagnostics import Diagnostic +from ownlang.parser import parse + + +def _diags(src: str) -> list[Diagnostic]: + """Full parse -> CFG -> analyze pipeline, flattened to one diagnostic list.""" + mod = parse(src) + rnames = {r.name for r in mod.resources} + sigs = collect_signatures(mod) + pols = collect_policies(mod) + out: list[Diagnostic] = [] + for fn in mod.functions: + cfg, d1 = build_cfg(fn, rnames, sigs, pols) + out += d1 + analyze(cfg) + return out + + +def _pick(src: str, code: str) -> Diagnostic: + for d in _diags(src): + if d.code == code: + return d + raise AssertionError(f"expected a {code} diagnostic, got " + f"{sorted({d.code for d in _diags(src)})}") + + +# --- fixtures (line numbers matter: they are the evidence anchors) ---------- + +_OWN015 = ( + "module M\n" # 1 + "fn f() -> Buffer {\n" # 2 + " let b = Buffer.stack(64);\n" # 3 <- allocated + " return b;\n" # 4 <- escapes + "}\n" # 5 +) + +_OWN016 = ( + "module M\n" # 1 + "extern fn Store(consume Buffer);\n" # 2 + "fn f(n: int) {\n" # 3 + " let b = Buffer.scratch(n);\n" # 4 <- allocated + " Store(b);\n" # 5 <- consumed + "}\n" # 6 +) + +_OWN005 = ( + "module M\n" # 1 + "resource Conn { acquire open release close }\n" # 2 + "fn f() {\n" # 3 + " let c = acquire Conn(1);\n" # 4 + " let d = move c;\n" # 5 <- moved + " use c;\n" # 6 <- use after move + " release d;\n" # 7 + "}\n" # 8 +) + +# a second move of an already-moved handle is itself an OWN005; the *later* +# use-after-move must still be explained by the FIRST (real) move site, not by +# the failed second move (Codex P2 regression). +_OWN005_DOUBLE = ( + "module M\n" # 1 + "resource Conn { acquire open release close }\n" # 2 + "fn f() {\n" # 3 + " let a = acquire Conn(1);\n" # 4 + " let b = move a;\n" # 5 <- the real move + " let c = move a;\n" # 6 <- failed second move (OWN005) + " use a;\n" # 7 <- use after move (OWN005) + " release b;\n" # 8 + " release c;\n" # 9 + "}\n" # 10 +) + +# moved on both arms at *different* lines, then used after the merge: the move +# site is genuinely one-of-N, so the evidence must not name a single path's line +# as if it were certain. +_OWN005_MERGE = ( + "module M\n" # 1 + "resource Conn { acquire open release close }\n" # 2 + "fn f(n: int) {\n" # 3 + " let c = acquire Conn(1);\n" # 4 + " if (n) {\n" # 5 + " let x = move c;\n" # 6 + " } else {\n" # 7 + " let y = move c;\n" # 8 + " }\n" # 9 + " use c;\n" # 10 <- use after move (either path) + "}\n" # 11 +) + + +# OWN001 leak: the acquire site is the actionable "you opened it here" step the +# leak diagnostic (reported at the function exit) cannot name on its own. +_OWN001_LEAK = ( + "module M\n" # 1 + "resource Conn { acquire open release close }\n" # 2 + "fn f() {\n" # 3 + " let c = acquire Conn(1);\n" # 4 <- acquired here + " use c;\n" # 5 + "}\n" # 6 <- leak reported at exit +) + +# a leaked owned *parameter* is minted with no in-body acquire site, so it must +# carry no acquire step (honest — there is no source line to point at). +_OWN001_PARAM = ( + "module M\n" # 1 + "resource Conn { acquire open release close }\n" # 2 + "fn f(c: Conn) {\n" # 3 + " use c;\n" # 4 + "}\n" # 5 +) + + +def run() -> int: + fails: list[str] = [] + checks = 0 + + def expect(cond: bool, msg: str) -> None: + nonlocal checks + checks += 1 + if not cond: + fails.append(msg) + + # -- OWN015: acquire -> escape, both steps present and ordered ----------- + d = _pick(_OWN015, "OWN015") + steps = [(e.line, e.role, e.label) for e in d.evidence] + expect(steps == [ + (3, "acquired", "'b' allocated here"), + (4, "escaped", "escapes the function by return here"), + ], f"OWN015 evidence slice wrong: {steps}") + rendered = d.render("") + expect(rendered.splitlines()[1:] == [ + " note: 'b' allocated here at :3", + " note: escapes the function by return here at :4", + ], f"OWN015 render notes wrong:\n{rendered}") + + # -- OWN016: acquire -> consumed-by-call -------------------------------- + d = _pick(_OWN016, "OWN016") + steps = [(e.line, e.role, e.label) for e in d.evidence] + expect(steps == [ + (4, "acquired", "'b' allocated here"), + (5, "consumed", "consumed by 'Store' here"), + ], f"OWN016 evidence slice wrong: {steps}") + + # -- OWN005: exact move site -------------------------------------------- + d = _pick(_OWN005, "OWN005") + steps = [(e.line, e.role, e.label) for e in d.evidence] + expect(steps == [(5, "moved", "moved here")], + f"OWN005 evidence slice wrong: {steps}") + rendered = d.render("") + expect(rendered.splitlines()[-1] == " note: moved here at :5", + f"OWN005 render note wrong:\n{rendered}") + + # -- OWN005 double move: later use is explained by the FIRST move site --- + own005 = [d for d in _diags(_OWN005_DOUBLE) if d.code == "OWN005"] + use_after = [d for d in own005 if d.line == 7] + expect(len(use_after) == 1 + and [(e.line, e.label) for e in use_after[0].evidence] + == [(5, "moved here")], + "use-after-move must point at the first (real) move site, not the " + f"failed second move: " + f"{[(d.line, [(e.line, e.label) for e in d.evidence]) for d in own005]}") + + # -- OWN005 at a merge: the move site is one-of-N, labelled honestly ---- + d = _pick(_OWN005_MERGE, "OWN005") + expect(len(d.evidence) == 1 and not d.evidence[0].label.endswith("here") + and "one of several paths" in d.evidence[0].label, + f"OWN005 merge evidence should be marked inexact: " + f"{[(e.line, e.label) for e in d.evidence]}") + + # -- OWN001 leak: acquire site is the actionable step ------------------- + d = _pick(_OWN001_LEAK, "OWN001") + steps = [(e.line, e.role, e.label) for e in d.evidence] + expect(steps == [(4, "acquired", "'c' acquired here")], + f"OWN001 leak must point at the acquire site: {steps}") + expect(d.line != 4, "sanity: the leak is reported away from the acquire line") + + # a leaked owned parameter has no in-body acquire site -> no step + d = _pick(_OWN001_PARAM, "OWN001") + expect(d.evidence == (), + "a leaked owned parameter must carry no acquire step (no source site)") + + # -- empty-evidence invariant: OWN003 (double release) carries no slice -- + d = _pick("module M\nresource Conn { acquire open release close }\n" + "fn f(){ let c = acquire Conn(1); release c; release c; }\n", "OWN003") + expect(d.evidence == (), "OWN003 must not carry evidence (unchanged)") + expect("\n note:" not in d.render(""), + "a diagnostic with no evidence must render without note: lines") + + for f in fails: + print(f"EVIDENCE FAIL: {f}") + print(f"evidence: {checks - len(fails)}/{checks} evidence-coverage checks pass") + return 1 if fails else 0 + + +if __name__ == "__main__": + raise SystemExit(run())