[coord-e]

Fixes #346.

Cause

MaybeLiveLocals treats a write such as s.f = v (a projection with no Deref) as neither a use nor a definition of s. When s is never read afterwards, it is already dead, and already dropped, by the time the write runs:

• If the write is in a later block, s is not a block parameter there. analyze_assignment then hits assert!(lhs.projection.is_empty()).
• If the write is in the same block, s is not dropped again after it. A &mut stored this way (s.0 = &mut b) is never resolved, so b is havoc'd and a correct program gets Unsat.

Fix

local_def::Analyzer::remove_dead_partial_writes runs before mutabilities and drop points are computed. It turns into Nop every assignment whose place has a projection, does not go through a Deref, and whose local is not live after the statement. Such a write cannot be observed. Once it is gone, its operands die where they are defined and get dropped there, so the stored reborrow is resolved. Removing one write can make another write dead, so the pass repeats until it finds none.

Tests

tests/ui/{pass,fail}/dead_field_write.rs retarget a &mut field of a tuple inside a branch after the tuple's last read. Before this change, both files panic with lhs.projection.is_empty(). After it, the pass file verifies, and the fail file, which breaks the assertion on the newly borrowed referent, is Unsat.

I also ran the reproductions from the issue by hand: the Stats dead store, if c { t.1 = 3; }, and the same-block s.0 = &mut b. All of them now verify, and the versions with a broken assertion are rejected.

cargo test passes (402 UI tests), along with cargo fmt --check and cargo clippy -- -D warnings.

---

Generated by Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-19T22:18:22.040335Z	dcf3e1c	PR opened

ℹ️ 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" or "@codex security review".

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]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: dcf3e1c859

ℹ️ 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".

[chatgpt-codex-connector]

Traverse statements in backward analysis order

For functions containing large basic blocks, this forward enumeration drives the ResultsCursor opposite MaybeLiveLocals' backward direction; the cursor only has linear performance when statements are visited in the analysis direction and can otherwise repeatedly replay the block (rustc documentation). That makes each scan quadratic, and the surrounding fixpoint loop can require one scan per link in a chain of partial writes, producing cubic behavior and potentially making verification of generated or otherwise large functions impractically slow. Iterate the statements in reverse while retaining their original indices, or use a results visitor.

Useful? React with 👍 / 👎.