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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
//===-- Constraints.cpp ---------------------------------------------------===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#include "klee/Expr/Constraints.h"
#include "klee/Expr/ExprVisitor.h"
#include "klee/Module/KModule.h"
#include "klee/Support/OptionCategories.h"
#include "llvm/IR/Function.h"
#include "llvm/Support/CommandLine.h"
#include <map>
using namespace klee;
namespace {
llvm::cl::opt<bool> RewriteEqualities(
"rewrite-equalities",
llvm::cl::desc("Rewrite existing constraints when an equality with a "
"constant is added (default=true)"),
llvm::cl::init(true),
llvm::cl::cat(SolvingCat));
} // namespace
class ExprReplaceVisitor : public ExprVisitor {
private:
ref<Expr> src, dst;
public:
ExprReplaceVisitor(const ref<Expr> &_src, const ref<Expr> &_dst)
: src(_src), dst(_dst) {}
Action visitExpr(const Expr &e) override {
if (e == *src) {
return Action::changeTo(dst);
}
return Action::doChildren();
}
Action visitExprPost(const Expr &e) override {
if (e == *src) {
return Action::changeTo(dst);
}
return Action::doChildren();
}
};
class ExprReplaceVisitor2 : public ExprVisitor {
private:
const std::map< ref<Expr>, ref<Expr> > &replacements;
public:
explicit ExprReplaceVisitor2(
const std::map<ref<Expr>, ref<Expr>> &_replacements)
: ExprVisitor(true), replacements(_replacements) {}
Action visitExprPost(const Expr &e) override {
auto it = replacements.find(ref<Expr>(const_cast<Expr *>(&e)));
if (it!=replacements.end()) {
return Action::changeTo(it->second);
}
return Action::doChildren();
}
};
bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
ConstraintSet old;
bool changed = false;
std::swap(constraints, old);
for (auto &ce : old) {
ref<Expr> e = visitor.visit(ce);
if (e!=ce) {
addConstraintInternal(e); // enable further reductions
changed = true;
} else {
constraints.push_back(ce);
}
}
return changed;
}
ref<Expr> ConstraintManager::simplifyExpr(const ConstraintSet &constraints,
const ref<Expr> &e) {
if (isa<ConstantExpr>(e))
return e;
std::map< ref<Expr>, ref<Expr> > equalities;
for (auto &constraint : constraints) {
if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
if (isa<ConstantExpr>(ee->left)) {
equalities.insert(std::make_pair(ee->right,
ee->left));
} else {
equalities.insert(
std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool)));
}
} else {
equalities.insert(
std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool)));
}
}
return ExprReplaceVisitor2(equalities).visit(e);
}
void ConstraintManager::addConstraintInternal(const ref<Expr> &e) {
// rewrite any known equalities and split Ands into different conjuncts
switch (e->getKind()) {
case Expr::Constant:
assert(cast<ConstantExpr>(e)->isTrue() &&
"attempt to add invalid (false) constraint");
break;
// split to enable finer grained independence and other optimizations
case Expr::And: {
BinaryExpr *be = cast<BinaryExpr>(e);
addConstraintInternal(be->left);
addConstraintInternal(be->right);
break;
}
case Expr::Eq: {
if (RewriteEqualities) {
// XXX: should profile the effects of this and the overhead.
// traversing the constraints looking for equalities is hardly the
// slowest thing we do, but it is probably nicer to have a
// ConstraintSet ADT which efficiently remembers obvious patterns
// (byte-constant comparison).
BinaryExpr *be = cast<BinaryExpr>(e);
if (isa<ConstantExpr>(be->left)) {
ExprReplaceVisitor visitor(be->right, be->left);
rewriteConstraints(visitor);
}
}
constraints.push_back(e);
break;
}
default:
constraints.push_back(e);
break;
}
}
void ConstraintManager::addConstraint(const ref<Expr> &e) {
ref<Expr> simplified = simplifyExpr(constraints, e);
addConstraintInternal(simplified);
}
ConstraintManager::ConstraintManager(ConstraintSet &_constraints)
: constraints(_constraints) {}
bool ConstraintSet::empty() const { return constraints.empty(); }
klee::ConstraintSet::constraint_iterator ConstraintSet::begin() const {
return constraints.begin();
}
klee::ConstraintSet::constraint_iterator ConstraintSet::end() const {
return constraints.end();
}
size_t ConstraintSet::size() const noexcept { return constraints.size(); }
void ConstraintSet::push_back(const ref<Expr> &e) { constraints.push_back(e); }
|
