Struct Z3Model

pub struct Z3Model<'ctx, A: Arch, S: SmtSolver<'ctx>> { /* private fields */ }

An SMT solver mode of an encoding’s semantics.

Implementations

impl<'ctx, A: Arch, S: SmtSolver<'ctx>> Z3Model<'ctx, A, S>

pub fn of<'a, C: Computation + AsComputationRef>( encoding: &'a Encoding<A, C>, storage: &mut StorageLocations<'ctx, A, S>, context: &mut S, ) -> Self

Constructs an SMT model for the provided encoding.

pub fn intermediate_outputs(&self) -> &[IntermediateOutput<'ctx, A, S>]

Returns the intermediate outputs in the model.

These are all the dataflows. Some outputs may already have a concrete destination. Other outputs’ destinations may depend on part values in the instruction bitstring.

pub fn constraints(&self) -> &[S::Bool]

Returns a set of constraints on the part values in the instruction bitstring.

pub fn compute_concrete_outputs<C: Computation>( &self, encoding: &Encoding<A, C>, storage: &mut StorageLocations<'ctx, A, S>, context: &mut S, ) -> ConcreteZ3Model<'ctx, A, S>

Builds an SMT model that only uses concrete outputs.

Outputs that depend on a part value are rewritten as follows:

For each possible part value, the output is computed. Then, for each output, an expression is formed of the following shape:

let new_value = if part_value == EXPECTED_VALUE {
    intermediate_output_bv
} else {
    old_value
};

Trait Implementations

impl<'ctx, A: Clone + Arch, S: Clone + SmtSolver<'ctx>> Clone for Z3Model<'ctx, A, S>

where S::Bool: Clone,

fn clone(&self) -> Z3Model<'ctx, A, S>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx, A: Debug + Arch, S: Debug + SmtSolver<'ctx>> Debug for Z3Model<'ctx, A, S>

where S::Bool: Debug,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.