From bca684ecb5a62e1c5b15d5b2e98feef67646cc13 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 20:18:35 +0000 Subject: [PATCH 1/6] docs: add execution-surfaces ADR (reject Forth stack VM as internal IR) Record the audit outcome for the "Forth-like stack VM as internal IR" idea: reject the stack VM / stack-DSL, adopt a problem-oriented execution surface (typed primitive registry, extended structured evidence via diagnostics.Evidence, per-finding explain later). Includes rationale, target design, acceptance criteria, non-goals, evolution ladder and a trigger table for reconsidering Datalog / stack bytecode. --- AGENTS.execution-surfaces.md | 365 +++++++++++++++++++++++++++++++++++ 1 file changed, 365 insertions(+) create mode 100644 AGENTS.execution-surfaces.md 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 или другие проекты. From 15db5f561fa6fdbd7c596fc171cc92cdf482eadc Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 20:32:02 +0000 Subject: [PATCH 2/6] docs: add evidence-coverage task spec (first rung of execution-surfaces ADR) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Executable ТЗ derived from AGENTS.execution-surfaces.md §3/§5: wire the idle Diagnostic.evidence machinery for three flow diagnostics (OWN015/OWN016 escape+lifetime, OWN005 use-after-move), with a golden human-render test and an honest README note on partial merge-point evidence. Grounded in concrete emit sites in ownlang/analysis.py. --- docs/tasks/evidence-coverage.md | 170 ++++++++++++++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 docs/tasks/evidence-coverage.md diff --git a/docs/tasks/evidence-coverage.md b/docs/tasks/evidence-coverage.md new file mode 100644 index 00000000..2c5378ec --- /dev/null +++ b/docs/tasks/evidence-coverage.md @@ -0,0 +1,170 @@ +# 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 three target diagnostics + +Class coverage required by acceptance: two from escape/lifetime, one from +use-after-move. + +### 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, int] = field(default_factory=dict)` — RID → + line where `MOVED` was set. +- Record it wherever `{VarState.MOVED}` is set (`MoveInto` and the consume-like + transitions): `st.moved_at[st.rid_of(ins.src)] = ins.line`. +- Thread it through `State.copy()`. +- In `join()`: union the map. When a RID is moved on both paths with **different** + lines, do not fabricate a precise line — keep one and mark the label as + approximate (see §5). Do **not** add an invariant `assert` like the `loans` + one: multiple move paths are legitimate here. +- On the OWN005 emit: + `evidence=(Evidence(line=st.moved_at.get(rid), label="moved here", role="step"),)` + when present. + +> OWN001 (leak, acquire site) is a **stretch**, not part of the mandatory +> minimum: it needs a symmetric `acquired_at` map built the same way as +> `moved_at`. Do it only if in scope. + +## 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; at a +control-flow merge (state union) the move site may be one of several paths, so +such evidence is marked one-of-N, not exact. «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; 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 | +| ≥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. From 915b35faf696d2352a471425bb58611f254dc7bb Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 20:40:00 +0000 Subject: [PATCH 3/6] feat(analysis): structured evidence for OWN015/OWN016/OWN005 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wire the idle diagnostics.Evidence machinery into the flow analysis so three findings carry a structured reachability slice (rendered as note: lines / SARIF codeFlows), per the execution-surfaces ADR §3/§5: - OWN015: stack-backed buffer escapes by return -> acquire (buffer alloc site) + escape (return) steps. - OWN016: stack-backed buffer consumed into a longer-lived owner -> acquire + consumed-by-call steps. - OWN005: use/return after move -> move-site step. State now records a per-RID move site (line, exact); at a control-flow merge a move at different lines on different paths is labelled one-of-N rather than naming a single path's line. No semantic change: evidence only annotates existing findings, carries no lattice state, and changes no verdict. Adds tests/test_evidence_coverage.py (slice + human-render golden + merge-point honesty + empty-evidence invariant) folded into run_tests.py, and an honest README 'Where it cheats' note on partial merge-point evidence. Gate green: run_tests, ruff, mypy ownlang; no new type: ignore. --- README.md | 9 ++ ownlang/analysis.py | 83 ++++++++++++++-- tests/run_tests.py | 8 +- tests/test_evidence_coverage.py | 171 ++++++++++++++++++++++++++++++++ 4 files changed, 262 insertions(+), 9 deletions(-) create mode 100644 tests/test_evidence_coverage.py diff --git a/README.md b/README.md index 456dde6d..45613bd2 100644 --- a/README.md +++ b/README.md @@ -625,6 +625,15 @@ 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) is exact only on a straight-line path. At a control-flow +merge the analysis keeps the **union** of per-path state, so when a resource was +moved at *different* lines on different branches the move-site step is honestly +labelled "moved here (on one of several paths)" rather than naming the line only +one branch took — a static merge cannot say which path ran. Evidence coverage is +also partial by design: most findings still carry no slice yet (they render +exactly as before), and only the three producers above are wired so far. --- diff --git a/ownlang/analysis.py b/ownlang/analysis.py index d6f5b09a..58195212 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,20 @@ 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) 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), ) def rid_of(self, sym: Symbol) -> int: @@ -150,6 +158,28 @@ def _join_handle_rid(a: dict[int, int], b: dict[int, int]) -> dict[int, int]: return out +def _join_moved_at( + a: dict[int, tuple[int, bool]], b: dict[int, tuple[int, bool]] +) -> dict[int, tuple[int, bool]]: + """Merge the RID->move-site maps of two merging paths. Unlike the loan/handle + joins this carries NO invariant: a resource legitimately 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* OWN005 evidence.""" + 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 +194,7 @@ 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_moved_at(a.moved_at, b.moved_at) return out @@ -187,11 +218,24 @@ 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"),) # -- loan / permission helpers ----------------------------------------- @@ -227,7 +271,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, @@ -389,7 +434,11 @@ def step(self, ins: Instr, st: State) -> None: 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} + src_rid = st.rid_of(ins.src) + st.var[src_rid] = {VarState.MOVED} + # remember where the move happened, so a later use/return-after-move + # (OWN005) can point evidence at the move site. A single move is exact. + st.moved_at[src_rid] = (ins.line, True) st.var[st.mint(ins.dst)] = {VarState.OWNED} return @@ -489,7 +538,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 +558,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 +623,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..fcc49899 --- /dev/null +++ b/tests/test_evidence_coverage.py @@ -0,0 +1,171 @@ +#!/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 first three 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) + +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 +) + +# 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 +) + + +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 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]}") + + # -- empty-evidence invariant: a leak (OWN001) carries no slice --------- + d = _pick("module M\nfn f(n: int){ let b = Buffer.scratch(n); }\n", "OWN001") + expect(d.evidence == (), "OWN001 leak 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()) From 1155ac408b0813d32c21b27293f4eaaa9957e981 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 22:05:52 +0000 Subject: [PATCH 4/6] fix(analysis): keep first move site for OWN005 evidence on double move Codex P2: a second move of an already-moved handle is itself an OWN005, but the move-site record was overwritten with that failed move's line. A later use/return-after-move then rendered 'moved here' at the failed second move instead of the move that actually consumed the resource. Record moved_at only on a real ownership transfer (source still OWNED), so the first move site is preserved. Adds a double-move regression to tests/test_evidence_coverage.py. --- ownlang/analysis.py | 12 +++++++++--- tests/test_evidence_coverage.py | 26 ++++++++++++++++++++++++++ 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/ownlang/analysis.py b/ownlang/analysis.py index 58195212..53b71c00 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -435,10 +435,16 @@ def step(self, ins: Instr, st: State) -> None: if isinstance(ins, MoveInto): self._consume_like(st, ins.src, "move", ins.line, code_borrowed="OWN007") src_rid = st.rid_of(ins.src) - st.var[src_rid] = {VarState.MOVED} # remember where the move happened, so a later use/return-after-move - # (OWN005) can point evidence at the move site. A single move is exact. - st.moved_at[src_rid] = (ins.line, True) + # (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} st.var[st.mint(ins.dst)] = {VarState.OWNED} return diff --git a/tests/test_evidence_coverage.py b/tests/test_evidence_coverage.py index fcc49899..383b096f 100644 --- a/tests/test_evidence_coverage.py +++ b/tests/test_evidence_coverage.py @@ -90,6 +90,22 @@ def _pick(src: str, code: str) -> Diagnostic: "}\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. @@ -148,6 +164,16 @@ def expect(cond: bool, msg: str) -> None: 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") From 61ec4c37c582c02ab07d4f45c3a2aa5fb47ed649 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 22:14:42 +0000 Subject: [PATCH 5/6] docs: align evidence-coverage spec + README with implemented moved_at shape CodeRabbit review nits (both docs-only): - docs/tasks/evidence-coverage.md: the moved_at sketch showed dict[int, int]; update it to the implemented dict[int, tuple[int, bool]] with the exactness flag, the record-only-on-real-transfer rule, and the exact/inexact OWN005 label in the example. - README 'Where it cheats': the wording implied any merge loses precision; clarify that exact evidence is preserved when all incoming paths agree on the move line, and only disagreeing branches degrade to 'one of several paths'. No code change. --- README.md | 15 ++++++------- docs/tasks/evidence-coverage.md | 37 ++++++++++++++++++++------------- 2 files changed, 30 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index 45613bd2..c6113eac 100644 --- a/README.md +++ b/README.md @@ -627,13 +627,14 @@ Unsafe contracts (`UNS0xx`) are not yet implemented: `native` lowers into 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) is exact only on a straight-line path. At a control-flow -merge the analysis keeps the **union** of per-path state, so when a resource was -moved at *different* lines on different branches the move-site step is honestly -labelled "moved here (on one of several paths)" rather than naming the line only -one branch took — a static merge cannot say which path ran. Evidence coverage is -also partial by design: most findings still carry no slice yet (they render -exactly as before), and only the three producers above are wired so far. +move→use for OWN005) 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. Evidence coverage is also partial by +design: most findings still carry no slice yet (they render exactly as before), +and only the three producers above are wired so far. --- diff --git a/docs/tasks/evidence-coverage.md b/docs/tasks/evidence-coverage.md index 2c5378ec..93bda1bb 100644 --- a/docs/tasks/evidence-coverage.md +++ b/docs/tasks/evidence-coverage.md @@ -85,18 +85,25 @@ 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, int] = field(default_factory=dict)` — RID → - line where `MOVED` was set. -- Record it wherever `{VarState.MOVED}` is set (`MoveInto` and the consume-like - transitions): `st.moved_at[st.rid_of(ins.src)] = ins.line`. +- 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. When a RID is moved on both paths with **different** - lines, do not fabricate a precise line — keep one and mark the label as - approximate (see §5). Do **not** add an invariant `assert` like the `loans` - one: multiple move paths are legitimate here. -- On the OWN005 emit: - `evidence=(Evidence(line=st.moved_at.get(rid), label="moved here", role="step"),)` - when present. +- 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. > OWN001 (leak, acquire site) is a **stretch**, not part of the mandatory > minimum: it needs a symmetric `acquired_at` map built the same way as @@ -111,10 +118,10 @@ 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; at a -control-flow merge (state union) the move site may be one of several paths, so -such evidence is marked one-of-N, not exact. «Do not depict precision that isn't -there» (ADR §3.2). +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 From 92a48e2c6957850cbd097bb41f481d7544690c12 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 22:28:04 +0000 Subject: [PATCH 6/6] feat(analysis): acquire-site evidence for OWN001 leaks Symmetric counterpart to moved_at: a per-RID acquired_at (line, exact) map recorded when a resource is minted (Acquire, AcquireBuffer, MoveInto destination), threaded through State.copy() and the shared _join_sites merge helper (renamed from _join_moved_at, now used for both provenance maps). leak_check attaches an 'acquired here' step so an OWN001 leak -- reported at the function exit / a return -- points at the actionable open site instead of the dead end at function end. A leaked owned parameter is minted with no in-body site and carries no step (honest). An acquire site is effectively always exact: a RID is minted at a single acquire, so unlike a move it cannot disagree across paths. Extends tests/test_evidence_coverage.py (leak acquire step, leaked-param empty, move-destination leak) and switches the empty-evidence invariant anchor to OWN003. README + task spec updated. No semantic change: evidence only annotates existing findings. Gate green: run_tests, ruff, mypy ownlang; no new type: ignore. --- README.md | 19 ++++++----- docs/tasks/evidence-coverage.md | 23 +++++++++---- ownlang/analysis.py | 60 ++++++++++++++++++++++++++------- tests/test_evidence_coverage.py | 46 ++++++++++++++++++++++--- 4 files changed, 116 insertions(+), 32 deletions(-) diff --git a/README.md b/README.md index c6113eac..903b7bd1 100644 --- a/README.md +++ b/README.md @@ -627,14 +627,17 @@ Unsafe contracts (`UNS0xx`) are not yet implemented: `native` lowers into 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) 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. Evidence coverage is also partial by -design: most findings still carry no slice yet (they render exactly as before), -and only the three producers above are wired so far. +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 index 93bda1bb..80dc224d 100644 --- a/docs/tasks/evidence-coverage.md +++ b/docs/tasks/evidence-coverage.md @@ -54,10 +54,11 @@ def err(self, code: str, msg: str, line: int, `analysis.py`. The evidence branch must not do work before the `self.silent` early-return. -## 3. The three target diagnostics +## 3. The target diagnostics Class coverage required by acceptance: two from escape/lifetime, one from -use-after-move. +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)* @@ -105,9 +106,17 @@ state): `evidence=(Evidence(line=line, label=label, role="moved"),)` when a site is present. -> OWN001 (leak, acquire site) is a **stretch**, not part of the mandatory -> minimum: it needs a symmetric `acquired_at` map built the same way as -> `moved_at`. Do it only if in scope. +### 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 @@ -128,7 +137,7 @@ depict precision that isn't there» (ADR §3.2). 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; run `analyze`; assert each +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 @@ -148,7 +157,7 @@ folded into `tests/run_tests.py` (like `test_gallery` / `test_corpus`): | ADR criterion | How it is met | | --- | --- | -| ≥3 flow diagnostics with non-empty evidence | OWN015, OWN016, OWN005 | +| ≥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 | diff --git a/ownlang/analysis.py b/ownlang/analysis.py index 53b71c00..7ae63d68 100644 --- a/ownlang/analysis.py +++ b/ownlang/analysis.py @@ -107,6 +107,13 @@ class State: # 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( @@ -114,6 +121,7 @@ def copy(self) -> State: 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: @@ -158,15 +166,16 @@ def _join_handle_rid(a: dict[int, int], b: dict[int, int]) -> dict[int, int]: return out -def _join_moved_at( +def _join_sites( a: dict[int, tuple[int, bool]], b: dict[int, tuple[int, bool]] ) -> dict[int, tuple[int, bool]]: - """Merge the RID->move-site maps of two merging paths. Unlike the loan/handle - joins this carries NO invariant: a resource legitimately 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* OWN005 evidence.""" + """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: @@ -194,7 +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_moved_at(a.moved_at, b.moved_at) + out.moved_at = _join_sites(a.moved_at, b.moved_at) + out.acquired_at = _join_sites(a.acquired_at, b.acquired_at) return out @@ -237,6 +247,21 @@ def _moved_evidence(self, st: State, rid: int) -> tuple[Evidence, ...]: 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 ----------------------------------------- def loans_on(self, st: State, owner: Symbol) -> tuple[int, bool]: @@ -395,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"): @@ -425,11 +451,17 @@ 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): @@ -445,7 +477,11 @@ def step(self, ins: Instr, st: State) -> None: 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} - st.var[st.mint(ins.dst)] = {VarState.OWNED} + 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): diff --git a/tests/test_evidence_coverage.py b/tests/test_evidence_coverage.py index 383b096f..e2ab5718 100644 --- a/tests/test_evidence_coverage.py +++ b/tests/test_evidence_coverage.py @@ -4,12 +4,13 @@ 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 first three producers wired -into `ownlang/analysis.py`, one per acceptance class: +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 @@ -124,6 +125,28 @@ def _pick(src: str, code: str) -> Diagnostic: ) +# 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 @@ -181,9 +204,22 @@ def expect(cond: bool, msg: str) -> None: f"OWN005 merge evidence should be marked inexact: " f"{[(e.line, e.label) for e in d.evidence]}") - # -- empty-evidence invariant: a leak (OWN001) carries no slice --------- - d = _pick("module M\nfn f(n: int){ let b = Buffer.scratch(n); }\n", "OWN001") - expect(d.evidence == (), "OWN001 leak must not carry evidence (unchanged)") + # -- 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")