 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
83.9% |
47 / 56 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
89.3% |
50 / 56 |
| |
|
Line Coverage: |
91.1% |
41 / 45 |
| |
 |
|
 |
1 : #include "klee/util/ExprUtil.h"
2 : #include "klee/util/ExprHashMap.h"
3 :
4 : #include "klee/Expr.h"
5 :
6 : #include "klee/util/ExprVisitor.h"
7 :
8 : #include <set>
9 :
10 : using namespace klee;
11 :
12 : void klee::findReads(ref<Expr> e,
13 : bool visitUpdates,
14 19658: std::vector< ref<ReadExpr> > &results) {
15 : // Invariant: \forall_{i \in stack} !i.isConstant() && i \in visited
16 : std::vector< ref<Expr> > stack;
17 19658: ExprHashSet visited;
18 : std::set<const UpdateNode *> updates;
19 :
19658: branch 1 taken
0: branch 2 not taken
20 19658: if (!e.isConstant()) {
21 19658: visited.insert(e);
22 19658: stack.push_back(e);
23 : }
24 :
190596: branch 1 taken
19658: branch 2 taken
25 400850: while (!stack.empty()) {
26 : ref<Expr> top = stack.back();
27 : stack.pop_back();
28 :
58531: branch 0 taken
132065: branch 1 taken
29 190596: if (ReadExpr *re = dyn_ref_cast<ReadExpr>(top)) {
30 : // We memoized so can just add to list without worrying about
31 : // repeats.
32 58531: results.push_back(re);
33 :
8020: branch 1 taken
50511: branch 2 taken
8020: branch 4 taken
0: branch 5 not taken
8020: branch 6 taken
50511: branch 7 taken
34 58531: if (!re->index.isConstant() &&
35 : visited.insert(re->index).second)
36 8020: stack.push_back(re->index);
37 :
58531: branch 0 taken
0: branch 1 not taken
38 58531: if (visitUpdates) {
39 : // XXX this is probably suboptimal. We want to avoid a potential
40 : // explosion traversing update lists which can be quite
41 : // long. However, it seems silly to hash all of the update nodes
42 : // especially since we memoize all the expr results anyway. So
43 : // we take a simple approach of memoizing the results for the
44 : // head, which often will be shared among multiple nodes.
22776: branch 0 taken
35755: branch 1 taken
45 117062: if (updates.insert(re->updates.head).second) {
336207: branch 0 taken
22776: branch 1 taken
46 358983: for (const UpdateNode *un=re->updates.head; un; un=un->next) {
202: branch 1 taken
336005: branch 2 taken
202: branch 4 taken
0: branch 5 not taken
202: branch 6 taken
336005: branch 7 taken
47 336207: if (!un->index.isConstant() &&
48 : visited.insert(un->index).second)
49 202: stack.push_back(un->index);
20: branch 1 taken
336187: branch 2 taken
20: branch 4 taken
0: branch 5 not taken
20: branch 6 taken
336187: branch 7 taken
50 336207: if (!un->value.isConstant() &&
51 : visited.insert(un->value).second)
52 20: stack.push_back(un->value);
53 : }
54 : }
55 : }
132065: branch 1 taken
0: branch 2 not taken
56 132065: } else if (!top.isConstant()) {
57 132065: Expr *e = top.get();
257163: branch 2 taken
132065: branch 3 taken
58 389228: for (unsigned i=0; i<e->getNumKids(); i++) {
59 257163: ref<Expr> k = e->getKid(i);
189741: branch 1 taken
67422: branch 2 taken
162696: branch 4 taken
27045: branch 5 taken
162696: branch 6 taken
94467: branch 7 taken
60 257163: if (!k.isConstant() &&
61 : visited.insert(k).second)
62 162696: stack.push_back(k);
63 : }
64 : }
65 : }
66 19658: }
67 :
68 : ///
69 :
70 : namespace klee {
71 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
2899: branch 6 taken
72 5798: class SymbolicObjectFinder : public ExprVisitor {
73 : protected:
74 14157: Action visitRead(const ReadExpr &re) {
75 14157: const UpdateList &ul = re.updates;
76 :
77 : // XXX should we memo better than what ExprVisitor is doing for us?
63709: branch 0 taken
14157: branch 1 taken
78 77866: for (const UpdateNode *un=ul.head; un; un=un->next) {
79 63709: visit(un->index);
80 63709: visit(un->value);
81 : }
82 :
12755: branch 0 taken
1402: branch 1 taken
83 14157: if (ul.isRooted)
3806: branch 0 taken
8949: branch 1 taken
84 25510: if (results.insert(ul.root).second)
85 3806: objects.push_back(ul.root);
86 :
87 14157: return Action::doChildren();
88 : }
89 :
90 : public:
91 : std::set<const MemoryObject*> results;
92 : std::vector<const MemoryObject*> &objects;
93 :
94 2899: SymbolicObjectFinder(std::vector<const MemoryObject*> &_objects)
95 8697: : objects(_objects) {}
96 : };
97 :
98 : }
99 :
100 : template<typename InputIterator>
101 : void klee::findSymbolicObjects(InputIterator begin,
102 : InputIterator end,
103 2899: std::vector<const MemoryObject *> &results) {
104 2899: SymbolicObjectFinder of(results);
18611: branch 0 taken
18611: branch 1 taken
18611: branch 2 taken
18611: branch 3 taken
12813: branch 4 taken
2899: branch 5 taken
105 18611: for (; begin!=end; ++begin)
106 15712: of.visit(*begin);
107 2899: }
108 :
109 : void klee::findSymbolicObjects(ref<Expr> e,
110 0: std::vector<const MemoryObject *> &results) {
111 0: findSymbolicObjects(&e, &e+1, results);
112 :
113 0: }
114 :
115 : typedef std::vector< ref<Expr> >::iterator A;
116 : template void klee::findSymbolicObjects<A>(A, A, std::vector<const MemoryObject *> &);
117 :
118 : typedef std::set< ref<Expr> >::iterator B;
119 0: template void klee::findSymbolicObjects<B>(B, B, std::vector<const MemoryObject *> &);
Generated: 2009-05-17 22:47 by zcov