miri::concurrency::sync

Trait EvalContextExtPriv

source
pub(super) trait EvalContextExtPriv<'tcx>: MiriInterpCxExt<'tcx> {
    // Provided methods
    fn get_or_create_id<Id: SyncId + Idx, T>(
        &mut self,
        lock: &MPlaceTy<'tcx>,
        offset: u64,
        get_objs: impl for<'a> Fn(&'a mut MiriInterpCx<'tcx>) -> &'a mut IndexVec<Id, T>,
        create_obj: impl for<'a> FnOnce(&'a mut MiriInterpCx<'tcx>) -> InterpResult<'tcx, T>,
    ) -> InterpResult<'tcx, Option<Id>> { ... }
    fn create_id<Id: SyncId + Idx, T>(
        &mut self,
        lock: &MPlaceTy<'tcx>,
        offset: u64,
        get_objs: impl for<'a> Fn(&'a mut MiriInterpCx<'tcx>) -> &'a mut IndexVec<Id, T>,
        obj: T,
    ) -> InterpResult<'tcx, Id> { ... }
    fn condvar_reacquire_mutex(
        &mut self,
        mutex: MutexId,
        retval: Scalar,
        dest: MPlaceTy<'tcx>,
    ) -> InterpResult<'tcx> { ... }
}

Provided Methods§

source

fn get_or_create_id<Id: SyncId + Idx, T>( &mut self, lock: &MPlaceTy<'tcx>, offset: u64, get_objs: impl for<'a> Fn(&'a mut MiriInterpCx<'tcx>) -> &'a mut IndexVec<Id, T>, create_obj: impl for<'a> FnOnce(&'a mut MiriInterpCx<'tcx>) -> InterpResult<'tcx, T>, ) -> InterpResult<'tcx, Option<Id>>

Lazily initialize the ID of this Miri sync structure. If memory stores ‘0’, that indicates uninit and we generate a new instance. Returns None if memory stores a non-zero invalid ID.

get_objs must return the IndexVec that stores all the objects of this type. create_obj must create the new object if initialization is needed.

source

fn create_id<Id: SyncId + Idx, T>( &mut self, lock: &MPlaceTy<'tcx>, offset: u64, get_objs: impl for<'a> Fn(&'a mut MiriInterpCx<'tcx>) -> &'a mut IndexVec<Id, T>, obj: T, ) -> InterpResult<'tcx, Id>

Eagerly creates a Miri sync structure.

create_id will store the index of the sync_structure in the memory pointed to by lock_op, so that future calls to get_or_create_id will see it as initialized.

  • lock_op must hold a pointer to the sync structure.
  • lock_layout must be the memory layout of the sync structure.
  • offset must be the offset inside the sync structure where its miri id will be stored.
  • get_objs is described in get_or_create_id.
  • obj must be the new sync object.
source

fn condvar_reacquire_mutex( &mut self, mutex: MutexId, retval: Scalar, dest: MPlaceTy<'tcx>, ) -> InterpResult<'tcx>

Object Safety§

This trait is not object safe.

Implementors§

source§

impl<'tcx> EvalContextExtPriv<'tcx> for MiriInterpCx<'tcx>