ostd::mm::frame::linked_list

Struct CursorMut

pub struct CursorMut<M: AnyFrameMeta + Repr<MetaSlotSmall>> {
    pub list: PPtr<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: PPtr<LinkedList<M>>§current: Option<ReprPtr<MetaSlot, MetadataAsLink<M>>>

Implementations§

Source §

impl<M: AnyFrameMeta + Repr<MetaSlotSmall>> CursorMut<M>

Source

pub exec fn move_next(&mut self)

with

Tracked(owner): Tracked<CursorOwner<M>>,

requires

owner.inv(),

old(self).wf(owner),

ensures

self.model(owner.move_next_owner_spec()) == old(self).model(owner).move_next_spec(),

owner.move_next_owner_spec().inv(),

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

self.model(owner.move_prev_owner_spec()) == old(self).model(owner).move_prev_spec(),

owner.move_prev_owner_spec().inv(),

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 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(),

res.is_some()
    ==> res.unwrap().0.model(res.unwrap().1@).meta
        == old(owner).list_own.list[old(owner).index]@,

res.is_some() ==> self.model(*owner) == old(self).model(*old(owner)).remove(),

res.is_some() ==> res.unwrap().1@.frame_link_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

self.model(*owner) == old(self).model(*old(owner)).insert(frame_own.meta_own@),

self.wf(*owner),

owner.inv(),

owner.list_own.list
    == old(owner).list_own.list.insert(old(owner).index, frame_own.meta_own),

owner.list_own.list_id == old(owner).list_own.list_id,

frame_own.meta_own.paddr == old(frame_own).meta_own.paddr,

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) -> PPtr<LinkedList<M>>

Provides a reference to the linked list.

Trait Implementations§

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()
    &&& owner.list_perm.pptr() == self.list
    &&& owner.list_perm.is_init()
    &&& owner.list_perm.mem_contents().value().wf(owner.list_own)

}

Source §