ROSE  0.9.10.89
Classes | Public Types | Public Member Functions | Static Public Member Functions | Static Public Attributes | 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. Solvers are reference counted objects that are allocated with instance static methods or create virtual constructors and should not be explicitly deleted.

Definition at line 33 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 Sawyer::SharedPointer< SmtSolverPtr
 Reference counting pointer for SMT solvers. More...
 
typedef std::map< std::string, bool > Availability
 Solver availability map. 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::LeafPtr, CompareLeavesByNameVariableSet
 Set of variables. More...
 
typedef std::set< uint64_t > Definitions
 Free variables that have been defined. More...
 
typedef std::pair< SExpr::Ptr, TypeSExprTypePair
 
typedef boost::unordered_map< SymbolicExpr::Hash, SatisfiableMemoization
 

Public Member Functions

virtual Ptr create () const =0
 Virtual constructor. More...
 
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 void clearMemoization ()
 Clear memoization table. 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 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 size_t nAssertions (size_t backtrackingLevel)
 Number of assertions at a specific backtracking level. 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...
 
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...
 
SharedObjectoperator= (const SharedObject &)
 Assignment. More...
 

Static Public Member Functions

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

Static Public Attributes

static Sawyer::Message::Facility mlog
 Diagnostic facility. More...
 

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...
 
static std::vector< SymbolicExpr::PtrnormalizeVariables (const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)
 Normalize expressions by renaming variables. More...
 
static std::vector< SymbolicExpr::PtrundoNormalization (const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index)
 Undo the normalizations that were performed earlier. More...
 

Protected Attributes

LinkMode linkage_
 
std::string outputText_
 Additional output obtained by satisfiable(). More...
 
std::vector< SExpr::PtrparsedOutput_
 
TermNames termNames_
 
Memoization memoization_
 
bool doMemoization_
 
SymbolicExpr::Hash latestMemoizationId_
 
SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_
 
Stats stats
 

Static Protected Attributes

static boost::mutex classStatsMutex
 
static Stats classStats
 

Member Typedef Documentation

Reference counting pointer for SMT solvers.

Definition at line 36 of file BinarySmtSolver.h.

typedef std::map<std::string, bool> Rose::BinaryAnalysis::SmtSolver::Availability

Solver availability map.

Definition at line 39 of file BinarySmtSolver.h.

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 57 of file BinarySmtSolver.h.

Maps one symbolic expression to another.

Definition at line 61 of file BinarySmtSolver.h.

Set of variables.

Definition at line 106 of file BinarySmtSolver.h.

Free variables that have been defined.

Definition at line 108 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 42 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 54 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 78 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 190 of file BinarySmtSolver.h.

Member Function Documentation

virtual Ptr Rose::BinaryAnalysis::SmtSolver::create ( ) const
pure virtual
static Availability Rose::BinaryAnalysis::SmtSolver::availability ( )
static

Availability of all known solvers.

Returns a map whose keys are the names of the SMT solver APIs and whose value is true if the solver is avilable or false if not available.

static Ptr Rose::BinaryAnalysis::SmtSolver::instance ( const std::string &  name)
static

Allocate a new solver by name.

Create a new solver using one of the names returned by availability. The special name "" means no solver (return null) and "best" means return bestAvailable (which might also be null). It may be possible to create solvers by name that are not available, but attempting to use such a solver will fail loudly by calling requireLinkage. If an invalid name is supplied then an SmtSolver::Exception is thrown.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::LlvmSemantics::Transcoder::instanceX86().

static Ptr 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 233 of file BinarySmtSolver.h.

Referenced by Rose::BinaryAnalysis::SmtlibSolver::create().

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 234 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 240 of file BinarySmtSolver.h.

Referenced by Rose::BinaryAnalysis::SmtlibSolver::create(), Rose::BinaryAnalysis::YicesSolver::create(), and Rose::BinaryAnalysis::Z3Solver::create().

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.

bool Rose::BinaryAnalysis::SmtSolver::memoization ( ) const
inline

Property: Perform memoization.

If set, then perform memoization by caching all previous results.

Definition at line 259 of file BinarySmtSolver.h.

void Rose::BinaryAnalysis::SmtSolver::memoization ( bool  b)
inline

Property: Perform memoization.

If set, then perform memoization by caching all previous results.

Definition at line 260 of file BinarySmtSolver.h.

References clearMemoization().

SymbolicExpr::Hash Rose::BinaryAnalysis::SmtSolver::latestMemoizationId ( ) const
inline

Id for latest memoized result, or zero.

Definition at line 268 of file BinarySmtSolver.h.

virtual void Rose::BinaryAnalysis::SmtSolver::clearMemoization ( )
inlinevirtual

Clear memoization table.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 273 of file BinarySmtSolver.h.

Referenced by memoization().

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

Size of memoization table.

Definition at line 278 of file BinarySmtSolver.h.

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.

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

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 343 of file BinarySmtSolver.h.

virtual size_t Rose::BinaryAnalysis::SmtSolver::nAssertions ( size_t  backtrackingLevel)
virtual

Number of assertions at a specific backtracking level.

Backtracking levels are numbered starting at zero up to one less than the value returned by nLevels.

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.

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 396 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 405 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 428 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 433 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 456 of file BinarySmtSolver.h.

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

Property: Statistics across all solvers.

The class statistics are updated whenever a solver is destroyed or its resetStatistics method is invoked. However, the nSolversCreated member is updated as soon as a solver is created.

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

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

Resets statistics for this solver.

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 494 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 516 of file BinarySmtSolver.h.

static std::vector<SymbolicExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::normalizeVariables ( const std::vector< SymbolicExpr::Ptr > &  ,
SymbolicExpr::ExprExprHashMap index 
)
staticprotected

Normalize expressions by renaming variables.

This is used during memoization to rename all the variables. It performs a depth-first search and renames each variable it encounters. The variables are renumbered starting at zero. The return value is a vector new new expressions, some of which may be the unmodified original expressions if there were no variables. The index is also a return value which indicates how original variables were mapped to new variables.

static std::vector<SymbolicExpr::Ptr> Rose::BinaryAnalysis::SmtSolver::undoNormalization ( const std::vector< SymbolicExpr::Ptr > &  ,
const SymbolicExpr::ExprExprHashMap index 
)
staticprotected

Undo the normalizations that were performed earlier.

Each of the specified expressions are rewritten by undoing the variable renaming that was done by normalizeVariables. The index is the same index as returned by normalizeVariables, although the input expressions need not be those same expressions. For each input expression, the expression is rewritten by substituting the inverse of the index. That is, a depth first search is performed on the expression and if the subexpression matches a value of the index, then it's replaced by the corresponding key.

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 140 of file BinarySmtSolver.h.

Sawyer::Message::Facility Rose::BinaryAnalysis::SmtSolver::mlog
static

Diagnostic facility.

Definition at line 155 of file BinarySmtSolver.h.


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