klee
Z3Builder.h
Go to the documentation of this file.
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"
16
17#include <unordered_map>
18#include <z3.h>
19
20namespace klee {
21
22template <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.
27protected:
29 ::Z3_context context;
30
31private:
32 // To be specialised
33 inline ::Z3_ast as_ast();
34
35public:
36 Z3NodeHandle() : node(NULL), context(NULL) {}
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 };
44 if (node && context) {
45 ::Z3_dec_ref(context, as_ast());
46 }
47 }
49 if (node && context) {
50 ::Z3_inc_ref(context, as_ast());
51 }
52 }
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
77 operator T() const { return node; }
78};
79
80// Specialise for Z3_sort
81template <> 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}
87template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used));
88
89// Specialise for Z3_ast
90template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
92template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used));
93
95
96 friend class Z3Builder;
97
98public:
101 void clear();
102};
103
107
108private:
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);
117 Z3ASTHandle bvExtract(Z3ASTHandle expr, unsigned top, unsigned bottom);
119
120 // logical left and right shift (not arithmetic)
121 Z3ASTHandle bvLeftShift(Z3ASTHandle expr, unsigned shift);
122 Z3ASTHandle bvRightShift(Z3ASTHandle expr, unsigned shift);
126
136
137 // Array operations
139 Z3ASTHandle value);
141
142 // ITE-expression constructor
144 Z3ASTHandle whenFalse);
145
146 // Bitvector length
147 unsigned getBVLength(Z3ASTHandle expr);
148
149 // Bitvector comparison
154
156 Z3ASTHandle isSigned);
157
160
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);
171
172public:
173 Z3_context ctx;
174 std::unordered_map<const Array *, std::vector<Z3ASTHandle> >
178
181 Z3ASTHandle getInitialRead(const Array *os, unsigned index);
182
184 Z3ASTHandle res = construct(e, 0);
187 return res;
188 }
189
191};
192}
193
194#endif /* KLEE_Z3BUILDER_H */
void *__dso_handle __attribute__((__weak__))
Class representing a byte update of an array.
Definition: Expr.h:451
virtual ~Z3ArrayExprHash()
Z3ASTHandle getFalse()
Z3ASTHandle bvSignExtend(Z3ASTHandle src, unsigned width)
Z3ASTHandle bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle construct(ref< Expr > e)
Definition: Z3Builder.h:183
Z3ASTHandle bvVarArithRightShift(Z3ASTHandle expr, Z3ASTHandle shift)
Z3ASTHandle iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift)
Z3ASTHandle buildArray(const char *name, unsigned indexWidth, unsigned valueWidth)
Z3ASTHandle iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue, Z3ASTHandle whenFalse)
Z3ASTHandle bvConst32(unsigned width, uint32_t value)
Z3ASTHandle getInitialArray(const Array *os)
bool autoClearConstructCache
Definition: Z3Builder.h:169
Z3ASTHandle bvZExtConst(unsigned width, uint64_t value)
Z3ASTHandle bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort)
Z3ASTHandle bvExtract(Z3ASTHandle expr, unsigned top, unsigned bottom)
Z3ASTHandle bvMinusOne(unsigned width)
Z3SortHandle getBvSort(unsigned width)
Z3ASTHandle bvNotExpr(Z3ASTHandle expr)
Z3ASTHandle bvOne(unsigned width)
Z3ASTHandle bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
unsigned getBVLength(Z3ASTHandle expr)
Z3ASTHandle eqExpr(Z3ASTHandle a, Z3ASTHandle b)
Z3ASTHandle bvBoolExtract(Z3ASTHandle expr, int bit)
Z3ASTHandle sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle bvRightShift(Z3ASTHandle expr, unsigned shift)
Z3ASTHandle constructAShrByConstant(Z3ASTHandle expr, unsigned shift, Z3ASTHandle isSigned)
Z3ASTHandle writeExpr(Z3ASTHandle array, Z3ASTHandle index, Z3ASTHandle value)
std::unordered_map< const Array *, std::vector< Z3ASTHandle > > constant_array_assertions
Definition: Z3Builder.h:175
Z3ASTHandle bvSExtConst(unsigned width, uint64_t value)
Z3ASTHandle getInitialRead(const Array *os, unsigned index)
Z3ASTHandle bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift)
Z3ASTHandle bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
ExprHashMap< std::pair< Z3ASTHandle, unsigned > > constructed
Definition: Z3Builder.h:105
std::string z3LogInteractionFile
Definition: Z3Builder.h:170
Z3ASTHandle construct(ref< Expr > e, int *width_out)
Z3ASTHandle bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle bvZero(unsigned width)
Z3ASTHandle readExpr(Z3ASTHandle array, Z3ASTHandle index)
Z3ASTHandle bvConst64(unsigned width, uint64_t value)
Z3ASTHandle orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3ASTHandle bvLeftShift(Z3ASTHandle expr, unsigned shift)
void clearConstructCache()
Definition: Z3Builder.h:190
Z3ASTHandle getTrue()
Z3ASTHandle andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs)
Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile)
Z3ASTHandle notExpr(Z3ASTHandle expr)
Z3ASTHandle constructActual(ref< Expr > e, int *width_out)
Z3ArrayExprHash _arr_hash
Definition: Z3Builder.h:106
Z3ASTHandle getArrayForUpdate(const Array *root, const UpdateNode *un)
Z3_context ctx
Definition: Z3Builder.h:173
Z3NodeHandle(const T _node, const ::Z3_context _context)
Definition: Z3Builder.h:37
::Z3_context context
Definition: Z3Builder.h:29
Z3NodeHandle & operator=(const Z3NodeHandle &b)
Definition: Z3Builder.h:53
inline ::Z3_ast as_ast()
Z3NodeHandle(const Z3NodeHandle &b)
Definition: Z3Builder.h:48
Definition: main.cpp:291
Z3NodeHandle< Z3_ast > Z3ASTHandle
Definition: Z3Builder.h:91
Z3NodeHandle< Z3_sort > Z3SortHandle
Definition: Z3Builder.h:86