-Zmiri-strict-provenance reports UB when using the address-exposing Strict Provenance APIs correctly

[saethlin]

#![feature(strict_provenance)]
fn main() {
    let x = 0u8;
    let original_ptr = &x as *const u8;
    let addr = original_ptr.expose_addr();
    let new_ptr: *const u8 = core::ptr::from_exposed_addr(addr);
    unsafe {
        dbg!(*new_ptr);
    }
}

error: Undefined Behavior: dereferencing pointer failed: 0x27c02 is not a valid pointer
 --> src/main.rs:8:9
  |
8 |         dbg!(*new_ptr);
  |         ^^^^^^^^^^^^^^ dereferencing pointer failed: 0x27c02 is not a valid pointer
  |
  = 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: inside `main` at /home/ben/.rustup/toolchains/miri/lib/rustlib/src/rust/library/std/src/macros.rs:315:13
  = note: this error originates in the macro `dbg` (in Nightly builds, run with -Z macro-backtrace for more info)

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to previous error

I understand why this happens, but this is if nothing else incredibly surprising for users. The intuition is that the Strict Provenance mode in Miri should be compatible with the Strict Provenance APIs in the standard library. Could we make that happen? Or will this just be closed by the permissive provenance work?

[RalfJung]

Quoting the from_exposed_addr docs:

Using this method means that code is not following strict provenance rules.

So I think this is intended behavior.

However, after #2059 landed I want to add a warning (or maybe even an error?) so Miri in strict provenance mode says, the first time from_exposed_addr or an int2ptr cast is used, that this operation is not supported. This will require using some other operation for ptr::invalid though.

[RalfJung]

Also see #2133 which I literally wrote in parallel with you writing this. ;)

[Gankra]

Is there a way to invoke miri such that the distinction between these two APIs is actually useful? i.e. such that it attempts to be strict but incorporates exposing and from_exposed_addr as an operation? I forget, is angelic nondet a nightmare to actually support in an interpretter?

[RalfJung]

Not yet, but see #2133 for the plan to make that happen. :D My plan is to make that the default, and make -Zmiri-strict-provenance a flag to basically promise that one doesn't use the exposed stuff.

Yes, angelic is a nightmare, so this mode will miss some bugs where you use a from_exposed_addr-ptr in multiple mutually incompatible ways. That's why we also have -Zmiri-strict-provenance which will not miss bugs but will also not support the angelic stuff.

[RalfJung]

I will close this in favor of #2133. Currently this is intended behavior, and eventually the plan is that Miri would already error in the from_exposed_addr call and say that this is not supported with strict provenance enabled.