Trait miri::Provenance

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

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.

Required Methods§

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

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§

source

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§