Public Member Functions | Static Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::YicesSolver Class Reference


Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.

ROSE should be configured with –with-yices in order for the satisfiable() virtual method to work (otherwise, the YicesSolver class is still available but will fail an assertion when instantiated).

Yices provides two interfaces: an executable named "yices", and a library. The choice of which linkage to use to answer satisfiability questions is made at runtime (see set_linkage()).

Definition at line 26 of file BinaryYicesSolver.h.

#include <BinaryYicesSolver.h>

Inheritance diagram for Rose::BinaryAnalysis::YicesSolver:
Inheritance graph
Collaboration diagram for Rose::BinaryAnalysis::YicesSolver:
Collaboration graph

Public Member Functions

virtual Ptr create () const
 Virtual constructor. More...
virtual void reset () ROSE_OVERRIDE
 Reset solver state. More...
virtual void clearEvidence () ROSE_OVERRIDE
 Clears evidence information. More...
virtual std::vector< std::string > evidenceNames () ROSE_OVERRIDE
 Names of items for which satisfiability evidence exists. More...
virtual SymbolicExpr::Ptr evidenceForName (const std::string &) ROSE_OVERRIDE
 Evidence of satisfiability for a variable or memory address. More...
void varForSet (const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var)
SymbolicExpr::LeafPtr varForSet (const SymbolicExpr::InteriorPtr &set)
- Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
LinkMode linkage () const
 Property: How ROSE communicates with the solver. More...
void requireLinkage (LinkMode) const
 Assert required linkage. More...
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 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::Ptr
assertions () const
 All assertions. More...
virtual std::vector
< SymbolicExpr::Ptr
assertions (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 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 Ptr instance (unsigned linkages=LM_ANY)
 Constructs object to communicate with Yices solver. More...
static unsigned availableLinkages ()
 Returns a bit vector of linkage capabilities. More...
static unsigned available_linkage () ROSE_DEPRECATED("use availableLinkages")
- Static Public Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
static Availability availability ()
 Availability of all known solvers. More...
static Ptr instance (const std::string &name)
 Allocate a new solver by name. More...
static Ptr bestAvailable ()
 Best available solver. More...
static LinkMode bestLinkage (unsigned linkages)
 Given a bit vector of linkages, return the best one. More...
static Stats classStatistics ()
 Property: Statistics across all solvers. More...
static void resetClassStatistics ()
 Resets statistics for the class. More...
static void initDiagnostics ()
 Initialize diagnostic output facilities. More...
static Stats get_class_stats () ROSE_DEPRECATED("use classStatistics")

Protected Types

typedef std::map< std::string,
std::pair< size_t, uint64_t > > 
typedef std::pair< yices_expr,
typedef Sawyer::Container::Map
< SymbolicExpr::Ptr,
YExprTypePair > 
typedef yices_expr(* UnaryAPI )(yices_context, yices_expr operand)
typedef yices_expr(* BinaryAPI )(yices_context, yices_expr operand1, yices_expr operand2)
typedef yices_expr(* NaryAPI )(yices_context, yices_expr *operands, unsigned n_operands)
typedef yices_expr(* ShiftAPI )(yices_context, yices_expr, unsigned amount)

Protected Member Functions

 YicesSolver (unsigned linkages=LM_ANY)
virtual Satisfiable checkLib () ROSE_OVERRIDE
 Check satisfiability using a library API. More...
virtual void generateFile (std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
 Generates an input file for for the solver. More...
virtual std::string getCommand (const std::string &config_name) ROSE_OVERRIDE
 Given the name of a configuration file, return the command that is needed to run the solver. More...
virtual void parseEvidence () ROSE_OVERRIDE
 Parses evidence of satisfiability. More...
Type most_type (const std::vector< SExprTypePair > &)
std::vector< SExprTypePair > out_exprs (const std::vector< SymbolicExpr::Ptr > &)
std::vector< SExprTypePair > out_cast (const std::vector< SExprTypePair > &, Type toType)
void out_comments (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
void out_common_subexpressions (std::ostream &, const std::vector< SymbolicExpr::Ptr > &)
void out_define (std::ostream &, const std::vector< SymbolicExpr::Ptr > &, Definitions *)
void out_assert (std::ostream &, const SymbolicExpr::Ptr &)
void out_number (std::ostream &, const SymbolicExpr::Ptr &)
SExprTypePair out_cast (const SExprTypePair &, Type toType)
SExprTypePair out_expr (const SymbolicExpr::Ptr &)
SExprTypePair out_unary (const char *opname, const SExprTypePair &, Type rettype=NO_TYPE)
SExprTypePair out_binary (const char *opname, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
SExprTypePair out_ite (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_set (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_la (const char *opname, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
SExprTypePair out_la (const char *opname, const std::vector< SExprTypePair > &, Type rettype=NO_TYPE)
SExprTypePair out_extract (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_sext (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_uext (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_shift (const char *opname, const SymbolicExpr::InteriorPtr &, bool newbits)
SExprTypePair out_asr (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_zerop (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_mult (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_read (const SymbolicExpr::InteriorPtr &)
SExprTypePair out_write (const SymbolicExpr::InteriorPtr &)
Type most_type (const std::vector< YExprTypePair > &)
void ctx_common_subexpressions (const std::vector< SymbolicExpr::Ptr > &)
void ctx_define (const std::vector< SymbolicExpr::Ptr > &, Definitions *)
void ctx_assert (const SymbolicExpr::Ptr &)
std::vector< YExprTypePair > ctx_exprs (const std::vector< SymbolicExpr::Ptr > &)
YExprTypePair ctx_cast (const YExprTypePair &, Type toType)
std::vector< YExprTypePair > ctx_cast (const std::vector< YExprTypePair > &, Type toType)
YExprTypePair ctx_expr (const SymbolicExpr::Ptr &)
YExprTypePair ctx_unary (UnaryAPI, const YExprTypePair &, Type rettype=NO_TYPE)
YExprTypePair ctx_binary (BinaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
YExprTypePair ctx_ite (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_set (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_la (BinaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
YExprTypePair ctx_la (BinaryAPI, const std::vector< YExprTypePair > &, Type rettype=NO_TYPE)
YExprTypePair ctx_la (NaryAPI, const SymbolicExpr::InteriorPtr &, Type rettype=NO_TYPE)
YExprTypePair ctx_la (NaryAPI, const std::vector< YExprTypePair > &, Type rettype=NO_TYPE)
YExprTypePair ctx_extract (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_sext (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_uext (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_shift (ShiftAPI, const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_asr (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_zerop (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_mult (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_read (const SymbolicExpr::InteriorPtr &)
YExprTypePair ctx_write (const SymbolicExpr::InteriorPtr &)
- Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
 SmtSolver (const std::string &name, unsigned linkages)
 Construct with name and linkage. More...
virtual Satisfiable checkExe ()
 Check satisfiability using text files and an executable. More...
virtual 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...
std::vector< SExpr::PtrparseSExpressions (const std::string &)
 Parse all SExprs from the specified string. 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")

Protected Attributes

Evidence evidence
TermExprs termExprs
- Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
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

Additional Inherited Members

- Public Types inherited from Rose::BinaryAnalysis::SmtSolver
enum  LinkMode {
  LM_NONE = 0x0000,
  LM_LIBRARY = 0x0001,
  LM_EXECUTABLE = 0x0002,
  LM_ANY = 0x0003
 Bit flags to indicate the kind of solver interface. More...
enum  Type {
 Type (sort) of expression. More...
enum  Satisfiable {
  SAT_NO =0,
 Satisfiability constants. More...
typedef Sawyer::SharedPointer
< SmtSolver
 Reference counting pointer for SMT solvers. More...
typedef std::map< std::string,
bool > 
 Solver availability map. More...
typedef std::pair< std::string,
 Maps expression nodes to term names. More...
typedef Sawyer::Container::Map
< SymbolicExpr::Ptr,
typedef Sawyer::Container::Map
< SymbolicExpr::Ptr,
 Maps one symbolic expression to another. More...
typedef Sawyer::Container::Set
< SymbolicExpr::LeafPtr,
 Set of variables. More...
typedef std::set< uint64_t > Definitions
 Free variables that have been defined. More...
typedef std::pair< SExpr::Ptr,
typedef boost::unordered_map
< SymbolicExpr::Hash,
- Static Public Attributes inherited from Rose::BinaryAnalysis::SmtSolver
static Sawyer::Message::Facility mlog
 Diagnostic facility. More...
- Static Protected Member Functions inherited from Rose::BinaryAnalysis::SmtSolver
static void printSExpression (std::ostream &, const SExpr::Ptr &)
 Print an S-Expr for debugging. More...
static std::vector
< SymbolicExpr::Ptr
normalizeVariables (const std::vector< SymbolicExpr::Ptr > &, SymbolicExpr::ExprExprHashMap &index)
 Normalize expressions by renaming variables. More...
static std::vector
< SymbolicExpr::Ptr
undoNormalization (const std::vector< SymbolicExpr::Ptr > &, const SymbolicExpr::ExprExprHashMap &index)
 Undo the normalizations that were performed earlier. More...
- Static Protected Attributes inherited from Rose::BinaryAnalysis::SmtSolver
static boost::mutex classStatsMutex
static Stats classStats

Member Function Documentation

static Ptr Rose::BinaryAnalysis::YicesSolver::instance ( unsigned  linkages = LM_ANY)

Constructs object to communicate with Yices solver.

The solver will be named "Yices" (see Naming tips property) and will use the library linkage if the Yices library is present, otherwise the executable linkage. If neither is available then an SmtSolver::Exception is thrown.

Definition at line 67 of file BinaryYicesSolver.h.

Referenced by create().

virtual Ptr Rose::BinaryAnalysis::YicesSolver::create ( ) const

Virtual constructor.

Create a new solver just like this one.

Implements Rose::BinaryAnalysis::SmtSolver.

Definition at line 74 of file BinaryYicesSolver.h.

References instance(), and Rose::BinaryAnalysis::SmtSolver::linkage().

static unsigned Rose::BinaryAnalysis::YicesSolver::availableLinkages ( )

Returns a bit vector of linkage capabilities.

Returns a vector of LinkMode bits that say what possible modes of communicating with the Yices SMT solver are available. A return value of zero means the Yices solver is not supported in this configuration of ROSE.

virtual void Rose::BinaryAnalysis::YicesSolver::reset ( )

Reset solver state.

Resets the solver to an initial state containing no assertions. The evidence of satisfiability is cleared. For API-based solvers, this function might also create a new solver and/or solver context.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::YicesSolver::clearEvidence ( )

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 from Rose::BinaryAnalysis::SmtSolver.

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

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 from Rose::BinaryAnalysis::SmtSolver.

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

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 from Rose::BinaryAnalysis::SmtSolver.

virtual Satisfiable Rose::BinaryAnalysis::YicesSolver::checkLib ( )

Check satisfiability using a library API.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::YicesSolver::generateFile ( std::ostream &  ,
const std::vector< SymbolicExpr::Ptr > &  exprs,

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.

Implements Rose::BinaryAnalysis::SmtSolver.

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

Given the name of a configuration file, return the command that is needed to run the solver.

The first line of stdout emitted by the solver should be the word "sat" or "unsat".

Implements Rose::BinaryAnalysis::SmtSolver.

virtual void Rose::BinaryAnalysis::YicesSolver::parseEvidence ( )

Parses evidence of satisfiability.

Some solvers can emit information about what variable bindings satisfy the expression. This information is parsed by this function and added to a mapping of variable to value.

Reimplemented from Rose::BinaryAnalysis::SmtSolver.

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