ROSE  0.9.10.103
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 protected:
57  explicit YicesSolver(unsigned linkages = LM_ANY)
58  : SmtSolver("yices", (LinkMode)(linkages & availableLinkages())), context(NULL) {
59  memoization(false); // not supported in this solver
60  }
61 
62 public:
67  static Ptr instance(unsigned linkages = LM_ANY) {
68  return Ptr(new YicesSolver(linkages));
69  }
70 
74  virtual Ptr create() const {
75  return instance(linkage());
76  }
77 
82  static unsigned availableLinkages();
83 
84  // Reference counted object. Do not explicitly delete.
85  virtual ~YicesSolver();
86 
88  // Overrides of the parent class
90 public:
91  virtual void reset() ROSE_OVERRIDE;
92  virtual void clearEvidence() ROSE_OVERRIDE;
93  virtual std::vector<std::string> evidenceNames() ROSE_OVERRIDE;
94  virtual SymbolicExpr::Ptr evidenceForName(const std::string&) ROSE_OVERRIDE;
95 
96 protected:
97  virtual Satisfiable checkLib() ROSE_OVERRIDE;
98  virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) ROSE_OVERRIDE;
99  virtual std::string getCommand(const std::string &config_name) ROSE_OVERRIDE;
100  virtual void parseEvidence() ROSE_OVERRIDE;
101 
103  // Miscellaneous
105 public:
106  void varForSet(const SymbolicExpr::InteriorPtr &set, const SymbolicExpr::LeafPtr &var);
107  SymbolicExpr::LeafPtr varForSet(const SymbolicExpr::InteriorPtr &set);
108 
110  // Convert a SymbolicExpr into Yices text input
112 protected:
113  Type most_type(const std::vector<SExprTypePair>&);
114  std::vector<SExprTypePair> out_exprs(const std::vector<SymbolicExpr::Ptr>&);
115  std::vector<SExprTypePair> out_cast(const std::vector<SExprTypePair>&, Type toType);
116  void out_comments(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
117  void out_common_subexpressions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&);
118  void out_define(std::ostream&, const std::vector<SymbolicExpr::Ptr>&, Definitions*);
119  void out_assert(std::ostream&, const SymbolicExpr::Ptr&);
120  void out_number(std::ostream&, const SymbolicExpr::Ptr&);
121  SExprTypePair out_cast(const SExprTypePair&, Type toType);
122  SExprTypePair out_expr(const SymbolicExpr::Ptr&);
123  SExprTypePair out_unary(const char *opname, const SExprTypePair&, Type rettype = NO_TYPE);
124  SExprTypePair out_binary(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
125  SExprTypePair out_ite(const SymbolicExpr::InteriorPtr&);
126  SExprTypePair out_set(const SymbolicExpr::InteriorPtr&);
127  SExprTypePair out_la(const char *opname, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
128  SExprTypePair out_la(const char *opname, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
129  SExprTypePair out_extract(const SymbolicExpr::InteriorPtr&);
130  SExprTypePair out_sext(const SymbolicExpr::InteriorPtr&);
131  SExprTypePair out_uext(const SymbolicExpr::InteriorPtr&);
132  SExprTypePair out_shift(const char *opname, const SymbolicExpr::InteriorPtr&, bool newbits);
133  SExprTypePair out_asr(const SymbolicExpr::InteriorPtr&);
134  SExprTypePair out_zerop(const SymbolicExpr::InteriorPtr&);
135  SExprTypePair out_mult(const SymbolicExpr::InteriorPtr&);
136  SExprTypePair out_read(const SymbolicExpr::InteriorPtr&);
137  SExprTypePair out_write(const SymbolicExpr::InteriorPtr&);
138 
140  // Convert a SymbolicExpr to Yices IR using the Yices API
142 #ifdef ROSE_HAVE_LIBYICES
143  typedef std::pair<yices_expr, Type> YExprTypePair;
145  TermExprs termExprs; // for common subexpressions
146 
147  /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
148  typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
149  typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
150  typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
151  typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);
152 
153  Type most_type(const std::vector<YExprTypePair>&);
154  void ctx_common_subexpressions(const std::vector<SymbolicExpr::Ptr>&);
155  void ctx_define(const std::vector<SymbolicExpr::Ptr>&, Definitions*);
156  void ctx_assert(const SymbolicExpr::Ptr&);
157  std::vector<YExprTypePair> ctx_exprs(const std::vector<SymbolicExpr::Ptr>&);
158  YExprTypePair ctx_cast(const YExprTypePair&, Type toType);
159  std::vector<YExprTypePair> ctx_cast(const std::vector<YExprTypePair>&, Type toType);
160  YExprTypePair ctx_expr(const SymbolicExpr::Ptr&);
161  YExprTypePair ctx_unary(UnaryAPI, const YExprTypePair&, Type rettype = NO_TYPE);
162  YExprTypePair ctx_binary(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
163  YExprTypePair ctx_ite(const SymbolicExpr::InteriorPtr&);
164  YExprTypePair ctx_set(const SymbolicExpr::InteriorPtr&);
165  YExprTypePair ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
166  YExprTypePair ctx_la(BinaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
167  YExprTypePair ctx_la(NaryAPI, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
168  YExprTypePair ctx_la(NaryAPI, const std::vector<YExprTypePair>&, Type rettype = NO_TYPE);
169  YExprTypePair ctx_extract(const SymbolicExpr::InteriorPtr&);
170  YExprTypePair ctx_sext(const SymbolicExpr::InteriorPtr&);
171  YExprTypePair ctx_uext(const SymbolicExpr::InteriorPtr&);
172  YExprTypePair ctx_shift(ShiftAPI, const SymbolicExpr::InteriorPtr&);
173  YExprTypePair ctx_asr(const SymbolicExpr::InteriorPtr&);
174  YExprTypePair ctx_zerop(const SymbolicExpr::InteriorPtr&);
175  YExprTypePair ctx_mult(const SymbolicExpr::InteriorPtr&);
176  YExprTypePair ctx_read(const SymbolicExpr::InteriorPtr&);
177  YExprTypePair ctx_write(const SymbolicExpr::InteriorPtr&);
178 #endif
179 
181  // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
183 public:
184  static unsigned available_linkage() ROSE_DEPRECATED("use availableLinkages");
185 private:
186  static std::string get_typename(const SymbolicExpr::Ptr&);
187 };
188 
189 } // namespace
190 } // namespace
191 
192 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
193 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::YicesSolver);
194 #endif
195 
196 #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 Ptr create() const
Virtual constructor.
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.
Container associating values with keys.
Definition: Sawyer/Map.h:66
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.