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>
impl<'a> VmReader<'a>
Sourcepub unsafe exec fn from_user_space(ptr: VirtPtr) -> r : Self
pub unsafe exec fn from_user_space(ptr: VirtPtr) -> r : Self
Ghost(id): Ghost <nat>,
->
owner: Tracked <VmIoOwner <'a>>,ptr.inv(),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.
Sourcepub unsafe exec fn from_kernel_space(ptr: VirtPtr, len: usize) -> r : Self
pub unsafe exec fn from_kernel_space(ptr: VirtPtr, len: usize) -> r : Self
Ghost(id): Ghost <nat>,
->
owner: Tracked <VmIoOwner <'a>>,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(),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.
§Safety
ptr must be valid for reads of len bytes during the entire lifetime a.
Sourcepub exec fn from_pod<T: Pod>(val: &mut T) -> r : Result<VmReader<'a>, Error>
pub exec fn from_pod<T: Pod>(val: &mut T) -> r : Result<VmReader<'a>, Error>
Ghost(id): Ghost <nat>,
->
owner: Tracked <Result <VmIoOwner <'a>>>,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)
}
},Source§impl VmReader<'_>
impl VmReader<'_>
Sourcepub open spec fn remain_spec(&self) -> usize
pub open spec fn remain_spec(&self) -> usize
{ (self.end.vaddr - self.cursor.vaddr) as usize }Sourcepub exec fn remain(&self) -> r : usize
pub exec fn remain(&self) -> r : usize
self.inv(),r == self.remain_spec(),Returns the number of remaining bytes that can be read.
Sourcepub exec fn advance(&mut self, len: usize)
pub exec fn advance(&mut self, len: usize)
old(self).inv(),len <= old(self).remain_spec(),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. Requires that there are at least len bytes remaining.
Sourcepub exec fn read(&mut self, writer: &mut VmWriter<'_>) -> r : usize
pub exec fn read(&mut self, writer: &mut VmWriter<'_>) -> r : usize
Tracked(owner_r): Tracked <& mut VmIoOwner <'_>>,
Tracked(owner_w): Tracked <& mut VmIoOwner <'_>>,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_r).mem_view is Some,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,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 all data into the writer until one of the two conditions is met:
- The reader has no remaining data.
- The writer has no available space.
Returns the number of bytes read.
Sourcepub exec fn read_val<T: Pod>(&mut self) -> r : Result<T, Error>
pub exec fn read_val<T: Pod>(&mut self) -> r : Result<T, Error>
Ghost(id): Ghost <nat>,
Tracked(owner): Tracked <& mut VmIoOwner <'_>>,old(self).inv(),old(owner).inv(),old(owner).inv_with_reader(*old(self)),old(owner).mem_view is Some,self.inv(),owner.inv(),owner.inv_with_reader(*self),owner.params_eq(*old(owner)),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.
Sourcepub exec fn read_val_once<T: PodOnce>(&mut self) -> r : Result<T, Error>
pub exec fn read_val_once<T: PodOnce>(&mut self) -> r : Result<T, Error>
Tracked(owner): Tracked <& mut VmIoOwner <'_>>,old(self).inv(),old(owner).mem_view is Some,old(owner).inv(),old(owner).inv_with_reader(*old(self)),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.
Trait Implementations§
Source§impl<'a> TryFromSpecImpl<&'a [u8]> for VmReader<'a>
impl<'a> TryFromSpecImpl<&'a [u8]> for VmReader<'a>
Source§open spec fn obeys_try_from_spec() -> bool
open spec fn obeys_try_from_spec() -> bool
{ true }Source§open spec fn try_from_spec(slice: &'a [u8]) -> Result<Self, Error>
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,
})
}
}