ROSE 0.11.145.250
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#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
19#include <boost/serialization/access.hpp>
20#endif
21
22namespace Rose {
23namespace BinaryAnalysis {
24
35class Z3Solver: public SmtlibSolver {
36#ifdef ROSE_HAVE_Z3
37public:
38 typedef std::pair<z3::expr, Type> Z3ExprTypePair;
39private:
40 z3::context *ctx_;
41 z3::solver *solver_;
42 std::vector<std::vector<z3::expr> > z3Stack_; // lazily parallel with parent class' "stack_" data member
43
44 // The symbolic exprs in these maps are referenced (directly or indirectly) by the SymbolicExpression(s) being translated
45 // and therefore are guaranteed to remain allocated at least until the translation process completes.
47 CommonSubexpressions ctxCses_; // common subexpressions
49 VariableDeclarations ctxVarDecls_;
50
51 // Expressions that we need to hold on to for allocation/deallocation purposes until the translation process is completed.
52 std::vector<SymbolicExpression::Ptr> holdingExprs_;
53#endif
54
55private:
56#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
57 friend class boost::serialization::access;
58
59 template<class S>
60 void serialize(S &s, const unsigned /*version*/) {
61 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
62 // ctx_ -- not serialized
63 // solver_ -- not serialized
64 // z3Stack_ -- not serialized
65 // ctxCses_ -- not serialized
66 // ctxVarDecls_ -- not serialized
67 }
68#endif
69
70protected:
71 // Reference counted object. Use instance or create instead.
72 explicit Z3Solver(unsigned linkages = LM_ANY)
73 : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
74#ifdef ROSE_HAVE_Z3
75 , ctx_(NULL), solver_(NULL)
76#endif
77 {
78#ifdef ROSE_HAVE_Z3
79 ctx_ = new z3::context;
80 solver_ = new z3::solver(*ctx_);
81 z3Stack_.push_back(std::vector<z3::expr>());
82#endif
83 }
84
85public:
86 ~Z3Solver() {
87#ifdef ROSE_HAVE_Z3
88 ctxVarDecls_.clear();
89 ctxCses_.clear();
90 z3Stack_.clear();
91 delete solver_;
92 delete ctx_;
93#endif
94 }
95
96public:
101 static Ptr instance(unsigned linkages = LM_ANY) {
102 return Ptr(new Z3Solver(linkages));
103 }
104
108 virtual Ptr create() const override;
109
114 explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
115 : SmtlibSolver("Z3", exe, shellArgs) {}
116
121 static unsigned availableLinkages();
122
123#ifdef ROSE_HAVE_Z3
132 virtual z3::context *z3Context() const;
133
142 virtual z3::solver *z3Solver() const;
143
152 virtual std::vector<z3::expr> z3Assertions() const;
153 virtual std::vector<z3::expr> z3Assertions(size_t level) const;
155#endif
156
162 virtual void z3Update();
163
164protected:
165 SExprTypePair outputList(const std::string &name, const SymbolicExpression::InteriorPtr&, Type rettype = NO_TYPE);
166 SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);
167
168 // Overrides
169public:
170 virtual Satisfiable checkLib() override;
171 virtual void reset() override;
172 virtual void clearEvidence() override;
173 virtual void parseEvidence() override;
174 virtual void pop() override;
175 virtual void selfTest() override;
176 virtual void timeout(boost::chrono::duration<double>) override;
177protected:
178 virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&) override;
179 virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&) override;
180 virtual SExprTypePair outputExpression(const SymbolicExpression::Ptr&) override;
181 virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpression::InteriorPtr&) override;
182
183#ifdef ROSE_HAVE_Z3
184protected:
185 virtual Type mostType(const std::vector<Z3ExprTypePair>&);
186 using SmtlibSolver::mostType;
187 Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
188 std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
189 Z3ExprTypePair ctxLeaf(const SymbolicExpression::Leaf*);
190 Z3ExprTypePair ctxExpression(SymbolicExpression::Node*);
191 std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpression::Ptr>&);
192 void ctxVariableDeclarations(const VariableSet&);
193 void ctxCommonSubexpressions(const SymbolicExpression::Ptr&);
194 Z3ExprTypePair ctxArithmeticShiftRight(SymbolicExpression::Interior*);
195 Z3ExprTypePair ctxExtract(SymbolicExpression::Interior*);
196 Z3ExprTypePair ctxRead(SymbolicExpression::Interior*);
197 Z3ExprTypePair ctxRotateLeft(SymbolicExpression::Interior*);
198 Z3ExprTypePair ctxRotateRight(SymbolicExpression::Interior*);
199 Z3ExprTypePair ctxSet(SymbolicExpression::Interior*);
200 Z3ExprTypePair ctxSignExtend(SymbolicExpression::Interior*);
201 Z3ExprTypePair ctxShiftLeft(SymbolicExpression::Interior*);
202 Z3ExprTypePair ctxShiftRight(SymbolicExpression::Interior*);
203 Z3ExprTypePair ctxMultiply(SymbolicExpression::Interior*);
204 Z3ExprTypePair ctxUnsignedDivide(SymbolicExpression::Interior*);
205 Z3ExprTypePair ctxSignedDivide(SymbolicExpression::Interior*);
206 Z3ExprTypePair ctxUnsignedExtend(SymbolicExpression::Interior*);
207 Z3ExprTypePair ctxUnsignedModulo(SymbolicExpression::Interior*);
208 Z3ExprTypePair ctxSignedModulo(SymbolicExpression::Interior*);
209 Z3ExprTypePair ctxWrite(SymbolicExpression::Interior*);
210 Z3ExprTypePair ctxZerop(SymbolicExpression::Interior*);
211#endif
212};
213
214} // namespace
215} // namespace
216
217#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
218BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
219#endif
220
221#endif
222#endif
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition SmtSolver.h:43
const std::string & name() const
Property: Name of solver for debugging.
Definition SmtSolver.h:408
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition SmtSolver.h:49
Type
Type (sort) of expression.
Definition SmtSolver.h:67
@ LM_ANY
Any available mode.
Definition SmtSolver.h:59
Satisfiable
Satisfiability constants.
Definition SmtSolver.h:91
Wrapper around solvers that speak SMT-LIB.
Interior node of an expression tree for instruction semantics.
Leaf node of an expression tree for instruction semantics.
Base class for symbolic expression nodes.
Interface to the Z3 SMT solver.
Definition Z3Solver.h:35
virtual void selfTest() override
Unit tests.
virtual void parseEvidence() override
Parses evidence of satisfiability.
virtual void pop() override
Pop a backtracking point.
virtual void outputComparisonFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override
Generate functions for comparison of bitvectors.
virtual Satisfiable checkLib() override
Check satisfiability using a library API.
virtual void timeout(boost::chrono::duration< double >) override
Set the timeout for the solver.
virtual void z3Update()
Updates the Z3 state to match the ROSE state.
virtual void clearEvidence() override
Clears evidence information.
virtual Ptr create() const override
Virtual constructor.
static unsigned availableLinkages()
Returns a bit vector of linkage capabilities.
static Ptr instance(unsigned linkages=LM_ANY)
Construct Z3 solver preferring library linkage.
Definition Z3Solver.h:101
virtual void reset() override
Reset solver state.
Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs="")
Construct Z3 solver using a specified executable.
Definition Z3Solver.h:114
virtual void outputBvxorFunctions(std::ostream &, const std::vector< SymbolicExpression::Ptr > &) override
Generate definitions for bit-wise XOR functions.
Container associating values with keys.
Definition Sawyer/Map.h:72
Ordered set of values.
Definition Set.h:56
Reference-counting intrusive smart pointer.
The ROSE library.