Description
Wrapper around solvers that speak SMT-LIB.
Definition at line 14 of file SmtlibSolver.h.
#include <Rose/BinaryAnalysis/SmtlibSolver.h>
Public Member Functions | |
| virtual Ptr | create () const override |
| Virtual constructor. More... | |
| virtual void | reset () override |
| Reset solver state. More... | |
| virtual void | generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) override |
| virtual std::string | getCommand (const std::string &configName) 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) override |
| Error message from running a solver executable. More... | |
| virtual void | findVariables (const SymbolicExpr::Ptr &, VariableSet &) override |
| Return all variables that need declarations. More... | |
| virtual void | timeout (boost::chrono::duration< double >) override |
| Set the timeout for the solver. 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 ExprList &exprs) |
| Determines if expressions are trivially satisfiable or unsatisfiable. More... | |
| virtual void | push () |
| Create a backtracking point. More... | |
| virtual void | pop () |
| Pop 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 size_t | nAssertions () const |
| Total number of assertions across all backtracking levels. More... | |
| virtual ExprList | assertions () const |
| All assertions. More... | |
| virtual const ExprList & | 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 std::vector< std::string > | evidenceNames () const |
| Names of items for which satisfiability evidence exists. More... | |
| virtual SymbolicExpr::Ptr | evidenceForName (const std::string &) const |
| Evidence of satisfiability for a variable or memory address. More... | |
| virtual void | clearEvidence () |
| Clears evidence information. 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 void | generateFile (std::ostream &, const ExprList &exprs, Definitions *)=0 |
| Generates an input file for for the solver. More... | |
| virtual void | selfTest () |
| Unit tests. More... | |
| 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... | |
| Memoizer::Ptr | memoizer () const |
| Property: Memoizer. More... | |
| void | memoizer (const Memoizer::Ptr &) |
| Property: Memoizer. More... | |
| virtual Satisfiable | satisfiable (const SymbolicExpr::Ptr &) |
| Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More... | |
| virtual Satisfiable | satisfiable (const ExprList &) |
| Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown. More... | |
| bool | errorIfReset () const |
| Property: Throw an exception if the solver is reset. More... | |
| void | errorIfReset (bool b) |
| Property: Throw an exception if the solver is reset. More... | |
| virtual void | insert (const SymbolicExpr::Ptr &) |
| Insert assertions. More... | |
| virtual void | insert (const ExprList &) |
| Insert assertions. More... | |
| Evidence | evidenceByName () const |
| All evidence of satisfiability. More... | |
| ExprExprMap | evidence () const |
| All evidence of satisfiability. 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... | |
| Progress::Ptr | progress () const |
| Progress reporting object. More... | |
| void | progress (const Progress::Ptr &progress) |
| Progress reporting object. More... | |
Static Public Member Functions | |
| 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... | |
Protected Member Functions | |
| SmtlibSolver (const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs="", unsigned linkages=LM_EXECUTABLE) | |
| virtual void | parseEvidence () override |
| Parses evidence of satisfiability. More... | |
| virtual void | outputBvxorFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) |
| Generate definitions for bit-wise XOR functions. More... | |
| virtual void | outputComparisonFunctions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &) |
| Generate functions for comparison of bitvectors. More... | |
| 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 SExprTypePair | outputExpression (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 | outputArithmeticShiftRight (const SymbolicExpr::InteriorPtr &) |
| 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... | |
| virtual Satisfiable | checkLib () |
| Check satisfiability using a library API. More... | |
| std::vector< SExpr::Ptr > | parseSExpressions (const std::string &) |
| Parse all SExprs from the specified string. More... | |
Protected Attributes | |
| Sawyer::Optional< boost::chrono::duration< double > > | timeout_ |
| Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| LinkMode | linkage_ |
| std::string | outputText_ |
| Additional output obtained by satisfiable(). More... | |
| std::vector< SExpr::Ptr > | parsedOutput_ |
| ExprExprMap | evidence_ |
| TermNames | termNames_ |
| Memoizer::Ptr | memoizer_ |
| Progress::Ptr | progress_ |
| Stats | stats |
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... | |
| using | ExprList = std::vector< SymbolicExpr::Ptr > |
| Ordered list of expressions. More... | |
| using | Ptr = SmtSolverPtr |
| Reference counting pointer for SMT solvers. More... | |
| using | Availability = std::map< std::string, bool > |
| Solver availability map. More... | |
| using | StringTypePair = std::pair< std::string, Type > |
| Maps expression nodes to term names. More... | |
| using | TermNames = Sawyer::Container::Map< SymbolicExpr::Ptr, StringTypePair > |
| using | ExprExprMap = Sawyer::Container::Map< SymbolicExpr::Ptr, SymbolicExpr::Ptr > |
| Maps one symbolic expression to another. More... | |
| using | VariableSet = Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > |
| Set of variables. More... | |
| using | Definitions = std::set< uint64_t > |
| Free variables that have been defined. More... | |
| using | SExprTypePair = std::pair< SExpr::Ptr, Type > |
| using | Evidence = Sawyer::Container::Map< std::string, SymbolicExpr::Ptr > |
| Evidence of satisfiability. More... | |
| Static Public Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static Sawyer::Message::Facility | mlog |
| Diagnostic facility. More... | |
| 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 ExprList | normalizeVariables (const ExprList &, SymbolicExpr::ExprExprHashMap &index) |
| Normalize expressions by renaming variables. More... | |
| static ExprList | undoNormalization (const ExprList &, const SymbolicExpr::ExprExprHashMap &index) |
| Undo the normalizations that were performed earlier. More... | |
| Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver | |
| static boost::mutex | classStatsMutex |
| static Stats | classStats |
Member Function Documentation
|
inlinestatic |
Construct a solver using the specified program.
This object will communicate with the SMT solver using SMT-LIB version 2 text files, both for input to the solver and expected output from the solver. Diagnostics from the solver (standard error) are not redirected by the ROSE library. A separate invocation of the solver is used for each satisfiability check.
The executable should be the name of the solver executable, either to be found in $PATH or an absolute file name. Beware that some tools might change directories as they run, so absolute names are usually best. The optional shellArgs are the list of extra arguments to pass to the solver. WARNING: the entire command is pass to popen, which will invoke a shell to process the executable name and arguments; appropriate escaping of shell meta characters is the responsibility of the caller.
Definition at line 41 of file SmtlibSolver.h.
|
overridevirtual |
Virtual constructor.
The new solver will have the same settings as the source solver.
Implements Rose::BinaryAnalysis::SmtSolver.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
overridevirtual |
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::SmtSolver.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
overridevirtual |
Given the name of a configuration file, return the command that is needed to run the solver.
The first line of stdout emitted by the solver should be the word "sat" or "unsat".
Implements Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
Error message from running a solver executable.
Given the solver exit status and (implicitly) the output of the solver, either return an error message or the empty string. This can be overridden by subclasses because some solvers exit with non-zero status if you try to get the model when (check-sat) returns not-satisfiable.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
Return all variables that need declarations.
Reimplemented from Rose::BinaryAnalysis::SmtSolver.
|
overridevirtual |
Set the timeout for the solver.
This sets the maximum time that the solver will try to find a solution before returning "unknown".
Implements Rose::BinaryAnalysis::SmtSolver.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
protected |
Specify variable to use for OP_SET.
Each OP_SET needs a free variable to choose from the available members of the set. This function sets (two arguments) or retrives (one argument) the variable associated with a set.
|
protected |
Specify variable to use for OP_SET.
Each OP_SET needs a free variable to choose from the available members of the set. This function sets (two arguments) or retrives (one argument) the variable associated with a set.
|
overrideprotectedvirtual |
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::SmtSolver.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
|
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 in Rose::BinaryAnalysis::Z3Solver.
|
protectedvirtual |
Generate functions for comparison of bitvectors.
Reimplemented in Rose::BinaryAnalysis::Z3Solver.
The documentation for this class was generated from the following file:
