ROSE  0.9.9.168
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 
25 class Z3Solver: public SmtlibSolver {
26 #ifdef ROSE_HAVE_Z3
27 public:
28  typedef std::pair<z3::expr, Type> Z3ExprTypePair;
29 private:
30  z3::context *ctx_;
31  z3::solver *solver_;
32  std::vector<std::vector<z3::expr> > z3Stack_; // parallel with parent class' "stack_" data member
34  CommonSubexpressions ctxCses_; // common subexpressions
36  VariableDeclarations ctxVarDecls_;
37 #endif
38 
39 private:
40 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
41  friend class boost::serialization::access;
42 
43  template<class S>
44  void serialize(S &s, const unsigned version) {
45  // ctx_ -- not serialized
46  // solver_ -- not serialized
47  // ctxCses_ -- not serialized
48  // ctxVarDecls_ -- not serialized
49  }
50 #endif
51 
52 public:
57  explicit Z3Solver(unsigned linkages = LM_ANY)
58  : SmtlibSolver("Z3", ROSE_Z3, "", linkages & availableLinkages())
59 #ifdef ROSE_HAVE_Z3
60  , ctx_(NULL), solver_(NULL)
61 #endif
62  {
63 #ifdef ROSE_HAVE_Z3
64  ctx_ = new z3::context;
65  solver_ = new z3::solver(*ctx_);
66  z3Stack_.push_back(std::vector<z3::expr>());
67 #endif
68  }
69 
74  explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
75  : SmtlibSolver("Z3", exe, shellArgs) {}
76 
81  static unsigned availableLinkages();
82 
83 #ifdef ROSE_HAVE_Z3
84 
89  virtual z3::context *z3Context() const;
90 
96  virtual z3::solver *z3Solver() const;
97 
104  virtual std::vector<z3::expr> z3Assertions() const;
105  virtual std::vector<z3::expr> z3Assertions(size_t level) const;
107 #endif
108 
109 protected:
110  SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
111  SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
112 
113  // Overrides
114 public:
115  virtual Satisfiable checkLib() ROSE_OVERRIDE;
116  virtual void reset() ROSE_OVERRIDE;
117  virtual void clearEvidence() ROSE_OVERRIDE;
118  virtual void parseEvidence() ROSE_OVERRIDE;
119  virtual void push() ROSE_OVERRIDE;
120  virtual void pop() ROSE_OVERRIDE;
121  void insert(const SymbolicExpr::Ptr &expr) ROSE_OVERRIDE;
122  using SmtlibSolver::insert;
123  virtual void selfTest() ROSE_OVERRIDE;
124 protected:
125  virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
126  virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
127  virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
128  virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;
129 
130 #ifdef ROSE_HAVE_Z3
131 protected:
132  virtual Type mostType(const std::vector<Z3ExprTypePair>&);
133  using SmtlibSolver::mostType;
134  Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
135  std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
136  Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
137  Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
138  std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
139  void ctxVariableDeclarations(const VariableSet&);
140  void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
141  Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
142  Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
143  Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
144  Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
145  Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
146  Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
147  Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
148  Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
149  Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
150  Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
151  Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
152  Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
153  Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
154  Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
155  Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
156 #endif
157 };
158 
159 } // namespace
160 } // namespace
161 
162 #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 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.
Reference-counting smart pointer.
Definition: SharedPointer.h:34
Z3Solver(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Wrapper around solvers that speak SMT-LIB.
Sawyer::Container::Set< SymbolicExpr::LeafPtr > VariableSet
Set of variables.
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 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.
void insert(const SymbolicExpr::Ptr &expr) ROSE_OVERRIDE
Insert assertions.
virtual void push() ROSE_OVERRIDE
Create a backtracking point.
Container associating values with keys.
Definition: Sawyer/Map.h:64