Trait TargetSemantics 

pub trait TargetSemantics {
    type State;

    // Required methods
    fn fresh_state(&self) -> Self::State;
    fn apply_op(
        &self,
        state: &Self::State,
        op_name: &str,
        inputs: &[BV],
    ) -> Option<Self::State>;
    fn extract_result(
        &self,
        state: &Self::State,
        result_loc: &str,
    ) -> Option<BV>;
}

Encodes target (ARM, RISC-V, etc.) operation semantics as SMT formulas

Required Associated Types

type State

The target state type (registers, flags, memory)

Required Methods

fn fresh_state(&self) -> Self::State

Create a fresh symbolic state

fn apply_op( &self, state: &Self::State, op_name: &str, inputs: &[BV], ) -> Option<Self::State>

Apply a target operation to the state, returning updated state

fn extract_result(&self, state: &Self::State, result_loc: &str) -> Option<BV>

Extract the result bitvector from a state (e.g. read Rd register)

Dyn Compatibility

This trait is dyn compatible.

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

Implementors