ROSE  0.9.9.168
Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::Z3Solver Class Reference

Description

Interface to the Z3 SMT solver.

This interface has two modes: it can either talk to a "z3" executable using the SMT-LIB2 format, or it can connect directly to the z3 shared library. The former is easier to debug, but the latter is much faster since it avoids translating to an intermediate text representation both when sending data to the solver and when getting data from the solver. The mode is selected at runtime with the linkage property.

Definition at line 25 of file BinaryZ3Solver.h.

#include <BinaryZ3Solver.h>

Inheritance diagram for Rose::BinaryAnalysis::Z3Solver:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::Z3Solver:
Collaboration graph
[legend]

Public Member Functions

 Z3Solver (unsigned linkages=LM_ANY)
 Construct Z3 solver preferring library linkage. More...
 
 Z3Solver (const boost::filesystem::path &exe, const std::string &shellArgs="")
 Construct Z3 solver using a specified executable. More...
 
virtual Satisfiable checkLib () ROSE_OVERRIDE
 Check satisfiability using a library API. More...
 
virtual void reset () ROSE_OVERRIDE
 Reset solver state. More...
 
virtual void clearEvidence () ROSE_OVERRIDE
 Clears evidence information. More...
 
virtual void parseEvidence () ROSE_OVERRIDE
 Parses evidence of satisfiability. More...
 
virtual void push () ROSE_OVERRIDE
 Create a backtracking point. More...
 
virtual void pop () ROSE_OVERRIDE
 Pop a backtracking point. More...
 
void insert (const SymbolicExpr::Ptr &expr) ROSE_OVERRIDE
 Insert assertions. More...
 
virtual void selfTest () ROSE_OVERRIDE
 Unit tests. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::SmtlibSolver
 SmtlibSolver (const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE)
 Construct a solver using the specified program. More...
 
virtual void generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
 Generates an input file for for the solver. More...
 
virtual std::string getCommand (const std::string &configName) ROSE_OVERRIDE
 Given the name of a configuration file, return the command that is needed to run the solver. More...
 
virtual std::string getErrorMessage (int exitStatus) ROSE_OVERRIDE
 Error message from running a solver executable. More...
 
virtual VariableSet findVariables (const SymbolicExpr::Ptr &) ROSE_OVERRIDE
 Return all variables that need declarations. More...
 
virtual SymbolicExpr::Ptr evidenceForName (const std::string &) ROSE_OVERRIDE
 Evidence of satisfiability for a variable or memory address. More...
 
virtual std::vector< std::string > evidenceNames () ROSE_OVERRIDE
 Names of items for which satisfiability evidence exists. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
LinkMode linkage () const
 Property: How ROSE communicates with the solver. More...
 
void requireLinkage (LinkMode) const
 Assert required linkage. More...
 
virtual Satisfiable triviallySatisfiable (const std::vector< SymbolicExpr::Ptr > &exprs)
 Determines if expressions are trivially satisfiable or unsatisfiable. More...
 
virtual size_t nLevels () const
 Number of backtracking levels. More...
 
virtual std::vector< SymbolicExpr::Ptrassertions () const
 All assertions. More...
 
virtual std::vector< SymbolicExpr::Ptrassertions (size_t level) const
 Assertions for a particular level. More...
 
virtual Satisfiable check ()
 Check satisfiability of current stack. More...
 
virtual Satisfiable checkTrivial ()
 Check whether the stack of assertions is trivially satisfiable. More...
 
virtual SymbolicExpr::Ptr evidenceForAddress (uint64_t addr)
 Evidence of satisfiability for a memory address. More...
 
const Statsstatistics () const
 Property: Statistics for this solver. More...
 
void resetStatistics ()
 Resets statistics for this solver. More...
 
virtual Satisfiable trivially_satisfiable (const std::vector< SymbolicExpr::Ptr > &exprs) ROSE_DEPRECATED("use triviallySatisfiable")
 
virtual SymbolicExpr::Ptr evidence_for_variable (uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable")
 
virtual SymbolicExpr::Ptr evidence_for_variable (const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable")
 
virtual SymbolicExpr::Ptr evidence_for_name (const std::string &) ROSE_DEPRECATED("use evidenceForName")
 
virtual SymbolicExpr::Ptr evidence_for_address (uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress")
 
virtual std::vector< std::string > evidence_names () ROSE_DEPRECATED("use evidenceNames")
 
virtual void clear_evidence () ROSE_DEPRECATED("use clearEvidence")
 
const Statsget_stats () const ROSE_DEPRECATED("use statistics")
 
void reset_stats () ROSE_DEPRECATED("use resetStatistics")
 
void reset_class_stats () ROSE_DEPRECATED("use resetClassStatistics")
 
const std::string & name () const
 Property: Name of solver for debugging. More...
 
void name (const std::string &s)
 Property: Name of solver for debugging. More...
 
virtual Satisfiable satisfiable (const SymbolicExpr::Ptr &)
 Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More...
 
virtual Satisfiable satisfiable (const std::vector< SymbolicExpr::Ptr > &)
 Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More...
 
virtual void insert (const std::vector< SymbolicExpr::Ptr > &)
 Insert assertions. More...
 
virtual SymbolicExpr::Ptr evidenceForVariable (const SymbolicExpr::Ptr &var)
 Evidence of satisfiability for a bitvector variable. More...
 
virtual SymbolicExpr::Ptr evidenceForVariable (uint64_t varno)
 Evidence of satisfiability for a bitvector variable. More...
 

Static Public Member Functions

static unsigned availableLinkages ()
 Returns a bit vector of linkage capabilities. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
static SmtSolverbestAvailable ()
 Best available solver. More...
 
static LinkMode bestLinkage (unsigned linkages)
 Given a bit vector of linkages, return the best one. More...
 
static Stats classStatistics ()
 Property: Statistics across all solvers. More...
 
static void resetClassStatistics ()
 Resets statistics for the class. More...
 
static void initDiagnostics ()
 Initialize diagnostic output facilities. More...
 
static Stats get_class_stats () ROSE_DEPRECATED("use classStatistics")
 

Protected Member Functions

SExprTypePair outputList (const std::string &name, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
 
SExprTypePair outputList (const std::string &name, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE)
 
virtual void outputBvxorFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
 Generate definitions for bit-wise XOR functions. More...
 
virtual void outputComparisonFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
 Generate functions for comparison of bitvectors. More...
 
virtual SExprTypePair outputExpression (const SymbolicExpr::Ptr &) ROSE_OVERRIDE
 
virtual SExprTypePair outputArithmeticShiftRight (const SymbolicExpr::InteriorPtr &) ROSE_OVERRIDE
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::SmtlibSolver
virtual Type mostType (const std::vector< SExprTypePair > &)
 
virtual SExprTypePair outputCast (const SExprTypePair &, Type to)
 
virtual std::vector< SExprTypePair > outputCast (const std::vector< SExprTypePair > &, Type to)
 
virtual std::string typeName (const SymbolicExpr::Ptr &)
 
virtual std::vector< SmtSolver::SExprTypePair > outputExpressions (const std::vector< SymbolicExpr::Ptr > &)
 
virtual SExprTypePair outputLeaf (const SymbolicExpr::LeafPtr &)
 
virtual SExprTypePair outputLeftAssoc (const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
 
virtual SExprTypePair outputLeftAssoc (const std::string &func, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE)
 
virtual SExprTypePair outputLogicalShiftRight (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputShiftLeft (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputRotateLeft (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputRotateRight (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputXor (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputBinary (const std::string &func, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
 
virtual SExprTypePair outputUnary (const std::string &funcName, const SExprTypePair &arg)
 
virtual SExprTypePair outputExtract (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputSignExtend (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputUnsignedExtend (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputIte (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputNotEqual (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputSignedCompare (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputUnsignedCompare (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputZerop (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputMultiply (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputUnsignedDivide (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputUnsignedModulo (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputRead (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputWrite (const SymbolicExpr::InteriorPtr &)
 
virtual SExprTypePair outputSet (const SymbolicExpr::InteriorPtr &)
 
virtual void outputVariableDeclarations (std::ostream &, const VariableSet &)
 
virtual void outputComments (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
 
virtual void outputCommonSubexpressions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
 
virtual void outputAssertion (std::ostream &, const SymbolicExpr::Ptr &)
 
void varForSet (const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)
 Specify variable to use for OP_SET. More...
 
SymbolicExpr::LeafPtr varForSet (const SymbolicExpr::InteriorPtr &set)
 Specify variable to use for OP_SET. More...
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
 SmtSolver (const std::string &name, unsigned linkages)
 Construct with name and linkage. More...
 
virtual Satisfiable checkExe ()
 Check satisfiability using text files and an executable. More...
 
std::vector< SExpr::PtrparseSExpressions (const std::string &)
 Parse all SExprs from the specified string. More...
 
virtual void generate_file (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_DEPRECATED("use generateFile")
 
virtual std::string get_command (const std::string &config_name) ROSE_DEPRECATED("use getCommand")
 
virtual void parse_evidence () ROSE_DEPRECATED("use parseEvidence")
 

Additional Inherited Members

- Public Types inherited from Rose::BinaryAnalysis::SmtSolver
enum  LinkMode {
  LM_NONE = 0x0000,
  LM_LIBRARY = 0x0001,
  LM_EXECUTABLE = 0x0002,
  LM_ANY = 0x0003
}
 Bit flags to indicate the kind of solver interface. More...
 
enum  Type {
  NO_TYPE,
  BOOLEAN,
  BIT_VECTOR,
  MEM_STATE
}
 Type (sort) of expression. More...
 
enum  Satisfiable {
  SAT_NO =0,
  SAT_YES,
  SAT_UNKNOWN
}
 Satisfiability constants. More...
 
typedef std::pair< std::string, TypeStringTypePair
 Maps expression nodes to term names. More...
 
typedef Sawyer::Container::Map< SymbolicExpr::Ptr, StringTypePairTermNames
 
typedef Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::PtrExprExprMap
 Maps one symbolic expression to another. More...
 
typedef Sawyer::Container::Set< SymbolicExpr::LeafPtrVariableSet
 Set of variables. More...
 
typedef std::set< uint64_t > Definitions
 Free variables that have been defined. More...
 
typedef std::pair< SExpr::Ptr, TypeSExprTypePair
 
- Static Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
static void printSExpression (std::ostream &, const SExpr::Ptr &)
 Print an S-Expr for debugging. More...
 
- Protected Attributes inherited from Rose::BinaryAnalysis::SmtlibSolver
ExprExprMap evidence
 
- Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
LinkMode linkage_
 
std::string outputText_
 Additional output obtained by satisfiable(). More...
 
std::vector< SExpr::PtrparsedOutput_
 
TermNames termNames_
 
Stats stats
 
- Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
static boost::mutex classStatsMutex
 
static Stats classStats
 
static Sawyer::Message::Facility mlog
 

Constructor & Destructor Documentation

Rose::BinaryAnalysis::Z3Solver::Z3Solver ( unsigned  linkages = LM_ANY)
inlineexplicit

Construct Z3 solver preferring library linkage.

If executable (LM_EXECUTABLE) linkage is specified then the executable is that which was detected by the ROSE configuration script.

Definition at line 57 of file BinaryZ3Solver.h.

Rose::BinaryAnalysis::Z3Solver::Z3Solver ( const boost::filesystem::path &  exe,
const std::string &  shellArgs = "" 
)
inlineexplicit

Construct Z3 solver using a specified executable.

The exe should be only the name of the Z3 executable. The shellArgs are the rest of the command-line, all of which will be passed through a shell. The caller is responsible for appropriately escaping shell meta characters.

Definition at line 74 of file BinaryZ3Solver.h.

Member Function Documentation

static unsigned Rose::BinaryAnalysis::Z3Solver::availableLinkages ( )
static

Returns a bit vector of linkage capabilities.

Returns a vector of LinkMode bits that say what possible modes of communicating with the Z3 SMT solver are available. A return value of zero means the Z3 solver is not supported in this configuration of ROSE.

virtual Satisfiable Rose::BinaryAnalysis::Z3Solver::checkLib ( )
virtual

Check satisfiability using a library API.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::reset ( )
virtual

Reset solver state.

Resets the solver to an initial state containing no assertions. The evidence of satisfiability is cleared. For API-based solvers, this function might also create a new solver and/or solver context.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::clearEvidence ( )
virtual

Clears evidence information.

Evidence of satisfiability is cleared by calling this function or by calling any function that changes the state of the solver, such as pushing or popping assertion sets, inserting new assertions, or checking satisfiability. Checking satisfiability re-initializes the evidence.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::parseEvidence ( )
virtual

Parses evidence of satisfiability.

Some solvers can emit information about what variable bindings satisfy the expression. This information is parsed by this function and added to a mapping of variable to value.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::push ( )
virtual

Create a backtracking point.

Pushes a new, empty set of assertions onto the solver stack.

Note that although text-based solvers (executables) accept push and pop methods, they have no effect on the speed of the solver because ROSE invokes the executable in batch mode. In this case the push and pop apply to the stack within this solver object in ROSE.

See also, pop.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::pop ( )
virtual

Pop a backtracking point.

Pops the top set of assertions from the solver stack. The stack always contains one set of assertions, so popping the last set will cause a new, empty set to be created.

See also, push and reset.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

void Rose::BinaryAnalysis::Z3Solver::insert ( const SymbolicExpr::Ptr )
virtual

Insert assertions.

Inserts assertions into the set of assertions at the top of the backtracking stack.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::selfTest ( )
virtual

Unit tests.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::outputBvxorFunctions ( std::ostream &  ,
const std::vector< SymbolicExpr::Ptr > &   
)
protectedvirtual

Generate definitions for bit-wise XOR functions.

This method scans the supplied list of expressiosn and for each bit-wise XOR operation taking arguments of width n, it emits a binary function definition named "bvxor<em>n</em>".

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.

virtual void Rose::BinaryAnalysis::Z3Solver::outputComparisonFunctions ( std::ostream &  ,
const std::vector< SymbolicExpr::Ptr > &   
)
protectedvirtual

Generate functions for comparison of bitvectors.

Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.


The documentation for this class was generated from the following file: