Trait miri::Provenance

source · [−]

pub trait Provenance: Copy + Debug {
    const OFFSET_IS_ADDR: bool;
    const ERR_ON_PARTIAL_PTR_OVERWRITE: bool;

    fn fmt(ptr: &Pointer<Self>, f: &mut Formatter<'_>) -> Result<(), Error>;
    fn get_alloc_id(self) -> Option<AllocId>;
    fn join(left: Option<Self>, right: Option<Self>) -> Option<Self>;
}

Expand description

This trait abstracts over the kind of provenance that is associated with a Pointer. It is mostly opaque; the Machine trait extends it with some more operations that also have access to some global state. We don’t actually care about this Debug bound (we use Provenance::fmt to format the entire pointer), but derive adds some unnecessary bounds.

Required Associated Constants

source

const OFFSET_IS_ADDR: bool

Says whether the offset field of Pointers with this provenance is the actual physical address.

If false, the offset must be relative. This means the bytes representing a pointer are different from what the Abstract Machine prescribes, so the interpreter must prevent any operation that would inspect the underlying bytes of a pointer, such as ptr-to-int transmutation. A ReadPointerAsBytes error will be raised in such situations.
If true, the interpreter will permit operations to inspect the underlying bytes of a pointer, and implement ptr-to-int transmutation by stripping provenance.

source

const ERR_ON_PARTIAL_PTR_OVERWRITE: bool

We also use this trait to control whether to abort execution when a pointer is being partially overwritten (this avoids a separate trait in allocation.rs just for this purpose).

Required Methods

source

fn fmt(ptr: &Pointer<Self>, f: &mut Formatter<'_>) -> Result<(), Error>

Determines how a pointer should be printed.

source

fn get_alloc_id(self) -> Option<AllocId>

If OFFSET_IS_ADDR == false, provenance must always be able to identify the allocation this ptr points to (i.e., this must return Some). Otherwise this function is best-effort (but must agree with Machine::ptr_get_alloc). (Identifying the offset in that allocation, however, is harder – use Memory::ptr_get_alloc for that.)

source