ROSE  0.11.83.2
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 42 of file SmtSolver.h.

#include <Rose/BinaryAnalysis/SmtSolver.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...
 
class  Memoizer
 Memoizes calls to an SMT solver. 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...
 
class  Transaction
 RAII guard for solver stack. 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...
 
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...
 

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...
 
virtual void timeout (boost::chrono::duration< double > seconds)=0
 Set the timeout for the solver. More...
 
virtual Satisfiable triviallySatisfiable (const ExprList &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 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 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 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 void findVariables (const SymbolicExpr::Ptr &, VariableSet &)
 Return all variables that need declarations. 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...
 

Static Protected Member Functions

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

Protected Attributes

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
 

Static Protected Attributes

static boost::mutex classStatsMutex
 
static Stats classStats
 

Member Typedef Documentation

Ordered list of expressions.

Definition at line 45 of file SmtSolver.h.

Reference counting pointer for SMT solvers.

Definition at line 48 of file SmtSolver.h.

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

Solver availability map.

Definition at line 51 of file SmtSolver.h.

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

Maps expression nodes to term names.

This map is populated for common subexpressions.

Definition at line 69 of file SmtSolver.h.

Maps one symbolic expression to another.

Definition at line 73 of file SmtSolver.h.

Set of variables.

Definition at line 181 of file SmtSolver.h.

Free variables that have been defined.

Definition at line 183 of file SmtSolver.h.

Evidence of satisfiability.

Definition at line 569 of file SmtSolver.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 54 of file SmtSolver.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 66 of file SmtSolver.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 90 of file SmtSolver.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 362 of file SmtSolver.h.

Member Function Documentation

virtual Ptr Rose::BinaryAnalysis::SmtSolver::create ( ) const
pure virtual

Virtual constructor.

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

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

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 407 of file SmtSolver.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 408 of file SmtSolver.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 414 of file SmtSolver.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.

Memoizer::Ptr Rose::BinaryAnalysis::SmtSolver::memoizer ( ) const

Property: Memoizer.

The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.

void Rose::BinaryAnalysis::SmtSolver::memoizer ( const Memoizer::Ptr )

Property: Memoizer.

The value of this property is a pointer to the object that caches the memoization for this solver. Setting it to a non-null pointer turns on memoization (using that object) and setting it to a null pointer turns off memoization. Memoization can be turned on or off at any time, and multiple SMT solvers can share the same memoizer.

virtual void Rose::BinaryAnalysis::SmtSolver::timeout ( boost::chrono::duration< double >  seconds)
pure virtual

Set the timeout for the solver.

This sets the maximum time that the solver will try to find a solution before returning "unknown".

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

virtual Satisfiable Rose::BinaryAnalysis::SmtSolver::triviallySatisfiable ( const ExprList 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 ExprList )
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, and Rose::BinaryAnalysis::SmtlibSolver.

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

Property: Throw an exception if the solver is reset.

This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.

Definition at line 488 of file SmtSolver.h.

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

Property: Throw an exception if the solver is reset.

This is used mostly for debugging solvers that are intending to use transactions. If the solver is ever reset, say by accidentally invoking its satisfiable method, then an exception is thrown.

Definition at line 491 of file SmtSolver.h.

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 519 of file SmtSolver.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 size_t Rose::BinaryAnalysis::SmtSolver::nAssertions ( ) const
virtual

Total number of assertions across all backtracking levels.

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 ExprList )
virtual

Insert assertions.

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

virtual ExprList Rose::BinaryAnalysis::SmtSolver::assertions ( ) const
virtual

All assertions.

Returns the list of all assertions across all backtracking points.

virtual const ExprList& 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. Errors are emitted on mlog once per error message and returned as SAT_UNKNOWN.

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 ( ) const
virtual

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.

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

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.

Referenced by evidenceForVariable().

Evidence Rose::BinaryAnalysis::SmtSolver::evidenceByName ( ) const

All evidence of satisfiability.

The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.

The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.

Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.

ExprExprMap Rose::BinaryAnalysis::SmtSolver::evidence ( ) const

All evidence of satisfiability.

The version that returns a map indexed by variable name is the same as calling evidenceNames and then evidenceForName for each of those names.

The version that returns a map indexed by symbolic expression returns all the evidence in symbolic form. The keys for that return value are symbolic expressions that are simply variables.

Evidence is only returned if the previous check was satisfiable. Otherwise the return value is an empty map.

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.

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 620 of file SmtSolver.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 625 of file SmtSolver.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 648 of file SmtSolver.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.

Progress::Ptr Rose::BinaryAnalysis::SmtSolver::progress ( ) const

Progress reporting object.

If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.

void Rose::BinaryAnalysis::SmtSolver::progress ( const Progress::Ptr progress)

Progress reporting object.

If non-null, certain types of actions are reported to this progress object by pushing subtask progress objects.

virtual void Rose::BinaryAnalysis::SmtSolver::generateFile ( std::ostream &  ,
const ExprList exprs,
Definitions  
)
pure 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.

This function is also useful for debugging because it will convert ROSE's symbolic expressions to whatever format is used by the SMT solver.

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.

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 void Rose::BinaryAnalysis::SmtSolver::findVariables ( const SymbolicExpr::Ptr ,
VariableSet  
)
inlineprotectedvirtual

Return all variables that need declarations.

Reimplemented in Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 706 of file SmtSolver.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 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::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, and Rose::BinaryAnalysis::SmtlibSolver.

Definition at line 723 of file SmtSolver.h.

static ExprList Rose::BinaryAnalysis::SmtSolver::normalizeVariables ( const ExprList ,
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 ExprList Rose::BinaryAnalysis::SmtSolver::undoNormalization ( const ExprList ,
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 316 of file SmtSolver.h.

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

Diagnostic facility.

Definition at line 330 of file SmtSolver.h.


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