VmWriter

ostd::mm::io

Struct VmWriter 

Source 
pub struct VmWriter<'a> {
    pub id: Ghost<nat>,
    pub cursor: VirtPtr,
    pub end: VirtPtr,
    pub phantom: PhantomData<&'a [u8]>,
}
Expand description

VmWriter is a writer for writing data to a contiguous range of memory.

The memory range write by VmWriter can be in either kernel space or user space. When the operating range is in kernel space, the memory within that range is guaranteed to be valid, and the corresponding memory writes are infallible. When the operating range is in user space, it is ensured that the page table of the process creating the VmWriter is active for the duration of 'a, and the corresponding memory writes are considered fallible.

When perform writing with a VmReader, if one of them represents typed memory, it can ensure that the writing range in this writer and reading range in the reader are not overlapped.

NOTE: The overlap mentioned above is at both the virtual address level and physical address level. There is not guarantee for the operation results of VmReader and VmWriter in overlapping untyped addresses, and it is the user’s responsibility to handle this situation.

Fields§

§id: Ghost<nat>§cursor: VirtPtr§end: VirtPtr§phantom: PhantomData<&'a [u8]>

Implementations§

Source§

impl<'a> VmWriter<'a>

Source

pub unsafe exec fn from_kernel_space(ptr: VirtPtr, len: usize) -> r : Self

with
Ghost(id): Ghost <nat>,
Tracked(fallible): Tracked <bool>,
->
owner: Tracked <VmIoOwner <'a>>,
requires
!fallible,
ptr.inv(),
ptr.range@.start == ptr.vaddr,
len == ptr.range@.end - ptr.range@.start,
len == 0 || KERNEL_BASE_VADDR() <= ptr.vaddr,
len == 0 || ptr.vaddr + len <= KERNEL_END_VADDR(),
ensures
owner@.inv(),
owner@.inv_with_writer(r),
owner@.is_fallible == fallible,
owner@.id == id,
owner@.is_kernel,
owner@.mem_view is None,
r.cursor == ptr,
r.end.vaddr == ptr.vaddr + len,
r.cursor.range@ == ptr.range@,
r.end.range@ == ptr.range@,

Constructs a VmWriter from a pointer and a length, which represents a memory range in kernel space.

§Safety

ptr must be valid for writes of len bytes during the entire lifetime a.

Source

pub exec fn from_pod<T: Pod>(val: T) -> r : Result<VmWriter<'a>, Error>

with
Ghost(id): Ghost <nat>,
->
owner: Tracked <Result <VmIoOwner <'a>>>,
ensures
r is Ok <==> owner@ is Ok,
r matches Ok(
    r,
) ==> {
    &&& owner@ matches Ok(
        owner,
    ) ==> {
        &&& r.inv()
        &&& r.avail_spec() == core::mem::size_of::<T>()
        &&& owner.inv()
        &&& owner.inv_with_writer(r)

    }

},
Source§

impl<'a> VmWriter<'a>

Source

pub open spec fn avail_spec(&self) -> usize

{ (self.end.vaddr - self.cursor.vaddr) as usize }
Source

pub unsafe exec fn from_user_space(ptr: VirtPtr) -> r : Self

with
Ghost(id): Ghost <nat>,
->
owner: Tracked <VmIoOwner <'a>>,
requires
ptr.inv(),
ensures
r.inv(),
owner@.id == id,
owner@.inv(),
owner@.inv_with_writer(r),
owner@.range == ptr.range@,
owner@.mem_view is None,
!owner@.is_kernel,
!owner@.is_fallible,
Source

pub exec fn avail(&self) -> r : usize

requires
self.inv(),
ensures
r == self.avail_spec(),

Returns the number of available bytes that can be written.

This has the same implementation as VmReader::remain but semantically they are different.

Source

pub exec fn advance(&mut self, len: usize)

requires
old(self).inv(),
len <= old(self).avail_spec(),
ensures
self.inv(),
self.avail_spec() == old(self).avail_spec() - len,
self.cursor.vaddr == old(self).cursor.vaddr + len,
self.cursor.range@ == old(self).cursor.range@,
self.id == old(self).id,
self.end == old(self).end,

Advances the cursor by len bytes. Requires that there are at least len bytes available.

Source

pub exec fn write(&mut self, reader: &mut VmReader<'_>) -> r : usize

with
Tracked(owner_w): Tracked <& mut VmIoOwner <'_>>,
Tracked(owner_r): Tracked <& mut VmIoOwner <'_>>,
requires
old(self).inv(),
old(reader).inv(),
old(owner_w).inv(),
old(owner_r).inv(),
old(owner_w).inv_with_writer(*old(self)),
old(owner_r).inv_with_reader(*old(reader)),
old(owner_r).mem_view is Some,
old(owner_w).mem_view matches Some(VmIoMemView::WriteView(_)),
old(self).cursor.range@.start >= old(reader).cursor.range@.end
    || old(reader).cursor.range@.start >= old(self).cursor.range@.end,
ensures
self.inv(),
reader.inv(),
owner_w.inv(),
owner_r.inv(),
owner_w.inv_with_writer(*self),
owner_r.inv_with_reader(*reader),
r == vstd::math::min(old(self).avail_spec() as int, old(reader).remain_spec() as int),
self.avail_spec() == old(self).avail_spec() - r as usize,
self.cursor.vaddr == old(self).cursor.vaddr + r as usize,
reader.remain_spec() == old(reader).remain_spec() - r as usize,
reader.cursor.vaddr == old(reader).cursor.vaddr + r as usize,

Writes all data from the reader until one of the two conditions is met:

  1. The reader has no remaining data.
  2. The writer has no available space.

Returns the number of bytes written.

Source

pub exec fn write_val<T: Pod>(&mut self, val: &mut T) -> r : Result<(), Error>

with
Ghost(id): Ghost <nat>,
Tracked(owner_w): Tracked <& mut VmIoOwner <'_>>,
Tracked(memview_r): Tracked <& MemView>,
requires
old(self).inv(),
old(owner_w).inv(),
old(owner_w).inv_with_writer(*old(self)),
old(owner_w).mem_view is Some,
ensures
self.inv(),
owner_w.inv(),
owner_w.inv_with_writer(*self),
owner_w.params_eq(*old(owner_w)),
match r {
    Ok(_) => (
        &&& self.avail_spec() == old(self).avail_spec() - core::mem::size_of::<T>()
        &&& self.cursor.vaddr == old(self).cursor.vaddr + core::mem::size_of::<T>()

    ),
    Err(_) => *old(self) == *self,
},

Writes a value of Pod type.

If the length of the Pod type exceeds self.avail(), this method will return Err.

Source

pub exec fn write_once<T: PodOnce>(&mut self, new_val: &mut T) -> r : Result<(), Error>

with
Tracked(owner_w): Tracked <& mut VmIoOwner <'_>>,
requires
old(self).inv(),
old(owner_w).mem_view is Some,
old(owner_w).inv(),
old(owner_w).inv_with_writer(*old(self)),
ensures
self.inv(),
owner_w.inv(),
owner_w.inv_with_writer(*self),
match r {
    Ok(_) => (
        &&& self.avail_spec() == old(self).avail_spec() - core::mem::size_of::<T>()
        &&& self.cursor.vaddr == old(self).cursor.vaddr + core::mem::size_of::<T>()

    ),
    Err(_) => *old(self) == *self,
},

Trait Implementations§

Source§

impl Inv for VmWriter<'_>

Source§

open spec fn inv(self) -> bool

{
    &&& self.cursor.inv()
    &&& self.end.inv()
    &&& self.cursor.vaddr <= self.end.vaddr
    &&& self.cursor.range@ == self.end.range@

}
Source§

impl<'a> TryFrom<&'a [u8]> for VmWriter<'a>

Source§

exec fn try_from(slice: &'a [u8]) -> Result<Self, Error>

Source§

type Error = Error

The type returned in the event of a conversion error.
Source§

impl<'a> TryFromSpecImpl<&'a [u8]> for VmWriter<'a>

Source§

open spec fn obeys_try_from_spec() -> bool

{ true }
Source§

open spec fn try_from_spec(slice: &'a [u8]) -> Result<Self, Error>

{
    let addr = slice.as_ptr() as usize;
    let len = slice.len();
    if len != 0
        && (addr < KERNEL_BASE_VADDR() || len >= KERNEL_END_VADDR()
            || addr > KERNEL_END_VADDR() - slice.len()) || addr == 0
    {
        Err(Error::IoError)
    } else {
        Ok(Self {
            id: Ghost(arbitrary()),
            cursor: VirtPtr {
                vaddr: addr,
                range: Ghost(addr..(addr + len) as usize),
            },
            end: VirtPtr {
                vaddr: (addr + len) as usize,
                range: Ghost(addr..(addr + len) as usize),
            },
            phantom: PhantomData,
        })
    }
}

Auto Trait Implementations§

§

impl<'a> Freeze for VmWriter<'a>

§

impl<'a> RefUnwindSafe for VmWriter<'a>

§

impl<'a> Send for VmWriter<'a>

§

impl<'a> Sync for VmWriter<'a>

§

impl<'a> Unpin for VmWriter<'a>

§

impl<'a> UnwindSafe for VmWriter<'a>

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>