P-016 A1: loop support in the core (worklist fixpoint over back-edges)#17
Merged
Conversation
…k-edges)
Replace the single topological pass (which excluded any block in a cycle) with a
forward worklist to a fixpoint, so the core analyses `while` loops instead of
rejecting them as OWN020. The per-symbol lattice {OWNED,MOVED,RELEASED,ESCAPED}
is finite and union-merged, the transfer is monotone, so it converges without
widening. On a loop-free CFG it reduces to one pass per block — behaviour is
identical to the old walk (and __main__ sorts diagnostics by (line, code), so
emission order is unchanged).
Key pieces:
- lexer/AST/parser: `while (cond) { body }` (cond opaque like `if`); `while`
graduates out of REJECTED_KEYWORDS (`for`/`loop`/async stay OWN020).
- cfg: `lower_while` emits a header block with a back-edge from the body exit.
- analysis: two-phase run — a SILENT fixpoint converges the in-states (a looped
block is transferred many times), then ONE emitting pass reports diagnostics on
the converged state (so no per-iteration duplicates). Borrows stay block-scoped,
so the loan-set-equal-at-merge invariant holds across back-edges too.
- codegen/report/lifetimes: handle/descend into `While` (keeps mypy --strict
exhaustive and avoids dropping moves/buffers/subscribes inside a loop body).
This catches cross-iteration faults a single pass cannot see: a resource released
in a loop is double-released on the next turn (OWN003) and used after release
(OWN009); one acquired each turn and not released leaks (OWN001). Balanced
acquire/release — and a borrow that opens and closes within the body — stay clean.
Pinned by tests/test_loops.py (exact code sets, incl. nested loops), gallery
10_leak_in_loop.own, and run_tests CASES. Spec/README/P-016 updated.
https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Repository UI Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
🚧 Files skipped from review as they are similar to previous changes (1)
📝 WalkthroughWalkthroughAdds end-to-end Changeswhile Loop End-to-End Support
Sequence Diagram(s)sequenceDiagram
rect rgba(100, 149, 237, 0.5)
Note over Source,CFGBuilder: Frontend
Source->>Lexer: "while" keyword
Lexer->>Parser: Tok.WHILE
Parser->>Parser: parse_while() — collect cond_text, parse body block
Parser->>AST: A.While(cond_text, body, line)
end
rect rgba(144, 238, 144, 0.5)
Note over CFGBuilder,Analyzer: Analysis pipeline
AST->>CFGBuilder: lower_while(A.While)
CFGBuilder->>CFGBuilder: emit while.header, while.body, while.after
CFGBuilder->>CFGBuilder: add back-edge body→header
CFGBuilder-->>Analyzer: cyclic CFG
Analyzer->>Analyzer: phase 1 — worklist fixpoint (silent), join() asserts loan-set equality at merges
Analyzer->>Analyzer: phase 2 — re-run transfers, emit OWN001/OWN003/OWN009 diagnostics
end
rect rgba(255, 182, 193, 0.5)
Note over Analyzer,Codegen: Code generation
Analyzer-->>Codegen: converged ownership states
Codegen->>Codegen: _stmt_inline emits C# while(...){...}
Codegen-->>Output: C# source with while loop
end
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://cdn.github.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
🧹 Nitpick comments (1)
examples/gallery/10_leak_in_loop.own (1)
1-12: 💤 Low valueMinor inconsistency between comment and code pattern.
The comment on line 2 describes the C# analog as
while (reader.Read())(which naturally terminates when the reader is exhausted), but the actual code useswhile (n)wherenis never modified. While both patterns correctly demonstrate the per-iteration leak (OWN001), the difference might confuse readers about why the loop conditions differ.📝 Suggested clarification
Consider either:
- Matching the code to the comment:
while (n > 0) { n = n - 1; ... }(though this adds noise), or- Clarifying the comment:
// Real C#:while (condition) { var conn = Open(...); Use(conn); }— the loop body leaks regardless of how the loop terminates.🤖 Prompt for 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. In `@examples/gallery/10_leak_in_loop.own` around lines 1 - 12, The comment on line 2 describes a C# pattern using `while (reader.Read())` which naturally terminates, but the actual code in the drain function uses `while (n)` where n is never modified, creating an infinite loop. To resolve this inconsistency, update the comment to clarify that the resource leak occurs regardless of the loop's termination condition. Change the comment to explain that both patterns (naturally-terminating loops and explicit condition checks) demonstrate the same OWN001 leak issue—the key point is that a resource is acquired on every iteration but never released. This makes it clear to readers that the specific loop condition type is not the focus; the leak mechanism is.
🤖 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.
Nitpick comments:
In `@examples/gallery/10_leak_in_loop.own`:
- Around line 1-12: The comment on line 2 describes a C# pattern using `while
(reader.Read())` which naturally terminates, but the actual code in the drain
function uses `while (n)` where n is never modified, creating an infinite loop.
To resolve this inconsistency, update the comment to clarify that the resource
leak occurs regardless of the loop's termination condition. Change the comment
to explain that both patterns (naturally-terminating loops and explicit
condition checks) demonstrate the same OWN001 leak issue—the key point is that a
resource is acquired on every iteration but never released. This makes it clear
to readers that the specific loop condition type is not the focus; the leak
mechanism is.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: ee1bbf15-117b-44c7-84bd-cc2b49aa7987
📒 Files selected for processing (15)
README.mddocs/proposals/P-016-deep-fact-extraction.mdexamples/gallery/10_leak_in_loop.ownownlang/analysis.pyownlang/ast_nodes.pyownlang/cfg.pyownlang/codegen.pyownlang/lexer.pyownlang/lifetimes.pyownlang/parser.pyownlang/report.pyspec/OwnCore.mdtests/run_tests.pytests/test_gallery.pytests/test_loops.py
…he loop condition) The C# analog cited `while (reader.Read())` (which terminates) while the .own code is `while (n)` with an opaque condition — address a review nitpick by noting the condition is opaque to the checker and the per-iteration leak holds regardless of what ends the loop. Comment-only; the OWN001 verdict is unchanged. https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P-016 A1 — loops in the core
Replaces the single topological pass (which excluded any block in a cycle) with a forward worklist to a fixpoint, so the core now analyses
whileloops instead of rejecting them asOWN020. Builds on #16 (GTM UnitOfWork pin + never/every-path wording split + Option B ownership-transfer sample), which already landed inmain.Why it converges
The per-symbol lattice
{OWNED, MOVED, RELEASED, ESCAPED}is finite (height 4) and union-merged at joins; the transfer is monotone, so iterating until no out-state changes terminates — no widening needed. On a loop-free CFG it reduces to one pass per block, so loop-free behaviour is identical to the old topological walk (and__main__sorts diagnostics by(line, code), so emission order is unchanged).What changed
while (cond) { body }(condition opaque, likeif);whilegraduates out ofREJECTED_KEYWORDS—for/loop/ async stayOWN020.lower_whileemits a header block with a back-edge from the body exit (the CFG may now contain cycles).run— a silent fixpoint converges the in-states (a looped block is transferred many times), then one emitting pass reports diagnostics on the converged state, so there are no per-iteration duplicates. Borrows stay block-scoped (a loan opened in a loop body closes within the same iteration), so the "loans equal at every merge" invariant holds across back-edges too.While(keepsmypy --strictexhaustive and avoids dropping moves / buffers / subscribes inside a loop body).What it now catches
Cross-iteration faults a single pass cannot see:
Balanced acquire/release — and a borrow that opens and closes within the body — stay clean (no false positive).
Tests / docs
tests/test_loops.py(new): exact code-sets for clean / leak / cross-iteration / nested loops + regression guard thatfor/async still raiseOWN020.examples/gallery/10_leak_in_loop.own(new) wired intotest_gallery.tests/run_tests.pyCASES: clean / leak / cross-iteration double-release.spec/OwnCore.md,README.md,docs/proposals/P-016updated (A1 marked done).Full suite green locally (
analysis 125/125,loops 20/20,gallery 11/11,fuzz 3000 clean,spec 22/22,ownir 45/45) andruff check .clean.mypy --strictnot run locally (not installed) — verified by hand that bothassert_neversites stay exhaustive; CI confirms.Follow-ons (not in this PR)
The flow extractor still bails on loop bodies, so loopy C# methods are honestly skipped at the frontend — lowering
whileto back-edge flow facts is the natural Track-B next step now that the core handles loops.https://claude.ai/code/session_01Rg8kSk1YT14x7A1vo5zgED
Generated by Claude Code
Summary by CodeRabbit
Release Notes
New Features
whileloops are now supported end-to-end, including correct resource/ownership checking across loop iterations.Documentation
whilesemantics and the updated support/rejection matrix (withfor/loop/asyncstill rejected).Tests
whileregression suite and a new gallery example covering loop leak scenarios and expected error codes.