Confusing MIRI playground output

[nico-abram]

miri correctly reports UB for this snippet: https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=409c5066eff73741feb30e60f99a77b6

fn main() {
    let mut x: u8 = 0u8;
    let ptr_a = &mut x as *mut u8;
    
    x = 2;
    dbg!(&x);
    
    unsafe { *(&mut *ptr_a) = 1; }
    dbg!( unsafe { *ptr_a } );
}

But it fails to do so if we add the following: let _ptr_b = &mut x as *mut u8; in the middle (https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=beec17b4d3e748688ff24e9a263f166c)

fn main() {
    let mut x: u8 = 0u8;
    let ptr_a = &mut x as *mut u8;
    
    x = 2;
    dbg!(&x);
    
    let _ptr_b = &mut x as *mut u8;
    
    unsafe { *(&mut *ptr_a) = 1; }
    dbg!( unsafe { *ptr_a } );
}

MemeOverloard#4299(Yandros ꜰʀ-ᴇꜱ) in the rust community discord's #black-magic channel mentioned that using -Zmiri-track-raw-pointers fixes the issue and makes miri complain about the second snippet

I'm not sure what that flag or if this is expected behaviour without it, so I'm opening this issue in case this is a bug

[RalfJung]

Currently, this is expected behavior -- Miri (with default flags) does not attempt to differentiate different raw pointers, so in the second example it "mixes up" ptr_a and _ptr_b. This is to be able to support raw pointers being cast to integers and back, which is a tricky operation to specify.

But keep in mind that Stacked Borrows is just an experiment, and subject to change. The hope is that eventually we'll have a model that tracks raw pointers more precisely while still supporting int-to-ptr casts -- that's rust-lang/unsafe-code-guidelines#248.