feat(d5): D5.1a — first-party interprocedural ownership transfer#112
Conversation
Wire the D5.0 solver into the OwnIR bridge so cross-callee ownership transfer is checked compositionally, resolving the give-up that left a forwarded param plain (P-005 D5.1, docs/notes/d5-ownership-transfer.md). ownir.py: - _build_skeletons(): derive a Method Ownership Summary skeleton per functions[] entry, mirroring _infer_param_effect's rel/passed/used priority (release -> dispose, forward -> forward edge, used -> borrow). Non-unique names are dropped (overload keys aren't distinguishable yet -> forward to such a name stays unknown -> silent). - to_module(): solve() once up front (degrades to no-MOS on any error, never crashes the bridge); thread the MOS into _lower_fn_params. - _infer_param_effect() gains forward_transfer: a forwarded param now resolves through the callee's summary (must -> consume, no -> borrow, may/unknown -> plain, precision-first). rel/used/explicit paths are unchanged, so no regression on the non-forward cases. The former 'ambiguous pass-through stays plain' test is replaced by D5.1 tests: a transitive (incl. two-hop) consuming forward now makes a later release/use OWN002, a borrow-only forward stays borrow (no over-consume FP on a later release), and a correctly forwarded handoff that used to read as a false OWN001 is now silent (a precision win). Full suite green (ownir 130/130, all 19 corpus cases unchanged). D5.1b (leaveOpen, a per-call-site contract) is the next, additive slice. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
|
Warning Review limit reached
More reviews will be available in 5 minutes and 11 seconds. Learn how PR review limits work. To continue reviewing without waiting, enable usage-based billing in the billing tab. ⌛ How to resolve this issue?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 credits. 🚦 How do rate 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 see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
📝 WalkthroughWalkthroughThe PR adds interprocedural ownership-transfer solving in OwnIR, threads solved transfers into forwarded-parameter effect inference, updates tests for one-hop and two-hop forwarding cases, and splits the D5.1 planning note into separate first-party wiring and ChangesForwarded ownership transfer
Estimated code review effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4✅ Passed checks (4 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Lint-only: wrap two long assertion messages (extract the got-list into a var) and use [*_FWD, ...] unpacking instead of _FWD + [...]. No behaviour change; ownir 130/130. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
![chatgpt-codex-connector[bot]](https://cdn.github.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: 932ce2be6d
ℹ️ 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".
| if not isinstance(p, dict): | ||
| continue | ||
| cname = str(p.get("name", "?")) | ||
| rel, passed, used = _param_signals(cname, body) |
There was a problem hiding this comment.
When a callee has an explicit contract but little or no body evidence, this summary builder ignores p.get("effect") and derives transfer only from rel/passed/used. For example, with forward(s) { sink(s); } and sink(x effect=consume) represented as a contract-only function, the direct call path still consumes via _lower_fn_params, but the new MOS resolves sink as no, so forward is inferred as borrow and callers get an OWN001 leak instead of a use-after-handoff/transfer. Since explicit effects are documented as overrides elsewhere in this file, the skeleton needs to seed transfer from them before falling back to body inference.
Useful? React with 👍 / 👎.
| paths = tuple(PathAction("forward", c, j) | ||
| for c, j in _forward_targets(cname, body)) |
There was a problem hiding this comment.
For a parameter forwarded only in one branch, or inside a loop that may execute zero times, _forward_targets records only the forwarding edge and no action for the path where no handoff occurs. The solver then sees every listed path as transferring and returns must, so maybeForward(s) is lowered as consume and callers that use/release s after the non-forward path get false OWN002/OWN001 results. The D5 lattice already has may for this case; the skeleton needs to represent the non-forward path or avoid inferring must from conditional/loop forwards.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://cdn.github.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 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 `@ownlang/ownir.py`:
- Around line 945-1002: The `ParamSkeleton.paths` construction in
`_build_skeletons()` is flattening control-flow into a single set of
`PathAction`s, which loses whether forwards are mutually exclusive or sequential
and can make `solve()` infer `MUST` instead of `MAY`. Update
`_build_skeletons()` so it preserves per-path structure from `_param_signals()`
and `_forward_targets()` when creating `MethodSkeleton`/`ParamSkeleton` data,
especially for `if` and `while` branches; if that distinction cannot be
represented safely, skip emitting MOS for those mixed-control-flow cases rather
than flattening them.
🪄 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: 089833e9-61b8-4c7c-a1e3-b49a3919c32d
📒 Files selected for processing (3)
docs/notes/d5-ownership-transfer.mdownlang/ownir.pytests/test_ownir.py
…(Codex + CodeRabbit) Two precision bugs in the D5.1 skeleton derivation, both flagged in review: - Explicit param effects were ignored: _build_skeletons derived transfer only from body signals, so a contract-only (no release in body) resolved as , and a forwarder became -> false OWN001 instead of the handoff. Explicit effects now seed the skeleton (consume->dispose, borrow->borrow, other->non-owning), matching the documented override semantics. - Conditional/looped forwards were flattened to : a param forwarded only inside an if/while recorded just the forward edge, so solve() returned must (not may), upgrading callers to consume and fabricating OWN002/OWN001. A forward is now resolved only when it is a single, unconditional, straight-line handoff; any conditional / looped / multi-target forward also emits a non-transfer path so the lattice yields may/no (caller stays plain) -- precision-first, never a false must. (_forward_targets gains a recurse flag to tell top-level from nested forwards.) Two regression tests added (explicit-effect seed resolves a forwarder; conditional forward stays silent for a caller that releases after). ownir 132/132, full suite green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Fmwk5ruExKy5fQ77CJ2NtF
2 participants
What
Wires the D5.0 summary solver into the OwnIR bridge so cross-callee
IDisposableownership transfer is checked compositionally — the first livefindings from P-005 D5. See
docs/notes/d5-ownership-transfer.md(slice D5.1a).The core already applies per-param
consume/borroweffects (lower_call); theonly gap was that
_infer_param_effectgave up when a param was forwarded toanother call (left it plain). That's exactly the give-up the interprocedural
solver resolves.
Mechanism (no core change, no extractor change for first-party)
_build_skeletons()derives a Method Ownership Summary skeleton perfunctions[]entry, mirroring the existing rel/passed/used priority (release →
dispose,forward → a
forwardedge, used →borrow).to_module()runssolve()once up front (degrades to no-MOS on any error —never crashes the bridge) and threads the result into
_lower_fn_params._infer_param_effect()gainsforward_transfer: a forwarded param now resolvesthrough the callee's summary —
must → consume,no → borrow,may/unknown→stay plain (precision-first). The rel/used/explicit-effect paths are untouched,
so no regression on the non-forward cases.
distinguishable yet — note's open question 2), so a forward to such a name stays
unknown→ silent.Live catches (proven by synthetic OwnIR tests)
forward(s){ sink(s); } sink(consume)makes
forward's own paramconsume; a caller that releases/usessafterforwarding is now OWN002 (incl. a two-hop chain
outer→mid→sink).read as a false OWN001 leak is now silent — the obligation provably moved.
borrow, so releasingafter it is clean (no false positive).
The former "ambiguous pass-through stays plain" test — whose own comment said
"transitive inference is the follow-up that resolves it" — is replaced by these
D5.1 tests. Full suite green: ownir 130/130, all 19 corpus cases unchanged,
D5.0 37/37.
Not in scope (next)
D5.1b —
leaveOpenTier-B: a per-call-site contract (the sameStreamReaderctor consumes or borrows by the
leaveOpenbool), so it needs a per-call effectchannel + the extractor reading the literal, plus a CI A/B sample on real extractor
output. Small and additive; it follows.
🤖 Generated with Claude Code
Generated by Claude Code
Summary by CodeRabbit