Skip to main content

VmWriter

ostd::mm::io

Struct VmWriter 

Source 
pub struct VmWriter<'a, Fallibility = Fallible> {
    pub ghost_id: Ghost<nat>,
    pub cursor: VirtPtr,
    pub end: VirtPtr,
    pub phantom: PhantomData<(&'a [u8], Fallibility)>,
}
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§

§ghost_id: Ghost<nat>§cursor: VirtPtr§end: VirtPtr§phantom: PhantomData<(&'a [u8], Fallibility)>

Implementations§

Source§

impl<'a> VmWriter<'a, Infallible>

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>,
ensures
r.inv_wf(),
owner@.id == id,
owner@.is_fallible == fallible,
owner@.is_kernel,
r.cursor == ptr,
r.end == ptr.wrapping_add_spec(len),
r.cursor.range@ == ptr.range@,
r.end.range@ == ptr.range@,
fallible ==> owner@.mem_view is None,
!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)
    ==> {
        &&& r.inv()
        &&& owner@.inv()
        &&& r.wf(owner@)
        &&& owner@.has_write_view()

    },

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 to_fallible(self) -> r : VmWriter<'a, Fallible>

ensures
r.cursor == self.cursor,
r.end == self.end,
r.ghost_id == self.ghost_id,

Converts an infallible writer into a fallible one.

Source

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

with
Tracked(owner): Tracked<&mut VmIoOwner>,
requires
old(self).inv(),
old(self).wf(*old(owner)),
old(owner).has_write_view(),
ensures
final(self).inv(),
final(owner).inv(),
final(self).wf(*final(owner)),
match r {
    Ok(_) => (
        &&& final(self).avail_spec()
            == old(self).avail_spec() - core::mem::size_of::<T>()
        &&& final(self).cursor.vaddr
            == old(self).cursor.vaddr + core::mem::size_of::<T>()

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

Writes a value of Pod type to the kernel-space buffer.

If the length of the Pod type exceeds self.avail(), this method will return Err(InvalidArgs). Kernel-space writes don’t fault, so no rollback is needed — see VmWriter<Fallible>::write_val for the user-space variant with cursor rewind.

§Verified Properties
§Preconditions
  • The writer and its owner must satisfy their invariants.
  • The owner must match this writer and carry a write 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.
Source

pub open spec fn fill_panic_condition<T>(self) -> bool

{
    ||| self.cursor.vaddr as int % core::mem::align_of::<T>() as int != 0
    ||| (self.end.vaddr - self.cursor.vaddr) as int % core::mem::size_of::<T>() as int
        != 0

}

Panic condition for Self::fill: either the cursor isn’t aligned for T, or the available space isn’t a multiple of size_of::<T>().

Source

pub exec fn fill<T: Pod>(&mut self, value: T) -> r : usize

with
Tracked(writer_owner): Tracked<&mut VmIoOwner>,
->
reader_owner: Tracked<VmIoOwner>,
requires
old(self).inv(),
old(self).wf(*old(writer_owner)),
old(writer_owner).has_write_view(),
core::mem::size_of::<T>() > 0,
core::mem::align_of::<T>() > 0,
core::mem::size_of::<T>() % core::mem::align_of::<T>() == 0,
old(self).fill_panic_condition::<T>() ==> may_panic(),
ensures
final(self).inv(),
final(self).wf(*final(writer_owner)),
!old(self).fill_panic_condition::<T>(),
final(self).cursor == old(self).end,
final(self).end == old(self).end,
final(writer_owner).range.start == old(writer_owner).range.end,
final(writer_owner).range.end == old(writer_owner).range.end,
reader_owner@.inv(),
reader_owner@.range.start == old(writer_owner).range.start,
reader_owner@.range.end == old(writer_owner).range.end,
reader_owner@.has_read_view(),
reader_owner@.is_kernel == old(writer_owner).is_kernel,
r as int * core::mem::size_of::<T>() == old(self).avail_spec(),

Fills the available space by repeatedly writing the same Pod value.

Returns the number of elements written.

§Panics

If cursor isn’t aligned for T, or avail() isn’t a multiple of size_of::<T>() (Self::fill_panic_condition).

Source

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

with
Tracked(owner_w): Tracked<&mut VmIoOwner>,
Tracked(owner_r): Tracked<&mut VmIoOwner>,
requires
old(self).inv(),
old(reader).inv(),
old(self).wf(*old(owner_w)),
old(reader).wf(*old(owner_r)),
old(owner_w).has_write_view(),
old(owner_r).read_view_initialized(),
ensures
final(self).inv(),
final(reader).inv(),
final(owner_w).inv(),
final(owner_r).inv(),
final(self).wf(*final(owner_w)),
final(reader).wf(*final(owner_r)),
r == vstd::math::min(old(self).avail_spec() as int, old(reader).remain_spec() as int),
final(self).avail_spec() == old(self).avail_spec() - r as usize,
final(self).cursor.vaddr == old(self).cursor.vaddr + r as usize,
final(reader).remain_spec() == old(reader).remain_spec() - r as usize,
final(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_once<T: PodOnce>(&mut self, new_val: &T) -> r : Result<(), Error>

with
Tracked(owner): Tracked<&mut VmIoOwner>,
requires
old(self).inv(),
old(self).wf(*old(owner)),
old(owner).has_write_view(),
old(self).cursor.vaddr % core::mem::align_of::<T>() != 0 ==> may_panic(),
ensures
final(self).inv(),
final(owner).inv(),
final(self).wf(*final(owner)),
match r {
    Ok(_) => (
        &&& old(self).cursor.vaddr % core::mem::align_of::<T>() == 0
        &&& final(self).avail_spec()
            == old(self).avail_spec() - core::mem::size_of::<T>()
        &&& final(self).cursor.vaddr
            == old(self).cursor.vaddr + core::mem::size_of::<T>()

    ),
    Err(_) => *old(self) == *final(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.

§Panics

This method will panic if the current position of the writer does not meet the alignment requirements of type T.

§Verified Properties
§Preconditions
  • The writer and its owner must satisfy their invariants.
  • The owner must match this writer and carry a write memory view.
  • Every byte in the writable range must translate in the write view.
§Postconditions
  • The writer and owner still satisfy their invariants.
  • On success, the cursor advances by size_of::<T>() and the cursor was aligned to align_of::<T>() (the runtime assert! would otherwise diverge).
  • On error, the writer state is unchanged.
Source§

impl<'a, Fallibility> VmWriter<'a, Fallibility>

Source

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

{ (self.end.vaddr - self.cursor.vaddr) as usize }
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 cursor(&self) -> VirtPtr

Returns the cursor pointer, which refers to the address of the next byte to write.

Source

pub exec fn has_avail(&self) -> bool

requires
self.inv(),

Returns if it has available space to write.

Source

pub exec fn limit(&mut self, max_avail: usize) -> r : &mut Self

requires
old(self).inv(),
ensures
r.inv(),
r.avail_spec() <= max_avail,
r.avail_spec() <= old(self).avail_spec(),
r.cursor == old(self).cursor,
r.ghost_id == old(self).ghost_id,

Limits the length of available space.

This method ensures the post-condition self.avail() <= max_avail.

Source

pub exec fn skip(&mut self, nbytes: usize) -> r : &mut Self

requires
old(self).inv(),
nbytes <= old(self).avail_spec(),
ensures
r.inv(),
r.cursor.vaddr == old(self).cursor.vaddr + nbytes,
r.avail_spec() == old(self).avail_spec() - nbytes,
r.end == old(self).end,
r.ghost_id == old(self).ghost_id,

Skips the first nbytes of available space.

The length of available space is decreased accordingly.

§Panics

If nbytes is greater than self.avail(), then the method panics.

Source§

impl<'a> VmWriter<'a, Fallible>

Source

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

with
Ghost(id): Ghost<nat>,
->
owner: Tracked<VmIoOwner>,
ensures
r.inv_wf(),
owner@.id == id,
owner@.range == ptr.range@,
owner@.mem_view is None,
!owner@.is_kernel,
r.cursor == ptr,
r.end == ptr.wrapping_add_spec(len),
r.end.range@ == ptr.range@,
ptr.inv() && ptr.range@.start == ptr.vaddr && len == ptr.range@.end - ptr.range@.start
    ==> {
        &&& r.inv()
        &&& owner@.inv()
        &&& r.wf(owner@)

    },

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

§Verified Properties
§Preconditions
§Postconditions
  • The returned VmWriter satisfies its invariant.
  • The returned writer is associated with a VmIoOwner that satisfies both VmIoOwner::inv and VmWriter::wf.
  • The owner has the same range as ptr, has no memory view yet, and is marked as user-space.
Source

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

requires
old(self).inv(),
ensures
final(self).inv(),
final(self).end == old(self).end,
final(self).ghost_id == old(self).ghost_id,
final(self).cursor.range == old(self).cursor.range,
r is Err ==> *final(self) == *old(self),

Writes a value of Pod type to user space.

If the underlying memory access faults during the write, the cursor is rolled back to its starting position before returning Err.

§Verified Properties
§Postconditions
  • On success, the cursor advances by size_of::<T>().
  • On error, the cursor is at its original position (writer state preserved).
Source

pub exec fn fill_zeros(&mut self, len: usize) -> r : Result<usize, (Error, usize)>

requires
old(self).inv(),
ensures
final(self).inv(),
final(self).end == old(self).end,
final(self).ghost_id == old(self).ghost_id,
final(self).cursor.range == old(self).cursor.range,
final(self).cursor.vaddr >= old(self).cursor.vaddr,
final(self).cursor.vaddr <= old(self).end.vaddr,
match r {
    Ok(n) => (
        &&& n <= len
        &&& n <= old(self).avail_spec()
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n

    ),
    Err((_, n)) => (
        &&& n <= len
        &&& n <= old(self).avail_spec()
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n

    ),
},

Writes len zeros to the target memory.

This method attempts to fill up to len bytes with zeros. If the available memory from the current cursor position is less than len, it will only fill the available space.

If the memory write failed due to an unresolvable page fault, this method will return Err with the length set so far.

Source§

impl<'a> VmWriter<'a, Infallible>

Source

pub exec fn from(slice: &'a mut [u8]) -> r : Self

with
->
owner: Tracked<VmIoOwner>,
ensures
r.inv(),
owner@.inv(),
r.wf(*owner),
owner@.has_write_view(),
r.cursor.range == owner@.range,
owner@.range.end - owner@.range.start == old(slice).len(),

Constructs a VmWriter<'a, Infallible> from a mutable byte slice.

The slice’s address establishes the writer’s cursor range; the kernel-space trust (axiom_slice_in_kernel + axiom_kernel_mem_view via Self::from_kernel_space) supplies the tracked VmIoOwner with its WriteView. Callers receive the owner via proof_with!.

§Safety

The slice’s memory must be valid for writes during 'a — guaranteed by Rust’s borrow checker for &'a mut [u8].

Source§

impl<Fallibility> VmWriter<'_, Fallibility>

Source

pub open spec fn inv_wf(self) -> bool

{
    &&& self.cursor.range@ == self.end.range@

}

Structural well-formedness: cursor and end share the same ghost range.

Source

pub open spec fn wf(self, owner: VmIoOwner) -> bool

{
    &&& owner.inv()
    &&& owner.range.start == self.cursor.vaddr
    &&& owner.range.end == self.end.vaddr
    &&& owner.id == self.ghost_id@
    &&& owner
        .mem_view matches Some(
        VmIoMemView::WriteView(mv),
    ) ==> {
        forall |va: usize| {
            owner.range.start <= va < owner.range.end
                ==> {
                    &&& #[trigger] mv.addr_transl(va) is Some

                }
        }
    }

}

Relates a concrete writer to its ghost owner.

Trait Implementations§

Source§

impl<'a> FallibleVmWrite<Fallible> for VmWriter<'a, Fallible>

Source§

exec fn write_fallible( &mut self, reader: &mut VmReader<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires
old(self).inv(),
old(reader).inv(),
ensures
final(self).end == old(self).end,
final(self).ghost_id == old(self).ghost_id,
final(self).cursor.range == old(self).cursor.range,
final(reader).end == old(reader).end,
final(reader).ghost_id == old(reader).ghost_id,
final(reader).cursor.range == old(reader).cursor.range,
final(self).inv(),
final(reader).inv(),
match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + n
        &&& n <= old(self).avail_spec()
        &&& n <= old(reader).remain_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + copied_len
        &&& copied_len <= old(self).avail_spec()
        &&& copied_len <= old(reader).remain_spec()

    ),
},
Source§

impl<'a> FallibleVmWrite<Fallible> for VmWriter<'a, Infallible>

Source§

exec fn write_fallible( &mut self, reader: &mut VmReader<'_, Fallible>, ) -> r : Result<usize, (Error, usize)>

requires
old(self).inv(),
old(reader).inv(),
ensures
final(self).end == old(self).end,
final(self).ghost_id == old(self).ghost_id,
final(self).cursor.range == old(self).cursor.range,
final(reader).end == old(reader).end,
final(reader).ghost_id == old(reader).ghost_id,
final(reader).cursor.range == old(reader).cursor.range,
final(self).inv(),
final(reader).inv(),
match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + n
        &&& n <= old(self).avail_spec()
        &&& n <= old(reader).remain_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + copied_len
        &&& copied_len <= old(self).avail_spec()
        &&& copied_len <= old(reader).remain_spec()

    ),
},
Source§

impl<'a> FallibleVmWrite<Infallible> for VmWriter<'a, Fallible>

Source§

exec fn write_fallible( &mut self, reader: &mut VmReader<'_, Infallible>, ) -> r : Result<usize, (Error, usize)>

requires
old(self).inv(),
old(reader).inv(),
ensures
final(self).end == old(self).end,
final(self).ghost_id == old(self).ghost_id,
final(self).cursor.range == old(self).cursor.range,
final(reader).end == old(reader).end,
final(reader).ghost_id == old(reader).ghost_id,
final(reader).cursor.range == old(reader).cursor.range,
final(self).inv(),
final(reader).inv(),
match r {
    Ok(n) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + n
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + n
        &&& n <= old(self).avail_spec()
        &&& n <= old(reader).remain_spec()

    ),
    Err((_, copied_len)) => (
        &&& final(self).cursor.vaddr == old(self).cursor.vaddr + copied_len
        &&& final(reader).cursor.vaddr == old(reader).cursor.vaddr + copied_len
        &&& copied_len <= old(self).avail_spec()
        &&& copied_len <= old(reader).remain_spec()

    ),
},
Source§

impl<Fallibility> Inv for VmWriter<'_, Fallibility>

Source§

open spec fn inv(self) -> bool

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

}

Auto Trait Implementations§

§

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

§

impl<'a, Fallibility> RefUnwindSafe for VmWriter<'a, Fallibility>
where Fallibility: RefUnwindSafe,

§

impl<'a, Fallibility> Send for VmWriter<'a, Fallibility>
where Fallibility: Send,

§

impl<'a, Fallibility> Sync for VmWriter<'a, Fallibility>
where Fallibility: Sync,

§

impl<'a, Fallibility> Unpin for VmWriter<'a, Fallibility>
where Fallibility: Unpin,

§

impl<'a, Fallibility> UnsafeUnpin for VmWriter<'a, Fallibility>

§

impl<'a, Fallibility> UnwindSafe for VmWriter<'a, Fallibility>
where Fallibility: UnwindSafe,

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>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A