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
|
//===-- ExprUtil.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/util/ExprUtil.h"
#include "klee/util/ExprHashMap.h"
#include "klee/Expr.h"
#include "klee/util/ExprVisitor.h"
#include <set>
using namespace klee;
void klee::findReads(ref<Expr> e,
bool visitUpdates,
std::vector< ref<ReadExpr> > &results) {
// Invariant: \forall_{i \in stack} !i.isConstant() && i \in visited
std::vector< ref<Expr> > stack;
ExprHashSet visited;
std::set<const UpdateNode *> updates;
if (!isa<ConstantExpr>(e)) {
visited.insert(e);
stack.push_back(e);
}
while (!stack.empty()) {
ref<Expr> top = stack.back();
stack.pop_back();
if (ReadExpr *re = dyn_cast<ReadExpr>(top)) {
// We memoized so can just add to list without worrying about
// repeats.
results.push_back(re);
if (!isa<ConstantExpr>(re->index) &&
visited.insert(re->index).second)
stack.push_back(re->index);
if (visitUpdates) {
// XXX this is probably suboptimal. We want to avoid a potential
// explosion traversing update lists which can be quite
// long. However, it seems silly to hash all of the update nodes
// especially since we memoize all the expr results anyway. So
// we take a simple approach of memoizing the results for the
// head, which often will be shared among multiple nodes.
if (updates.insert(re->updates.head).second) {
for (const UpdateNode *un=re->updates.head; un; un=un->next) {
if (!isa<ConstantExpr>(un->index) &&
visited.insert(un->index).second)
stack.push_back(un->index);
if (!isa<ConstantExpr>(un->value) &&
visited.insert(un->value).second)
stack.push_back(un->value);
}
}
}
} else if (!isa<ConstantExpr>(top)) {
Expr *e = top.get();
for (unsigned i=0; i<e->getNumKids(); i++) {
ref<Expr> k = e->getKid(i);
if (!isa<ConstantExpr>(k) &&
visited.insert(k).second)
stack.push_back(k);
}
}
}
}
///
namespace klee {
class SymbolicObjectFinder : public ExprVisitor {
protected:
Action visitRead(const ReadExpr &re) {
const UpdateList &ul = re.updates;
// XXX should we memo better than what ExprVisitor is doing for us?
for (const UpdateNode *un=ul.head; un; un=un->next) {
visit(un->index);
visit(un->value);
}
if (ul.root->isSymbolicArray())
if (results.insert(ul.root).second)
objects.push_back(ul.root);
return Action::doChildren();
}
public:
std::set<const Array*> results;
std::vector<const Array*> &objects;
SymbolicObjectFinder(std::vector<const Array*> &_objects)
: objects(_objects) {}
};
ExprVisitor::Action ConstantArrayFinder::visitRead(const ReadExpr &re) {
const UpdateList &ul = re.updates;
// FIXME should we memo better than what ExprVisitor is doing for us?
for (const UpdateNode *un = ul.head; un; un = un->next) {
visit(un->index);
visit(un->value);
}
if (ul.root->isConstantArray()) {
results.insert(ul.root);
}
return Action::doChildren();
}
}
template<typename InputIterator>
void klee::findSymbolicObjects(InputIterator begin,
InputIterator end,
std::vector<const Array*> &results) {
SymbolicObjectFinder of(results);
for (; begin!=end; ++begin)
of.visit(*begin);
}
void klee::findSymbolicObjects(ref<Expr> e,
std::vector<const Array*> &results) {
findSymbolicObjects(&e, &e+1, results);
}
typedef std::vector< ref<Expr> >::iterator A;
template void klee::findSymbolicObjects<A>(A, A, std::vector<const Array*> &);
typedef std::set< ref<Expr> >::iterator B;
template void klee::findSymbolicObjects<B>(B, B, std::vector<const Array*> &);
|
