Miri: recursive validity: also recurse into Boxes

This commit is contained in:
Ralf Jung 2026-02-17 15:13:58 +01:00
parent 3f6250a7bb
commit f5421609d6
3 changed files with 22 additions and 6 deletions

View file

@ -647,13 +647,8 @@ impl<'rt, 'tcx, M: Machine<'tcx>> ValidityVisitor<'rt, 'tcx, M> {
} }
} else { } else {
// This is not CTFE, so it's Miri with recursive checking. // This is not CTFE, so it's Miri with recursive checking.
// FIXME: we do *not* check behind boxes, since creating a new box first creates it uninitialized // FIXME: should we also `UnsafeCell` behind shared references? Currently that is not
// and then puts the value in there, so briefly we have a box with uninit contents.
// FIXME: should we also skip `UnsafeCell` behind shared references? Currently that is not
// needed since validation reads bypass Stacked Borrows and data race checks. // needed since validation reads bypass Stacked Borrows and data race checks.
if matches!(ptr_kind, PointerKind::Box) {
return interp_ok(());
}
} }
let path = &self.path; let path = &self.path;
ref_tracking.track(place, || { ref_tracking.track(place, || {

View file

@ -0,0 +1,8 @@
//@compile-flags: -Zmiri-recursive-validation
fn main() {
let x = 3u8;
let xref = &x;
let xref_wrong_type: Box<bool> = unsafe { std::mem::transmute(xref) }; //~ERROR: encountered 0x03, but expected a boolean
let _val = *xref_wrong_type;
}

View file

@ -0,0 +1,13 @@
error: Undefined Behavior: constructing invalid value at .<deref>: encountered 0x03, but expected a boolean
--> tests/fail/validity/recursive-validity-box-bool.rs:LL:CC
|
LL | let xref_wrong_type: Box<bool> = unsafe { std::mem::transmute(xref) };
| ^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error