Skip to main content

VmIo

ostd::mm::io

Trait VmIo 

Source 
pub trait VmIo<P: Sized>:
    Send
    + Sync
    + Sized {
    // Required methods
    spec fn obeys_vmio_spec() -> bool;
    spec fn obeys_vmio_read_spec() -> bool;
    spec fn obeys_vmio_write_spec() -> bool;
    spec fn read_spec(
        self,
        offset: usize,
        old_writer: VmWriter<'_>,
        new_writer: VmWriter<'_>,
        old_writer_own: VmIoOwner<'_>,
        new_writer_own: VmIoOwner<'_>,
        old_owner: P,
        new_owner: P,
        r: Result<(), Error>,
    ) -> bool;
    spec fn write_spec(
        self,
        offset: usize,
        old_reader: VmReader<'_>,
        new_reader: VmReader<'_>,
        old_writer_own: VmIoOwner<'_>,
        new_writer_own: VmIoOwner<'_>,
        old_owner: P,
        new_owner: P,
        r: Result<(), Error>,
    ) -> bool;
    exec fn read(
        &self,
        offset: usize,
        writer: &mut VmWriter<'_>,
        verus_tmp_writer_own: Tracked<&mut VmIoOwner<'_>>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
    exec fn write(
        &self,
        offset: usize,
        reader: &mut VmReader<'_>,
        verus_tmp_writer_own: Tracked<&mut VmIoOwner<'_>>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> r : Result<(), Error>;
    exec fn read_byte<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>;

    // Provided methods
    open spec fn obeys_vmio_read_requires() -> bool { ... }
    fn obeys_vmio_write_requires() -> bool { ... }
    fn read_requires(
        self,
        offset: usize,
        writer: VmWriter<'_>,
        writer_own: VmIoOwner<'_>,
        owner: P,
    ) -> bool { ... }
    fn write_requires(
        self,
        offset: usize,
        reader: VmReader<'_>,
        reader_own: VmIoOwner<'_>,
        owner: P,
    ) -> bool { ... }
}
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_spec() -> bool

Source

spec fn obeys_vmio_read_spec() -> bool

recommends
Self::obeys_vmio_spec(),
Source

spec fn obeys_vmio_write_spec() -> bool

recommends
Self::obeys_vmio_spec(),
Source

spec fn read_spec( self, offset: usize, old_writer: VmWriter<'_>, new_writer: VmWriter<'_>, old_writer_own: VmIoOwner<'_>, new_writer_own: VmIoOwner<'_>, old_owner: P, new_owner: P, r: Result<(), Error>, ) -> bool

Source

spec fn write_spec( self, offset: usize, old_reader: VmReader<'_>, new_reader: VmReader<'_>, old_writer_own: VmIoOwner<'_>, new_writer_own: VmIoOwner<'_>, old_owner: P, new_owner: P, r: Result<(), Error>, ) -> bool

Source

exec fn read( &self, offset: usize, writer: &mut VmWriter<'_>, verus_tmp_writer_own: Tracked<&mut VmIoOwner<'_>>, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

requires
Self::obeys_vmio_read_requires()
    ==> Self::read_requires(*self, offset, *old(writer), *old(writer_own), *old(owner)),
ensures
Self::obeys_vmio_read_spec()
    ==> Self::read_spec(
        *self,
        offset,
        *old(writer),
        *final(writer),
        *old(writer_own),
        *final(writer_own),
        *old(owner),
        *final(owner),
        r,
    ),

Reads requested data at a specified offset into a given VmWriter.

§No short reads

On success, the writer must be written with the requested data completely. If, for any reason, the requested data is only partially available, then the method shall return an error.

Source

exec fn write( &self, offset: usize, reader: &mut VmReader<'_>, verus_tmp_writer_own: Tracked<&mut VmIoOwner<'_>>, verus_tmp_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

requires
Self::obeys_vmio_write_requires()
    ==> Self::write_requires(*self, offset, *old(reader), *old(writer_own), *old(owner)),
ensures
Self::obeys_vmio_write_spec()
    ==> Self::write_spec(
        *self,
        offset,
        *old(reader),
        *final(reader),
        *old(writer_own),
        *final(writer_own),
        *old(owner),
        *final(owner),
        r,
    ),

Writes all data from a given VmReader at a specified offset.

§No short writes

On success, the data from the reader must be read to the VM object entirely. If, for any reason, the input data can only be written partially, then the method shall return an error.

Source

exec fn read_byte<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>

Reads a specified number of bytes at a specified offset into a given buffer.

§No short reads

Similar to read.

Provided Methods§

Source

open spec fn obeys_vmio_read_requires() -> bool

recommends
Self::obeys_vmio_spec(),
{ false }
Source

open spec fn obeys_vmio_write_requires() -> bool

recommends
Self::obeys_vmio_spec(),
{ false }
Source

open spec fn read_requires( self, offset: usize, writer: VmWriter<'_>, writer_own: VmIoOwner<'_>, owner: P, ) -> bool

{ true }
Source

open spec fn write_requires( self, offset: usize, reader: VmReader<'_>, reader_own: VmIoOwner<'_>, owner: P, ) -> bool

{ true }

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§