ROSE  0.9.9.124
Classes | Public Types | Public Member Functions | Static Public Member Functions | 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 19 of file SMTSolver.h.

#include <SMTSolver.h>

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

Classes

struct  Exception
 
struct  Stats
 SMT solver statistics. More...
 

Public Types

enum  Satisfiable {
  SAT_NO =0,
  SAT_YES,
  SAT_UNKNOWN
}
 Satisfiability constants. More...
 
typedef std::set< uint64_t > Definitions
 Free variables that have been defined. More...
 

Public Member Functions

SMTSolverinstance (const std::string &name)
 Create a solver by name. More...
 
virtual Satisfiable trivially_satisfiable (const std::vector< SymbolicExpr::Ptr > &exprs)
 Determines if expressions are trivially satisfiable or unsatisfiable. More...
 
virtual SymbolicExpr::Ptr evidence_for_address (uint64_t addr)
 Evidence of satisfiability for a memory address. More...
 
virtual SymbolicExpr::Ptr evidence_for_name (const std::string &)
 Evidence of satisfiability for a variable or memory address. More...
 
virtual std::vector< std::string > evidence_names ()
 Names of items for which satisfiability evidence exists. More...
 
virtual void clear_evidence ()
 Clears evidence information. More...
 
void set_debug (FILE *f)
 Turns debugging on or off. More...
 
FILE * get_debug () const
 Obtain current debugging setting. More...
 
const Statsget_stats () const
 Returns statistics for this solver. More...
 
void reset_stats ()
 Resets statistics for this solver. More...
 
void reset_class_stats ()
 Resets statistics for the class. More...
 
const std::string & name () const
 Property: Name of solver for debugging.
 
void name (const std::string &s)
 Property: Name of solver for debugging.
 
virtual Satisfiable satisfiable (const SymbolicExpr::Ptr &)
 Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
 
virtual Satisfiable satisfiable (const std::vector< SymbolicExpr::Ptr > &)
 Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
 
virtual Satisfiable satisfiable (std::vector< SymbolicExpr::Ptr >, const SymbolicExpr::Ptr &)
 Determines if the specified expressions are all satisfiable, unsatisfiable, or unknown.
 
virtual SymbolicExpr::Ptr evidence_for_variable (uint64_t varno)
 Evidence of satisfiability for a bitvector variable. More...
 
virtual SymbolicExpr::Ptr evidence_for_variable (const SymbolicExpr::Ptr &var)
 Evidence of satisfiability for a bitvector variable. More...
 

Static Public Member Functions

static Stats get_class_stats ()
 Returns statistics for all solvers. More...
 

Protected Member Functions

virtual void generate_file (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *)=0
 Generates an input file for for the solver. More...
 
virtual std::string get_command (const std::string &config_name)=0
 Given the name of a configuration file, return the command that is needed to run the solver. More...
 
virtual void parse_evidence ()
 Parses evidence of satisfiability. More...
 

Protected Attributes

std::string output_text
 Additional output obtained by satisfiable(). More...
 
Stats stats
 

Static Protected Attributes

static boost::mutex class_stats_mutex
 
static Stats class_stats
 

Member Typedef Documentation

Free variables that have been defined.

Definition at line 41 of file SMTSolver.h.

Member Enumeration Documentation

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 28 of file SMTSolver.h.

Member Function Documentation

SMTSolver* Rose::BinaryAnalysis::SMTSolver::instance ( const std::string &  name)

Create a solver by name.

virtual Satisfiable Rose::BinaryAnalysis::SMTSolver::trivially_satisfiable ( 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.

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SMTSolver::evidence_for_variable ( 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 91 of file SMTSolver.h.

References evidence_for_name().

Referenced by evidence_for_variable().

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SMTSolver::evidence_for_variable ( 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 96 of file SMTSolver.h.

References evidence_for_variable().

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SMTSolver::evidence_for_address ( 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.

virtual SymbolicExpr::Ptr Rose::BinaryAnalysis::SMTSolver::evidence_for_name ( 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. The strings are those values returned by the evidence_names() method. Not all SMT solvers can return this information. Returns the null pointer if no evidence is available for the named item.

Reimplemented in Rose::BinaryAnalysis::YicesSolver.

Definition at line 113 of file SMTSolver.h.

Referenced by evidence_for_variable().

virtual std::vector<std::string> Rose::BinaryAnalysis::SMTSolver::evidence_names ( )
inlinevirtual

Names of items for which satisfiability evidence exists.

Returns a vector of strings (variable names or memory addresses) that can be passed to evidence_for_name(). Not all SMT solvers can return this information.

Reimplemented in Rose::BinaryAnalysis::YicesSolver.

Definition at line 119 of file SMTSolver.h.

virtual void Rose::BinaryAnalysis::SMTSolver::clear_evidence ( )
inlinevirtual

Clears evidence information.

Reimplemented in Rose::BinaryAnalysis::YicesSolver.

Definition at line 124 of file SMTSolver.h.

void Rose::BinaryAnalysis::SMTSolver::set_debug ( FILE *  f)
inline

Turns debugging on or off.

Definition at line 127 of file SMTSolver.h.

FILE* Rose::BinaryAnalysis::SMTSolver::get_debug ( ) const
inline

Obtain current debugging setting.

Definition at line 130 of file SMTSolver.h.

const Stats& Rose::BinaryAnalysis::SMTSolver::get_stats ( ) const
inline

Returns statistics for this solver.

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

Definition at line 133 of file SMTSolver.h.

static Stats Rose::BinaryAnalysis::SMTSolver::get_class_stats ( )
static

Returns statistics for all solvers.

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

void Rose::BinaryAnalysis::SMTSolver::reset_stats ( )
inline

Resets statistics for this solver.

Definition at line 137 of file SMTSolver.h.

void Rose::BinaryAnalysis::SMTSolver::reset_class_stats ( )

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

virtual void Rose::BinaryAnalysis::SMTSolver::generate_file ( 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.

virtual std::string Rose::BinaryAnalysis::SMTSolver::get_command ( 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.

virtual void Rose::BinaryAnalysis::SMTSolver::parse_evidence ( )
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::YicesSolver.

Definition at line 155 of file SMTSolver.h.

Member Data Documentation

std::string Rose::BinaryAnalysis::SMTSolver::output_text
protected

Additional output obtained by satisfiable().

Definition at line 155 of file SMTSolver.h.


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