ROSE  0.9.10.103
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 #ifdef ROSE_HAVE_Z3_VERSION_H
10 #include <z3_version.h>
11 #endif
12 
13 #ifndef ROSE_Z3
14 #define ROSE_Z3 ""
15 #endif
16 
17 #include <boost/serialization/access.hpp>
18 
19 namespace Rose {
20 namespace BinaryAnalysis {
21 
32 class Z3Solver: public SmtlibSolver {
33 #ifdef ROSE_HAVE_Z3
34 public:
35  typedef std::pair<z3::expr, Type> Z3ExprTypePair;
36 private:
37  z3::context *ctx_;
38  z3::solver *solver_;
39  std::vector<std::vector<z3::expr> > z3Stack_; // lazily parallel with parent class' "stack_" data member
41  CommonSubexpressions ctxCses_; // common subexpressions
43  VariableDeclarations ctxVarDecls_;
44 #endif
45 
46 private:
47 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
48  friend class boost::serialization::access;
49 
50  template<class S>
51  void serialize(S &s, const unsigned /*version*/) {
52  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
53  // ctx_ -- not serialized
54  // solver_ -- not serialized
55  // z3Stack_ -- not serialized
56  // ctxCses_ -- not serialized
57  // ctxVarDecls_ -- not serialized
58  }
59 #endif
60 
61 protected:
62  // Reference counted object. Use instance or create instead.
63  explicit Z3Solver(unsigned linkages = LM_ANY)
64  : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
65 #ifdef ROSE_HAVE_Z3
66  , ctx_(NULL), solver_(NULL)
67 #endif
68  {
69 #ifdef ROSE_HAVE_Z3
70  ctx_ = new z3::context;
71  solver_ = new z3::solver(*ctx_);
72  z3Stack_.push_back(std::vector<z3::expr>());
73 #endif
74  }
75 
76 public:
81  static Ptr instance(unsigned linkages = LM_ANY) {
82  return Ptr(new Z3Solver(linkages));
83  }
84 
88  virtual Ptr create() const {
89  return Ptr(instance(linkage()));
90  }
91 
96  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
97  : SmtlibSolver("Z3", exe, shellArgs) {}
98 
103  static unsigned availableLinkages();
104 
105 #ifdef ROSE_HAVE_Z3
106 
114  virtual z3::context *z3Context() const;
115 
124  virtual z3::solver *z3Solver() const;
125 
134  virtual std::vector<z3::expr> z3Assertions() const;
135  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
137 #endif
138 
144  virtual void z3Update();
145 
146 protected:
147  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
148  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
149 
150  // Overrides
151 public:
152  virtual Satisfiable checkLib() ROSE_OVERRIDE;
153  virtual void reset() ROSE_OVERRIDE;
154  virtual void clearEvidence() ROSE_OVERRIDE;
155  virtual void parseEvidence() ROSE_OVERRIDE;
156  virtual void pop() ROSE_OVERRIDE;
157  virtual void selfTest() ROSE_OVERRIDE;
158 protected:
159  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
160  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
161  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
162  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
163 
164 #ifdef ROSE_HAVE_Z3
165 protected:
166  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
167  using SmtlibSolver::mostType;
168  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
169  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
170  Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
171  Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
172  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
173  void ctxVariableDeclarations(const VariableSet&);
174  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
175  Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
176  Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
177  Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
178  Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
179  Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
180  Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
181  Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
182  Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
183  Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
184  Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
185  Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
186  Z3ExprTypePair ctxSignedDivide(const SymbolicExpr::InteriorPtr&);
187  Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
188  Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
189  Z3ExprTypePair ctxSignedModulo(const SymbolicExpr::InteriorPtr&);
190  Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
191  Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
192 #endif
193 };
194 
195 } // namespace
196 } // namespace
197 
198 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
199 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
200 #endif
201 
202 #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.
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:66
LinkMode linkage() const
Property: How ROSE communicates with the solver.