Skip to main content

CursorMut

ostd::mm::frame::linked_list

Struct CursorMut 

Source 
pub struct CursorMut<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: &'a mut LinkedList<M>,
    pub current: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>,
}
Expand description

A cursor that can mutate the linked list links.

The cursor points to either a frame or the “ghost” non-element. It points to the “ghost” non-element when the cursor surpasses the back of the list.

Fields§

§list: &'a mut LinkedList<M>§current: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>

Implementations§

Source§

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<'a, M>

Source

pub exec fn move_next(&mut self)

with
Tracked(owner): Tracked<CursorOwner<M>>,
requires
owner.inv(),
old(self).wf(owner),
ensures
final(self).model(owner.move_next_owner_spec())
    == old(self).model(owner).move_next_spec(),
owner.move_next_owner_spec().inv(),
final(self).wf(owner.move_next_owner_spec()),

Moves the cursor to the next frame towards the back.

If the cursor is pointing to the “ghost” non-element then this will move it to the first element of the LinkedList. If it is pointing to the last element of the LinkedList then this will move it to the “ghost” non-element.

Source

pub exec fn move_prev(&mut self)

with
Tracked(owner): Tracked<CursorOwner<M>>,
requires
owner.inv(),
old(self).wf(owner),
ensures
final(self).model(owner.move_prev_owner_spec())
    == old(self).model(owner).move_prev_spec(),
owner.move_prev_owner_spec().inv(),
final(self).wf(owner.move_prev_owner_spec()),

Moves the cursor to the previous frame towards the front.

If the cursor is pointing to the “ghost” non-element then this will move it to the last element of the LinkedList. If it is pointing to the first element of the LinkedList then this will move it to the “ghost” non-element.

Source

pub exec fn current_meta(&mut self) -> res : Option<&mut M>

with
Tracked(owner): Tracked<&mut CursorOwner<M>>,
requires
old(self).wf(*old(owner)),
old(owner).inv(),
ensures
final(self).wf(*final(owner)),
final(owner).inv(),
*final(owner) == *old(owner),
*final(self) == *old(self),
res.is_some() == (0 <= final(owner).index < final(owner).length()),

Gets the mutable reference to the current frame’s metadata.

§Verified Properties
§Preconditions

The cursor must be well-formed with respect to the tracked CursorOwner.

§Postconditions

If the cursor is on an element, returns Some(&mut meta) borrowing the current link’s metadata. The cursor state and owner are otherwise unchanged.

§Safety

The &mut self guarantees exclusive access to the cursor; the tracked CursorOwner guarantees the perm for the current link is live. Together they justify the mutable borrow of link.meta. The body is external_body because the map-indexed perm extraction needed to call ReprPtr::borrow_mut runs into a Verus modelling gap — see vstd_extra::map_extra::tracked_borrow_mut_points_to. The ownership invariants in the requires/ensures are what we rely on.

Source

pub exec fn take_current( &mut self, ) -> res : Option<(UniqueFrame<Link<M>>, Tracked<UniqueFrameOwner<Link<M>>>)>

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut CursorOwner<M>>,
requires
old(self).wf(*old(owner)),
old(owner).inv(),
old(regions).inv(),
old(owner).length() > 0
    ==> old(regions)
        .slot_owners
        .contains_key(frame_to_index(old(self).current.unwrap().addr())),
ensures
old(owner).length() == 0 ==> res.is_none(),
old(self).current.is_some() ==> res.is_some(),
res.is_some()
    ==> res.unwrap().0.model(res.unwrap().1@).meta
        == old(owner).list_own.list[old(owner).index]@,
res.is_some()
    ==> final(self).model(*final(owner)) == old(self).model(*old(owner)).remove(),
res.is_some() ==> res.unwrap().1@.frame_link_inv(),
res.is_some() ==> final(owner).inv(),
res.is_some() ==> final(self).wf(*final(owner)),
res.is_none() ==> (*final(owner) =~= *old(owner)),
final(regions).inv(),
res.is_some() ==> final(owner).index == old(owner).index,
res.is_some()
    ==> final(owner).list_own.list == old(owner).list_own.list.remove(old(owner).index),
res.is_some()
    ==> {
        let paddr = old(self).current.unwrap().addr();
        let idx = frame_to_index(meta_to_frame(paddr));
        &&& final(regions).slot_owners[idx].raw_count
            == old(regions).slot_owners[idx].raw_count - 1
        &&& final(regions).slots =~= old(regions).slots

    },
res.is_some()
    ==> forall |idx: usize| {
        idx != frame_to_index(meta_to_frame(old(self).current.unwrap().addr()))
            ==> final(regions).slot_owners[idx] == old(regions).slot_owners[idx]
    },
res.is_none() ==> (*final(regions) =~= *old(regions)),
res.is_some() ==> res.unwrap().0.wf(res.unwrap().1@),
res.is_some() ==> res.unwrap().1@.inv(),

Takes the current pointing frame out of the linked list.

If successful, the frame is returned and the cursor is moved to the next frame. If the cursor is pointing to the back of the list then it is moved to the “ghost” non-element.

§Verified Properties
§Preconditions

The cursor must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects. The list must be non-empty, so that the current frame is valid.

§Postconditions

The current frame is removed from the list, and the cursor is moved to the next frame. The list invariants are preserved.

§Safety

This function calls from_raw on the frame, but we guarantee that the frame is forgotten if it is in the list. So, double-free will not occur. All loads and stores are through track tracked permissions, so there are no illegal memory accesses. No data races are possible.

Source

pub exec fn insert_before(&mut self, frame: UniqueFrame<Link<M>>)

with
Tracked(regions): Tracked<&mut MetaRegionOwners>,
Tracked(owner): Tracked<&mut CursorOwner<M>>,
Tracked(frame_own): Tracked<&mut UniqueFrameOwner<Link<M>>>,
requires
old(self).wf(*old(owner)),
old(owner).inv(),
old(owner).list_own.list_id != 0,
old(frame_own).inv(),
old(frame_own).global_inv(*old(regions)),
frame.wf(*old(frame_own)),
old(owner).length() < usize::MAX,
old(regions).inv(),
old(regions).slots.contains_key(old(frame_own).slot_index),
old(regions)
    .slot_owners[old(frame_own).slot_index]
    .inner_perms
    .in_list
    .is_for(old(regions).slots[old(frame_own).slot_index].value().in_list),
old(frame_own).meta_perm.addr() == frame.ptr.addr(),
old(frame_own).frame_link_inv(),
ensures
final(self).model(*final(owner))
    == old(self).model(*old(owner)).insert(final(frame_own).meta_own@),
final(self).wf(*final(owner)),
final(owner).inv(),
final(owner).list_own.list
    == old(owner).list_own.list.insert(old(owner).index, final(frame_own).meta_own),
final(owner).list_own.list_id == old(owner).list_own.list_id,
final(frame_own).meta_own.paddr == old(frame_own).meta_own.paddr,
final(frame_own).meta_own.in_list == old(owner).list_own.list_id,

Inserts a frame before the current frame.

If the cursor is pointing at the “ghost” non-element then the new element is inserted at the back of the LinkedList.

§Verified Properties
§Preconditions

The cursor must be well-formed, with the pointers to its links’ metadata slots matching the tracked permission objects.

  • The new frame must be active, so that it is valid to call into_raw on it.
§Postconditions
  • The new frame is inserted into the list, immediately before the current index.
  • The list invariants are preserved.
§Safety
  • This function calls into_raw on the frame, so the caller must ensure that the frame is active and has not been forgotten already to avoid a memory leak. If the caller attempts to insert a forgotten frame, the invariant around into_raw and from_raw will be violated. But, it is the safe failure case in that it will not cause a double-free. (Note: we should be able to move this requirement into the UniqueFrame invariants.)
Source

pub exec fn as_list(&self) -> &LinkedList<M>

Provides a reference to the linked list.

Trait Implementations§

Source§

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> ModelOf for CursorMut<'a, M>

§

fn model(self, owner: Self::Owner) -> <Self::Owner as View>::V

Source§

impl<'a, M: AnyFrameMeta + Repr<MetaSlotSmall>> OwnerOf for CursorMut<'a, M>

Source§

open spec fn wf(self, owner: Self::Owner) -> bool

{
    &&& 0 <= owner.index < owner.length()
        ==> self.current.is_some()
            && self.current.unwrap().addr() == owner.list_own.list[owner.index].paddr
            && owner.list_own.perms[owner.index].pptr().addr()
                == self.current.unwrap().addr()
            && self.current.unwrap().ptr
                == owner.list_own.perms[owner.index].points_to.pptr()
    &&& owner.index == owner.list_own.list.len() ==> self.current.is_none()
    &&& (*self.list).wf(owner.list_own)

}
Source§

type Owner = CursorOwner<M>

The owner of the concrete type. The Owner must implement Inv, indicating that it must has a consistent state.

Auto Trait Implementations§

§

impl<'a, M> Freeze for CursorMut<'a, M>

§

impl<'a, M> !RefUnwindSafe for CursorMut<'a, M>

§

impl<'a, M> Send for CursorMut<'a, M>
where M: Send,

§

impl<'a, M> Sync for CursorMut<'a, M>
where M: Sync,

§

impl<'a, M> Unpin for CursorMut<'a, M>
where M: Unpin,

§

impl<'a, M> UnsafeUnpin for CursorMut<'a, M>

§

impl<'a, M> !UnwindSafe for CursorMut<'a, M>

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>