Repository navigation
Conversation
`bind_locals` assumes that a non-flow parameter local still holds the function's argument and equates the two at every block with its own precondition. A parameter that is moved out and then re-initialized stays non-flow, because `reassign_local_mutabilities` marks a local mutable only when it is assigned while initialized, yet it holds a different value from then on. The equation then contradicts the incoming state at the next join point, so the function's postcondition becomes vacuous and callers verify panicking programs as safe. Skip the equation when the parameter local is the destination of any assignment in the body. Fixes #334 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LhtkSy2XUScvjq9LXzmTQS
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![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: af427bdb11
ℹ️ 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".
Skipping the entry-argument equation whenever the body assigns the parameter anywhere also dropped it at blocks that no assignment can reach, such as a loop header before the parameter is moved out and re-initialized, so a loop invariant relating the parameter to its argument could no longer be established. Compute, once per body, which parameters may have been assigned on entry to each block by forward reachability from their assignment sites, and skip the equation only there. This also avoids rescanning the whole body for every parameter of every block. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LhtkSy2XUScvjq9LXzmTQS
There was a problem hiding this comment.
🟢 Approval recommended
The dataflow guard addresses the unsound assumption while paired tests cover both the regression and invariant preservation.
0 open findings
What changed in this PR
Fixes unsound parameter-to-argument equality assumptions after parameter reassignment.
Changes:
- Tracks parameter assignments per basic-block entry.
- Suppresses invalid argument equality assumptions after reassignment.
- Adds regression coverage for joins and loop invariants.
| File | Description |
|---|---|
src/analyze/basic_block.rs |
Adds assignment tracking and guards equality assumptions. |
src/analyze/local_def.rs |
Supplies assignment state to block analysis. |
tests/ui/pass/fn_param_reinit_after_move.rs |
Verifies correct reinitialization result. |
tests/ui/fail/fn_param_reinit_after_move.rs |
Rejects the previously vacuous assertion. |
tests/ui/pass/fn_param_reinit_after_loop.rs |
Preserves valid loop-invariant reasoning. |
tests/ui/fail/fn_param_reinit_after_loop.rs |
Rejects an invalid postcondition after a loop. |
🧠 Review effort: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b896c632b2
ℹ️ 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".
| location: mir::Location, | ||
| ) { | ||
| let is_param = (1..=self.arg_count).contains(&local.index()); | ||
| if is_param && ctxt.is_place_assignment() { |
There was a problem hiding this comment.
When a parameter is assigned through a projection, such as let t = s.field; s.field = replacement;, MIR's visitor changes the base local's context to MutatingUse::Projection, for which is_place_assignment() returns false. If the non-Copy field was moved out first, the parameter can remain classified as non-flow, so this assignment is absent from assigned_params; at a later join block bind_locals therefore reinstates the false entry-argument equality, makes the path inconsistent, and can verify a caller containing a failing assertion. Record the base local from projected assignment destinations as well as direct-local assignments.
Useful? React with 👍 / 👎.
Fixes #334.
bind_localsassumes that a non-flow parameter local still holds the function's argument, and addsentry == currentat every block that has its own precondition. A parameter that is moved out and then re-initialized (let t = s; s = S { .. };) stays non-flow, becausereassign_local_mutabilitiesmarks a local mutable only when it is assigned while initialized. From then on it holds a different value. At the next join point the equation contradicts the incoming state, so the function's postcondition becomes vacuous. Callers then verify panicking programs, evenassert!(false), as safe.This change skips the equation when the parameter local is the destination of any assignment in the body. It uses
PlaceContext::is_place_assignment(), asdrop_point::def_localdoes. A parameter that is never assigned always holds its argument, so the invariant-header case the workaround exists for keeps working.Tests
tests/ui/{pass,fail}/fn_param_reinit_after_move.rs. Before this change thefailprogram was reported assafe.cargo test: all 396 UI tests pass, including theloop_invariant_*ones and the PCSat-backed ones.cargo fmt --checkandcargo clippy -D warningsare clean.🤖 Generated with Claude Code
https://claude.ai/code/session_01LhtkSy2XUScvjq9LXzmTQS
Generated by Claude Code