ROSE  0.11.83.2
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::SmtlibSolver Class Reference

Description

Wrapper around solvers that speak SMT-LIB.

Definition at line 14 of file SmtlibSolver.h.

#include <Rose/BinaryAnalysis/SmtlibSolver.h>

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

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 ExprListassertions (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 Statsstatistics () 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::PtrparseSExpressions (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::PtrparsedOutput_
 
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

static Ptr Rose::BinaryAnalysis::SmtlibSolver::instance ( const std::string &  name,
const boost::filesystem::path &  executable,
const std::string &  shellArgs = "",
unsigned  linkages = LM_EXECUTABLE 
)
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.

virtual Ptr Rose::BinaryAnalysis::SmtlibSolver::create ( ) const
overridevirtual

Virtual constructor.

The new solver will have the same settings as the source solver.

Implements Rose::BinaryAnalysis::SmtSolver.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::reset ( )
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.

virtual std::string Rose::BinaryAnalysis::SmtlibSolver::getCommand ( const std::string &  config_name)
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.

virtual std::string Rose::BinaryAnalysis::SmtlibSolver::getErrorMessage ( int  exitStatus)
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.

virtual void Rose::BinaryAnalysis::SmtlibSolver::findVariables ( const SymbolicExpr::Ptr ,
VariableSet  
)
overridevirtual

Return all variables that need declarations.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::SmtlibSolver::timeout ( boost::chrono::duration< double >  seconds)
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.

void Rose::BinaryAnalysis::SmtlibSolver::varForSet ( const SymbolicExpr::InteriorPtr set,
const SymbolicExpr::LeafPtr var 
)
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.

SymbolicExpr::LeafPtr Rose::BinaryAnalysis::SmtlibSolver::varForSet ( const SymbolicExpr::InteriorPtr 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.

virtual void Rose::BinaryAnalysis::SmtlibSolver::parseEvidence ( )
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.

virtual void Rose::BinaryAnalysis::SmtlibSolver::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 in Rose::BinaryAnalysis::Z3Solver.

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

Generate functions for comparison of bitvectors.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.


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