ostd::mm::io

Struct VmIoOwner

pub struct VmIoOwner<'a> {
    pub id: Ghost<nat>,
    pub range: Ghost<Range<usize>>,
    pub is_fallible: bool,
    pub phantom: PhantomData<&'a [u8]>,
    pub is_kernel: bool,
    pub mem_view: Option<VmIoMemView<'a>>,
}

Expand description

The owner of a VM I/O operation, which tracks the memory range and the memory view for the operation.

Basically the caller should be only interested in this struct when using VmReader and VmWriter to perform VM I/O operations, since the safety of these operations depends on the validity of the memory range and memory view tracked by this struct.

Fields§

§id: Ghost<nat>

The unique identifier of this owner.

§range: Ghost<Range<usize>>

The virtual address range owned by this owner.

§is_fallible: bool

Whether this reader is fallible.

§phantom: PhantomData<&'a [u8]>

The mem view associated with this owner.

§is_kernel: bool

Whether this owner is for kernel space.

§mem_view: Option<VmIoMemView<'a>>

The mem view associated with this owner.

Implementations§

Source §

impl VmIoOwner<'_>

Source

pub open spec fn overlaps(self, other: VmIoOwner<'_>) -> bool

{ !self.disjoint(other) }

Checks whether this owner overlaps with another owner.

Source

pub open spec fn overlaps_with_range(self, range: Range<usize>) -> bool

{
    &&& self.range@.start <= range.end
    &&& range.start <= self.range@.end

}

Source

pub open spec fn disjoint(self, other: VmIoOwner<'_>) -> bool

{
    &&& !self.overlaps_with_range(other.range@)
    &&& match (self.mem_view, other.mem_view) {
        (Some(lhs), Some(rhs)) => {
            match (lhs, rhs) {
                (VmIoMemView::WriteView(lmv), VmIoMemView::WriteView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::WriteView(lmv), VmIoMemView::ReadView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::ReadView(lmv), VmIoMemView::WriteView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::ReadView(lmv), VmIoMemView::ReadView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
            }
        }
        _ => true,
    }

}

Checks whether this owner is disjoint with another owner.

Source

pub open spec fn params_eq(self, other: VmIoOwner<'_>) -> bool

{
    &&& self.range@ == other.range@
    &&& self.is_fallible == other.is_fallible

}

Source

pub proof fn change_fallible(tracked &mut self, tracked fallible: bool)

requires

old(self).inv(),

old(self).is_fallible != fallible,

ensures

self.inv(),

self.is_fallible == fallible,

Changes the fallibility of this owner.

§Verified Properties

§Preconditions

The owner must satisfy its invariant.
The new fallibility must differ from the current one.

§Postconditions

The updated owner still satisfies its invariant.
The is_fallible field is updated to fallible.

Source

pub proof fn advance(tracked &mut self, nbytes: usize) -> tracked res : VmIoMemView<'_>

requires

old(self).inv(),

old(self).mem_view is Some,

nbytes <= old(self).range@.end - old(self).range@.start,

ensures

self.inv(),

self.range@.start == old(self).range@.start + nbytes,

self.range@.end == old(self).range@.end,

self.is_fallible == old(self).is_fallible,

self.id == old(self).id,

self.is_kernel == old(self).is_kernel,

Advances the cursor of the reader/writer by the given number of bytes.

Note this will return the advanced VmIoMemView as the previous permission is no longer needed and must be discarded then.

§Verified Properties

§Preconditions

The owner must satisfy its invariant.
The owner must carry a memory view.
nbytes must not exceed the remaining length of the owned range.

§Postconditions

The updated owner still satisfies its invariant.
The start of the owned range is advanced by nbytes.
The end of the owned range and the other owner parameters are preserved.
The returned VmIoMemView is the portion advanced past.

Source

pub proof fn tracked_read_view_unwrap(tracked &self) -> tracked r : &MemView

requires

self.inv(),

self.mem_view matches Some(VmIoMemView::ReadView(_)),

ensures

VmIoMemView::ReadView(r) == self.mem_view.unwrap(),

Unwraps the read view.

§Verified Properties

§Preconditions

The owner must satisfy its invariant.
The owner must carry a read memory view.

§Postconditions

The returned reference is exactly the read view stored in self.mem_view.

Source §

impl VmIoOwner<'_>

Source

pub open spec fn inv_with_reader(self, reader: VmReader<'_>) -> bool

{
    &&& self.inv()
    &&& self.range@.start == reader.cursor.vaddr
    &&& self.range@.end == reader.end.vaddr
    &&& self.id == reader.id
    &&& self
        .mem_view matches Some(
        VmIoMemView::ReadView(mv),
    ) ==> {
        forall |va: usize| (
            self.range@.start <= va < self.range@.end
                ==> {
                    &&& #[trigger] mv.addr_transl(va) is Some

                }
        )
    }

}

Source

pub open spec fn inv_with_writer(self, writer: VmWriter<'_>) -> bool

{
    &&& self.inv()
    &&& self.range@.start == writer.cursor.vaddr
    &&& self.range@.end == writer.end.vaddr
    &&& self.id == writer.id
    &&& self
        .mem_view matches Some(
        VmIoMemView::WriteView(mv),
    ) ==> {
        forall |va: usize| (
            self.range@.start <= va < self.range@.end
                ==> {
                    &&& #[trigger] mv.addr_transl(va) is Some

                }
        )
    }

}

Trait Implementations§

Source §

impl Inv for VmIoOwner<'_>

Source §

open spec fn inv(self) -> bool

{
    &&& self.range@.start <= self.range@.end
    &&& match self.mem_view {
        Some(VmIoMemView::WriteView(mv)) => (
            &&& mv.mappings.finite()
            &&& mv.mappings_are_disjoint()
            &&& forall |va: usize| (
                self.range@.start <= va < self.range@.end
                    ==> {
                        &&& #[trigger] mv.addr_transl(va) is Some

                    }
            )

        ),
        Some(VmIoMemView::ReadView(mv)) => (
            &&& mv.mappings.finite()
            &&& mv.mappings_are_disjoint()
            &&& forall |va: usize| (
                self.range@.start <= va < self.range@.end
                    ==> {
                        &&& #[trigger] mv.addr_transl(va) is Some

                    }
            )

        ),
        None => true,
    }

}

The invariant of a VmIoOwner.

The owned virtual-address range must be ordered. When a memory view is present, its mappings must be finite, disjoint, and cover the whole range. If the memory view is None, then this owner acts as a placeholder that grants no accessible memory.