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]>§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 inv_wf(self) -> bool

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

Structural well-formedness: the range is ordered. Always holds after construction.

Source §

impl VmIoOwner<'_>

Source

pub open spec fn has_read_view(self) -> bool

{ self.mem_view matches Some(VmIoMemView::ReadView(_)) }

Whether this owner carries a read memory view.

Source

pub open spec fn has_write_view(self) -> bool

{ self.mem_view matches Some(VmIoMemView::WriteView(_)) }

Whether this owner carries a write memory view.

Source

pub open spec fn can_read(self) -> bool

{ self.has_read_view() }

Whether this owner is ready to serve as the readable side of a copy.

Source

pub open spec fn can_write(self) -> bool

{ self.has_write_view() }

Whether this owner is ready to serve as the writable side of a copy.

Source

pub open spec fn read_view_initialized(self) -> bool

{
    match self.mem_view {
        Some(VmIoMemView::ReadView(mem_src)) => {
            forall |i: usize| (
                self.range@.start <= i < self.range@.end
                    ==> {
                        &&& mem_src.addr_transl(i) is Some
                        &&& mem_src
                            .memory
                            .contains_key(mem_src.addr_transl(i).unwrap().0)
                        &&& mem_src
                            .memory[mem_src.addr_transl(i).unwrap().0]
                            .contents[mem_src.addr_transl(i).unwrap().1 as int] is Init

                    }
            )
        }
        _ => false,
    }
}

Whether the read view initializes the entire owner range.

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

final(self).inv(),

final(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

final(self).inv(),

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

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

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

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

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

old(self)
    .mem_view matches Some(
    VmIoMemView::ReadView(_),
) ==> final(self).mem_view matches Some(VmIoMemView::ReadView(_)),

old(self)
    .mem_view matches Some(
    VmIoMemView::WriteView(_),
) ==> final(self).mem_view matches Some(VmIoMemView::WriteView(_)),

old(self).read_view_initialized() ==> final(self).read_view_initialized(),

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.

Trait Implementations§

Source §

impl Inv for VmIoOwner<'_>

Source §

open spec fn inv(self) -> bool

{
    &&& self.inv_wf()
    &&& 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,
    }

}