Capture partial reborrows of &mut aggregate fields in mut_locals

[coord-e]

Summary

Fixes#125.

Analyzing a function that takes an aggregate parameter (tuple/struct) and reborrows a &mut-typed field out of it panicked with deref unbound var in Env::locate_place:

fnbump(_r:&muti64){}fnf(w:(&muti64,)){bump(w.0);// reborrow of the `&mut` field `w.0`}

Root cause

The base local of the aggregate (_1) was never recognized as being (partially) mutably borrowed, so it was neither box-elaborated nor flow-decomposed, and resolving the _1.0 projection during reborrow elaboration failed.

reassign_local_mutabilities derives local mutability from mut_locals, whose operand rule only matched Operand::Move:

iflet mir::Operand::Move(place) = operand {if place.ty(..).ty.is_mutable_ptr(){self.locals.insert(place.local);}}

But a &mut field read out of an aggregate lowers to Operand::Copy, so _1 was never marked. This is despite ReborrowVisitor::visit_operand reborrowing any&mut-typed operand place (operand.place(), Copy or Move) — the two passes were inconsistent.

Why a &mut read is Operand::Copy

Operand::Copy vs Operand::Move is not about whether the type is Copy — it records whether the source place stays valid after the read. Per the rustc doc comment on Operand::Copy: "Before drop elaboration, the type of the place must be Copy. After drop elaboration there is no such requirement." The MIR thrust consumes (optimized_mir) is post-drop-elaboration, so a non-Copy&mut is legally read via copy. rustc emits copy whenever the source is dead/reborrowed, which is essentially every &mut read:

reborrow bump(w.0): _3 = copy (_1.0: &mut i64); _2 = bump(move _3)
move-out ret w.0: _0 = copy (_1.0: &mut i64); return

So Move-only matched a case that almost never occurs for &mut. (Top-level &mut locals still worked because bind_local has a separate rty.ty.is_mut() type-check; a tuple isn't is_mut(), so the aggregate field fell through both.)

Fix

Match Copy as well, and narrow the type test from is_mutable_ptr() to a &mutreference:

iflet mir::Operand::Move(place) | mir::Operand::Copy(place) = operand {ifmatches!(place.ty(..).ty.kind(),TyKind::Ref(_, _, m)if m.is_mut()){self.locals.insert(place.local);}}

The narrowing is required: is_mutable_ptr() also matches *mut T raw pointers, which genuinely areCopy and are read by copy constantly, but are never reborrowed. The old Move-only gate excluded them for free (a *mut is Copy, so it never appeared as Move); adding Copy without restricting to references would over-mark every raw-pointer copy. This now aligns exactly with what ReborrowVisitor reborrows.

This makes the type-based contains_mut workaround from earlier revisions unnecessary; it was reverted and removed.

Tests

Added pass/fail UI regression tests (reborrow_mut_field_of_aggregate_param). Full suite green (234 passed, 0 failed) with z3 4.13.0 and the COAR docker image, matching CI.

References

• rustc Operand doc comment (Copy/Move semantics): https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.Operand.html
• UCG#188 (operational semantics of Move): What about: use-after-move and (maybe) use-after-drop rust-lang/unsafe-code-guidelines#188

🤖 Generated with Claude Code

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, you can upgrade your account or add credits to your account and enable them for code reviews in your settings.

[Copilot]

Pull request overview

Fixes a panic in the MIR analysis pipeline when reborrowing a &mut-typed field out of an aggregate (tuple/struct) parameter by ensuring the base local is recognized as (partially) mutably borrowed in mut_locals.

Changes:

• Extend mut_locals operand handling to treat both Operand::Move and Operand::Copy of &mut references as indicating a mutable borrow.
• Narrow the mutability detection to &mut references (excluding *mut raw pointers) to avoid over-marking locals.
• Add UI pass/fail regression tests covering reborrowing a &mut field from an aggregate parameter.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
tests/ui/pass/reborrow_mut_field_of_aggregate_param.rs	Adds a passing regression case ensuring aggregate-field &mut reborrow no longer panics and behaves as expected.
tests/ui/fail/reborrow_mut_field_of_aggregate_param.rs	Adds a failing regression case ensuring the analysis reports Unsat (rather than panicking) for an inconsistent postcondition.
src/analyze/local_def.rs	Updates mut_locals to detect &mut reborrows through Operand::Copy as well as Operand::Move, aligned with ReborrowVisitor.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.