Trait miri::Provenance

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

    fn get_alloc_id(self) -> Option<AllocId>;
    fn join(left: Option<Self>, right: Option<Self>) -> Option<Self>;

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

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. The Debug rendering is used to distplay bare provenance, and for the default impl of fmt.

Required Associated Constants

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.

Required Methods

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.)

fn join(left: Option<Self>, right: Option<Self>) -> Option<Self>

Defines the ‘join’ of provenance: what happens when doing a pointer load and different bytes have different provenance.

Provided Methods

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

Determines how a pointer should be printed.

Default impl is only good for when OFFSET_IS_ADDR == true.

Implementors

impl Provenance for Provenance

const OFFSET_IS_ADDR: bool = true