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
|
//===-- 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>
#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;
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:
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 getInitialRead(const Array *os, unsigned index);
ExprHandle construct(ref<Expr> e) {
ExprHandle res = construct(e, 0);
constructed.clear();
return res;
}
};
}
#endif
|
