ostd::specs::mm::io

Struct VmIoOwner

pub struct VmIoOwner {
    pub id: nat,
    pub range: Range<usize>,
    pub is_fallible: bool,
    pub is_kernel: bool,
    pub mem_view: Option<VmIoMemView>,
}

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: nat

The unique identifier of this owner.

§range: Range<usize>

The virtual address range owned by this owner.

§is_fallible: bool

Whether this reader is fallible.

§is_kernel: bool

Whether this owner is for kernel space.

§mem_view: Option<VmIoMemView>

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(),

old(self)
    .mem_view matches Some(
    VmIoMemView::ReadView(_),
) ==> forall |va: usize| {
    old(self).range.start + nbytes <= va < old(self).range.end
        && old(self).read_view_of().addr_transl(va) is Some
        && old(self)
            .read_view_of()
            .memory
            .contains_key(old(self).read_view_of().addr_transl(va).unwrap().0)
        ==> {
            &&& old(self).read_view_of().addr_transl(va)
                == final(self).read_view_of().addr_transl(va)
            &&& old(self).read_view_of().read(va) == final(self).read_view_of().read(va)

        }
},

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 split(tracked &mut self, nbytes: usize) -> tracked r : VmIoOwner

requires

old(self).inv(),

old(self).mem_view is Some,

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

ensures

r.inv(),

r.range.start == old(self).range.start,

r.range.end == old(self).range.start + nbytes,

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

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

r.mem_view is Some,

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,

final(self).mem_view is Some,

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


},

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


},

old(self).read_view_initialized()
    ==> {
        &&& r.read_view_initialized()
        &&& final(self).read_view_initialized()

    },

Splits this owner at nbytes, returning the front portion as a new owner and shrinking self to cover the back portion.

§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

Both the returned front owner and the updated self satisfy their invariants and carry the same kind of memory view as the original.
The front owner covers [old.start, old.start + nbytes).
self’s range becomes [old.start + nbytes, old.end).
is_fallible, is_kernel are preserved on both sides.
If the original was an initialized read view, both sides remain initialized.

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(),

*r == Self::read_view_of(*self),

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

pub open spec fn read_view_of(self) -> MemView

{
    match self.mem_view {
        Some(VmIoMemView::ReadView(mv)) => mv,
        _ => arbitrary(),
    }
}

Spec helper: extract the MemView from a read-view owner.

Defined only when self.mem_view matches Some(ReadView(_)); otherwise returns an arbitrary value. Callers should establish the matching pattern via [has_read_view] before using this.

Source

pub proof fn write_to_read(tracked &mut self)

requires

old(self).inv(),

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

ensures

final(self).inv(),

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

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

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

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

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

old(self)
    .mem_view matches Some(
    VmIoMemView::WriteView(mv),
) ==> final(self).mem_view matches Some(VmIoMemView::ReadView(rv)) && rv == mv,

Converts the owner’s VmIoMemView::WriteView into a VmIoMemView::ReadView wrapping the same underlying MemView.

Used after a write-only phase (e.g., VmWriter::fill) to hand the buffer back as a read-only handle.

§Verified Properties

§Preconditions

The owner must satisfy its invariant and carry a write memory view.

§Postconditions

The owner still satisfies its invariant.
All structural fields (range, is_fallible, is_kernel, id) are preserved.
The memory view is now VmIoMemView::ReadView wrapping the same MemView as the original VmIoMemView::WriteView.

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

}