ROSE  0.9.9.109
YicesSolver.h
1 #ifndef Rose_YicesSolver_H
2 #define Rose_YicesSolver_H
3 
4 #include "rosePublicConfig.h"
5 #include "SMTSolver.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 public:
29  enum LinkMode {
30  LM_NONE=0x0000,
31  LM_LIBRARY=0x0001,
32  LM_EXECUTABLE=0x0002
33  };
34 
37 
38 protected:
39  typedef std::map<std::string/*name or hex-addr*/, std::pair<size_t/*nbits*/, uint64_t/*value*/> > Evidence;
40 
41 private:
42  LinkMode linkage;
43  TermNames termNames; // only used by Yices executable translator; library uses termExprs
44 #ifdef ROSE_HAVE_LIBYICES
45  yices_context context;
46 #else
47  void *context; /*unused for now*/
48 #endif
49 protected:
50  Evidence evidence;
51 
52 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
53 private:
54  friend class boost::serialization::access;
55 
56  template<class S>
57  void serialize(S &s, const unsigned version) {
58  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SMTSolver);
59  s & BOOST_SERIALIZATION_NVP(linkage);
60  s & BOOST_SERIALIZATION_NVP(termNames);
61  s & BOOST_SERIALIZATION_NVP(evidence);
62  //s & context; -- not saved
63  }
64 #endif
65 
66 public:
68  YicesSolver(): linkage(LM_NONE), context(NULL) {
69  init();
70  }
71  virtual ~YicesSolver();
72 
73  virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*);
74  virtual std::string get_command(const std::string &config_name);
75 
77  static unsigned available_linkage();
78 
81  return linkage;
82  }
83 
85  void set_linkage(LinkMode lm) {
86  ROSE_ASSERT(lm & available_linkage());
87  linkage = lm;
88  }
89 
95  virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);
97  std::vector<SymbolicExpr::Ptr> exprs;
98  exprs.push_back(tn);
99  return satisfiable(exprs);
100  }
103  virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) /*overrides*/;
104  virtual std::vector<std::string> evidence_names() /*overrides*/;
105  virtual void clear_evidence() /*overrides*/;
106 
107 protected:
108  virtual uint64_t parse_variable(const char *nptr, char **endptr, char first_char);
109  virtual void parse_evidence();
110 
111 private:
112  void init();
113 
114  static std::string get_typename(const SymbolicExpr::Ptr&);
115 
116  /* These out_*() functions convert a SymbolicExpr expression into text which is suitable as input to "yices"
117  * executable. */
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  void out_expr(std::ostream&, const SymbolicExpr::Ptr&);
124  void out_unary(std::ostream&, const char *opname, const SymbolicExpr::InteriorPtr&);
125  void out_binary(std::ostream&, const char *opname, const SymbolicExpr::InteriorPtr&);
126  void out_ite(std::ostream&, const SymbolicExpr::InteriorPtr&);
127  void out_set(std::ostream&, const SymbolicExpr::InteriorPtr&);
128  void out_la(std::ostream&, const char *opname, const SymbolicExpr::InteriorPtr&, bool identity_elmt);
129  void out_la(std::ostream&, const char *opname, const SymbolicExpr::InteriorPtr&);
130  void out_extract(std::ostream&, const SymbolicExpr::InteriorPtr&);
131  void out_sext(std::ostream&, const SymbolicExpr::InteriorPtr&);
132  void out_uext(std::ostream&, const SymbolicExpr::InteriorPtr&);
133  void out_shift(std::ostream&, const char *opname, const SymbolicExpr::InteriorPtr&, bool newbits);
134  void out_asr(std::ostream&, const SymbolicExpr::InteriorPtr&);
135  void out_zerop(std::ostream&, const SymbolicExpr::InteriorPtr&);
136  void out_mult(std::ostream &o, const SymbolicExpr::InteriorPtr&);
137  void out_read(std::ostream &o, const SymbolicExpr::InteriorPtr&);
138  void out_write(std::ostream &o, const SymbolicExpr::InteriorPtr&);
139 
140 #ifdef ROSE_HAVE_LIBYICES
142  TermExprs termExprs; // for common subexpressions
143 
144  /* These ctx_*() functions build a Yices context object if Yices is linked into this executable. */
145  typedef yices_expr (*UnaryAPI)(yices_context, yices_expr operand);
146  typedef yices_expr (*BinaryAPI)(yices_context, yices_expr operand1, yices_expr operand2);
147  typedef yices_expr (*NaryAPI)(yices_context, yices_expr *operands, unsigned n_operands);
148  typedef yices_expr (*ShiftAPI)(yices_context, yices_expr, unsigned amount);
149 
150  void ctx_common_subexpressions(const std::vector<SymbolicExpr::Ptr>&);
151  void ctx_define(const std::vector<SymbolicExpr::Ptr>&, Definitions*);
152  void ctx_assert(const SymbolicExpr::Ptr&);
153  yices_expr ctx_expr(const SymbolicExpr::Ptr&);
154  yices_expr ctx_unary(UnaryAPI, const SymbolicExpr::InteriorPtr&);
155  yices_expr ctx_binary(BinaryAPI, const SymbolicExpr::InteriorPtr&);
156  yices_expr ctx_ite(const SymbolicExpr::InteriorPtr&);
157  yices_expr ctx_set(const SymbolicExpr::InteriorPtr&);
158  yices_expr ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&, bool identity_elmt);
159  yices_expr ctx_la(NaryAPI, const SymbolicExpr::InteriorPtr&, bool identity_elmt);
160  yices_expr ctx_la(BinaryAPI, const SymbolicExpr::InteriorPtr&);
161  yices_expr ctx_extract(const SymbolicExpr::InteriorPtr&);
162  yices_expr ctx_sext(const SymbolicExpr::InteriorPtr&);
163  yices_expr ctx_uext(const SymbolicExpr::InteriorPtr&);
164  yices_expr ctx_shift(ShiftAPI, const SymbolicExpr::InteriorPtr&);
165  yices_expr ctx_asr(const SymbolicExpr::InteriorPtr&);
166  yices_expr ctx_zerop(const SymbolicExpr::InteriorPtr&);
167  yices_expr ctx_mult(const SymbolicExpr::InteriorPtr&);
168  yices_expr ctx_read(const SymbolicExpr::InteriorPtr&);
169  yices_expr ctx_write(const SymbolicExpr::InteriorPtr&);
170 #endif
171 
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
std::set< uint64_t > Definitions
Free variables that have been defined.
Definition: SMTSolver.h:41
virtual std::vector< std::string > evidence_names()
Names of items for which satisfiability evidence exists.
Sawyer::Container::Map< SymbolicExpr::Ptr, std::string > TermNames
Maps expression nodes to term names.
Definition: YicesSolver.h:36
void set_linkage(LinkMode lm)
Sets the linkage style.
Definition: YicesSolver.h:85
LinkMode
Bit flags to indicate what style of calls are made to Yices.
Definition: YicesSolver.h:29
Main namespace for the ROSE library.
virtual Satisfiable satisfiable(const SymbolicExpr::Ptr &tn)
Determines if the specified expression is satisfiable.
Definition: YicesSolver.h:96
The Yices runtime library is available.
Definition: YicesSolver.h:31
virtual std::string get_command(const std::string &config_name)
Given the name of a configuration file, return the command that is needed to run the solver...
The "yices" executable is available.
Definition: YicesSolver.h:32
virtual void parse_evidence()
Parses evidence of satisfiability.
Satisfiable
Satisfiability constants.
Definition: SMTSolver.h:28
Interface to the Yices Satisfiability Modulo Theory (SMT) Solver.
Definition: YicesSolver.h:26
virtual void generate_file(std::ostream &, const std::vector< SymbolicExpr::Ptr > &exprs, Definitions *)
Generates an input file for for the solver.
virtual SymbolicExpr::Ptr evidence_for_name(const std::string &)
Evidence of satisfiability for a variable or memory address.
virtual void clear_evidence()
Clears evidence information.
LinkMode get_linkage() const
Returns the style of linkage currently enabled.
Definition: YicesSolver.h:80
YicesSolver()
Constructor prefers to use the Yices executable interface.
Definition: YicesSolver.h:68
virtual Satisfiable satisfiable(const std::vector< SymbolicExpr::Ptr > &exprs)
Determines if the specified expression is satisfiable.
static unsigned available_linkage()
Returns a bit vector indicating what calling modes are available.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19