Skip to main content

VmIo

ostd::mm::io

Trait VmIo 

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

Show 18 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>;

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

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_owner: Tracked<&mut P>, ) -> r : Result<(), Error>

requires
!Self::obeys_vmio_read_requires(),

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

Wraps buf in a VmWriter (whose tracked owner is minted internally from the slice via VmWriter::from) and delegates to Self::read. The shallow contract here only forwards the result; impls with non-trivial read_requires must override.

Source

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

requires
!Self::obeys_vmio_read_requires(),

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

Source

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

requires
!Self::obeys_vmio_read_requires(),

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

Source

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

requires
!Self::obeys_vmio_write_requires(),

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

Wraps buf in a VmReader (whose tracked owner is minted internally from the slice via VmReader::from) and delegates to Self::write. The shallow contract here only forwards the result; impls with non-trivial write_requires must override.

Source

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

requires
!Self::obeys_vmio_write_requires(),

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

Source

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

requires
!Self::obeys_vmio_write_requires(),

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

Source

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

requires
!Self::obeys_vmio_write_requires(),
offset as int + align as int <= usize::MAX as int,
core::mem::size_of::<T>() as int + align as int <= usize::MAX as int,
iter.obeys_prophetic_iter_laws(),
iter.decrease() is Some,
!(align <= 1 || is_pow2(align as int)) ==> may_panic(),
ensures
align <= 1 || is_pow2(align as int),

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. Bad align panics at runtime — this is captured as a post-condition, not a pre-condition, since the panic is what enforces it.

Preconditions left for the caller:

  • offset + (align - 1) and size_of::<T>() + (align - 1) don’t overflow (so the post-panic call to align_up is safe).
  • The supplied iterator obeys Verus’ prophetic iterator laws and provides a decrease measure (true for slice iterators, repeat_n, and the stdlib iterator combinators ostd uses).
  • self’s impl has no custom write_requires (use the override route for impls that do).

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§