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.

§Verified Properties
§Preconditions
  • The memory region represented by ptr and len must be valid for writes of len bytes during the entire lifetime a. This means that the underlying pages must remain alive, and the kernel must access the memory region using only the APIs provided in this module.
  • The range ptr.vaddr..ptr.vaddr + len must represent a kernel space memory range.
§Postconditions
  • An infallible VmWriter will be created with the range ptr.vaddr..ptr.vaddr + len.
  • The created VmWriter will have a unique identifier id, and its cursor will be initialized to ptr.
  • The created VmWriter will be associated with a VmIoOwner that has the same id, the same memory range, and is marked as kernel space and infallible.
  • The memory view of the associated VmIoOwner will be None, indicating that it does not have any specific permissions yet.
§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)

    }

},

Converts a PoD value into a VmWriter that writes to the memory occupied by the PoD value.

§Verified Properties
§Preconditions

None as the Rust’s type system guarantees that if T is valid, then we can always create a valid VmWriter for it.

§Postconditions
  • If the memory region occupied by val is valid for writes, then an infallible VmWriter will be created that points to the memory region of val.
  • If the memory region occupied by val is not valid for writes, then an IoError will be returned.
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,

Constructs a VmWriter from a pointer, which represents a memory range in USER space.

⚠️ WARNING: Currently not implemented yet.

§Verified Properties
§Preconditions
§Postconditions
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.

§Verified Properties
§Preconditions
  • self must satisfy its invariant.
§Postconditions
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.

§Verified Properties
§Preconditions
  • self must satisfy its invariant.
  • len must not exceed the remaining writable bytes.
§Postconditions
  • self still satisfies its invariant.
  • The cursor advances by len.
  • The remaining writable bytes decrease by len.
  • The writer identity and end cursor are preserved.
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_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,
old(owner_r)
    .mem_view matches Some(
    VmIoMemView::ReadView(mem_src),
) && forall |i: usize| {
    old(reader).cursor.vaddr <= i < old(reader).cursor.vaddr + old(reader).remain_spec()
        ==> {
            &&& 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

        }
},
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 data into self by reading from the provided reader.

This function treats self as the destination buffer. It pulls data from the source reader and writes it into the current instance.

§Arguments
  • reader - The source VmReader to read data from.
§Returns

Returns the number of bytes written to self (which is equal to the number of bytes read from reader).

§Verified Properties
§Preconditions
  • The writer, reader, and both associated owners must satisfy their invariants.
  • The owners must match the given writer and reader.
  • The writer owner must carry a write memory view.
  • The source and destination ranges must not overlap.
  • The reader owner must provide initialized readable memory for the readable range.
§Postconditions
  • The writer, reader, and both owners still satisfy their invariants.
  • The owners still match the updated writer and reader.
  • The returned byte count equals the minimum of writable bytes and readable bytes.
  • Both cursors advance by exactly the returned byte count.
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),
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.

§Verified Properties
§Preconditions
  • The writer and its owner must satisfy their invariants.
  • The owner must match this writer and carry a memory view.
§Postconditions
  • The writer and owner still satisfy their invariants.
  • The owner parameters tracked by VmIoOwner::params_eq are preserved.
  • On success, the cursor advances by size_of::<T>().
  • On error, the writer state is unchanged.
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,
},

Writes a value of the PodOnce type using one non-tearing memory store.

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

§Verified Properties
§Preconditions
  • The writer and its owner must satisfy their invariants.
  • The owner must match this writer and carry a memory view.
§Postconditions
  • The writer and owner still satisfy their invariants.
  • On success, the cursor advances by size_of::<T>().
  • On error, the writer state is unchanged.

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>