Trait Memory 

pub trait Memory: Obj {
    type T: Target + Obj + for<'de> Deserialize<'de> + Serialize;
    type Provenance: Obj + for<'de> Deserialize<'de> + Serialize;
    type FrameExtra: Obj + for<'de> Deserialize<'de> + Serialize;
    type Params: Default + Obj + for<'de> Deserialize<'de> + Serialize;

    // Required methods
    fn new(params: Self::Params) -> Self;
    fn allocate(
        &mut self,
        kind: AllocationKind,
        size: Size,
        align: Align,
    ) -> NdResult<ThinPointer<Self::Provenance>, TerminationInfo>;
    fn deallocate(
        &mut self,
        ptr: ThinPointer<Self::Provenance>,
        kind: AllocationKind,
        size: Size,
        align: Align,
    ) -> Result<(), TerminationInfo>;
    fn store(
        &mut self,
        ptr: ThinPointer<Self::Provenance>,
        bytes: List<AbstractByte<Self::Provenance>>,
        align: Align,
    ) -> Result<(), TerminationInfo>;
    fn load(
        &mut self,
        ptr: ThinPointer<Self::Provenance>,
        len: Size,
        align: Align,
    ) -> Result<List<AbstractByte<Self::Provenance>>, TerminationInfo>;
    fn dereferenceable(
        &self,
        ptr: ThinPointer<Self::Provenance>,
        len: Size,
    ) -> Result<(), TerminationInfo>;
    fn new_call() -> Self::FrameExtra;
    fn leak_check(&self) -> Result<(), TerminationInfo>;

    // Provided methods
    fn signed_dereferenceable(
        &self,
        ptr: ThinPointer<Self::Provenance>,
        len: Int,
    ) -> Result<(), TerminationInfo> { ... }
    fn retag_ptr(
        &mut self,
        _frame_extra: &mut Self::FrameExtra,
        ptr: Pointer<Self::Provenance>,
        _ptr_type: PtrType,
        _fn_entry: bool,
        _fn_implicit_writes: bool,
        _vtable_lookup: impl Fn(ThinPointer<Self::Provenance>) -> VTable + 'static,
    ) -> Result<Pointer<Self::Provenance>, TerminationInfo> { ... }
    fn end_call(
        &mut self,
        _extra: Self::FrameExtra,
    ) -> Result<(), TerminationInfo> { ... }
}

Note: All memory operations can be non-deterministic, which means that executing the same operation on the same memory can have different results. We also let read operations potentially mutate memory (they actually can change the current state in concurrent memory models and in Stacked Borrows).

Required Associated Types

type T: Target + Obj + for<'de> Deserialize<'de> + Serialize

The target information. This doesn’t really belong to the memory, but avoids having to quantify over both memory and target everywhere.

type Provenance: Obj + for<'de> Deserialize<'de> + Serialize

The type of pointer provenance.

type FrameExtra: Obj + for<'de> Deserialize<'de> + Serialize

Extra information for each stack frame.

type Params: Default + Obj + for<'de> Deserialize<'de> + Serialize

Parameters controlling memory model behavior, passed at construction time.

Required Methods

fn new(params: Self::Params) -> Self

Create a new instance of the memory model with the given parameters.

fn allocate( &mut self, kind: AllocationKind, size: Size, align: Align, ) -> NdResult<ThinPointer<Self::Provenance>, TerminationInfo>

Create a new allocation. The initial contents of the allocation are AbstractByte::Uninit.

This is the only non-deterministic operation in the memory interface.

fn deallocate( &mut self, ptr: ThinPointer<Self::Provenance>, kind: AllocationKind, size: Size, align: Align, ) -> Result<(), TerminationInfo>

Remove an allocation.

fn store( &mut self, ptr: ThinPointer<Self::Provenance>, bytes: List<AbstractByte<Self::Provenance>>, align: Align, ) -> Result<(), TerminationInfo>

Write some bytes to memory.

fn load( &mut self, ptr: ThinPointer<Self::Provenance>, len: Size, align: Align, ) -> Result<List<AbstractByte<Self::Provenance>>, TerminationInfo>

Read some bytes from memory.

Needs &mut self because in the aliasing model, reading changes the machine state.

fn dereferenceable( &self, ptr: ThinPointer<Self::Provenance>, len: Size, ) -> Result<(), TerminationInfo>

Test whether the given pointer is dereferenceable for the given size.

fn new_call() -> Self::FrameExtra

Create the extra information for a stack frame.

fn leak_check(&self) -> Result<(), TerminationInfo>

Check if there are any memory leaks.

Provided Methods

fn signed_dereferenceable( &self, ptr: ThinPointer<Self::Provenance>, len: Int, ) -> Result<(), TerminationInfo>

A derived form of dereferenceable that works with a signed notion of “length”.

fn retag_ptr( &mut self, _frame_extra: &mut Self::FrameExtra, ptr: Pointer<Self::Provenance>, _ptr_type: PtrType, _fn_entry: bool, _fn_implicit_writes: bool, _vtable_lookup: impl Fn(ThinPointer<Self::Provenance>) -> VTable + 'static, ) -> Result<Pointer<Self::Provenance>, TerminationInfo>

Retag the given pointer, which has the given type. fn_entry indicates whether this is one of the special retags that happen right at the top of each function.

This can assume the pointer satisfies the language invariant, in particular, it must be dereferenceable for its size. Violating this or breaking this for the return value is a spec bug.

The vtable_lookup is given, since computing the size and UnsafeCell positions requires information about vtables.

Return the retagged pointer.

fn end_call(&mut self, _extra: Self::FrameExtra) -> Result<(), TerminationInfo>

Memory model hook invoked at the end of each function call.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<T> Memory for BasicMemory<T>

where T: Target + Obj + for<'de> Deserialize<'de> + Serialize,

type Provenance = (AllocId, ())

type T = T

type FrameExtra = ()

type Params = ()

impl<T> Memory for TreeBorrowsMemory<T>

where T: Target + Obj + for<'de> Deserialize<'de> + Serialize,

type Provenance = (AllocId, List<Int>)

type FrameExtra = TreeBorrowsFrameExtra

type T = T

type Params = TreeBorrowsParams