ROSE  0.9.10.54
BinaryZ3Solver.h
1 #ifndef Rose_BinaryAnalysis_Z3Solver_H
2 #define Rose_BinaryAnalysis_Z3Solver_H
3 
4 #include <rosePublicConfig.h>
5 #include <BinarySmtlibSolver.h>
6 #ifdef ROSE_HAVE_Z3
7 #include <z3++.h>
8 #endif
9 
10 #ifndef ROSE_Z3
11 #define ROSE_Z3 ""
12 #endif
13 
14 #include <boost/serialization/access.hpp>
15 
16 namespace Rose {
17 namespace BinaryAnalysis {
18 
29 class Z3Solver: public SmtlibSolver {
30 #ifdef ROSE_HAVE_Z3
31 public:
32  typedef std::pair<z3::expr, Type> Z3ExprTypePair;
33 private:
34  z3::context *ctx_;
35  z3::solver *solver_;
36  std::vector<std::vector<z3::expr> > z3Stack_; // lazily parallel with parent class' "stack_" data member
38  CommonSubexpressions ctxCses_; // common subexpressions
40  VariableDeclarations ctxVarDecls_;
41 #endif
42 
43 private:
44 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
45  friend class boost::serialization::access;
46 
47  template<class S>
48  void serialize(S &s, const unsigned /*version*/) {
49  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
50  // ctx_ -- not serialized
51  // solver_ -- not serialized
52  // z3Stack_ -- not serialized
53  // ctxCses_ -- not serialized
54  // ctxVarDecls_ -- not serialized
55  }
56 #endif
57 
58 protected:
59  // Reference counted object. Use instance or create instead.
60  explicit Z3Solver(unsigned linkages = LM_ANY)
61  : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
62 #ifdef ROSE_HAVE_Z3
63  , ctx_(NULL), solver_(NULL)
64 #endif
65  {
66 #ifdef ROSE_HAVE_Z3
67  ctx_ = new z3::context;
68  solver_ = new z3::solver(*ctx_);
69  z3Stack_.push_back(std::vector<z3::expr>());
70 #endif
71  }
72 
73 public:
78  static Ptr instance(unsigned linkages = LM_ANY) {
79  return Ptr(new Z3Solver(linkages));
80  }
81 
85  virtual Ptr create() const {
86  return Ptr(instance(linkage()));
87  }
88 
93  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
94  : SmtlibSolver("Z3", exe, shellArgs) {}
95 
100  static unsigned availableLinkages();
101 
102 #ifdef ROSE_HAVE_Z3
103 
111  virtual z3::context *z3Context() const;
112 
121  virtual z3::solver *z3Solver() const;
122 
131  virtual std::vector<z3::expr> z3Assertions() const;
132  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
134 #endif
135 
141  virtual void z3Update();
142 
143 protected:
144  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
145  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
146 
147  // Overrides
148 public:
149  virtual Satisfiable checkLib() ROSE_OVERRIDE;
150  virtual void reset() ROSE_OVERRIDE;
151  virtual void clearEvidence() ROSE_OVERRIDE;
152  virtual void parseEvidence() ROSE_OVERRIDE;
153  virtual void pop() ROSE_OVERRIDE;
154  virtual void selfTest() ROSE_OVERRIDE;
155 protected:
156  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
157  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
158  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
159  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
160 
161 #ifdef ROSE_HAVE_Z3
162 protected:
163  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
164  using SmtlibSolver::mostType;
165  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
166  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
167  Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
168  Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
169  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
170  void ctxVariableDeclarations(const VariableSet&);
171  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
172  Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
173  Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
174  Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
175  Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
176  Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
177  Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
178  Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
179  Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
180  Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
181  Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
182  Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
183  Z3ExprTypePair ctxSignedDivide(const SymbolicExpr::InteriorPtr&);
184  Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
185  Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
186  Z3ExprTypePair ctxSignedModulo(const SymbolicExpr::InteriorPtr&);
187  Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
188  Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
189 #endif
190 };
191 
192 } // namespace
193 } // namespace
194 
195 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
196 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
197 #endif
198 
199 #endif
virtual void selfTest() ROSE_OVERRIDE
Unit tests.
Interface to the Z3 SMT solver.
virtual void pop() ROSE_OVERRIDE
Pop a backtracking point.
virtual Satisfiable checkLib() ROSE_OVERRIDE
Check satisfiability using a library API.
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
STL namespace.
const std::string & name() const
Property: Name of solver for debugging.
virtual Ptr create() const
Virtual constructor.
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.
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
Sawyer::Container::Set< SymbolicExpr::LeafPtr, CompareLeavesByName > VariableSet
Set of variables.
Reference-counting smart pointer.
Definition: SharedPointer.h:34
Wrapper around solvers that speak SMT-LIB.
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.
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for SMT solvers.
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Container associating values with keys.
Definition: Sawyer/Map.h:64
LinkMode linkage() const
Property: How ROSE communicates with the solver.