Unsound: at `-C opt-level >= 1` GVN rewrites the `Box` deref temp from `deref_copy` to `copy`, so `unelaborate_derefs` misses it and every write through a nested `Box` lands on a copy — panicking programs verify as `safe`

[coord-e]

Summary

unelaborate_derefs/extract_elaborated_deref (src/analyze/local_def.rs) recognizes an elaborated Box deref chain in two steps: a deref temp _t = deref_copy P (Rvalue::CopyForDeref), followed by the ElaborateBoxDerefs shape _p = (_t.0.0 as *const T) Transmute. Both temps are NOP'd and replaced by P, so *_p is analyzed as a deref of the original place.

rustc's GVN pass rewrites _t = deref_copy P into _t = copy P — a plain Rvalue::Use(Operand::Copy). GVN runs from mir_opt_level >= 2, i.e. from -C opt-level=1 upward. extract_elaborated_deref only matches Rvalue::CopyForDeref, so _t is no longer replaced. The Transmute pattern that follows still matches, but its rest_place is now the surviving temp _t instead of P.

Thrust models Box<T> by value (PointerType::own), so _t = copy P binds _t to an independent copy of the box's contents. The mutable borrow and the write therefore land on that copy, while P keeps its pre-write value. Every later read of P sees the stale value.

Both failure directions follow, and both are silent:

• a program whose assertion is false at run time verifies as safe — unsound;
• a program whose assertion is true is rejected with Unsat — over-rejection.

Thrust's verdict therefore depends on the optimization level, and in the direction that matters: the same source is correctly rejected in a debug build and verifies as safe in a release build.

A single Box local (let mut x = Box::new(1i64); *x += 1;) is unaffected: there is no preceding deref temp, so the Transmute pattern matches on the box local itself. The bug needs the box to sit behind one more projection or deref — which is every way a Box actually appears in a program: a struct field, a tuple element, an enum payload, a Vec element, another Box, or a &mut Box<T> parameter.

Minimal reproducer

No annotations needed — a Box in a tuple:

fn main() {
    let mut t = (Box::new(1_i64), 0_i64);
    *t.0 += 1;
    assert!(*t.0 == 1);   // false: *t.0 is 2
}

$ cargo run -- -Adead_code -C debug-assertions=false min.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

$ cargo run -- -Adead_code -C debug-assertions=false -C opt-level=2 min.rs && echo safe
safe

The program panics when run:

$ rustc -O -o min min.rs && ./min
thread 'main' panicked at min.rs:4:5:
assertion failed: *t.0 == 1

The same holds for a struct field:

struct S { b: Box<i64> }

fn main() {
    let mut s = S { b: Box::new(1_i64) };
    *s.b += 1;
    assert!(*s.b == 1);   // false: *s.b is 2 — `safe` at -C opt-level >= 1
}

and for a nested Box — which is tests/ui/pass/box_nested.rs with the assertion negated:

fn main() {
    let mut x = Box::new(Box::new(1_i64));
    **x += 1;
    assert!(**x == 1);    // false: **x is 2 — `safe` at -C opt-level >= 1
}

tests/ui/pass/box_nested.rs itself (the honest assert!(**x == 2)) is the over-rejection side: it is safe at the default optimization level and Unsat from -C opt-level=1 upward.

Behavior matrix (all with -Adead_code -C debug-assertions=false)

program	0 (default)	1	2	3	s	z
tuple, assert!(*t.0 == 1) — false	Unsat ✔	safe ❌	safe ❌	safe ❌	safe ❌	safe ❌
tuple, assert!(*t.0 == 2) — true	safe ✔	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌
struct field, assert!(*s.b == 1) — false	Unsat ✔	safe ❌	safe ❌	safe ❌	safe ❌	safe ❌
struct field, assert!(*s.b == 2) — true	safe ✔	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌
nested box, assert!(**x == 1) — false	Unsat ✔	safe ❌	safe ❌	safe ❌	safe ❌	safe ❌
tests/ui/pass/box_nested.rs	safe ✔	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌	Unsat ❌
let mut x = Box::new(1i64); *x += 1; (single box)	safe ✔	safe ✔	safe ✔	safe ✔	safe ✔	safe ✔

Every other shape that puts a Box behind one more projection reproduces the unsoundness at -C opt-level=1 too — an enum payload (enum E { A(Box<i64>) }, mutated through match &mut e), a Vec<Box<i64>> element, a Box field mutated through a &mut self method, a &mut Box<i64> parameter, and a write performed by a callee (fn incr(x: &mut i64) applied to &mut **x). Some of these additionally hit an unrelated Option::unwrap() panic in src/refine/env.rs:399 at -C opt-level=2/3 (const-propagated aggregate constants), which only masks the wrong answer at those two levels; at 1, s and z they all report safe.

Root cause

ElaborateBoxDerefs lowers *boxed into a Unique/NonNull/Transmute chain, and Derefer hoists the base of that chain into a deref temp. For *t.0 the runtime MIR at -C opt-level=0 is:

_6 = deref_copy (_1.0: std::boxed::Box<i64>);                     // Rvalue::CopyForDeref
_8 = copy ((_6.0: Unique<i64>).0: NonNull<i64>) as *const i64 (Transmute);
_3 = &mut (*_8);
(*_3) = Add(copy (*_3), const 1_i64);

unelaborate_derefs NOPs the first statement and replaces _6 with (_1.0); the second then matches the Box pattern with rest_place = (_1.0) and is NOP'd too, replacing _8 with (_1.0). The write is analyzed as a mutable borrow of (_1.0) — correct.

GVN rewrites exactly those two statements (3-2-013.GVN diff for the struct-field variant):

-        _6 = deref_copy (_1.0: std::boxed::Box<i64>);
+        _6 = copy (_1.0: std::boxed::Box<i64>);
         _8 = copy ((_6.0: Unique<i64>).0: NonNull<i64>) as *const i64 (Transmute);
         (*_8) = Add(copy (*_8), const 1_i64);
         StorageLive(_3);
         StorageLive(_4);
-        _7 = deref_copy (_1.0: std::boxed::Box<i64>);
+        _7 = copy (_1.0: std::boxed::Box<i64>);
         _9 = copy ((_7.0: Unique<i64>).0: NonNull<i64>) as *const i64 (Transmute);
         _4 = copy (*_9);

extract_elaborated_deref returns None for _6 = copy (_1.0):

if let mir::Rvalue::CopyForDeref(place) = &rvalue {
    return Some((lhs_local, *place));
}

so _6 survives as an ordinary local, and the Transmute statement is unelaborated against rest_place = _6. The analyzed write becomes a borrow of *_6, where _6 was bound by analyze_assignment to a fresh copy of (_1.0)'s value — Box<i64> is Own(Int) in rty, so copying it copies the pointee rather than aliasing it. (_1.0) is never borrowed, so its value is never replaced by a prophecy, and the read-back through _7 (another independent copy) returns the original value.

CHC evidence

For the tuple reproducer, THRUST_OUTPUT_DIR at -C opt-level=1 gives (c1, the assertion-holds clause; v10 is t):

(= v10 (tuple<Int-Int> v11 0))         ; t = (v11, 0)  with v11 = 1
(= v4 (tuple_proj<Int-Int>.0 v10)) (= v5 v4) (= v14 v5)   ; copy #2 of the box  -> read back
(= v6 (tuple_proj<Int-Int>.0 v10)) (= v7 v6) (= v15 v7)   ; copy #3 of the box  -> written
(= (mut<Int> v18 v17) (mut<Int> v15 v16))                 ; &mut of copy #3
(= (mut_final<Int> (mut<Int> v18 v17)) (+ v9 1))          ; the write: v17 = 2
(= v1 v14) (= v12 v1) (= v12 1)                           ; the assert reads copy #2

v10 is never rebuilt from a prophecy, so v12 = v14 = tuple_proj.0(v10) = v11 = 1. The panic clause c2 carries (not (= v12 1)) in its body with head false, so it is discharged vacuously and the system is sat — reported as safe.

The same clause at -C opt-level=0 shows the correct threading: the borrow is taken on the tuple's own field and the tuple is rebuilt around the prophecy,

(= v1 (tuple<Int-Int> v11 v10))                           ; t rebuilt with the prophecy v11
(= (mut<Int> v13 v12) (mut<Int> v9 v11))                  ; current = v9, final = v11
(= (mut_final<Int> (mut<Int> v13 v12)) (+ v6 1))          ; v11 = 2
(= v8 (tuple_proj<Int-Int>.0 v1)) (= v8 1)                ; v8 = v11 = 2, contradicts 1

so the false assertion is correctly rejected there.

Confirmed by experiment

Teaching extract_elaborated_deref the post-GVN shape — a copy of a Box-typed place, which in MIR is only ever the pointer copy of such a deref temp, since Box is not Copy:

         if let mir::Rvalue::CopyForDeref(place) = &rvalue {
             return Some((lhs_local, *place));
         }
+
+        if let mir::Rvalue::Use(mir::Operand::Copy(place)) = &rvalue {
+            if place.ty(&self.body.local_decls, self.tcx).ty.is_box() {
+                return Some((lhs_local, *place));
+            }
+        }

makes every reproducer above behave identically at -C opt-level=0..3, s and z: the false assertions are rejected at every level, the true ones (including tests/ui/pass/box_nested.rs) verify at every level, and the whole tests/ui/pass suite still passes at the default optimization level. This is offered as evidence for the diagnosis, not as a proposed patch — matching the rewritten shape in extract_elaborated_deref may not be the right place, and the guard wants more thought than "the place is a box".

Notes

• Not vacuity on the accepting side: the accepted programs are genuinely mis-verified, not proved from an inconsistent environment. The negated tuple reproducer (assert!(*t.0 == 2), which is what actually holds) is rejected at the same optimization levels, so exactly one of the two contradictory assertions is accepted at each level — the environment says *t.0 == 1 after the write.
• Distinct from Incompleteness: v.len() on a &mut [T] leaves an unresolved reborrow that havocs the referent, so every safe &mut slice program that guards an index with len() is rejected at any -C opt-level >= 1 #240, the other optimization-level-dependent bug: there the trigger is PtrMetadata on a &mut [T] and the mechanism is a ReborrowVisitor-created reborrow whose prophecy is never resolved, which havocs the referent and only ever over-rejects. Here no reborrow is discarded and nothing is havoc'd — a Box deref temp is left un-unelaborated, the write is redirected to a copy, and the result is a wrong safe. The reproducers here contain no slices and no len().
• Distinct from Incompleteness: a &mut stored in a Box has its prophecy resolved only at the Box's drop, so reading the referent before the box is dropped wrongly rejects safe programs #175 (a &mut stored in a Box has its prophecy resolved only at the box's drop): the &mut here is a short-lived borrow of the box's pointee, and the value that goes missing is the box's own contents.
• Distinct from Incompleteness: Box<T> (Own) is related invariantly in subtyping, wrongly rejecting valid refinement weakening through a box #157 (Own related invariantly in subtyping) and Refinements on Box (own-pointer) pointee in return position are not enforced — unsound #97 (Box pointee refinements in return position); no subtyping or annotation is involved — the reproducers carry no annotations at all.
• Numerical-range / overflow concerns are not involved.
• tests/ui/pass/box_nested.rs already fails at -C opt-level >= 1 on main, so the bug is reachable from the existing suite; CI never sees it because the suite runs at the default optimization level, even though tests/ui/pass/list_sum_const.rs shows -C opt-level=3 is a supported configuration.
• A sweep of tests/ui/pass at -C opt-level=1 turns up one further regression, ghost_field.rs, which is not this bug: there GVN const-folds the ZST __ghost_marker result into const Ghost::<..>(PhantomData), so the ghost assignment loses its link to the marker call. It survives the experimental patch above and wants its own issue.

Environment

• branch main @ cd6b330
• solver: Z3 5.0.0 (HORN / Spacer)