1 //===-- Z3Builder.h --------------------------------------------*- C++ -*-====//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9
10 #ifndef KLEE_Z3BUILDER_H
11 #define KLEE_Z3BUILDER_H
12
13 #include "klee/Config/config.h"
14 #include "klee/Expr/ArrayExprHash.h"
15 #include "klee/Expr/ExprHashMap.h"
16
17 #include <unordered_map>
18 #include <z3.h>
19
20 namespace klee {
21
22 template <typename T> class Z3NodeHandle {
23 // Internally these Z3 types are pointers
24 // so storing these should be cheap.
25 // It would be nice if we could infer the Z3_context from the node
26 // but I can't see a way to do this from Z3's API.
27 protected:
28 T node;
29 ::Z3_context context;
30
31 private:
32 // To be specialised
33 inline ::Z3_ast as_ast();
34
35 public:
Z3NodeHandle()36 Z3NodeHandle() : node(NULL), context(NULL) {}
Z3NodeHandle(const T _node,const::Z3_context _context)37 Z3NodeHandle(const T _node, const ::Z3_context _context)
38 : node(_node), context(_context) {
39 if (node && context) {
40 ::Z3_inc_ref(context, as_ast());
41 }
42 };
~Z3NodeHandle()43 ~Z3NodeHandle() {
44 if (node && context) {
45 ::Z3_dec_ref(context, as_ast());
46 }
47 }
Z3NodeHandle(const Z3NodeHandle & b)48 Z3NodeHandle(const Z3NodeHandle &b) : node(b.node), context(b.context) {
49 if (node && context) {
50 ::Z3_inc_ref(context, as_ast());
51 }
52 }
53 Z3NodeHandle &operator=(const Z3NodeHandle &b) {
54 if (node == NULL && context == NULL) {
55 // Special case for when this object was constructed
56 // using the default constructor. Try to inherit a non null
57 // context.
58 context = b.context;
59 }
60 assert(context == b.context && "Mismatched Z3 contexts!");
61 // node != nullptr ==> context != NULL
62 assert((node == NULL || context) &&
63 "Can't have non nullptr node with nullptr context");
64
65 if (node && context) {
66 ::Z3_dec_ref(context, as_ast());
67 }
68 node = b.node;
69 if (node && context) {
70 ::Z3_inc_ref(context, as_ast());
71 }
72 return *this;
73 }
74 // To be specialised
75 void dump();
76
T()77 operator T() const { return node; }
78 };
79
80 // Specialise for Z3_sort
as_ast()81 template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() {
82 // In Z3 internally this call is just a cast. We could just do that
83 // instead to simplify our implementation but this seems cleaner.
84 return ::Z3_sort_to_ast(context, node);
85 }
86 typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
87 template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used));
88
89 // Specialise for Z3_ast
as_ast()90 template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
91 typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
92 template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used));
93
94 class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> {
95
96 friend class Z3Builder;
97
98 public:
Z3ArrayExprHash()99 Z3ArrayExprHash(){};
100 virtual ~Z3ArrayExprHash();
101 void clear();
102 };
103
104 class Z3Builder {
105 ExprHashMap<std::pair<Z3ASTHandle, unsigned> > constructed;
106 Z3ArrayExprHash _arr_hash;
107
108 private:
109 Z3ASTHandle bvOne(unsigned width);
110 Z3ASTHandle bvZero(unsigned width);
111 Z3ASTHandle bvMinusOne(unsigned width);
112 Z3ASTHandle bvConst32(unsigned width, uint32_t value);
113 Z3ASTHandle bvConst64(unsigned width, uint64_t value);
114 Z3ASTHandle bvZExtConst(unsigned width, uint64_t value);
115 Z3ASTHandle bvSExtConst(unsigned width, uint64_t value);
116 Z3ASTHandle bvBoolExtract(Z3ASTHandle expr, int bit);
117 Z3ASTHandle bvExtract(Z3ASTHandle expr, unsigned top, unsigned bottom);
118 Z3ASTHandle eqExpr(Z3ASTHandle a, Z3ASTHandle b);
119
120 // logical left and right shift (not arithmetic)
121 Z3ASTHandle bvLeftShift(Z3ASTHandle expr, unsigned shift);
122 Z3ASTHandle bvRightShift(Z3ASTHandle expr, unsigned shift);
123 Z3ASTHandle bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift);
124 Z3ASTHandle bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift);
125 Z3ASTHandle bvVarArithRightShift(Z3ASTHandle expr, Z3ASTHandle shift);
126
127 Z3ASTHandle notExpr(Z3ASTHandle expr);
128 Z3ASTHandle bvNotExpr(Z3ASTHandle expr);
129 Z3ASTHandle andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
130 Z3ASTHandle bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
131 Z3ASTHandle orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
132 Z3ASTHandle bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
133 Z3ASTHandle iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
134 Z3ASTHandle bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
135 Z3ASTHandle bvSignExtend(Z3ASTHandle src, unsigned width);
136
137 // Array operations
138 Z3ASTHandle writeExpr(Z3ASTHandle array, Z3ASTHandle index,
139 Z3ASTHandle value);
140 Z3ASTHandle readExpr(Z3ASTHandle array, Z3ASTHandle index);
141
142 // ITE-expression constructor
143 Z3ASTHandle iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue,
144 Z3ASTHandle whenFalse);
145
146 // Bitvector length
147 unsigned getBVLength(Z3ASTHandle expr);
148
149 // Bitvector comparison
150 Z3ASTHandle bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
151 Z3ASTHandle bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
152 Z3ASTHandle sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
153 Z3ASTHandle sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
154
155 Z3ASTHandle constructAShrByConstant(Z3ASTHandle expr, unsigned shift,
156 Z3ASTHandle isSigned);
157
158 Z3ASTHandle getInitialArray(const Array *os);
159 Z3ASTHandle getArrayForUpdate(const Array *root, const UpdateNode *un);
160
161 Z3ASTHandle constructActual(ref<Expr> e, int *width_out);
162 Z3ASTHandle construct(ref<Expr> e, int *width_out);
163
164 Z3ASTHandle buildArray(const char *name, unsigned indexWidth,
165 unsigned valueWidth);
166
167 Z3SortHandle getBvSort(unsigned width);
168 Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort);
169 bool autoClearConstructCache;
170 std::string z3LogInteractionFile;
171
172 public:
173 Z3_context ctx;
174 std::unordered_map<const Array *, std::vector<Z3ASTHandle> >
175 constant_array_assertions;
176 Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile);
177 ~Z3Builder();
178
179 Z3ASTHandle getTrue();
180 Z3ASTHandle getFalse();
181 Z3ASTHandle getInitialRead(const Array *os, unsigned index);
182
construct(ref<Expr> e)183 Z3ASTHandle construct(ref<Expr> e) {
184 Z3ASTHandle res = construct(e, 0);
185 if (autoClearConstructCache)
186 clearConstructCache();
187 return res;
188 }
189
clearConstructCache()190 void clearConstructCache() { constructed.clear(); }
191 };
192 }
193
194 #endif /* KLEE_Z3BUILDER_H */
195