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.
If memoization is enabled, then the Z3 state may lag behind the ROSE state in order to avoid making any calls to Z3 until after the memoization check. If the caller wants to make the Z3 state up-to-date with the ROSE state then he should invoke the z3Update function.
Definition at line 29 of file BinaryZ3Solver.h.
#include <BinaryZ3Solver.h>
Public Member Functions | |
| virtual Ptr | create () const |
| Virtual constructor. More... | |
| Z3Solver (const boost::filesystem::path &exe, const std::string &shellArgs="") | |
| Construct Z3 solver using a specified executable. More... | |
| virtual void | z3Update () |
| Updates the Z3 state to match the ROSE state. 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 | pop () ROSE_OVERRIDE |
| Pop a backtracking point. More... | |
| virtual void | selfTest () ROSE_OVERRIDE |
| Unit tests. More... | |
 Public Member Functions inherited from Rose::BinaryAnalysis::SmtlibSolver | |
| 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... | |
| virtual void | clearMemoization () ROSE_OVERRIDE |
| Clear memoization table. 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... | |
| SymbolicExpr::Hash | latestMemoizationId () const |
| Id for latest memoized result, or zero. More... | |
| virtual size_t | memoizationNEntries () const |
| Size of memoization table. More... | |
| virtual Satisfiable | triviallySatisfiable (const std::vector< SymbolicExpr::Ptr > &exprs) |
| Determines if expressions are trivially satisfiable or unsatisfiable. More... | |
| virtual void | push () |
| Create a backtracking point. More... | |
| virtual size_t | nLevels () const |
| Number of backtracking levels. More... | |
| virtual size_t | nAssertions (size_t backtrackingLevel) |
| Number of assertions at a specific backtracking level. More... | |
| virtual std::vector< SymbolicExpr::Ptr > | assertions () const |
| All assertions. More... | |
| virtual std::vector< SymbolicExpr::Ptr > | assertions (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 Stats & | statistics () 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 Stats & | get_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... | |
| bool | memoization () const |
| Property: Perform memoization. More... | |
| void | memoization (bool b) |
| Property: Perform memoization. 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 SymbolicExpr::Ptr &) |
| Insert assertions. 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... | |
| Public Member Functions inherited from Sawyer::SharedObject | |
| SharedObject () | |
| Default constructor. More... | |
| SharedObject (const SharedObject &) | |
| Copy constructor. More... | |
| virtual | ~SharedObject () |
| Virtual destructor. More... | |
| SharedObject & | operator= (const SharedObject &) |
| Assignment. More... | |
Static Public Member Functions | |
| static Ptr | instance (unsigned linkages=LM_ANY) |
| Construct Z3 solver preferring library linkage. More... | |
| static unsigned | availableLinkages () |
| Returns a bit vector of linkage capabilities. More... | |
| Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtlibSolver | |
| static Ptr | instance (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... | |
| Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| static Availability | availability () |
| Availability of all known solvers. More... | |
| static Ptr | instance (const std::string &name) |
| Allocate a new solver by name. More... | |
| static Ptr | bestAvailable () |
| 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 | |
| Z3Solver (unsigned linkages=LM_ANY) | |
| 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 | |
| SmtlibSolver (const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE) | |
| 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 | outputDivide (const SymbolicExpr::InteriorPtr &, const std::string &operation) |
| virtual SExprTypePair | outputModulo (const SymbolicExpr::InteriorPtr &, const std::string &operation) |
| 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::Ptr > | parseSExpressions (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 Sawyer::SharedPointer< SmtSolver > | Ptr |
| Reference counting pointer for SMT solvers. More... | |
| typedef std::map< std::string, bool > | Availability |
| Solver availability map. More... | |
| typedef std::pair< std::string, Type > | StringTypePair |
| Maps expression nodes to term names. More... | |
| typedef Sawyer::Container::Map< SymbolicExpr::Ptr, StringTypePair > | TermNames |
| typedef Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > | ExprExprMap |
| Maps one symbolic expression to another. More... | |
| typedef Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > | VariableSet |
| Set of variables. More... | |
| typedef std::set< uint64_t > | Definitions |
| Free variables that have been defined. More... | |
| typedef std::pair< SExpr::Ptr, Type > | SExprTypePair |
| typedef boost::unordered_map< SymbolicExpr::Hash, Satisfiable > | Memoization |
| Static Public Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static Sawyer::Message::Facility | mlog |
| Diagnostic facility. More... | |
| Protected Types inherited from Rose::BinaryAnalysis::SmtlibSolver | |
| typedef boost::unordered_map< SymbolicExpr::Hash, ExprExprMap > | MemoizedEvidence |
| Static Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver | |
| static void | printSExpression (std::ostream &, const SExpr::Ptr &) |
| Print an S-Expr for debugging. More... | |
| static std::vector< SymbolicExpr::Ptr > | normalizeVariables (const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index) |
| Normalize expressions by renaming variables. More... | |
| static std::vector< SymbolicExpr::Ptr > | undoNormalization (const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index) |
| Undo the normalizations that were performed earlier. More... | |
| Protected Attributes inherited from Rose::BinaryAnalysis::SmtlibSolver | |
| ExprExprMap | evidence |
| MemoizedEvidence | memoizedEvidence |
| Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| LinkMode | linkage_ |
| std::string | outputText_ |
| Additional output obtained by satisfiable(). More... | |
| std::vector< SExpr::Ptr > | parsedOutput_ |
| TermNames | termNames_ |
| Memoization | memoization_ |
| bool | doMemoization_ |
| SymbolicExpr::Hash | latestMemoizationId_ |
| SymbolicExpr::ExprExprHashMap | latestMemoizationRewrite_ |
| Stats | stats |
| Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static boost::mutex | classStatsMutex |
| static Stats | classStats |
Constructor & Destructor Documentation
|
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 93 of file BinaryZ3Solver.h.
Member Function Documentation
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 78 of file BinaryZ3Solver.h.
Referenced by create().
|
inlinevirtual |
Virtual constructor.
Create a new solver just like this one.
Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.
Definition at line 85 of file BinaryZ3Solver.h.
References instance(), and Rose::BinaryAnalysis::SmtSolver::linkage().
|
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 |
Updates the Z3 state to match the ROSE state.
ROSE tries to avoid making any Z3 calls until it knows they're necessary. Therefore the Z3 state may lag behind the ROSE state. This function's purpose is to bring the Z3 state up-to-date with the ROSE state. You may call it as often as you like, and it is called automatically by some other functions in this API.
|
virtual |
Check satisfiability using a library API.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
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 |
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 |
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 |
Pop a backtracking point.
Pops the top set of assertions from the solver stack. It is not legal to call pop when the assertion stack is only one level deep; use reset in that case instead.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
virtual |
Unit tests.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
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.
|
protectedvirtual |
Generate functions for comparison of bitvectors.
Reimplemented from Rose::BinaryAnalysis::SmtlibSolver.
The documentation for this class was generated from the following file:
