ROSE  0.11.50.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
42  CommonSubexpressions ctxCses_; // common subexpressions
44  VariableDeclarations ctxVarDecls_;
45 #endif
46 
47 private:
48 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
49  friend class boost::serialization::access;
50 
51  template<class S>
52  void serialize(S &s, const unsigned /*version*/) {
53  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
54  // ctx_ -- not serialized
55  // solver_ -- not serialized
56  // z3Stack_ -- not serialized
57  // ctxCses_ -- not serialized
58  // ctxVarDecls_ -- not serialized
59  }
60 #endif
61 
62 protected:
63  // Reference counted object. Use instance or create instead.
64  explicit Z3Solver(unsigned linkages = LM_ANY)
65  : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
66 #ifdef ROSE_HAVE_Z3
67  , ctx_(NULL), solver_(NULL)
68 #endif
69  {
70 #ifdef ROSE_HAVE_Z3
71  ctx_ = new z3::context;
72  solver_ = new z3::solver(*ctx_);
73  z3Stack_.push_back(std::vector<z3::expr>());
74 #endif
75  }
76 
77 public:
78  ~Z3Solver() {
79 #ifdef ROSE_HAVE_Z3
80  ctxVarDecls_.clear();
81  ctxCses_.clear();
82  z3Stack_.clear();
83  delete solver_;
84  delete ctx_;
85 #endif
86  }
87 
88 public:
93  static Ptr instance(unsigned linkages = LM_ANY) {
94  return Ptr(new Z3Solver(linkages));
95  }
96 
100  virtual Ptr create() const ROSE_OVERRIDE {
101  return Ptr(instance(linkage()));
102  }
103 
108  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
109  : SmtlibSolver("Z3", exe, shellArgs) {}
110 
115  static unsigned availableLinkages();
116 
117 #ifdef ROSE_HAVE_Z3
118 
126  virtual z3::context *z3Context() const;
127 
136  virtual z3::solver *z3Solver() const;
137 
146  virtual std::vector<z3::expr> z3Assertions() const;
147  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
149 #endif
150 
156  virtual void z3Update();
157 
158 protected:
159  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
160  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
161 
162  // Overrides
163 public:
164  virtual Satisfiable checkLib() ROSE_OVERRIDE;
165  virtual void reset() ROSE_OVERRIDE;
166  virtual void clearEvidence() ROSE_OVERRIDE;
167  virtual void parseEvidence() ROSE_OVERRIDE;
168  virtual void pop() ROSE_OVERRIDE;
169  virtual void selfTest() ROSE_OVERRIDE;
170  virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
171 protected:
172  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
173  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
174  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
175  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
176 
177 #ifdef ROSE_HAVE_Z3
178 protected:
179  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
180  using SmtlibSolver::mostType;
181  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
182  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
183  Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
184  Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
185  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
186  void ctxVariableDeclarations(const VariableSet&);
187  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
188  Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
189  Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
190  Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
191  Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
192  Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
193  Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
194  Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
195  Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
196  Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
197  Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
198  Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
199  Z3ExprTypePair ctxSignedDivide(const SymbolicExpr::InteriorPtr&);
200  Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
201  Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
202  Z3ExprTypePair ctxSignedModulo(const SymbolicExpr::InteriorPtr&);
203  Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
204  Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
205 #endif
206 };
207 
208 } // namespace
209 } // namespace
210 
211 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
212 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
213 #endif
214 
215 #endif
216 #endif
virtual void selfTest() ROSE_OVERRIDE
Unit tests.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
Interface to the Z3 SMT solver.
Definition: Z3Solver.h:33
virtual void pop() ROSE_OVERRIDE
Pop a backtracking point.
virtual Satisfiable checkLib() ROSE_OVERRIDE
Check satisfiability using a library API.
virtual Ptr create() const ROSE_OVERRIDE
Virtual constructor.
Definition: Z3Solver.h:100
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
STL namespace.
const std::string & name() const
Property: Name of solver for debugging.
Definition: SmtSolver.h:300
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
Generate definitions for bit-wise XOR functions.
Main namespace for the ROSE library.
Satisfiable
Satisfiability constants.
Definition: SmtSolver.h:81
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Definition: SmtSolver.h:172
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
Wrapper around solvers that speak SMT-LIB.
Definition: SmtlibSolver.h:14
virtual void parseEvidence() ROSE_OVERRIDE
Parses evidence of satisfiability.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpr::Ptr > &) ROSE_OVERRIDE
Generate functions for comparison of bitvectors.
virtual void z3Update()
Updates the Z3 state to match the ROSE state.
virtual void reset() ROSE_OVERRIDE
Reset solver state.
Type
Type (sort) of expression.
Definition: SmtSolver.h:57
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Definition: Z3Solver.h:108
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SmtSolver.h:36
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Definition: Z3Solver.h:93
Container associating values with keys.
Definition: Sawyer/Map.h:66
LinkMode linkage() const
Property: How ROSE communicates with the solver.
Definition: SmtSolver.h:307