Panic: "deref unbound var" when reborrowing a `&mut` field out of an aggregate parameter

[coord-e]

Summary

Analyzing a function that takes an aggregate parameter (a tuple or struct) and reborrows a &mut-typed field out of it panics with deref unbound var in Env::locate_place (src/refine/env.rs:1024). The parameter local is never registered in the env's flow bindings, so resolving the field projection during reborrow elaboration fails.

Reproduction (minimal)

fn bump(_r: &mut i64) {}
fn f(w: (&mut i64,)) {
    bump(w.0); // reborrow of `w.0` (a `&mut` field of the aggregate param `w`)
}
fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' panicked at src/refine/env.rs:1024:55:
deref unbound var

f does not even need to be called, and bump's body can be empty — the panic happens while analyzing f. A named struct (struct Wrap { r: &mut i32 }) triggers the identical panic; a tuple is the smaller form.

Note that writing through the field instead of reborrowing it (*w.0 = 2;) does not panic — the bug is specific to the reborrow path.

Analysis

The optimized MIR of f is:

fn f(_1: (&mut i64,)) -> () {
    bb0: {
        _3 = deref_copy (_1.0: &mut i64);
        _2 = bump(copy _3) -> [return: bb1, unwind continue];
    }
    bb1: {
        return;
    }
}

ReborrowVisitor turns the copy of the &mut field into a reborrow of _1.0, calling Env::borrow_place(_1.0) → locate_place(_1.0). locate_place starts at _1 and calls flow_binding(_1), which is None — the aggregate parameter _1 has no flow binding — and the .expect("deref unbound var") fires.

4: thrust::refine::env::Env<T>::locate_place        (src/refine/env.rs:1024)
5: thrust::refine::env::Env<T>::borrow_place         (src/refine/env.rs:1042)
6: thrust::analyze::basic_block::Analyzer::borrow_place_  (src/analyze/basic_block.rs:990)
7: ReborrowVisitor::insert_reborrow                  (src/analyze/basic_block/visitor/reborrow.rs:28)
...

This appears to be about how aggregate-typed parameters are bound when entering a basic block — they don't get the Tuple flow binding that field projections in locate_place expect.

Relationship to #122

Found while fixing #122. #122's literal Wrap { r: &mut i32 } reproduction trips this panic before ever reaching the drop logic, because the directly-&mut-typed field becomes a reborrow rather than an owned move. This is a distinct, pre-existing issue: the drop double-resolution in #122 is exercised (and fixed in #124) with an owned aggregate field (e.g. ((&mut i32,),)), whereas this panic is about reborrowing a &mut field out of an aggregate parameter.

Environment

• thrust @ 1d85b18
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.13.4