ROSE  0.11.52.0
YicesSolver.h
1 #ifndef ROSE_BinaryAnalysis_YicesSolver_H
2 #define ROSE_BinaryAnalysis_YicesSolver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/SmtSolver.h>
7 #include <Sawyer/Map.h>
8 #include <boost/serialization/access.hpp>
9 #include <boost/serialization/base_object.hpp>
10 #include <boost/serialization/export.hpp>
11 
12 #ifdef ROSE_HAVE_LIBYICES
13 # include <yices_c.h>
14 #endif
15 
16 namespace Rose {
17 namespace BinaryAnalysis {
18 
19 
27 class YicesSolver: public SmtSolver {
28 protected:
29  typedef std::map<std::string/*name or hex-addr*/, std::pair<size_t/*nbits*/, uint64_t/*value*/> > Evidence;
30 
31 private:
32 #ifdef ROSE_HAVE_LIBYICES
33  yices_context context;
34 #endif
35  ExprExprMap varsForSets_; // variables to use for sets
36 protected:
37  Evidence evidence;
38 
39 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
40 private:
41  friend class boost::serialization::access;
42 
43  template<class S>
44  void serialize(S &s, const unsigned /*version*/) {
45  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
46  // varsForSets_ -- not saved
47  // evidence -- not saved
48  // context -- not saved
49  }
50 #endif
51 
53  // Construction-related things
55 protected:
56  explicit YicesSolver(unsigned linkages = LM_ANY)
57  : SmtSolver("yices", (LinkMode)(linkages & availableLinkages()))
58 #ifdef ROSE_HAVE_LIBYICES
59  , context(NULL)
60 #endif
61  {
62  memoization(false); // not supported in this solver
63  }
64 
65 public:
70  static Ptr instance(unsigned linkages = LM_ANY) {
71  return Ptr(new YicesSolver(linkages));
72  }
73 
77  virtual Ptr create() const override;
78 
83  static unsigned availableLinkages();
84 
85  // Reference counted object. Do not explicitly delete.
86  virtual ~YicesSolver();
87 
89  // Overrides of the parent class
91 public:
92  virtual void reset() ROSE_OVERRIDE;
93  virtual void clearEvidence() ROSE_OVERRIDE;
94  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
95  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
96  virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
97 
98 protected:
99  virtual Satisfiable checkLib() ROSE_OVERRIDE;
100  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
101  virtual std::string getCommand(const std::string &config_name) ROSE_OVERRIDE;
102  virtual void parseEvidence() ROSE_OVERRIDE;
103 
105  // Miscellaneous
107 public:
108  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
109  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
110 
112  // Convert a SymbolicExpr into Yices text input
114 protected:
115  Type most_type(const std::vector<SExprTypePair>&);
116  std::vector<SExprTypePair> out_exprs(const std::vector<SymbolicExpr::Ptr>&);
117  std::vector<SExprTypePair> out_cast(const std::vector<SExprTypePair>&, Type toType);
118  void out_comments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
119  void out_common_subexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
120  void out_define(std::ostream&, const std::vector<SymbolicExpr::Ptr>&, Definitions*);
121  void out_assert(std::ostream&, const SymbolicExpr::Ptr&);
122  void out_number(std::ostream&, const SymbolicExpr::Ptr&);
123  SExprTypePair out_cast(const SExprTypePair&, Type toType);
124  SExprTypePair out_expr(const SymbolicExpr::Ptr&);
125  SExprTypePair out_unary(const char *opname, const SExprTypePair&, Type rettype = NO_TYPE);
126  SExprTypePair out_binary(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
127  SExprTypePair out_ite(const SymbolicExpr::InteriorPtr&);
128  SExprTypePair out_set(const SymbolicExpr::InteriorPtr&);
129  SExprTypePair out_la(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
130  SExprTypePair out_la(const char *opname, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
131  SExprTypePair out_extract(const SymbolicExpr::InteriorPtr&);
132  SExprTypePair out_sext(const SymbolicExpr::InteriorPtr&);
133  SExprTypePair out_uext(const SymbolicExpr::InteriorPtr&);
134  SExprTypePair out_shift(const char *opname, const SymbolicExpr::InteriorPtr&, bool newbits);
135  SExprTypePair out_asr(const SymbolicExpr::InteriorPtr&);
136  SExprTypePair out_zerop(const SymbolicExpr::InteriorPtr&);
137  SExprTypePair out_mult(const SymbolicExpr::InteriorPtr&);
138  SExprTypePair out_read(const SymbolicExpr::InteriorPtr&);
139  SExprTypePair out_write(const SymbolicExpr::InteriorPtr&);
140 
142  // Convert a SymbolicExpr to Yices IR using the Yices API
144 #ifdef ROSE_HAVE_LIBYICES
145  typedef std::pair<yices_expr, Type> YExprTypePair;
147  TermExprs termExprs; // for common subexpressions
148 
149  /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
150  typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
151  typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
152  typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
153  typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);
154 
155  Type most_type(const std::vector<YExprTypePair>&);
156  void ctx_common_subexpressions(const std::vector<SymbolicExpr::Ptr>&);
157  void ctx_define(const std::vector<SymbolicExpr::Ptr>&, Definitions*);
158  void ctx_assert(const SymbolicExpr::Ptr&);
159  std::vector<YExprTypePair> ctx_exprs(const std::vector<SymbolicExpr::Ptr>&);
160  YExprTypePair ctx_cast(const YExprTypePair&, Type toType);
161  std::vector<YExprTypePair> ctx_cast(const std::vector<YExprTypePair>&, Type toType);
162  YExprTypePair ctx_expr(const SymbolicExpr::Ptr&);
163  YExprTypePair ctx_unary(UnaryAPI, const YExprTypePair&, Type rettype = NO_TYPE);
164  YExprTypePair ctx_binary(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
165  YExprTypePair ctx_ite(const SymbolicExpr::InteriorPtr&);
166  YExprTypePair ctx_set(const SymbolicExpr::InteriorPtr&);
167  YExprTypePair ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
168  YExprTypePair ctx_la(BinaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
169  YExprTypePair ctx_la(NaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
170  YExprTypePair ctx_la(NaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
171  YExprTypePair ctx_extract(const SymbolicExpr::InteriorPtr&);
172  YExprTypePair ctx_sext(const SymbolicExpr::InteriorPtr&);
173  YExprTypePair ctx_uext(const SymbolicExpr::InteriorPtr&);
174  YExprTypePair ctx_shift(ShiftAPI, const SymbolicExpr::InteriorPtr&);
175  YExprTypePair ctx_asr(const SymbolicExpr::InteriorPtr&);
176  YExprTypePair ctx_zerop(const SymbolicExpr::InteriorPtr&);
177  YExprTypePair ctx_mult(const SymbolicExpr::InteriorPtr&);
178  YExprTypePair ctx_read(const SymbolicExpr::InteriorPtr&);
179  YExprTypePair ctx_write(const SymbolicExpr::InteriorPtr&);
180 #endif
181 
182 private:
183  static std::string get_typename(const SymbolicExpr::Ptr&);
184 };
185 
186 } // namespace
187 } // namespace
188 
189 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
190 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::YicesSolver);
191 #endif
192 
193 #endif
194 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
STL namespace.
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
LinkMode
Bit flags to indicate the kind of solver interface.
Definition: SmtSolver.h:45
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SmtSolver.h:174
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:81
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...
bool memoization() const
Property: Perform memoization.
Definition: SmtSolver.h:328
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Definition: SmtSolver.h:257
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
Definition: YicesSolver.h:27
virtual void reset() ROSE_OVERRIDE
Reset solver state.
static Ptr instance(unsigned linkages=LM_ANY)
Constructs object to communicate with Yices solver.
Definition: YicesSolver.h:70
virtual void generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
Generates an input file for for the solver.
Type
Type (sort) of expression.
Definition: SmtSolver.h:57
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:36
virtual Satisfiable checkLib() ROSE_OVERRIDE
Check satisfiability using a library API.
virtual std::vector< std::string > evidenceNames() ROSE_OVERRIDE
Names of items for which satisfiability evidence exists.
virtual SymbolicExpr::Ptr evidenceForName(const std::string &) ROSE_OVERRIDE
Evidence of satisfiability for a variable or memory address.
virtual Ptr create() const override
Virtual constructor.
Evidence evidence()
All evidence of satisfiability.