Skip to main content

VmIo

ostd::mm::io

Trait VmIo 

Source 
pub trait VmIo<P: Sized>:
    Send
    + Sync
    + Sized {

Show 19 methods    // 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 { ... }
    fn read_bytes(
        &self,
        offset: usize,
        buf: &mut [u8],
        verus_tmp_writer_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<(), Error> { ... }
    fn read_val<T: Pod>(
        &self,
        offset: usize,
        verus_tmp_writer_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<T, Error> { ... }
    fn read_slice<T: Pod>(
        &self,
        offset: usize,
        slice: &mut [T],
        verus_tmp_writer_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<(), Error> { ... }
    fn write_bytes(
        &self,
        offset: usize,
        buf: &[u8],
        verus_tmp_reader_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<(), Error> { ... }
    fn write_val<T: Pod>(
        &self,
        offset: usize,
        new_val: &T,
        verus_tmp_reader_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<(), Error> { ... }
    fn write_slice<T: Pod>(
        &self,
        offset: usize,
        slice: &[T],
        verus_tmp_reader_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<(), Error> { ... }
    fn write_vals<'a, T: Pod + 'a, I: Iterator<Item = &'a T>>(
        &self,
        offset: usize,
        iter: I,
        align: usize,
        verus_tmp_reader_own: Tracked<&mut VmIoOwner>,
        verus_tmp_owner: Tracked<&mut P>,
    ) -> Result<usize, 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_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 }
Source

exec fn read_bytes( &self, offset: usize, buf: &mut [u8], verus_tmp_writer_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<(), Error>

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

This default impl wraps buf in a VmWriter and delegates to Self::read. Mirrors vostd’s read_bytes default.

Source

exec fn read_val<T: Pod>( &self, offset: usize, verus_tmp_writer_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<T, Error>

Reads a value of a specified type at a specified offset.

Mirrors vostd’s read_val default.

Source

exec fn read_slice<T: Pod>( &self, offset: usize, slice: &mut [T], verus_tmp_writer_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<(), Error>

Reads a slice of a specified type at a specified offset.

Mirrors vostd’s read_slice default.

Source

exec fn write_bytes( &self, offset: usize, buf: &[u8], verus_tmp_reader_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<(), Error>

Writes a specified number of bytes from a given buffer at a specified offset.

This default impl wraps buf in a VmReader and delegates to Self::write. Mirrors vostd’s write_bytes default.

Source

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

Writes a value of a specified type at a specified offset.

Mirrors vostd’s write_val default.

Source

exec fn write_slice<T: Pod>( &self, offset: usize, slice: &[T], verus_tmp_reader_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<(), Error>

Writes a slice of a specified type at a specified offset.

Mirrors vostd’s write_slice default.

Source

exec fn write_vals<'a, T: Pod + 'a, I: Iterator<Item = &'a T>>( &self, offset: usize, iter: I, align: usize, verus_tmp_reader_own: Tracked<&mut VmIoOwner>, verus_tmp_owner: Tracked<&mut P>, ) -> Result<usize, Error>

Writes a sequence of values given by an iterator (iter) from the specified offset (offset).

Stops on iterator exhaustion or write error. Returns Ok(nr_written) if at least one value was written; only the first-call error path surfaces as Err.

align rounds the offset and item size up: 0/1 means no padding, otherwise must be a power of two.

Mirrors vostd’s write_vals default.

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§