Trait move_bytecode_verifier::absint::TransferFunctions

pub trait TransferFunctions {
    type State: AbstractDomain;
    type AnalysisError;
    fn execute(
        &mut self, 
        pre: &mut Self::State, 
        instr: &Bytecode, 
        index: CodeOffset, 
        last_index: CodeOffset
    ) -> Result<(), Self::AnalysisError>;
}

Take a pre-state + instruction and mutate it to produce a post-state Auxiliary data can be stored in self.

Associated Types

type State: AbstractDomain

type AnalysisError

Required methods

fn execute(
    &mut self,
    pre: &mut Self::State,
    instr: &Bytecode,
    index: CodeOffset,
    last_index: CodeOffset
) -> Result<(), Self::AnalysisError>

Execute local@instr found at index local@index in the current basic block from pre-state local@pre. Should return an AnalysisError if executing the instruction is unsuccessful, and () if the effects of successfully executing local@instr have been reflected by mutatating local@pre. Auxilary data from the analysis that is not part of the abstract state can be collected by mutating local@self. The last instruction index in the current block is local@last_index. Knowing this information allows clients to detect the end of a basic block and special-case appropriately (e.g., normalizing the abstract state before a join).

Implementors