ROSE  0.11.2.0
BinaryYicesSolver.h
1 #ifndef Rose_BinaryAnalysis_YicesSolver_H
2 #define Rose_BinaryAnalysis_YicesSolver_H
3 #include <rosePublicConfig.h>
4 #ifdef ROSE_BUILD_BINARY_ANALYSIS_SUPPORT
5 
6 #include "BinarySmtSolver.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 ROSE_OVERRIDE {
78  return instance(linkage());
79  }
80 
85  static unsigned availableLinkages();
86 
87  // Reference counted object. Do not explicitly delete.
88  virtual ~YicesSolver();
89 
91  // Overrides of the parent class
93 public:
94  virtual void reset() ROSE_OVERRIDE;
95  virtual void clearEvidence() ROSE_OVERRIDE;
96  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
97  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
98  virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
99 
100 protected:
101  virtual Satisfiable checkLib() ROSE_OVERRIDE;
102  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
103  virtual std::string getCommand(const std::string &config_name) ROSE_OVERRIDE;
104  virtual void parseEvidence() ROSE_OVERRIDE;
105 
107  // Miscellaneous
109 public:
110  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
111  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
112 
114  // Convert a SymbolicExpr into Yices text input
116 protected:
117  Type most_type(const std::vector<SExprTypePair>&);
118  std::vector<SExprTypePair> out_exprs(const std::vector<SymbolicExpr::Ptr>&);
119  std::vector<SExprTypePair> out_cast(const std::vector<SExprTypePair>&, Type toType);
120  void out_comments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
121  void out_common_subexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
122  void out_define(std::ostream&, const std::vector<SymbolicExpr::Ptr>&, Definitions*);
123  void out_assert(std::ostream&, const SymbolicExpr::Ptr&);
124  void out_number(std::ostream&, const SymbolicExpr::Ptr&);
125  SExprTypePair out_cast(const SExprTypePair&, Type toType);
126  SExprTypePair out_expr(const SymbolicExpr::Ptr&);
127  SExprTypePair out_unary(const char *opname, const SExprTypePair&, Type rettype = NO_TYPE);
128  SExprTypePair out_binary(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
129  SExprTypePair out_ite(const SymbolicExpr::InteriorPtr&);
130  SExprTypePair out_set(const SymbolicExpr::InteriorPtr&);
131  SExprTypePair out_la(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
132  SExprTypePair out_la(const char *opname, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
133  SExprTypePair out_extract(const SymbolicExpr::InteriorPtr&);
134  SExprTypePair out_sext(const SymbolicExpr::InteriorPtr&);
135  SExprTypePair out_uext(const SymbolicExpr::InteriorPtr&);
136  SExprTypePair out_shift(const char *opname, const SymbolicExpr::InteriorPtr&, bool newbits);
137  SExprTypePair out_asr(const SymbolicExpr::InteriorPtr&);
138  SExprTypePair out_zerop(const SymbolicExpr::InteriorPtr&);
139  SExprTypePair out_mult(const SymbolicExpr::InteriorPtr&);
140  SExprTypePair out_read(const SymbolicExpr::InteriorPtr&);
141  SExprTypePair out_write(const SymbolicExpr::InteriorPtr&);
142 
144  // Convert a SymbolicExpr to Yices IR using the Yices API
146 #ifdef ROSE_HAVE_LIBYICES
147  typedef std::pair<yices_expr, Type> YExprTypePair;
149  TermExprs termExprs; // for common subexpressions
150 
151  /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
152  typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
153  typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
154  typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
155  typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);
156 
157  Type most_type(const std::vector<YExprTypePair>&);
158  void ctx_common_subexpressions(const std::vector<SymbolicExpr::Ptr>&);
159  void ctx_define(const std::vector<SymbolicExpr::Ptr>&, Definitions*);
160  void ctx_assert(const SymbolicExpr::Ptr&);
161  std::vector<YExprTypePair> ctx_exprs(const std::vector<SymbolicExpr::Ptr>&);
162  YExprTypePair ctx_cast(const YExprTypePair&, Type toType);
163  std::vector<YExprTypePair> ctx_cast(const std::vector<YExprTypePair>&, Type toType);
164  YExprTypePair ctx_expr(const SymbolicExpr::Ptr&);
165  YExprTypePair ctx_unary(UnaryAPI, const YExprTypePair&, Type rettype = NO_TYPE);
166  YExprTypePair ctx_binary(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
167  YExprTypePair ctx_ite(const SymbolicExpr::InteriorPtr&);
168  YExprTypePair ctx_set(const SymbolicExpr::InteriorPtr&);
169  YExprTypePair ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
170  YExprTypePair ctx_la(BinaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
171  YExprTypePair ctx_la(NaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
172  YExprTypePair ctx_la(NaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
173  YExprTypePair ctx_extract(const SymbolicExpr::InteriorPtr&);
174  YExprTypePair ctx_sext(const SymbolicExpr::InteriorPtr&);
175  YExprTypePair ctx_uext(const SymbolicExpr::InteriorPtr&);
176  YExprTypePair ctx_shift(ShiftAPI, const SymbolicExpr::InteriorPtr&);
177  YExprTypePair ctx_asr(const SymbolicExpr::InteriorPtr&);
178  YExprTypePair ctx_zerop(const SymbolicExpr::InteriorPtr&);
179  YExprTypePair ctx_mult(const SymbolicExpr::InteriorPtr&);
180  YExprTypePair ctx_read(const SymbolicExpr::InteriorPtr&);
181  YExprTypePair ctx_write(const SymbolicExpr::InteriorPtr&);
182 #endif
183 
185  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
187 public:
188  static unsigned available_linkage() ROSE_DEPRECATED("use availableLinkages");
189 private:
190  static std::string get_typename(const SymbolicExpr::Ptr&);
191 };
192 
193 } // namespace
194 } // namespace
195 
196 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
197 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::YicesSolver);
198 #endif
199 
200 #endif
201 #endif
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.
virtual Ptr create() const ROSE_OVERRIDE
Virtual constructor.
STL namespace.
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
LinkMode
Bit flags to indicate the kind of solver interface.
Main namespace for the ROSE library.
std::set< uint64_t > Definitions
Free variables that have been defined.
Satisfiable
Satisfiability constants.
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.
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.
SmtSolver(const std::string &name, unsigned linkages)
Construct with name and linkage.
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
virtual void reset() ROSE_OVERRIDE
Reset solver state.
static Ptr instance(unsigned linkages=LM_ANY)
Constructs object to communicate with Yices solver.
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.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for SMT solvers.
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.
LinkMode linkage() const
Property: How ROSE communicates with the solver.
virtual SymbolicExpr::Ptr evidenceForName(const std::string &) ROSE_OVERRIDE
Evidence of satisfiability for a variable or memory address.