klee
ExprUtil.cpp
Go to the documentation of this file.
1//===-- ExprUtil.cpp ------------------------------------------------------===//
2//
3// The KLEE Symbolic Virtual Machine
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===//
9
10#include "klee/Expr/ExprUtil.h"
11#include "klee/Expr/Expr.h"
14
15#include <set>
16
17using namespace klee;
18
20 bool visitUpdates,
21 std::vector< ref<ReadExpr> > &results) {
22 // Invariant: \forall_{i \in stack} !i.isConstant() && i \in visited
23 std::vector< ref<Expr> > stack;
24 ExprHashSet visited;
25 std::set<const UpdateNode *> updates;
26
27 if (!isa<ConstantExpr>(e)) {
28 visited.insert(e);
29 stack.push_back(e);
30 }
31
32 while (!stack.empty()) {
33 ref<Expr> top = stack.back();
34 stack.pop_back();
35
36 if (ReadExpr *re = dyn_cast<ReadExpr>(top)) {
37 // We memoized so can just add to list without worrying about
38 // repeats.
39 results.push_back(re);
40
41 if (!isa<ConstantExpr>(re->index) &&
42 visited.insert(re->index).second)
43 stack.push_back(re->index);
44
45 if (visitUpdates) {
46 // XXX this is probably suboptimal. We want to avoid a potential
47 // explosion traversing update lists which can be quite
48 // long. However, it seems silly to hash all of the update nodes
49 // especially since we memoize all the expr results anyway. So
50 // we take a simple approach of memoizing the results for the
51 // head, which often will be shared among multiple nodes.
52 if (updates.insert(re->updates.head.get()).second) {
53 for (const auto *un = re->updates.head.get(); un;
54 un = un->next.get()) {
55 if (!isa<ConstantExpr>(un->index) &&
56 visited.insert(un->index).second)
57 stack.push_back(un->index);
58 if (!isa<ConstantExpr>(un->value) &&
59 visited.insert(un->value).second)
60 stack.push_back(un->value);
61 }
62 }
63 }
64 } else if (!isa<ConstantExpr>(top)) {
65 Expr *e = top.get();
66 for (unsigned i=0; i<e->getNumKids(); i++) {
67 ref<Expr> k = e->getKid(i);
68 if (!isa<ConstantExpr>(k) &&
69 visited.insert(k).second)
70 stack.push_back(k);
71 }
72 }
73 }
74}
75
77
78namespace klee {
79
81protected:
83 const UpdateList &ul = re.updates;
84
85 // XXX should we memo better than what ExprVisitor is doing for us?
86 for (const auto *un = ul.head.get(); un; un = un->next.get()) {
87 visit(un->index);
88 visit(un->value);
89 }
90
91 if (ul.root->isSymbolicArray())
92 if (results.insert(ul.root).second)
93 objects.push_back(ul.root);
94
95 return Action::doChildren();
96 }
97
98public:
99 std::set<const Array*> results;
100 std::vector<const Array*> &objects;
101
102 SymbolicObjectFinder(std::vector<const Array*> &_objects)
103 : objects(_objects) {}
104};
105
107 const UpdateList &ul = re.updates;
108
109 // FIXME should we memo better than what ExprVisitor is doing for us?
110 for (const auto *un = ul.head.get(); un; un = un->next.get()) {
111 visit(un->index);
112 visit(un->value);
113 }
114
115 if (ul.root->isConstantArray()) {
116 results.insert(ul.root);
117 }
118
119 return Action::doChildren();
120}
121}
122
123template<typename InputIterator>
124void klee::findSymbolicObjects(InputIterator begin,
125 InputIterator end,
126 std::vector<const Array*> &results) {
127 SymbolicObjectFinder of(results);
128 for (; begin!=end; ++begin)
129 of.visit(*begin);
130}
131
133 std::vector<const Array*> &results) {
134 findSymbolicObjects(&e, &e+1, results);
135}
136
137typedef std::vector< ref<Expr> >::iterator A;
138template void klee::findSymbolicObjects<A>(A, A, std::vector<const Array*> &);
139
140typedef std::set< ref<Expr> >::iterator B;
141template void klee::findSymbolicObjects<B>(B, B, std::vector<const Array*> &);
std::vector< ref< Expr > >::iterator A
Definition: ExprUtil.cpp:137
std::set< ref< Expr > >::iterator B
Definition: ExprUtil.cpp:140
bool isConstantArray() const
Definition: Expr.h:525
bool isSymbolicArray() const
Definition: Expr.h:524
ExprVisitor::Action visitRead(const ReadExpr &re)
Definition: ExprUtil.cpp:106
std::set< const Array * > results
Definition: ExprUtil.h:48
static Action doChildren()
Definition: ExprVisitor.h:39
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:26
Class representing symbolic expressions.
Definition: Expr.h:91
virtual unsigned getNumKids() const =0
virtual ref< Expr > getKid(unsigned i) const =0
Class representing a one byte read from an array.
Definition: Expr.h:565
UpdateList updates
Definition: Expr.h:571
Action visitRead(const ReadExpr &re)
Definition: ExprUtil.cpp:82
std::vector< const Array * > & objects
Definition: ExprUtil.cpp:100
SymbolicObjectFinder(std::vector< const Array * > &_objects)
Definition: ExprUtil.cpp:102
std::set< const Array * > results
Definition: ExprUtil.cpp:99
Class representing a complete list of updates into an array.
Definition: Expr.h:539
ref< UpdateNode > head
pointer to the most recent update node
Definition: Expr.h:546
const Array * root
Definition: Expr.h:543
T * get() const
Definition: Ref.h:129
Definition: main.cpp:291
void findSymbolicObjects(ref< Expr > e, std::vector< const Array * > &results)
Definition: ExprUtil.cpp:132
void findReads(ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
Definition: ExprUtil.cpp:19
std::unordered_set< ref< Expr >, klee::util::ExprHash, klee::util::ExprCmp > ExprHashSet
Definition: ExprHashMap.h:39