Do not reborrow the operand of PtrMetadata

[coord-e]

Closes #240.

<[T]>::len is lowered to PtrMetadata. From -C opt-level=1 upward rustc applies it directly to the &mut [T] local (_len = PtrMetadata(copy _v)) rather than through the shared reborrow it inserts at -C opt-level=0, so ReborrowVisitor::visit_operand rewrote the operand into a fresh &mut reborrow.

analyze_assignment then discarded that reborrow and took its own shared borrow of the referent, leaving the reborrow's prophecy unresolved: the synthetic local is absent from the MIR DropPoints was computed over, so nothing ever equated it to its current value. Since borrowing a place replaces its value with the prophecy, *v was havoc'd for the rest of the function and if i < v.len() no longer discharged the bound on the following v[i].

PtrMetadata only reads the length out of its operand, so this skips the reborrow and lets analyze_assignment borrow the referent itself — which it already does.

Testing

Verified against Z3 5.0.0 and the COAR image CI pins.

The behavior matrix in the issue is now green in every cell: -C opt-level=0,1,2,3,s,z × the &mut [i32] reader, the &[i32] reader, the &mut [i32] writer and double_all.

This is an over-rejection fix, not a vacuity one — the unsafe variants stay rejected, and a genuine write-then-read verifies:

program	opt=0	opt=2
if i < v.len() { let x = v[i]; assert!(x == 0); }	Unsat	Unsat
if i < v.len() { v[i] = 7; assert!(v[i] == 8); }	Unsat	Unsat
unguarded let x = v[i];	Unsat	Unsat
if i < v.len() { v[i] = 7; assert!(v[i] == 7); }	safe	safe

cargo test passes (328 UI tests, plus unit and doc tests); cargo fmt --check and cargo clippy --all-targets are clean.

Tests added

A pass/fail pair at -C opt-level=2, so the suite exercises the PtrMetadata(copy <&mut>) shape that CI never saw before:

• tests/ui/pass/slice_len_guard_mut.rs — if i < v.len() { v[i] = 7; assert!(v[i] == 7); }
• tests/ui/fail/slice_len_guard_mut.rs — the same with the asserted value broken to 8

---

Generated by Claude Code

[Copilot]

🟢 Approval recommended

The targeted fix is consistent with metadata handling and is covered by paired regression tests.

Pull request overview

Fixes optimization-dependent over-rejection when reading mutable slice metadata by preventing an unnecessary mutable reborrow.

Changes:

• Exempts PtrMetadata operands from reborrowing.
• Adds paired positive and negative regression tests at optimization level 2.

File summaries

File	Description
src/analyze/basic_block/visitor/reborrow.rs	Skips reborrowing for PtrMetadata.
tests/ui/pass/slice_len_guard_mut.rs	Verifies guarded mutable-slice indexing succeeds.
tests/ui/fail/slice_len_guard_mut.rs	Ensures an incorrect assertion remains rejected.

Review details

• Files reviewed: 3/3 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.