Skip to content

The plan for provenance #2133

Closed
Closed
@RalfJung

Description

@RalfJung

#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, use with_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 on from_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:

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-intptrcastArea: affects int2ptr and ptr2int castsC-projectCategory: a larger project is being tracked here, usually with checkmarks for individual steps

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions