From 9d842ec494d81c357d3ba10306401cbe69952dfd Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 26 Aug 2026 12:01:22 +0000 Subject: [PATCH] Unelaborate the `Box` deref temps GVN rewrites into copies `ElaborateBoxDerefs` lowers `*boxed` into a `Unique`/`NonNull`/`Transmute` chain, and `Derefer` hoists the base of that chain into a deref temp. That temp is what `unelaborate_derefs` recognizes by its `CopyForDeref` rvalue, so that the deref below it is analyzed on the place the box lives in rather than on the temp. From `-C opt-level=1` upward, GVN rewrites `_t = deref_copy P` into `_t = copy P`. The temp then survived unelaboration and the chain was resolved against it instead of against `P`. A `Box` is modeled by value, so the temp took a copy of the box's contents: the write landed on the copy while `P` kept its pre-write value, and every later read of `P` saw the stale one. A `Box` behind one more projection -- a struct field, a tuple element, an enum payload, a nested `Box` -- was thus verified against the wrong value, silently in both directions: a program whose assertion is false at run time verified as `safe`, and one whose assertion holds was rejected with `Unsat`. Match the rewritten shape too, for the locals an `ElaborateBoxDerefs` chain dereferences as a whole. Those are exactly the deref temps: a chain reads its base through `Unique`/`NonNull` field projections, which no local other than a hoisted temp stands in for. Fixes #244 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YXdyimRB3Fpje8fbfmqhiB --- src/analyze/local_def.rs | 67 +++++++++++++++++++++++----- tests/ui/fail/box_field_optimized.rs | 12 +++++ tests/ui/pass/box_field_optimized.rs | 12 +++++ 3 files changed, 80 insertions(+), 11 deletions(-) create mode 100644 tests/ui/fail/box_field_optimized.rs create mode 100644 tests/ui/pass/box_field_optimized.rs diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index a98eb1ce..d0c18927 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -13,6 +13,21 @@ use crate::pretty::PrettyDisplayExt as _; use crate::refine::{self, BasicBlockType, TypeBuilder}; use crate::rty; +/// The local a statement assigns to, together with the assigned rvalue, if the statement is an +/// assignment to a whole local. +fn assignment_to_local<'a, 'tcx>( + stmt: &'a mir::Statement<'tcx>, +) -> Option<(Local, &'a mir::Rvalue<'tcx>)> { + let mir::StatementKind::Assign(assign) = &stmt.kind else { + return None; + }; + let (lhs, rvalue) = &**assign; + if !lhs.projection.is_empty() { + return None; + } + Some((lhs.local, rvalue)) +} + fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option { use rustc_ast::LitKind; use rustc_hir::{Expr, ExprKind, Stmt, StmtKind}; @@ -379,20 +394,31 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn extract_elaborated_deref( &self, stmt: &mir::Statement<'tcx>, + box_deref_temps: &DenseBitSet, ) -> Option<(Local, mir::Place<'tcx>)> { - let mir::StatementKind::Assign(assign) = &stmt.kind else { - return None; - }; - let (lhs, rvalue) = &**assign; - if !lhs.projection.as_ref().is_empty() { - return None; - } - let lhs_local = lhs.local; + let (lhs_local, rvalue) = assignment_to_local(stmt)?; - if let mir::Rvalue::CopyForDeref(place) = &rvalue { + if let mir::Rvalue::CopyForDeref(place) = rvalue { return Some((lhs_local, *place)); } + // GVN rewrites the deref temp of a `Box` deref into a plain copy of the box. `Box` is + // modeled by value, so taking that copy at face value would bind the temp to an + // independent box and make the deref below it miss the original place. + if let mir::Rvalue::Use(mir::Operand::Copy(place)) = rvalue { + if box_deref_temps.contains(lhs_local) { + return Some((lhs_local, *place)); + } + } + + self.extract_box_deref(stmt) + } + + /// The `ElaborateBoxDerefs` shape `_p = (_b.0.0 as *const T) Transmute`, as the local it + /// assigns and the `Box` place `_b` it dereferences. + fn extract_box_deref(&self, stmt: &mir::Statement<'tcx>) -> Option<(Local, mir::Place<'tcx>)> { + let (lhs_local, rvalue) = assignment_to_local(stmt)?; + let unique_did = self.ctx.def_ids.unique()?; let nonnull_did = self.ctx.def_ids.nonnull()?; @@ -403,7 +429,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { // Box deref pattern: `(_box.0.0 as *const T) Transmute` // projection = [..., Field(0, Unique), Field(0, NonNull)], transmuted to *const T let mir::Rvalue::Cast(mir::CastKind::Transmute, mir::Operand::Copy(place), cast_ty) = - &rvalue + rvalue else { return None; }; @@ -437,7 +463,24 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { Some((lhs_local, rest_place)) } + /// Locals that an `ElaborateBoxDerefs` chain dereferences as a whole, which is the shape of + /// the temps `Derefer` hoists out of a `Box` deref. + fn box_deref_temps(&self) -> DenseBitSet { + let mut temps = DenseBitSet::new_empty(self.body.local_decls.len()); + for data in self.body.basic_blocks.iter() { + for stmt in &data.statements { + if let Some((_, box_place)) = self.extract_box_deref(stmt) { + if box_place.projection.is_empty() { + temps.insert(box_place.local); + } + } + } + } + temps + } + fn unelaborate_derefs(&mut self) { + let box_deref_temps = self.box_deref_temps(); let mut v = analyze::ReplacePlacesVisitor::new(self.tcx); for (block, data) in self.body.basic_blocks.clone().iter_enumerated() { for (idx, _stmt) in data.statements.iter().enumerate() { @@ -445,7 +488,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { &mut self.body.basic_blocks.as_mut().as_mut_slice()[block].statements[idx]; v.visit_statement(stmt); let stmt = stmt.clone(); - let Some((dest_local, box_place)) = self.extract_elaborated_deref(&stmt) else { + let Some((dest_local, box_place)) = + self.extract_elaborated_deref(&stmt, &box_deref_temps) + else { continue; }; self.body.basic_blocks.as_mut().as_mut_slice()[block].statements[idx].kind = diff --git a/tests/ui/fail/box_field_optimized.rs b/tests/ui/fail/box_field_optimized.rs new file mode 100644 index 00000000..3d3faf49 --- /dev/null +++ b/tests/ui/fail/box_field_optimized.rs @@ -0,0 +1,12 @@ +//@error-in-other-file: Unsat +//@compile-flags: -C debug-assertions=off -C opt-level=1 + +struct S { + b: Box, +} + +fn main() { + let mut s = S { b: Box::new(1) }; + *s.b += 1; + assert!(*s.b == 1); +} diff --git a/tests/ui/pass/box_field_optimized.rs b/tests/ui/pass/box_field_optimized.rs new file mode 100644 index 00000000..866630cf --- /dev/null +++ b/tests/ui/pass/box_field_optimized.rs @@ -0,0 +1,12 @@ +//@check-pass +//@compile-flags: -C debug-assertions=off -C opt-level=1 + +struct S { + b: Box, +} + +fn main() { + let mut s = S { b: Box::new(1) }; + *s.b += 1; + assert!(*s.b == 2); +}