ROSE  0.11.2.0
BinaryZ3Solver.h
1 #ifndef Rose_BinaryAnalysis_Z3Solver_H
2 #define Rose_BinaryAnalysis_Z3Solver_H
3 #include <rosePublicConfig.h>
4 #ifdef ROSE_BUILD_BINARY_ANALYSIS_SUPPORT
5 
6 #include <BinarySmtlibSolver.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:
82  static Ptr instance(unsigned linkages = LM_ANY) {
83  return Ptr(new Z3Solver(linkages));
84  }
85 
89  virtual Ptr create() const ROSE_OVERRIDE {
90  return Ptr(instance(linkage()));
91  }
92 
97  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
98  : SmtlibSolver("Z3", exe, shellArgs) {}
99 
104  static unsigned availableLinkages();
105 
106 #ifdef ROSE_HAVE_Z3
107 
115  virtual z3::context *z3Context() const;
116 
125  virtual z3::solver *z3Solver() const;
126 
135  virtual std::vector<z3::expr> z3Assertions() const;
136  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
138 #endif
139 
145  virtual void z3Update();
146 
147 protected:
148  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
149  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
150 
151  // Overrides
152 public:
153  virtual Satisfiable checkLib() ROSE_OVERRIDE;
154  virtual void reset() ROSE_OVERRIDE;
155  virtual void clearEvidence() ROSE_OVERRIDE;
156  virtual void parseEvidence() ROSE_OVERRIDE;
157  virtual void pop() ROSE_OVERRIDE;
158  virtual void selfTest() ROSE_OVERRIDE;
159  virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
160 protected:
161  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
162  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
163  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
164  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
165 
166 #ifdef ROSE_HAVE_Z3
167 protected:
168  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
169  using SmtlibSolver::mostType;
170  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
171  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
172  Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
173  Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
174  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
175  void ctxVariableDeclarations(const VariableSet&);
176  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
177  Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
178  Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
179  Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
180  Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
181  Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
182  Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
183  Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
184  Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
185  Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
186  Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
187  Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
188  Z3ExprTypePair ctxSignedDivide(const SymbolicExpr::InteriorPtr&);
189  Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
190  Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
191  Z3ExprTypePair ctxSignedModulo(const SymbolicExpr::InteriorPtr&);
192  Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
193  Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
194 #endif
195 };
196 
197 } // namespace
198 } // namespace
199 
200 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
201 BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
202 #endif
203 
204 #endif
205 #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 Ptr create() const ROSE_OVERRIDE
Virtual constructor.
virtual void clearEvidence() ROSE_OVERRIDE
Clears evidence information.
STL namespace.
const std::string & name() const
Property: Name of solver for debugging.
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.
virtual void timeout(boost::chrono::duration< double >) ROSE_OVERRIDE
Set the timeout for the solver.
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.