Repository navigation
Conversation
From `-C opt-level=1`, GVN rewrites a deref temp `_t = deref_copy P` of a `&mut`-typed place into `_t = copy P`. `extract_elaborated_deref` only recognized `CopyForDeref`, so `_t` survived as an independent local and each such copy was analyzed as its own borrow of `P`. With two of them alive at once (`**w += 3` reads through one and writes through the other) the prophecies contradict, the body is vacuous, and callers verify any assertion, `assert!(false)` included. Treat a copy of a projected `&mut`-typed place as such a deref temp. Whole-local copies are left alone: rustc emits those for ordinary moves of a `&mut` local. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KKfGn15ekWG5r4cKqzoP9a
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: 7be8e8add8
ℹ️ 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 !place.projection.is_empty() && ty.ref_mutability() == Some(mir::Mutability::Mut) { | ||
| return Some((lhs_local, *place)); |
There was a problem hiding this comment.
Projected copies are not exclusive to GVN-generated deref temps: rustc also emits them for ordinary mutable bindings such as let mut r = &mut *w.a. If r is later reassigned from w.b, ReplacePlacesVisitor retains the permanent r -> w.a replacement, so the reassignment's destination is rewritten into w.a itself. For a borrowed aggregate this makes Thrust analyze the function as changing the caller's reference field even though the real program only reassigns a local, which can corrupt post-state constraints and accept an invalid assertion or reject a valid one. Check that lhs_local is marked as a DerefTemp rather than classifying every projected &mut copy.
Useful? React with 👍 / 👎.
Fixes the
&mutside of #244 (details in #244 (comment)). TheBoxside is handled separately by #245.From
-C opt-level=1upward, GVN rewrites a deref temp_t = deref_copy Pof a&mut-typed place into_t = copy P.extract_elaborated_derefonly recognizedCopyForDeref, so the temp survived as its own local. Each such copy was then analyzed as a separate borrow ofP. Infn bump(w: &mut &mut i64) { **w += 3; }there are two of them, one read and one written. Their prophecies contradict each other, so the body becomes vacuous and any caller verifies,assert!(false)included (alsoensures(false)onbump, and*self.r += 3on a struct holding a&mut).This PR treats a
copyof a projected place of&muttype as such a deref temp. Whole-local copies (_3 = copy _1) are left alone: rustc emits those for ordinary moves of a&mutlocal even at opt-level 0 (take_max), and matching them would breaktake_max.rs/return_mut.rs.Tests:
tests/ui/{pass,fail}/mut_ref_deref_optimized.rsat-C opt-level=1. Without the fix, thefailcase verifies as safe. The fullcargo testsuite passes locally (Z3 5.0.0 + the pinned PCSat), andcargo fmt --checkandcargo clippy -D warningsare clean.Generated by Claude Code