VmReader

ostd::mm::io

Struct VmReader 

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

VmReader is a reader for reading data from a contiguous range of memory.

The memory range read by VmReader 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 reads are infallible. When the operating range is in user space, it is ensured that the page table of the process creating the VmReader is active for the duration of 'a, and the corresponding memory reads are considered fallible.

When perform reading with a VmWriter, if one of them represents typed memory, it can ensure that the reading range in this reader and writing range in the writer 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> VmReader<'a>

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_reader(r),
owner@.range == ptr.range@,
owner@.mem_view is None,
!owner@.is_kernel,
!owner@.is_fallible,

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

⚠️ WARNING: Currently not implemented yet.

§Verified Properties
§Preconditions
§Postconditions
Source

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

with
Ghost(id): Ghost<nat>,
->
owner: Tracked<VmIoOwner<'a>>,
requires
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_reader(r),
r.cursor.vaddr == ptr.vaddr,
r.end.vaddr == ptr.vaddr + len,
r.cursor == ptr,
r.end.range@ == ptr.range@,
owner@.is_kernel,
owner@.id == id,

Constructs a VmReader 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 reads 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 VmReader will be created with the range ptr.vaddr..ptr.vaddr + len.
  • The created VmReader will have a unique identifier id, and its cursor will be initialized to ptr.
  • The created VmReader will be associated with a VmIoOwner that has the same id, the same memory range, and is marked as kernel space and infallible.
§Safety

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

Source

pub exec fn from_pod<T: Pod>(val: &mut T) -> r : Result<VmReader<'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.remain_spec() == core::mem::size_of::<T>()
        &&& owner.inv()
        &&& owner.inv_with_reader(r)

    }

},

Converts a PoD value into a VmReader that reads from the memory occupied by the PoD value.

§Verified Properties
§Preconditions

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

§Postconditions
  • If the memory region occupied by val is valid for reads, then an infallible VmReader will be created that points to the memory region of val.
  • If the memory region occupied by val is not valid for reads, then an IoError will be returned.
Source§

impl VmReader<'_>

Source

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

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

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

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

Returns the number of remaining bytes that can be read.

§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).remain_spec(),
ensures
self.inv(),
self.cursor.vaddr == old(self).cursor.vaddr + len,
self.remain_spec() == old(self).remain_spec() - len,
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 readable bytes.
§Postconditions
  • self still satisfies its invariant.
  • The cursor advances by len.
  • The remaining readable bytes decrease by len.
  • The reader identity and end cursor are preserved.
Source

pub exec fn read(&mut self, writer: &mut VmWriter<'_>) -> r : usize

with
Tracked(owner_r): Tracked<&mut VmIoOwner<'_>>,
Tracked(owner_w): Tracked<&mut VmIoOwner<'_>>,
requires
old(self).inv(),
old(writer).inv(),
old(owner_r).inv(),
old(owner_w).inv(),
old(owner_r).inv_with_reader(*old(self)),
old(owner_w).inv_with_writer(*old(writer)),
old(owner_w).mem_view matches Some(VmIoMemView::WriteView(_)),
old(writer).cursor.range@.start >= old(self).cursor.range@.end
    || old(self).cursor.range@.start >= old(writer).cursor.range@.end,
old(owner_r)
    .mem_view matches Some(
    VmIoMemView::ReadView(mem_src),
) && forall |i: usize| {
    old(self).cursor.vaddr <= i < old(self).cursor.vaddr + old(self).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(),
writer.inv(),
owner_r.inv(),
owner_w.inv(),
owner_r.inv_with_reader(*self),
owner_w.inv_with_writer(*writer),
r == vstd::math::min(old(self).remain_spec() as int, old(writer).avail_spec() as int),
self.remain_spec() == old(self).remain_spec() - r as usize,
self.cursor.vaddr == old(self).cursor.vaddr + r as usize,
writer.avail_spec() == old(writer).avail_spec() - r as usize,
writer.cursor.vaddr == old(writer).cursor.vaddr + r as usize,

Reads data from self and writes it into the provided writer.

This function acts as the source side of a transfer. It copies data from the current instance (self) into the destination writer, up to the limit of available data in self or available space in writer (whichever is smaller).

§Logic
  1. Calculates the copy length: min(self.remaining_data, writer.available_space).
  2. Copies bytes from self’s internal buffer to writer’s buffer.
  3. Advances the cursors of both self and writer.
§Arguments
  • writer - The destination VmWriter where the data will be copied to.
§Returns

The number of bytes actually transferred.

§Verified Properties
§Preconditions
  • The reader, writer, and both associated owners must satisfy their invariants.
  • The owners must match the given reader and writer.
  • 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 reader, writer, and both owners still satisfy their invariants.
  • The owners still match the updated reader and writer.
  • The returned byte count equals the minimum of readable bytes and writable bytes.
  • Both cursors advance by exactly the returned byte count.
Source

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

with
Tracked(owner): Tracked<&mut VmIoOwner<'_>>,
requires
old(self).inv(),
old(owner).inv(),
old(owner).inv_with_reader(*old(self)),
old(owner).mem_view matches Some(VmIoMemView::ReadView(_)),
old(owner)
    .mem_view matches Some(
    VmIoMemView::ReadView(mem_src),
) ==> {
    forall |i: usize| {
        old(self).cursor.vaddr <= i < old(self).cursor.vaddr + old(self).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(),
owner.inv(),
owner.inv_with_reader(*self),
match r {
    Ok(_) => (
        &&& self.remain_spec() == old(self).remain_spec() - core::mem::size_of::<T>()
        &&& self.cursor.vaddr == old(self).cursor.vaddr + core::mem::size_of::<T>()

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

Reads a value of Pod type.

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

§Verified Properties
§Preconditions
  • The reader and its owner must satisfy their invariants.
  • The owner must match this reader and carry a read memory view.
  • The readable range must translate to initialized bytes in the read view.
§Postconditions
  • The reader and owner still satisfy their invariants.
  • On success, the cursor advances by size_of::<T>().
  • On error, the reader state is unchanged.
Source

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

with
Tracked(owner): Tracked<&mut VmIoOwner<'_>>,
requires
old(self).inv(),
old(owner).inv(),
old(owner).inv_with_reader(*old(self)),
old(owner).mem_view matches Some(VmIoMemView::ReadView(_)),
old(self).cursor.vaddr % core::mem::align_of::<T>() == 0,
old(owner)
    .mem_view matches Some(
    VmIoMemView::ReadView(mem_src),
) ==> {
    forall |i: usize| {
        old(self).cursor.vaddr <= i < old(self).cursor.vaddr + core::mem::size_of::<T>()
            ==> {
                &&& 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(),
owner.inv(),
owner.inv_with_reader(*self),
match r {
    Ok(_) => (
        &&& self.remain_spec() == old(self).remain_spec() - core::mem::size_of::<T>()
        &&& self.cursor.vaddr == old(self).cursor.vaddr + core::mem::size_of::<T>()

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

Reads a value of the PodOnce type using one non-tearing memory load.

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

This method will not compile if the Pod type is too large for the current architecture and the operation must be tear into multiple memory loads.

§Panics

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

§Verified Properties
§Preconditions
  • The reader and its owner must satisfy their invariants.
  • The owner must match this reader and carry a read memory view.
  • The readable range must translate to initialized bytes in the read view.
  • The current cursor must satisfy the alignment requirements of T.
§Postconditions
  • The reader and owner still satisfy their invariants.
  • On success, the cursor advances by size_of::<T>().
  • On error, the reader state is unchanged.

Trait Implementations§

Source§

impl Clone for VmReader<'_>

Source§

exec fn clone(&self) -> Self

Clone can be implemented for VmReader because it either points to untyped memory or represents immutable references.

Note that we cannot implement Clone for VmWriter because it can represent mutable references, which must remain exclusive.

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl Inv for VmReader<'_>

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 VmReader<'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 VmReader<'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 VmReader<'a>

§

impl<'a> RefUnwindSafe for VmReader<'a>

§

impl<'a> Send for VmReader<'a>

§

impl<'a> Sync for VmReader<'a>

§

impl<'a> Unpin for VmReader<'a>

§

impl<'a> UnwindSafe for VmReader<'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> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. 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> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
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>