ROSE  0.9.9.168
Classes | Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Static Protected Member Functions | Protected Attributes | Static Protected Attributes | List of all members
Rose::BinaryAnalysis::SmtSolver Class Referenceabstract

Description

Interface to Satisfiability Modulo Theory (SMT) solvers.

The purpose of an SMT solver is to determine if an expression is satisfiable.

Definition at line 20 of file BinarySmtSolver.h.

#include <BinarySmtSolver.h>

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

Classes

struct  Exception
 Exceptions for all things SMT related. More...
 
struct  ParseError
 Exception for parse errors when reading SMT solver output. More...
 
class  SExpr
 S-Expr parsed from SMT solver text output. More...
 
struct  Stats
 SMT solver statistics. More...
 

Public Types

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
 

Public Member Functions

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 void reset ()
 Reset solver state. 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 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 std::vector< std::string > evidenceNames ()
 Names of items for which satisfiability evidence exists. More...
 
virtual SymbolicExpr::Ptr evidenceForName (const std::string &)
 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 selfTest ()
 Unit tests. 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 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...
 

Static Public Member Functions

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

 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...
 
virtual std::string getErrorMessage (int exitStatus)
 Error message from running a solver executable. More...
 
virtual VariableSet findVariables (const SymbolicExpr::Ptr &)
 Return all variables that need declarations. More...
 
virtual void generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *)=0
 Generates an input file for for the solver. More...
 
virtual std::string getCommand (const std::string &config_name)=0
 Given the name of a configuration file, return the command that is needed to run the solver. More...
 
std::vector< SExpr::PtrparseSExpressions (const std::string &)
 Parse all SExprs from the specified string. More...
 
virtual void parseEvidence ()
 Parses evidence of satisfiability. 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")
 

Static Protected Member Functions

static void printSExpression (std::ostream &, const SExpr::Ptr &)
 Print an S-Expr for debugging. More...
 

Protected Attributes

LinkMode linkage_
 
std::string outputText_
 Additional output obtained by satisfiable(). More...
 
std::vector< SExpr::PtrparsedOutput_
 
TermNames termNames_
 
Stats stats
 

Static Protected Attributes

static boost::mutex classStatsMutex
 
static Stats classStats
 
static Sawyer::Message::Facility mlog
 

Member Typedef Documentation

typedef std::pair<std::string, Type> Rose::BinaryAnalysis::SmtSolver::StringTypePair

Maps expression nodes to term names.

This map is populated for common subexpressions.

Definition at line 38 of file BinarySmtSolver.h.

Maps one symbolic expression to another.

Definition at line 42 of file BinarySmtSolver.h.

Set of variables.

Definition at line 73 of file BinarySmtSolver.h.

Free variables that have been defined.

Definition at line 75 of file BinarySmtSolver.h.

Member Enumeration Documentation

Bit flags to indicate the kind of solver interface.

Enumerator
LM_NONE 

No available linkage.

LM_LIBRARY 

A runtime library is available.

LM_EXECUTABLE 

An executable is available.

LM_ANY 

Any available mode.

Definition at line 23 of file BinarySmtSolver.h.

Type (sort) of expression.

ROSE uses bit constants "#b1" and "#b0" (in SMT-LIB syntax) to represent Boolean true and false, but most solvers distinguish between bit vector and Boolean types and don't allow them to be mixed (e.g., "(and #b1 true)" is an error).

Definition at line 35 of file BinarySmtSolver.h.

Satisfiability constants.

Enumerator
SAT_NO 

Provably unsatisfiable.

SAT_YES 

Satisfiable and evidence of satisfiability may be available.

SAT_UNKNOWN 

Could not be proved satisfiable or unsatisfiable.

Definition at line 59 of file BinarySmtSolver.h.

Constructor & Destructor Documentation

Rose::BinaryAnalysis::SmtSolver::SmtSolver ( const std::string &  name,
unsigned  linkages 
)
inlineprotected

Construct with name and linkage.

Every solver should have a name that will appear in diagnostic messages, such as "z3", and a linkage mode that describes how ROSE communicates with the solver. The linkage mode is chosen as the least significant set bit of linkages, therefore the subclass should ensure that linkages contains only valid bits. If linkages is zero then the constructed object will be useless since it has no way to communicate with the solver. You can check for this situation by reading the linkage property, or just wait for one of the other methods to throw an SmtSolver::Exception.

Definition at line 146 of file BinarySmtSolver.h.

Member Function Documentation

static SmtSolver* Rose::BinaryAnalysis::SmtSolver::bestAvailable ( )
static

Best available solver.

Returns a new solver, an instance of the best available solver. If no solver is possible then returns null.

const std::string& Rose::BinaryAnalysis::SmtSolver::name ( ) const
inline

Property: Name of solver for debugging.

This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.

Definition at line 170 of file BinarySmtSolver.h.

void Rose::BinaryAnalysis::SmtSolver::name ( const std::string &  s)
inline

Property: Name of solver for debugging.

This name gets printed in various diagnostic messages. It's initialized to something reasonable by constructors, but can be changed at any time by the user.

Definition at line 171 of file BinarySmtSolver.h.

LinkMode Rose::BinaryAnalysis::SmtSolver::linkage ( ) const
inline

Property: How ROSE communicates with the solver.

The linkage is set when the solver object is created, and is read-only.

Definition at line 177 of file BinarySmtSolver.h.

void Rose::BinaryAnalysis::SmtSolver::requireLinkage ( LinkMode  ) const

Assert required linkage.

If the specified linkage is not available, then throw an exception.

static LinkMode Rose::BinaryAnalysis::SmtSolver::bestLinkage ( unsigned  linkages)
static

Given a bit vector of linkages, return the best one.

"Best" is defined as that with the best performance, which is usually direct calls to the solver's API.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::triviallySatisfiable ( const std::vector< SymbolicExpr::Ptr > &  exprs)
virtual

Determines if expressions are trivially satisfiable or unsatisfiable.

If all expressions are known 1-bit values that are true, then this function returns SAT_YES. If any expression is a known 1-bit value that is false, then this function returns SAT_NO. Otherwise this function returns SAT_UNKNOWN.

This is a high-level abstraction that resets this object state so it contains a single assertion set on its stack, and clears evidence of satisfiability.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::satisfiable ( const SymbolicExpr::Ptr )
virtual

Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.

This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::satisfiable ( const std::vector< SymbolicExpr::Ptr > &  )
virtual

Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.

This is a high-level abstraction that starts a new SMT solver session. For text-based interfaces, this solver object is reset, a temporary text file is created, the solver is run with the file as input, text output is read, and the evidence of satisfiability is parsed and stored in this object.

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

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

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

virtual size_t Rose::BinaryAnalysis::SmtSolver::nLevels ( ) const
inlinevirtual

Number of backtracking levels.

This is the number of sets of assertions. The push and pop increment and decrement this number. The return valued is always positive.

Definition at line 252 of file BinarySmtSolver.h.

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

Insert assertions.

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

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

virtual void Rose::BinaryAnalysis::SmtSolver::insert ( const std::vector< SymbolicExpr::Ptr > &  )
virtual

Insert assertions.

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

virtual std::vector<SymbolicExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::assertions ( ) const
virtual

All assertions.

Returns the list of all assertions across all backtracking points.

virtual std::vector<SymbolicExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::assertions ( size_t  level) const
virtual

Assertions for a particular level.

Returns the assertions associated with a particular level of the stack. Level zero is the oldest entry in the stack; all smt objects have a level zero. See also, nLevels.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::check ( )
virtual

Check satisfiability of current stack.

Checks whether all assertions in the entire stack of assertion sets are satisfiable. A set of no assertions is trivially satisfiable.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::checkTrivial ( )
virtual

Check whether the stack of assertions is trivially satisfiable.

This function returns true if all assertions have already been simplified in ROSE to the single bit "1", and returns true if so; false otherwise. If no assertions are present, this function returns true. This function does not invoke any functions in the underlying SMT solver.

virtual std::vector<std::string> Rose::BinaryAnalysis::SmtSolver::evidenceNames ( )
inlinevirtual

Names of items for which satisfiability evidence exists.

Returns a vector of strings (variable names or memory addresses) that can be passed to evidenceForName. Not all SMT solvers can return this information, in which case they return an empty vector.

The returned names are only for those variables and addresses whose evidence of satisfiability can be parsed by ROSE. The subclasses provide additional methods for obtaining more detailed information.

Reimplemented in Rose::BinaryAnalysis::YicesSolver, and Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 300 of file BinarySmtSolver.h.

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForName ( const std::string &  )
inlinevirtual

Evidence of satisfiability for a variable or memory address.

If the string starts with the letter 'v' then variable evidence is returned, otherwise the string must be an address. Valid strings are those returned by the evidenceNames method; other strings result in a null return value. Subclasses might define additional methods for obtaining evidence of satisfiability.

Reimplemented in Rose::BinaryAnalysis::YicesSolver, and Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 309 of file BinarySmtSolver.h.

Referenced by evidenceForVariable().

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

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForVariable ( const SymbolicExpr::Ptr var)
inlinevirtual

Evidence of satisfiability for a bitvector variable.

If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.

Definition at line 332 of file BinarySmtSolver.h.

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForVariable ( uint64_t  varno)
inlinevirtual

Evidence of satisfiability for a bitvector variable.

If an expression is satisfiable, this function will return a value for the specified bitvector variable that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the variable.

Definition at line 337 of file BinarySmtSolver.h.

References evidenceForName().

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SmtSolver::evidenceForAddress ( uint64_t  addr)
virtual

Evidence of satisfiability for a memory address.

If an expression is satisfiable, this function will return a value for the specified memory address that satisfies the expression in conjunction with the other evidence. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the memory address.

const Stats& Rose::BinaryAnalysis::SmtSolver::statistics ( ) const
inline

Property: Statistics for this solver.

The statistics are not reset by this call, but continue to accumulate.

Definition at line 360 of file BinarySmtSolver.h.

static Stats Rose::BinaryAnalysis::SmtSolver::classStatistics ( )
static

Property: Statistics across all solvers.

The statistics are not reset by this call, but continue to accumulate.

void Rose::BinaryAnalysis::SmtSolver::resetStatistics ( )
inline

Resets statistics for this solver.

Definition at line 368 of file BinarySmtSolver.h.

static void Rose::BinaryAnalysis::SmtSolver::resetClassStatistics ( )
static

Resets statistics for the class.

Statistics are reset to initial values for the class as a whole. Resetting statistics for the class does not affect statistics of any particular SMT solver object.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::checkExe ( )
protectedvirtual

Check satisfiability using text files and an executable.

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::checkLib ( )
protectedvirtual

Check satisfiability using a library API.

Reimplemented in Rose::BinaryAnalysis::Z3Solver, and Rose::BinaryAnalysis::YicesSolver.

virtual std::string Rose::BinaryAnalysis::SmtSolver::getErrorMessage ( int  exitStatus)
protectedvirtual

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

virtual VariableSet Rose::BinaryAnalysis::SmtSolver::findVariables ( const SymbolicExpr::Ptr )
inlineprotectedvirtual

Return all variables that need declarations.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 395 of file BinarySmtSolver.h.

static void Rose::BinaryAnalysis::SmtSolver::printSExpression ( std::ostream &  ,
const SExpr::Ptr  
)
staticprotected

Print an S-Expr for debugging.

A null pointer is printed as "nil" and an empty list is printed as "()" in order to distinguish the two cases. There should be no null pointers though in well-formed S-Exprs.

virtual void Rose::BinaryAnalysis::SmtSolver::generateFile ( std::ostream &  ,
const std::vector< SymbolicExpr::Ptr > &  exprs,
Definitions  
)
protectedpure virtual

Generates an input file for for the solver.

Usually the input file will be SMT-LIB format, but subclasses might override this to generate some other kind of input. Throws Excecption if the solver does not support an operation that is necessary to determine the satisfiability.

Implemented in Rose::BinaryAnalysis::YicesSolver, and Rose::BinaryAnalysis::SmtlibSolver.

virtual std::string Rose::BinaryAnalysis::SmtSolver::getCommand ( const std::string &  config_name)
protectedpure virtual

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".

Implemented in Rose::BinaryAnalysis::YicesSolver, and Rose::BinaryAnalysis::SmtlibSolver.

std::vector<SExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::parseSExpressions ( const std::string &  )
protected

Parse all SExprs from the specified string.

virtual void Rose::BinaryAnalysis::SmtSolver::parseEvidence ( )
inlineprotectedvirtual

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 in Rose::BinaryAnalysis::Z3Solver, Rose::BinaryAnalysis::YicesSolver, and Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 417 of file BinarySmtSolver.h.

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

Unit tests.

Reimplemented in Rose::BinaryAnalysis::Z3Solver.

static void Rose::BinaryAnalysis::SmtSolver::initDiagnostics ( )
static

Initialize diagnostic output facilities.

Called when the ROSE library is initialized.

Member Data Documentation

std::string Rose::BinaryAnalysis::SmtSolver::outputText_
protected

Additional output obtained by satisfiable().

Definition at line 105 of file BinarySmtSolver.h.


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