Replacing a `Box`/`&mut`-typed struct or tuple field (`c.page = Box::new(..)`) is elaborated into a write *through* the old pointer, so the field's type in the env becomes its pointee and every later use of the struct aborts the analyzer

[coord-e]

Summary

ReborrowVisitor::visit_assign picks the elaboration for an assignment from the type of inner_place, but inner_place == place whenever the assigned place does not end in Deref. For a place that is itself of pointer type — a Box<T>- or &mut T-typed struct/tuple field — the Ref/Box arms then borrow the place's pointee instead of the place, and the assignment

c.page = Box::new(5);   // replace the box

is rewritten as if it were

*c.page = 5;            // write through the old box

The environment afterwards records c.page as int where its declared type is own int, and the next use of c — a deref, or relating c to Cache when it is passed anywhere — aborts the compiler.

This is not a missing feature: every ingredient is supported on its own, the _ => arm two lines below already handles this shape correctly (which is why a Vec-typed field works), and the same statement on a Box local verifies fine. The analyzer's own diagnostic says the MIR it built is ill-typed:

thread 'rustc' panicked at src/rty/subtyping.rs:147:14:
inconsistent types: got=int, expected=own int

Replacing an owned sub-object held in a struct field (self.buffer = Box::new(..), self.current = next, cursor.at = &mut other) is routine Rust, so today no struct that owns a Box field and ever reassigns it can be analyzed at all.

Minimal reproduction

repro.rs:

struct Cache { page: Box<i64> }
impl thrust_models::Model for Cache { type Ty = Self; }

fn main() {
    let mut c = Cache { page: Box::new(1) };
    c.page = Box::new(5);
    assert!(*c.page == 5);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' (10095) panicked at src/refine/env.rs:388:48:
called `Option::unwrap()` on a `None` value
stack backtrace:
   ...
   5: thrust::refine::env::PlaceType::deref
             at ./src/refine/env.rs:388:48
   6: thrust::refine::env::Env<T>::path_type
             at ./src/refine/env.rs:1097:55
   7: thrust::refine::env::Env<T>::place_type
             at ./src/refine/env.rs:1107:14

Expected: safe. Actual: the compiler aborts.

Ground truth

All four failing programs below are valid, safe Rust that real rustc compiles and runs to completion (exit=0, assertion holds); none of them can panic.

$ rustc -Adead_code --edition 2021 -o gt gt.rs && ./gt; echo "exit=$?"
exit=0

The same defect, three different aborts

The reassigned field is left with its pointee's type, so which unwrap/expect fires just depends on how the value is used next.

#	Program (the only difference is the marked line)	Result
f1	c.page = Box::new(5); then assert!(*c.page == 5)	Option::unwrap() on None at src/refine/env.rs:388 (PlaceType::deref)
f2	tuple field: let mut t = (Box::new(1i64), 0i64); t.0 = Box::new(5); then assert!(*t.0 == 5)	same abort at env.rs:388
f3	&mut-typed field: c.at = &mut y; then *c.at = 20	borrowing unbound var at src/refine/env.rs:1014 (Env::borrow_var)
f4	c.page = Box::new(5); then read(&c) for fn read(c: &Cache) -> i64 { *c.page }	inconsistent types: got=int, expected=own int at src/rty/subtyping.rs:147

f4 is the clearest statement of what went wrong: at the point where c is related to its declared type, field page carries int, not own int.

f2 / f3 / f4 sources

// f2
fn main() {
    let mut t = (Box::new(1i64), 0i64);
    t.0 = Box::new(5);
    assert!(*t.0 == 5);
}

// f3
struct Cursor<'a> { at: &'a mut i64 }
fn main() {
    let mut x = 1i64;
    let mut y = 2i64;
    let mut c = Cursor { at: &mut x };
    *c.at = 10;
    c.at = &mut y;
    *c.at = 20;
    assert!(y == 20);
}

// f4
struct Cache { page: Box<i64> }
impl thrust_models::Model for Cache { type Ty = Self; }
fn read(c: &Cache) -> i64 { *c.page }
fn main() {
    let mut c = Cache { page: Box::new(1) };
    c.page = Box::new(5);
    assert!(read(&c) == 5);
}

Controls — everything adjacent verifies

Program	Result	Why it is fine
let mut b = Box::new(1i64); b = Box::new(5); assert!(*b == 5);	safe	empty projection → caught by the is_mut_local branch at reborrow.rs:51
let c = Cache { page: Box::new(1) }; assert!(*c.page == 1);	safe	no reassignment
c = Cache { page: Box::new(5) }; (replace the whole struct)	safe	empty projection again
c.page = Vec::new(); c.n = 5; for Cache { page: Vec<i64>, n: i64 }	safe	a non-pointer field takes the correct _ => arm
*c.page = 5; (write through the box, don't replace it)	safe	place ends in Deref, so inner_place != place

So the trigger is exactly: an assignment whose destination place has a non-empty projection and whose own type is Box<T> or &mut T.

One case looks like an exception and is worth calling out, because it shows the corruption is real rather than an artifact of main: the same assignment inside fn set(c: &mut Cache) { c.page = Box::new(5); } lets main verify (assert!(*c.page == 5) is accepted and the flipped == 1 is correctly rejected). The callee never touches c.page again, so the corrupted binding is simply never observed, and the caller works from set's inferred spec. Adding a single read inside set — fn set(c: &mut Cache) { c.page = Box::new(5); assert!(*c.page == 5); } — aborts at env.rs:388 exactly like f1.

Root cause

src/analyze/basic_block/visitor/reborrow.rs:62-90:

let inner_place = if place.projection.last() == Some(&mir::PlaceElem::Deref) {
    // *m = *m + 1 => m1 = &mut m; *m1 = *m + 1
    let mut projection = place.projection.as_ref().to_vec();
    projection.pop();
    mir::Place { local: place.local, projection: self.tcx.mk_place_elems(&projection) }
} else {
    // s.0 = s.0 + 1 => m1 = &mut s.0; *m1 = *m1 + 1
    *place
};

let ty = inner_place.ty(&self.analyzer.local_decls, self.tcx).ty;
let (new_local, new_place) = match ty.kind() {
    mir_ty::TyKind::Ref(_, inner_ty, m) if m.is_mut() => {
        let new_local = self.insert_reborrow(*place, *inner_ty);   // borrows place's POINTEE
        (new_local, new_local.into())
    }
    mir_ty::TyKind::Adt(adt, args) if adt.is_box() => {
        let inner_ty = args.type_at(0);
        let new_local = self.insert_borrow(*place, inner_ty);      // borrows place's POINTEE
        (new_local, new_local.into())
    }
    _ => {
        let new_local = self.insert_borrow(*place, ty);            // borrows the place itself
        (new_local, self.tcx.mk_place_deref(new_local.into()))
    }
};

The two pointer arms are written for — and are only correct in — the Deref-stripped case. There inner_place is the pointer (m, type &mut T/Box<T>) and place is its pointee (*m, type T), so insert_{re,}borrow(*place, inner_ty) correctly borrows a T, and substituting new_place = new_local (a pointer of the same shape) for inner_place in the rvalue keeps (*m) reading as (*m1). That is the *m = *m + 1 => m1 = &mut m; *m1 = *m + 1 case the comment describes, and it works.

In the else branch inner_place == place, so ty is the type of the assigned place itself. When that place happens to be pointer-typed, the arms are selected on a completely different meaning of ty: they borrow place's pointee, bind new_local as &mut T::Pointee, and rewrite the statement to *new_local = <rvalue> — a write of a whole Box<i64>/&mut i64 value into an i64 slot. Env::borrow_var also swaps the field's flow binding to Box(prophecy)/Mut(prophecy, ..) over the pointee var, which is why the field's type in the environment degrades from own int to int and stays wrong for the rest of the block.

The correct treatment for a non-Deref place is precisely the _ => arm — borrow the place itself and write through the fresh borrow — which is what a Vec-typed field already gets. Guarding the two pointer arms on inner_place != *place (i.e. on a trailing Deref actually having been stripped) makes all four programs above take that arm.

Relationship to #176

Same file and function, different arm, and the fix for one does not obviously give the other:

• Panic: "borrowing unbound var" when writing through a reassigned &mut local #176 is the first branch, reborrow.rs:51 (place.projection.is_empty() && is_mut_local(..)), and is about reassigning a &mut local. Its own trigger table is explicit that the crash needs a reference-typed local.
• This issue needs a non-empty projection, never reassigns any local, and hits the arms at reborrow.rs:77/81 selected via inner_place's type at line 75.
• The clearest separation: a Box local reassignment verifies (control row 1 above — it goes through Panic: "borrowing unbound var" when writing through a reassigned &mut local #176's branch and is fine there), while a Box field reassignment aborts. Box-typed places are not mentioned in Panic: "borrowing unbound var" when writing through a reassigned &mut local #176 at all.

They plausibly share a theme ("reassigning an owning/reference-typed place does not re-establish its flow binding"), so a fix may well want to cover both, but they are distinct code paths with distinct triggers and distinct aborts.

Scope / when it bites

Any struct that owns a boxed sub-object and ever swaps it — self.buffer = Box::new(..), self.page = next_page, a cursor struct retargeted with cursor.at = &mut other — is unanalyzable, and the failure is a compiler abort rather than a diagnostic. It is independent of the enum-expansion depth limit and of recursive ADTs (Cache is a flat one-field struct), needs no annotations, and involves no numeric-range/overflow reasoning: every constant is 1, 2, 5, 10, 20. It reproduces with and without impl thrust_models::Model for Cache (without it the &mut-parameter variants first hit #266 instead), and at -C opt-level=0, so it is unrelated to #244/#248.

Environment

• thrust @ 5c74a7f
• rustc nightly-2025-09-08 (per rust-toolchain.toml), x86_64-unknown-linux-gnu
• Z3 5.0.0, default solver configuration
• Flags: -Adead_code -C debug-assertions=false