Miri warns about int2ptr when Stacked Borrows is disabled

[saethlin]

In response to a suggestion from @RalfJung, I tried running the tests for bitvec with -Zmiri-disable-stacked-borrows, only to be greeted with a bunch of warnings about int2ptr. It seems to me like those are just noise with that flag applied?

[RalfJung]

Provenance is very much a thing even without Stacked Borrows, so the warning is definitely deliberate.

[saethlin]

Sure provenance exists, but in a world without Stacked Borrows, is there any downside from the perspective of Miri's analysis to doing ptr-int-ptr roundtrips? I thought the point of those warnings were to indicate that if the user wants to tighten up the results they get from Miri, those are the places to work. But with Stacked Borrows disabled, are there any approximate operations?

[RalfJung]

Yes there is. Miri will still miss UB. For instance this should be flagged as UB (independent of stacked borrows) but is not:

#![feature(strict_provenance)]
use std::ptr;

fn main() {
    let x0 = &0;
    let x1 = &1;
    let addr0 = (x0 as *const i32).expose_addr();
    let addr1 = (x1 as *const i32).expose_addr();
    let ptr0 = ptr::from_exposed_addr::<i32>(addr0);
    // Now we use a ptr with the same provenance to access two different locations.
    // This is definitely UB, but Miri doesn't see it: ptr0 in Miri has "wildcard"
    // provenance and hence may access any exposed allocation.
    assert_eq!(unsafe { *ptr0 }, 0);
    assert_eq!(unsafe { *ptr0.with_addr(addr1) }, 1);
}

from_exposed_addr can only guess one provenance, and it must be either that of x0 or that of x1, so at least one of the two accesses at the end is UB due to using a pointer that has provenance for the wrong allocation.

[saethlin]

I am upset that I didn't already know this. 😂

[RalfJung]

If you have ideas for better documenting/communicating this, I am all ears. :D