add -Zmiri-strict-provenance

[RalfJung]

This implements strict provenance in Miri. The only change is that casting an integer to a pointer does not even attempt to produce a good provenance for the given address; instead, it always uses the invalid provenance. This stricter than even -Zmiri-tag-raw-pointers in that it also rejects the following example (which does not even involve Stacked Borrows):

fn main() {
    let x = 22;
    let ptr = &x as *const _ as *const u8;
    let roundtrip = ptr as usize as *const u8;
    let _ = unsafe { roundtrip.offset(1) };
}

The new flag also implies -Zmiri-tag-raw-pointers since the only reason one would not want to tag raw pointers is to support ptr-int-ptr roundtrips.

Note that the flag does not check against ptr-to-int transmutes; that still requires -Zmiri-check-number-validity. You can also check for strict provenance without Stacked Borrows by adding -Zmiri-disable-stacked-borrows.

The new "Miri hard mode" flags for maximal checking are -Zmiri-strict-provenance -Zmiri-check-number-validity. (Add -Zmiri-symbolic-alignment-check if you feel extra spicy today.)

[JakobDegen]

And don't forget RUSTFLAGS="-Zrandomize-layout"!

[bgeron]

I'm trying to convince the community that strict_provenance doesn't mean we need to break backwards compatibility. The confusion between "new functionality" vs "break existing code" has been causing anger and confusion.

In that context, I propose to rename this flag to -Zmiri-strict-only-provenance — as permissive provenance is no more.

Ideally I would like specific functions to stdlib for strict-provenance conversions, so that we have interpret both sets of operations differently in Miri. But we can't do that in this MR. So a rename is preferable.

[RalfJung]

@bgeron I don't quite see what that extra "only" would accomplish. The entire thing is called "strict provenance experiment", and "following strict provenance" means to follow the rules of the experiment. The confusion is around whether rustc is been given license to assume that all code follows strict provenance (no, it is not). But following strict provenance makes it much easier (or sometimes is required to make it possible) to check your code with Miri or CHERI, and that is what this flag corresponds to.

What the flag does is enforce the rules of strict provenance. If anything we could name it -Zmiri-enforce-strict-provenance but that seems just unnecessarily verbose.

[RalfJung]

interpret both sets of operations differently in Miri

That would basically mean not having a strict provenance memory model, so it doesn't need a flag. It is currently the default.

Maybe one day we can swap the default, but that's a different question.

[bgeron]

Fair point.

[RalfJung]

@bors r+

[bors]

📌 Commit 9af03bf has been approved by RalfJung

[bors]

⌛ Testing commit 9af03bf with merge 732461b...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 732461b to master...