VmIo

ostd::mm::io

Trait VmIo 

Source 
pub trait VmIo<P: Sized>:
    Send
    + Sync
    + Sized {
    // Required methods
    spec fn obeys_vmio_read_requires() -> bool;
    spec fn obeys_vmio_read_ensures() -> bool;
    spec fn obeys_vmio_write_requires() -> bool;
    spec fn obeys_vmio_write_ensures() -> bool;
    spec fn vmio_read_requires(self, owner: P, offset: usize) -> bool;
    spec fn vmio_read_ensures(
        self,
        owner: P,
        offset: usize,
        new_owner: P,
        r: Result<(), Error>,
    ) -> bool;
    spec fn vmio_write_requires(self, owner: P, offset: usize) -> bool;
    spec fn vmio_write_ensures(
        self,
        owner: P,
        offset: usize,
        new_owner: P,
        r: Result<(), Error>,
    ) -> bool;
    exec fn read_slice<T: Pod, const N: usize>(
        &self,
        offset: usize,
        slice: ArrayPtr<T, N>,
        verus_tmp_slice_owner: Tracked<&mut PointsToArray<u8, N>>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
    exec fn write_bytes<const N: usize>(
        &self,
        offset: usize,
        bytes: ArrayPtr<u8, N>,
        verus_tmp_bytes_owner: Tracked<&mut PointsToArray<u8, N>>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
    exec fn write_val<T: Pod>(
        &self,
        offset: usize,
        val: T,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
    exec fn write_slice<T: Pod, const N: usize>(
        &self,
        offset: usize,
        slice: ArrayPtr<T, N>,
        verus_tmp_slice_owner: Tracked<&mut PointsToArray<T, N>>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
}
Expand description

A trait that enables reading/writing data from/to a VM object, e.g., USegment, [Vec<UFrame>] and UFrame.

§Concurrency

The methods may be executed by multiple concurrent reader and writer threads. In this case, if the results of concurrent reads or writes desire predictability or atomicity, the users should add extra mechanism for such properties.

Note: In this trait we follow the standard of vstd trait that allows precondition and postcondition overriding by introducing obeys_, _requires, and _ensures spec functions.

P is the type of the permission/ownership token used to track the state of the VM object.

Required Methods§

Source

spec fn obeys_vmio_read_requires() -> bool

If this returns true then the requires clause of read will be active.

Source

spec fn obeys_vmio_read_ensures() -> bool

If this returns true then the ensures clause of read will be active.

Source

spec fn obeys_vmio_write_requires() -> bool

If this returns true then the requires clause of write will be active.

Source

spec fn obeys_vmio_write_ensures() -> bool

If this returns true then the ensures clause of write will be active.

Source

spec fn vmio_read_requires(self, owner: P, offset: usize) -> bool

Checks whether the preconditions for read are met.

Source

spec fn vmio_read_ensures( self, owner: P, offset: usize, new_owner: P, r: Result<(), Error>, ) -> bool

Checks whether the postconditions for read are met.

Source

spec fn vmio_write_requires(self, owner: P, offset: usize) -> bool

Checks whether the preconditions for write are met.

Source

spec fn vmio_write_ensures( self, owner: P, offset: usize, new_owner: P, r: Result<(), Error>, ) -> bool

Checks whether the postconditions for write are met.

Source

exec fn read_slice<T: Pod, const N: usize>( &self, offset: usize, slice: ArrayPtr<T, N>, verus_tmp_slice_owner: Tracked<&mut PointsToArray<u8, N>>, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

Source

exec fn write_bytes<const N: usize>( &self, offset: usize, bytes: ArrayPtr<u8, N>, verus_tmp_bytes_owner: Tracked<&mut PointsToArray<u8, N>>, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

Source

exec fn write_val<T: Pod>( &self, offset: usize, val: T, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

Source

exec fn write_slice<T: Pod, const N: usize>( &self, offset: usize, slice: ArrayPtr<T, N>, verus_tmp_slice_owner: Tracked<&mut PointsToArray<T, N>>, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

requires
Self::obeys_vmio_write_requires()
    ==> Self::vmio_write_requires(*self, *old(owner), offset),
ensures
Self::obeys_vmio_write_ensures()
    ==> Self::vmio_write_ensures(*self, *old(owner), offset, *owner, r),

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§