1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
//===-- STPBuilder.h --------------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef __UTIL_STPBUILDER_H__
#define __UTIL_STPBUILDER_H__
#include "klee/util/ExprHashMap.h"
#include "klee/util/ArrayExprHash.h"
#include "klee/Config/config.h"
#include <vector>
#define Expr VCExpr
#include <stp/c_interface.h>
#if ENABLE_STPLOG == 1
#include "stp/stplog.h"
#endif
#undef Expr
namespace klee {
class ExprHolder {
friend class ExprHandle;
::VCExpr expr;
unsigned count;
public:
ExprHolder(const ::VCExpr _expr) : expr(_expr), count(0) {}
~ExprHolder() {
if (expr) vc_DeleteExpr(expr);
}
};
class ExprHandle {
ExprHolder *H;
public:
ExprHandle() : H(new ExprHolder(0)) { H->count++; }
ExprHandle(::VCExpr _expr) : H(new ExprHolder(_expr)) { H->count++; }
ExprHandle(const ExprHandle &b) : H(b.H) { H->count++; }
~ExprHandle() { if (--H->count == 0) delete H; }
ExprHandle &operator=(const ExprHandle &b) {
if (--H->count == 0) delete H;
H = b.H;
H->count++;
return *this;
}
operator bool () { return H->expr; }
operator ::VCExpr () { return H->expr; }
};
class STPArrayExprHash : public ArrayExprHash< ::VCExpr > {
friend class STPBuilder;
public:
STPArrayExprHash() {};
virtual ~STPArrayExprHash();
};
class STPBuilder {
::VC vc;
ExprHandle tempVars[4];
ExprHashMap< std::pair<ExprHandle, unsigned> > constructed;
/// optimizeDivides - Rewrite division and reminders by constants
/// into multiplies and shifts. STP should probably handle this for
/// use.
bool optimizeDivides;
STPArrayExprHash _arr_hash;
private:
unsigned getShiftBits(unsigned amount) {
unsigned bits = 1;
amount--;
while (amount >>= 1)
bits++;
return bits;
}
ExprHandle bvOne(unsigned width);
ExprHandle bvZero(unsigned width);
ExprHandle bvMinusOne(unsigned width);
ExprHandle bvConst32(unsigned width, uint32_t value);
ExprHandle bvConst64(unsigned width, uint64_t value);
ExprHandle bvZExtConst(unsigned width, uint64_t value);
ExprHandle bvSExtConst(unsigned width, uint64_t value);
ExprHandle bvBoolExtract(ExprHandle expr, int bit);
ExprHandle bvExtract(ExprHandle expr, unsigned top, unsigned bottom);
ExprHandle eqExpr(ExprHandle a, ExprHandle b);
//logical left and right shift (not arithmetic)
ExprHandle bvLeftShift(ExprHandle expr, unsigned shift);
ExprHandle bvRightShift(ExprHandle expr, unsigned shift);
ExprHandle bvVarLeftShift(ExprHandle expr, ExprHandle shift);
ExprHandle bvVarRightShift(ExprHandle expr, ExprHandle shift);
ExprHandle bvVarArithRightShift(ExprHandle expr, ExprHandle shift);
ExprHandle constructAShrByConstant(ExprHandle expr, unsigned shift,
ExprHandle isSigned);
ExprHandle constructMulByConstant(ExprHandle expr, unsigned width, uint64_t x);
ExprHandle constructUDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
ExprHandle constructSDivByConstant(ExprHandle expr_n, unsigned width, uint64_t d);
::VCExpr getInitialArray(const Array *os);
::VCExpr getArrayForUpdate(const Array *root, const UpdateNode *un);
ExprHandle constructActual(ref<Expr> e, int *width_out);
ExprHandle construct(ref<Expr> e, int *width_out);
::VCExpr buildVar(const char *name, unsigned width);
::VCExpr buildArray(const char *name, unsigned indexWidth, unsigned valueWidth);
public:
STPBuilder(::VC _vc, bool _optimizeDivides=true);
~STPBuilder();
ExprHandle getTrue();
ExprHandle getFalse();
ExprHandle getTempVar(Expr::Width w);
ExprHandle getInitialRead(const Array *os, unsigned index);
ExprHandle construct(ref<Expr> e) {
ExprHandle res = construct(e, 0);
constructed.clear();
return res;
}
};
}
#endif
|
