ROSE  0.9.12.28
BinaryYicesSolver.h
1 #ifndef Rose_BinaryAnalysis_YicesSolver_H
2 #define Rose_BinaryAnalysis_YicesSolver_H
3 
4 #include "rosePublicConfig.h"
5 #include "BinarySmtSolver.h"
6 #include <Sawyer/Map.h>
7 #include <boost/serialization/access.hpp>
8 #include <boost/serialization/base_object.hpp>
9 #include <boost/serialization/export.hpp>
10 
11 #ifdef ROSE_HAVE_LIBYICES
12 # include <yices_c.h>
13 #endif
14 
15 namespace Rose {
16 namespace BinaryAnalysis {
17 
18 
26 class YicesSolver: public SmtSolver {
27 protected:
28  typedef std::map<std::string/*name or hex-addr*/, std::pair<size_t/*nbits*/, uint64_t/*value*/> > Evidence;
29 
30 private:
31 #ifdef ROSE_HAVE_LIBYICES
32  yices_context context;
33 #endif
34  ExprExprMap varsForSets_; // variables to use for sets
35 protected:
36  Evidence evidence;
37 
38 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
39 private:
40  friend class boost::serialization::access;
41 
42  template<class S>
43  void serialize(S &s, const unsigned /*version*/) {
44  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
45  // varsForSets_ -- not saved
46  // evidence -- not saved
47  // context -- not saved
48  }
49 #endif
50 
52  // Construction-related things
54 protected:
55  explicit YicesSolver(unsigned linkages = LM_ANY)
56  : SmtSolver("yices", (LinkMode)(linkages & availableLinkages()))
57 #ifdef ROSE_HAVE_LIBYICES
58  , context(NULL)
59 #endif
60  {
61  memoization(false); // not supported in this solver
62  }
63 
64 public:
69  static Ptr instance(unsigned linkages = LM_ANY) {
70  return Ptr(new YicesSolver(linkages));
71  }
72 
76  virtual Ptr create() const ROSE_OVERRIDE {
77  return instance(linkage());
78  }
79 
84  static unsigned availableLinkages();
85 
86  // Reference counted object. Do not explicitly delete.
87  virtual ~YicesSolver();
88 
90  // Overrides of the parent class
92 public:
93  virtual void reset() ROSE_OVERRIDE;
94  virtual void clearEvidence() ROSE_OVERRIDE;
95  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
96  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) 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 
183  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
185 public:
186  static unsigned available_linkage() ROSE_DEPRECATED("use availableLinkages");
187 private:
188  static std::string get_typename(const SymbolicExpr::Ptr&);
189 };
190 
191 } // namespace
192 } // namespace
193 
194 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
195 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::YicesSolver);
196 #endif
197 
198 #endif
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
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.