execution surfaces ADR + evidence coverage for OWN015/OWN016/OWN005#164
Conversation
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.
|
Warning Review limit reached
Next review available in: 37 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (4)
📝 WalkthroughWalkthroughThis PR threads structured ChangesEvidence Coverage Implementation
Estimated code review effort: 3 (Moderate) | ~25 minutes Sequence Diagram(s)sequenceDiagram
participant Analyzer
participant State
participant Diagnostic
participant Test as test_evidence_coverage
Analyzer->>State: record moved_at(rid, line, exact) on MoveInto
Analyzer->>State: join moved_at across CFG paths (_join_moved_at)
Analyzer->>Analyzer: _moved_evidence() builds evidence tuple
Analyzer->>Diagnostic: err(code, evidence=...)
Diagnostic-->>Analyzer: render() appends note: lines
Test->>Analyzer: analyze fixture source
Test->>Diagnostic: inspect .evidence and render() output
Possibly related PRs
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…es ADR) 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.
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.
PhysShell
changed the title
|
@coderabbitai review Requesting a review of the evidence-coverage change (commit
Generated by Claude Code |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "== Git / PR context =="
git rev-parse --short HEAD
git log --oneline --decorate -n 5
echo
echo "== Changed files in commit 915b35f =="
git show --stat --name-only --format=fuller 915b35f
echo
echo "== Diff for ownlang/analysis.py in 915b35f =="
git diff 915b35f^ 915b35f -- ownlang/analysis.py
echo
echo "== Find evidence-related files =="
fd -i 'analysis.py|diagnostic|evidence|sarif|render|test_evidence_coverage.py|run_tests.py|README|adr|evidence-coverage' .
echo
echo "== AST outline for ownlang/analysis.py =="
ast-grep outline ownlang/analysis.py --view expanded || true
echo
echo "== Relevant snippets from ownlang/analysis.py (first 260 lines) =="
sed -n '1,260p' ownlang/analysis.py
echo
echo "== Relevant snippets from ownlang/analysis.py (261-620 lines) =="
sed -n '261,620p' ownlang/analysis.py
echo
echo "== Relevant snippets from tests/test_evidence_coverage.py =="
sed -n '1,260p' tests/test_evidence_coverage.py
echo
echo "== Search for OWN015/OWN016/OWN005 and evidence APIs =="
rg -n -C3 'OWN015|OWN016|OWN005|Evidence|evidence|codeFlow|note:' ownlang tests README.md docs
echo
echo "== If present, diagnostics/evidence implementation =="
for f in $(fd -i 'diagnostic*.py|*evidence*.py|sarif*.py|render*.py' ownlang tests docs .); do
echo
echo "---- FILE: $f ----"
sed -n '1,260p' "$f"
doneLength of output: 158054 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "== ownlang/analysis.py: _apply_effect tail =="
sed -n '616,690p' ownlang/analysis.py
echo
echo "== ownlang/diagnostics.py =="
sed -n '190,320p' ownlang/diagnostics.py
echo
echo "== Focused diff around tests/run_tests.py =="
git diff 915b35f^ 915b35f -- tests/run_tests.pyLength of output: 10206
What I checked:
Looks good to me. Approving. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 915b35faf6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| 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) |
There was a problem hiding this comment.
When a value is moved a second time, _consume_like first reports the line's OWN005 using the original move site, but this assignment then overwrites moved_at for the RID. A later use or return of that same handle will render moved here at the failed second move rather than at the move that actually made the resource unavailable, so fixing the annotated line can leave the real use-after-move unexplained. Keep the first recorded move site, or only replace it when the move is valid.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Good catch — fixed in 1155ac4. moved_at is now written only on a real ownership transfer (source still OWNED before the move), so a failed second move no longer overwrites the first move site. A later use/return-after-move is explained by the move that actually consumed the resource. Added a double-move regression to tests/test_evidence_coverage.py (a use after move a; move a; reports its evidence at the first move line, not the failed second one).
Generated by Claude Code
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.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/tasks/evidence-coverage.md`:
- Around line 88-99: The `moved_at` sketch is missing the exactness flag needed
to distinguish an exact move line from a merged representative. Update the
`State.moved_at` shape and every reference to it in `State.copy()`, `join()`,
`MoveInto`/consume-like transitions, and the OWN005 evidence emission in
`ownlang/analysis.py` so the stored value carries exactness and the example uses
that flag instead of assuming `dict[int, int]`. Keep the join behavior for
multiple move paths, but mark merged entries as approximate rather than
inventing a precise line.
In `@README.md`:
- Around line 628-636: Update the merge-point wording in README so it states
that exact move-site evidence is preserved when all incoming paths agree on the
same line, and only conflicting branches should be described as “moved here (on
one of several paths)”. Adjust the explanatory text around the control-flow
merge behavior to reflect the union logic in ownlang/analysis.py without
implying that every merge loses precision.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: 2993bd2c-2c04-4664-8f4e-4aa51207493f
📒 Files selected for processing (6)
AGENTS.execution-surfaces.mdREADME.mddocs/tasks/evidence-coverage.mdownlang/analysis.pytests/run_tests.pytests/test_evidence_coverage.py
… 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.
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.
|
@coderabbitai review New commit
Generated by Claude Code |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "== Log =="
git log --oneline --decorate -n 8
echo
echo "== Diff for ownlang/analysis.py in 92a48e2 =="
git diff 92a48e2^ 92a48e2 -- ownlang/analysis.py
echo
echo "== Diff for other files in 92a48e2 =="
git show --stat --name-only 92a48e2
echo
echo "== Full diff 92a48e2 =="
git diff 92a48e2^ 92a48e2Length of output: 23474 🏁 Script executed: #!/bin/bash
set -euo pipefail
sed -n '380,430p' ownlang/analysis.py
echo "---"
sed -n '1,40p' ownlang/diagnostics.py | rg -n 'class Evidence' -A 10
echo "--- err() signature ---"
rg -n 'def err' ownlang/analysis.py -A 15
echo "--- mint() ---"
rg -n 'def mint' ownlang/analysis.py -A 10
echo "--- _sym_by_id ---"
rg -n '_sym_by_id' ownlang/analysis.py -A 10Length of output: 2863 🏁 Script executed: #!/bin/bash
set -euo pipefail
grep -n "class Evidence" -A 10 ownlang/diagnostics.py
echo "--- err ---"
grep -n "def err" ownlang/analysis.py -A 15
echo "--- mint ---"
grep -n "def mint" ownlang/analysis.py -A 12
echo "--- _sym_by_id full ---"
grep -n "_sym_by_id" ownlang/analysis.py -A 15Length of output: 5945 🏁 Script executed: #!/bin/bash
set -euo pipefail
grep -n "move-destination\|dst_rid\|MoveInto" tests/test_evidence_coverage.py -A 5 -B 5
echo "---full test diff context---"
sed -n '1,260p' tests/test_evidence_coverage.pyLength of output: 509 🏁 Script executed: #!/bin/bash
sed -n '1,260p' tests/test_evidence_coverage.pyLength of output: 9974 🏁 Script executed: #!/bin/bash
grep -n "leak_check" ownlang/analysis.py -B3 -A3Length of output: 1120
What I checked:
Nice symmetric extension of the pattern from the previous commit. Approving. [approve] |
2 participants
Что и зачем
Заносит ADR по «execution surfaces» (итог аудита идеи Forth-like stack VM: reject VM, adopt typed primitive registry + расширение
diagnostics.Evidence) и реализует его первую ступень: подключает простаивавшую evidence-машинерию к flow-анализу. Три диагностики теперь несут структурированную reachability-цепочку (рендерится какnote:-строки / SARIF codeFlows):return→ шаги allocated (место аллокации буфера) + escapes by return;Stateтеперь хранит per-RID место move(line, exact); на control-flow merge move по разным строкам на разных путях честно помечается «one of several paths», а не именует строку одного пути.Семантику проверок не меняли: evidence лишь аннотирует существующие findings, не несёт lattice-состояния и не влияет на вердикт. Плюс ADR и исполнимое ТЗ (
docs/tasks/evidence-coverage.md).Тип изменения
Как проверено
python tests/run_tests.py— зелёный (добавленtests/test_evidence_coverage.py: slice + human-render golden + merge-point honesty + empty-evidence invariant, свёрнут в аггрегатор)ruff check .иmypy— чисто, без новых# type: ignoreСвязанные issue
Нет связанного issue.
Чеклист
tests/test_evidence_coverage.pyfeat:,docs:)🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Documentation
Tests