ROSE  0.11.98.0
Z3Solver.h
1 #ifndef ROSE_BinaryAnalysis_Z3Solver_H
2 #define ROSE_BinaryAnalysis_Z3Solver_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/SmtlibSolver.h>
7 #ifdef ROSE_HAVE_Z3
8 #include <z3++.h>
9 #endif
10 #ifdef ROSE_HAVE_Z3_VERSION_H
11 #include <z3_version.h>
12 #endif
13 
14 #ifndef ROSE_Z3
15 #define ROSE_Z3 ""
16 #endif
17 
18 #include <boost/serialization/access.hpp>
19 
20 namespace Rose {
21 namespace BinaryAnalysis {
22 
33 class Z3Solver: public SmtlibSolver {
34 #ifdef ROSE_HAVE_Z3
35 public:
36  typedef std::pair<z3::expr, Type> Z3ExprTypePair;
37 private:
38  z3::context *ctx_;
39  z3::solver *solver_;
40  std::vector<std::vector<z3::expr> > z3Stack_; // lazily parallel with parent class' "stack_" data member
41 
42  // The symbolic exprs in these maps are referenced (directly or indirectly) by the SymbolicExpr(s) being translated and therefore
43  // are guaranteed to remain allocated at least until the translation process completes.
45  CommonSubexpressions ctxCses_; // common subexpressions
47  VariableDeclarations ctxVarDecls_;
48 
49  // Expressions that we need to hold on to for allocation/deallocation purposes until the translation process is completed.
50  std::vector<SymbolicExpr::Ptr> holdingExprs_;
51 #endif
52 
53 private:
54 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
55  friend class boost::serialization::access;
56 
57  template<class S>
58  void serialize(S &s, const unsigned /*version*/) {
59  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
60  // ctx_ -- not serialized
61  // solver_ -- not serialized
62  // z3Stack_ -- not serialized
63  // ctxCses_ -- not serialized
64  // ctxVarDecls_ -- not serialized
65  }
66 #endif
67 
68 protected:
69  // Reference counted object. Use instance or create instead.
70  explicit Z3Solver(unsigned linkages = LM_ANY)
71  : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
72 #ifdef ROSE_HAVE_Z3
73  , ctx_(NULL), solver_(NULL)
74 #endif
75  {
76 #ifdef ROSE_HAVE_Z3
77  ctx_ = new z3::context;
78  solver_ = new z3::solver(*ctx_);
79  z3Stack_.push_back(std::vector<z3::expr>());
80 #endif
81  }
82 
83 public:
84  ~Z3Solver() {
85 #ifdef ROSE_HAVE_Z3
86  ctxVarDecls_.clear();
87  ctxCses_.clear();
88  z3Stack_.clear();
89  delete solver_;
90  delete ctx_;
91 #endif
92  }
93 
94 public:
99  static Ptr instance(unsigned linkages = LM_ANY) {
100  return Ptr(new Z3Solver(linkages));
101  }
102 
106  virtual Ptr create() const override;
107 
112  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
113  : SmtlibSolver("Z3", exe, shellArgs) {}
114 
119  static unsigned availableLinkages();
120 
121 #ifdef ROSE_HAVE_Z3
122 
130  virtual z3::context *z3Context() const;
131 
140  virtual z3::solver *z3Solver() const;
141 
150  virtual std::vector<z3::expr> z3Assertions() const;
151  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
153 #endif
154 
160  virtual void z3Update();
161 
162 protected:
163  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
164  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
165 
166  // Overrides
167 public:
168  virtual Satisfiable checkLib() override;
169  virtual void reset() override;
170  virtual void clearEvidence() override;
171  virtual void parseEvidence() override;
172  virtual void pop() override;
173  virtual void selfTest() override;
174  virtual void timeout(boost::chrono::duration<double>) override;
175 protected:
176  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) override;
177  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) override;
178  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) override;
179  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) override;
180 
181 #ifdef ROSE_HAVE_Z3
182 protected:
183  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
184  using SmtlibSolver::mostType;
185  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
186  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
187  Z3ExprTypePair ctxLeaf(const SymbolicExpr::Leaf*);
188  Z3ExprTypePair ctxExpression(SymbolicExpr::Node*);
189  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
190  void ctxVariableDeclarations(const VariableSet&);
191  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
192  Z3ExprTypePair ctxArithmeticShiftRight(SymbolicExpr::Interior*);
193  Z3ExprTypePair ctxExtract(SymbolicExpr::Interior*);
194  Z3ExprTypePair ctxRead(SymbolicExpr::Interior*);
195  Z3ExprTypePair ctxRotateLeft(SymbolicExpr::Interior*);
196  Z3ExprTypePair ctxRotateRight(SymbolicExpr::Interior*);
197  Z3ExprTypePair ctxSet(SymbolicExpr::Interior*);
198  Z3ExprTypePair ctxSignExtend(SymbolicExpr::Interior*);
199  Z3ExprTypePair ctxShiftLeft(SymbolicExpr::Interior*);
200  Z3ExprTypePair ctxShiftRight(SymbolicExpr::Interior*);
201  Z3ExprTypePair ctxMultiply(SymbolicExpr::Interior*);
202  Z3ExprTypePair ctxUnsignedDivide(SymbolicExpr::Interior*);
203  Z3ExprTypePair ctxSignedDivide(SymbolicExpr::Interior*);
204  Z3ExprTypePair ctxUnsignedExtend(SymbolicExpr::Interior*);
205  Z3ExprTypePair ctxUnsignedModulo(SymbolicExpr::Interior*);
206  Z3ExprTypePair ctxSignedModulo(SymbolicExpr::Interior*);
207  Z3ExprTypePair ctxWrite(SymbolicExpr::Interior*);
208  Z3ExprTypePair ctxZerop(SymbolicExpr::Interior*);
209 #endif
210 };
211 
212 } // namespace
213 } // namespace
214 
215 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
216 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
217 #endif
218 
219 #endif
220 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
virtual void reset() override
Reset solver state.
virtual void parseEvidence() override
Parses evidence of satisfiability.
Interface to the Z3 SMT solver.
Definition: Z3Solver.h:33
Leaf node of an expression tree for instruction semantics.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:178
Interior node of an expression tree for instruction semantics.
virtual void timeout(boost::chrono::duration< double >) override
Set the timeout for the solver.
virtual void pop() override
Pop a backtracking point.
const std::string & name() const
Property: Name of solver for debugging.
Definition: SmtSolver.h:404
Main namespace for the ROSE library.
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:87
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual void selfTest() override
Unit tests.
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) override
Generate definitions for bit-wise XOR functions.
virtual Satisfiable checkLib() override
Check satisfiability using a library API.
Wrapper around solvers that speak SMT-LIB.
Definition: SmtlibSolver.h:14
Binary analysis.
virtual void z3Update()
Updates the Z3 state to match the ROSE state.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) override
Generate functions for comparison of bitvectors.
Type
Type (sort) of expression.
Definition: SmtSolver.h:63
Base class for symbolic expression nodes.
Definition: SymbolicExpr.h:456
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Definition: Z3Solver.h:112
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:39
virtual void clearEvidence() override
Clears evidence information.
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Definition: Z3Solver.h:99
Container associating values with keys.
Definition: Sawyer/Map.h:66
virtual Ptr create() const override
Virtual constructor.