Trait EvalContextExt 

pub(super) trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
    // Provided methods
    fn buffered_atomic_rmw(
        &mut self,
        new_val: Scalar,
        place: &MPlaceTy<'tcx>,
        atomic: AtomicRwOrd,
        init: Scalar,
    ) -> InterpResult<'tcx> { ... }
    fn buffered_atomic_read(
        &self,
        place: &MPlaceTy<'tcx>,
        atomic: AtomicReadOrd,
        latest_in_mo: Scalar,
        validate: impl FnOnce(Option<&VClock>) -> InterpResult<'tcx>,
    ) -> InterpResult<'tcx, Option<Scalar>> { ... }
    fn buffered_atomic_write(
        &mut self,
        val: Scalar,
        dest: &MPlaceTy<'tcx>,
        atomic: AtomicWriteOrd,
        init: Option<Scalar>,
    ) -> InterpResult<'tcx> { ... }
    fn perform_read_on_buffered_latest(
        &self,
        place: &MPlaceTy<'tcx>,
        atomic: AtomicReadOrd,
    ) -> InterpResult<'tcx> { ... }
}

Provided Methods

fn buffered_atomic_rmw( &mut self, new_val: Scalar, place: &MPlaceTy<'tcx>, atomic: AtomicRwOrd, init: Scalar, ) -> InterpResult<'tcx>

Update the store buffer after an RMW. Does nothing if we are currently not detecting races (e.g. single-threaded mode).

fn buffered_atomic_read( &self, place: &MPlaceTy<'tcx>, atomic: AtomicReadOrd, latest_in_mo: Scalar, validate: impl FnOnce(Option<&VClock>) -> InterpResult<'tcx>, ) -> InterpResult<'tcx, Option<Scalar>>

Perform a store buffer load. Returning None indicates a read of uninitialized memory. Does nothing if we are currently not detecting races (e.g. single-threaded mode).

latest_in_mo must be the most recent value according to the mo relation. The argument to validate is the synchronization clock of the memory that is being read, if we are reading from a store buffer element.

fn buffered_atomic_write( &mut self, val: Scalar, dest: &MPlaceTy<'tcx>, atomic: AtomicWriteOrd, init: Option<Scalar>, ) -> InterpResult<'tcx>

Add the given write to the store buffer. (Does not change machine memory.) Must only be called after we determined that there is no data race or mixed-size race. Does nothing if we are currently not detecting races (e.g. single-threaded mode).

init says with which value to initialize the store buffer in case there wasn’t a store buffer for this memory range before. None means the memory does not contain a valid scalar.

Must be called after validate_atomic_store to ensure that sync_clock is up-to-date.

fn perform_read_on_buffered_latest( &self, place: &MPlaceTy<'tcx>, atomic: AtomicReadOrd, ) -> InterpResult<'tcx>

Caller should never need to consult the store buffer for the latest value. This function is used exclusively for failed atomic_compare_exchange_scalar to perform load_impl on the latest store element

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<'tcx> EvalContextExt<'tcx> for MiriInterpCx<'tcx>