What does -Zmiri-disable-validation mean for pointers from transmutes (now?)

[saethlin]

The README says

-Zmiri-disable-validation disables enforcing validity invariants, which are enforced by default.

Which to me suggests that I shouldn't see errors about how "0xsomething is not a valid pointer", but I do. This program:

fn main() {
    let x = 0u8;
    let ptr = &x as *const u8;
    let val = ptr as usize;
    unsafe {
        let ptr = std::mem::transmute::<usize, *const u8>(val);
        dbg!(*ptr);
    }
}

produces this error, with -Zmiri-disable-stacked-borrows -Zmiri-disable-validation:

error: Undefined Behavior: dereferencing pointer failed: 0x24881 is not a valid pointer
 --> src/main.rs:7:9
  |
7 |         dbg!(*ptr);
  |         ^^^^^^^^^^ dereferencing pointer failed: 0x24881 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 rustc_src/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

So for me the problem here is that

1. The documentation seems wrong, I disabled validity checks so why is Miri complaining about validity?
2. This is exactly the same error message that Miri emits for a wild pointer dereference; if I transmute any old usize instead of val I see the same error. It should be possible to distinguish between "that's an invalid pointer" and "there's no memory at that address". When I as a somewhat expert Miri user see that error I immediately guess that there is a transmute happening, but when I shared that error message with people some assumed it was a wild pointer access. Perhaps the problem is that the validity issue here has to do with provenance not the address, but Miri prints the address in the diagnostic, absent the lack of provenance which is what makes this invalid.

[RalfJung]

The problem is that the term "valid" is awfully overloaded.^^

"disable-validation" specifically refers to checking the "validity invariant", which says things like "2 is not a valid bool". This is the part of the UB definition that talks about "Producing an invalid value" -- that kind of UB is no longer detected.

Your example program violates a different UB clause, namely the one which says "Evaluating a dereference expression (*expr) on a raw pointer that is dangling or unaligned". The flag does not affect checking that UB clause.

And indeed, the reason this pointer is dangling is that pointers created via transmute are ptr::invalid pointers, which are dangling.

[RalfJung]

Miri prints the address in the diagnostic, absent the lack of provenance which is what makes this invalid.

When an access is invalid, Miri doesn't have a clue whether a different provenance could have made the access valid -- and at least in general, that is quite hard to detect as well. All it can say is "this address with this provenance doesn't work".

Maybe it should print the pointer as 0x24881[noalloc], mirroring the "usual" 0x24881[alloc1234]?

[saethlin]

I think it would be a nice improvement to note these two kinds of validity in the docs and always print pointers with their provenance. Though I'm not yet sold on that syntax and at this point we definitely need a glossary.

But I also think the English part of this could do with a bit of adjustment. To my brain at least, the pointer itself is perfectly valid, but all dereferences of it are invalid. Or just this dereference is invalid. So it would be nice to see the error distinguish between the validity of the pointer itself and the dereference of it.

[RalfJung]

So are you suggesting we rename ptr::invalid to something else?
Because if not, we'll use two different words for the same thing, which is not great either.

[saethlin]

I think that name could be better. The point of that function is to create a ptr::without_provenance 🤷

But I don't think we need to rename that function to improve things here. An error that says "0x1234[noalloc] is invalid for read/write/offset because it has no provenance" would be a nice reuse of the wording in the docs for ptr::invalid.

Then for pointers that have a provenance we could say "0x1234[alloc567] is invalid for read/write/offset because its address is outside its provenance" or something like that.