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
|
//===-- 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 (!e->isConstant()) {
visited.insert(e);
stack.push_back(e);
}
while (!stack.empty()) {
ref<Expr> top = stack.back();
stack.pop_back();
if (ReadExpr *re = dyn_ref_cast<ReadExpr>(top)) {
// We memoized so can just add to list without worrying about
// repeats.
results.push_back(re);
if (!re->index->isConstant() &&
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 (!un->index->isConstant() &&
visited.insert(un->index).second)
stack.push_back(un->index);
if (!un->value->isConstant() &&
visited.insert(un->value).second)
stack.push_back(un->value);
}
}
}
} else if (!top->isConstant()) {
Expr *e = top.get();
for (unsigned i=0; i<e->getNumKids(); i++) {
ref<Expr> k = e->getKid(i);
if (!k->isConstant() &&
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.isRooted)
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) {}
};
}
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*> &);
|
