ROSE  0.9.9.168
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 #else
34  void *context; /*unused for now*/
35 #endif
36  ExprExprMap varsForSets_; // variables to use for sets
37 protected:
38  Evidence evidence;
39 
40 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
41 private:
42  friend class boost::serialization::access;
43 
44  template<class S>
45  void serialize(S &s, const unsigned version) {
46  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
47  // varsForSets_ -- not saved
48  // evidence -- not saved
49  // context -- not saved
50  }
51 #endif
52 
54  // Construction-related things
56 public:
61  explicit YicesSolver(unsigned linkages = LM_ANY)
62  : SmtSolver("Yices", (LinkMode)(linkages & availableLinkages())), context(NULL) {}
63 
68  static unsigned availableLinkages();
69 
70  virtual ~YicesSolver();
71 
73  // Overrides of the parent class
75 public:
76  virtual void reset() ROSE_OVERRIDE;
77  virtual void clearEvidence() ROSE_OVERRIDE;
78  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
79  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
80 
81 protected:
82  virtual Satisfiable checkLib() ROSE_OVERRIDE;
83  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
84  virtual std::string getCommand(const std::string &config_name) ROSE_OVERRIDE;
85  virtual void parseEvidence() ROSE_OVERRIDE;
86 
88  // Miscellaneous
90 public:
91  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
92  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
93 
95  // Convert a SymbolicExpr into Yices text input
97 protected:
98  Type most_type(const std::vector<SExprTypePair>&);
99  std::vector<SExprTypePair> out_exprs(const std::vector<SymbolicExpr::Ptr>&);
100  std::vector<SExprTypePair> out_cast(const std::vector<SExprTypePair>&, Type toType);
101  void out_comments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
102  void out_common_subexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
103  void out_define(std::ostream&, const std::vector<SymbolicExpr::Ptr>&, Definitions*);
104  void out_assert(std::ostream&, const SymbolicExpr::Ptr&);
105  void out_number(std::ostream&, const SymbolicExpr::Ptr&);
106  SExprTypePair out_cast(const SExprTypePair&, Type toType);
107  SExprTypePair out_expr(const SymbolicExpr::Ptr&);
108  SExprTypePair out_unary(const char *opname, const SExprTypePair&, Type rettype = NO_TYPE);
109  SExprTypePair out_binary(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
110  SExprTypePair out_ite(const SymbolicExpr::InteriorPtr&);
111  SExprTypePair out_set(const SymbolicExpr::InteriorPtr&);
112  SExprTypePair out_la(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
113  SExprTypePair out_la(const char *opname, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
114  SExprTypePair out_extract(const SymbolicExpr::InteriorPtr&);
115  SExprTypePair out_sext(const SymbolicExpr::InteriorPtr&);
116  SExprTypePair out_uext(const SymbolicExpr::InteriorPtr&);
117  SExprTypePair out_shift(const char *opname, const SymbolicExpr::InteriorPtr&, bool newbits);
118  SExprTypePair out_asr(const SymbolicExpr::InteriorPtr&);
119  SExprTypePair out_zerop(const SymbolicExpr::InteriorPtr&);
120  SExprTypePair out_mult(const SymbolicExpr::InteriorPtr&);
121  SExprTypePair out_read(const SymbolicExpr::InteriorPtr&);
122  SExprTypePair out_write(const SymbolicExpr::InteriorPtr&);
123 
125  // Convert a SymbolicExpr to Yices IR using the Yices API
127 #ifdef ROSE_HAVE_LIBYICES
128  typedef std::pair<yices_expr, Type> YExprTypePair;
130  TermExprs termExprs; // for common subexpressions
131 
132  /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
133  typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
134  typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
135  typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
136  typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);
137 
138  Type most_type(const std::vector<YExprTypePair>&);
139  void ctx_common_subexpressions(const std::vector<SymbolicExpr::Ptr>&);
140  void ctx_define(const std::vector<SymbolicExpr::Ptr>&, Definitions*);
141  void ctx_assert(const SymbolicExpr::Ptr&);
142  std::vector<YExprTypePair> ctx_exprs(const std::vector<SymbolicExpr::Ptr>&);
143  YExprTypePair ctx_cast(const YExprTypePair&, Type toType);
144  std::vector<YExprTypePair> ctx_cast(const std::vector<YExprTypePair>&, Type toType);
145  YExprTypePair ctx_expr(const SymbolicExpr::Ptr&);
146  YExprTypePair ctx_unary(UnaryAPI, const YExprTypePair&, Type rettype = NO_TYPE);
147  YExprTypePair ctx_binary(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
148  YExprTypePair ctx_ite(const SymbolicExpr::InteriorPtr&);
149  YExprTypePair ctx_set(const SymbolicExpr::InteriorPtr&);
150  YExprTypePair ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
151  YExprTypePair ctx_la(BinaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
152  YExprTypePair ctx_la(NaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
153  YExprTypePair ctx_la(NaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
154  YExprTypePair ctx_extract(const SymbolicExpr::InteriorPtr&);
155  YExprTypePair ctx_sext(const SymbolicExpr::InteriorPtr&);
156  YExprTypePair ctx_uext(const SymbolicExpr::InteriorPtr&);
157  YExprTypePair ctx_shift(ShiftAPI, const SymbolicExpr::InteriorPtr&);
158  YExprTypePair ctx_asr(const SymbolicExpr::InteriorPtr&);
159  YExprTypePair ctx_zerop(const SymbolicExpr::InteriorPtr&);
160  YExprTypePair ctx_mult(const SymbolicExpr::InteriorPtr&);
161  YExprTypePair ctx_read(const SymbolicExpr::InteriorPtr&);
162  YExprTypePair ctx_write(const SymbolicExpr::InteriorPtr&);
163 #endif
164 
166  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
168 public:
169  static unsigned available_linkage() ROSE_DEPRECATED("use availableLinkages");
170 private:
171  static std::string get_typename(const SymbolicExpr::Ptr&);
172 };
173 
174 } // namespace
175 } // namespace
176 
177 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
178 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::YicesSolver);
179 #endif
180 
181 #endif
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
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...
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
virtual void reset() ROSE_OVERRIDE
Reset solver state.
virtual void generateFile(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *) ROSE_OVERRIDE
Generates an input file for for the solver.
YicesSolver(unsigned linkages=LM_ANY)
Constructs object to communicate with Yices solver.
Type
Type (sort) of expression.
Interface to Satisfiability Modulo Theory (SMT) solvers.
virtual Satisfiable checkLib() ROSE_OVERRIDE
Check satisfiability using a library API.
Container associating values with keys.
Definition: Sawyer/Map.h:64
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.