VirtPtr

ostd::specs::mm::virt_mem_newer

Struct VirtPtr 

Source 
pub struct VirtPtr {
    pub vaddr: Vaddr,
    pub range: Ghost<Range<Vaddr>>,
}
Expand description

This module implements a model of virtual memory that can be used to reason about the behavior of code that interacts with virtual memory. It interfaces with the [vm_space] module for mapping and unmapping frames. Concrete representation of a pointer

Fields§

§vaddr: Vaddr§range: Ghost<Range<Vaddr>>

Implementations§

Source§

impl VirtPtr

Source

pub open spec fn new_spec(vaddr: Vaddr, len: usize) -> Self

{
    Self {
        vaddr,
        range: Ghost(Range {
            start: vaddr,
            end: (vaddr + len) as usize,
        }),
    }
}
Source

pub exec fn new(vaddr: Vaddr, len: usize) -> Self

Source

pub open spec fn is_defined(self) -> bool

{
    &&& self.vaddr != 0
    &&& self.range@.start <= self.vaddr <= self.range@.end

}
Source

pub open spec fn is_valid(self) -> bool

{
    &&& self.is_defined()
    &&& self.vaddr < self.range@.end

}
Source

pub exec fn read(self, Tracked(mem): Tracked<&MemView>) -> u8

requires
mem.addr_transl(self.vaddr) is Some,
mem
    .memory[mem.addr_transl(self.vaddr).unwrap().0]
    .contents[mem.addr_transl(self.vaddr).unwrap().1 as int] is Init,
self.is_valid(),
Source

pub exec fn write(self, Tracked(mem): Tracked<&mut MemView>, x: u8)

requires
old(mem).addr_transl(self.vaddr) is Some,
self.is_valid(),
ensures
*mem == old(mem).write(self.vaddr, x),
Source

pub open spec fn add_spec(self, n: usize) -> Self

{
    VirtPtr {
        vaddr: (self.vaddr + n) as usize,
        range: self.range,
    }
}
Source

pub exec fn add(&mut self, n: usize)

requires
0 <= old(self).vaddr + n < usize::MAX,
ensures
*self == old(self).add_spec(n),
Source

pub open spec fn read_offset_spec(self, mem: MemView, n: usize) -> u8

{ mem.read((self.vaddr + n) as usize).value() }
Source

pub exec fn read_offset(&self, Tracked(mem): Tracked<&MemView>, n: usize) -> u8

requires
0 < self.vaddr + n < usize::MAX,
self.range@.start <= self.vaddr + n < self.range@.end,
mem.addr_transl((self.vaddr + n) as usize) is Some,
mem
    .memory[mem.addr_transl((self.vaddr + n) as usize).unwrap().0]
    .contents[mem.addr_transl((self.vaddr + n) as usize).unwrap().1 as int] is Init,

Unlike add, we just create a temporary pointer value and read that When self.vaddr == self.range.start this acts like array index notation

Source

pub open spec fn write_offset_spec(self, mem: MemView, n: usize, x: u8) -> MemView

{ mem.write((self.vaddr + n) as usize, x) }
Source

pub exec fn write_offset( &self, verus_tmp_mem: Tracked<&mut MemView>, n: usize, x: u8, )

requires
self.inv(),
self.range@.start <= self.vaddr + n < self.range@.end,
old(mem).addr_transl((self.vaddr + n) as usize) is Some,
Source

pub open spec fn copy_offset_spec(src: Self, dst: Self, mem: MemView, n: usize) -> MemView

{
    let x = src.read_offset_spec(mem, n);
    dst.write_offset_spec(mem, n, x)
}
Source

pub exec fn copy_offset( src: &Self, dst: &Self, verus_tmp_mem: Tracked<&mut MemView>, n: usize, )

requires
src.inv(),
dst.inv(),
src.range@.start <= src.vaddr + n < src.range@.end,
dst.range@.start <= dst.vaddr + n < dst.range@.end,
old(mem).addr_transl((src.vaddr + n) as usize) is Some,
old(mem).addr_transl((dst.vaddr + n) as usize) is Some,
old(mem).memory.contains_key(old(mem).addr_transl((src.vaddr + n) as usize).unwrap().0),
old(mem)
    .memory[old(mem).addr_transl((src.vaddr + n) as usize).unwrap().0]
    .contents[old(mem).addr_transl((src.vaddr + n) as usize).unwrap().1 as int] is Init,
ensures
*mem == Self::copy_offset_spec(*src, *dst, *old(mem), n),
Source

pub open spec fn memcpy_spec(src: Self, dst: Self, mem: MemView, n: usize) -> MemView

{
    if n == 0 {
        mem
    } else {
        let mem = Self::copy_offset_spec(src, dst, mem, (n - 1) as usize);
        Self::memcpy_spec(src, dst, mem, (n - 1) as usize)
    }
}
Source

pub exec fn copy_nonoverlapping( src: &Self, dst: &Self, verus_tmp_mem: Tracked<&mut MemView>, n: usize, )

requires
src.inv(),
dst.inv(),
src.range@.start <= src.vaddr,
src.vaddr + n <= src.range@.end,
dst.range@.start <= dst.vaddr,
dst.vaddr + n < dst.range@.end,
src.range@.end <= dst.range@.start || dst.range@.end <= src.range@.start,
forall |i: usize| {
    src.vaddr <= i < src.vaddr + n
        ==> {
            &&& #[trigger] old(mem).addr_transl(i) is Some
            &&& old(mem).memory.contains_key(old(mem).addr_transl(i).unwrap().0)
            &&& old(mem)
                .memory[old(mem).addr_transl(i).unwrap().0]
                .contents[old(mem).addr_transl(i).unwrap().1 as int] is Init

        }
},
forall |i: usize| {
    dst.vaddr <= i < dst.vaddr + n
        ==> {
            &&& old(mem).addr_transl(i) is Some

        }
},
ensures
*mem == Self::memcpy_spec(*src, *dst, *old(mem), n),

Copies n bytes from src to dst in the given memory view.

The source and destination must not overlap. copy_nonoverlapping is semantically equivalent to C’s memcpy, but with the source and destination arguments swapped.

Source

pub exec fn from_vaddr(vaddr: usize, len: usize) -> r : Self

requires
vaddr != 0,
0 < len <= usize::MAX - vaddr,
ensures
r.is_valid(),
r.range@.start == vaddr,
r.range@.end == (vaddr + len) as usize,
Source

pub exec fn split(self, n: usize) -> r : (Self, Self)

requires
self.is_valid(),
0 <= n <= self.range@.end - self.range@.start,
self.vaddr == self.range@.start,
ensures
r.0.range@.start == self.range@.start,
r.0.range@.end == self.range@.start + n,
r.0.vaddr == self.range@.start,
r.1.range@.start == self.range@.start + n,
r.1.range@.end == self.range@.end,
r.1.vaddr == self.range@.start + n,

Executable helper to split the VirtPtr struct This updates the ghost ranges to match a MemView::split operation

Trait Implementations§

Source§

impl Clone for VirtPtr

Source§

exec fn clone(&self) -> res : Self

ensures
res == self,
1.0.0 · Source§

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

Performs copy-assignment from source. Read more
Source§

impl Inv for VirtPtr

Source§

open spec fn inv(self) -> bool

{
    &&& self.range@.start <= self.vaddr <= self.range@.end
    &&& self.range@.start > 0
    &&& self.range@.end >= self.range@.start

}
Source§

impl Copy for VirtPtr

Auto Trait Implementations§

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>