Description
#2059 is nearing completion, so I figured it would make sense to lay down my current plan for the future of provenance in Miri.
My idea is that, by default, we will work in "permissive" provenance mode, implementing as good as we can the angelic from_exposed_addr
semantics for int2ptr cast. This is different from now: pointers created in this way get a "wildcard" provenance, and on each access we check if that access happens in the range of some previously exposed provenance. This resolves problems like #1866. There also will be no more "untagged" in Stacked Borrows, but instead Stacked Borrows will have support for the "wildcard" provenance and track which tags have been exposed. That should, hopefully, be much less confusing than the current default. (In particular, if you do not use from_expose_addr
/int2ptr casts, it is equivalent to -Zmiri-tag-raw-pointers
.) Meanwhile, if you use addr
/ptr::invalid
, then the restrictions documented in their spec are actually enforced.
When the program actually executes an int2ptr cast or calls from_exposed_addr
, a warning is shown:
warning: this program is using integer-to-pointer casts. This is equivalent to calling
from_exposed_addr
, which means that Miri might miss pointer bugs in this program.
See https://doc.rust-lang.org/nightly/std/ptr/fn.from_exposed_addr.html for more details on that operation.
To ensure that Miri does not miss bugs in your program, usewith_addr
instead; see https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance for more details. You can then pass the-Zmiri-strict-provenance
flag to Miri, to ensure you are not relying onfrom_exposed_addr
semantics.
To silence this warning, pass the-Zmiri-permissive-provenance
flag to Miri.
-Zmiri-permissive-provenance
literally just disables the warning.
-Zmiri-strict-provenance
turns expose_addr
into an alias for addr
(i.e., it no longer tracks which pointers have been exposed), and it turns ptr::from_exposed_addr
into an alias for ptr::invalid
(i.e., the pointers produced that way cause UB when being dereferenced, except for ZST accesses). Or maybe it should just make ptr::from_exposed_addr
a hard error? That would be a very clear story ("just make the above warning an error"), but it means code that uses from_exposed_addr
but then doesn't actually dereference the pointer stops working. But is there any reason to have such code? I say we try this, and see if it causes any trouble.
What I am not entirely sure about is what to do with ptr-to-int transmutes (via mem::transmute
or other means of type punning). With -Zmiri-strict-provenance
they should trigger UB. They should probably also trigger UB by default because we do have to consider these programs buggy. -Zmiri-permissive-provenance
is meant to be a sound flag so it should not enable them either. For now, we have the -Zmiri-allow-ptr-int-transmute
flag to allow them, but not everything that you think might work will work. (In particular, doing a bytewise copy at type u8
will never work, that just requires way too deep changes in the interpreter.)
TODO:
- Initial work on Miri permissive-exposed-provenance #2059
- Permissive provenance support in Stacked Borrows: Handle wildcard pointers in SB #2196
- Make
addr
not expose the provenance: interpret: better control over whether we read data with provenance rust#97684, implement ptr.addr() via transmute rust#97710 - Make
ptr::invalid
always produce a pointer with invalid provenance: make ptr::invalid not the same as a regular int2ptr cast rust#97219, with permissive-provenance set, we already treat ptr::invalid correctly #2153 - Once permissive provenance and raw ptr tagging are enabled by default, make int2ptr casts with
-Zmiri-strict-provenance
an error - Review the intptrcast issues.