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

This looks like we can implement a single struct with a type parameter

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.

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.

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.

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,
    }

}