klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
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/util/ExprUtil.h"
11 #include "klee/util/ExprHashMap.h"
12 
13 #include "klee/Expr.h"
14 
15 #include "klee/util/ExprVisitor.h"
16 
17 #include <set>
18 
19 using namespace klee;
20 
22  bool visitUpdates,
23  std::vector< ref<ReadExpr> > &results) {
24  // Invariant: \forall_{i \in stack} !i.isConstant() && i \in visited
25  std::vector< ref<Expr> > stack;
26  ExprHashSet visited;
27  std::set<const UpdateNode *> updates;
28 
29  if (!isa<ConstantExpr>(e)) {
30  visited.insert(e);
31  stack.push_back(e);
32  }
33 
34  while (!stack.empty()) {
35  ref<Expr> top = stack.back();
36  stack.pop_back();
37 
38  if (ReadExpr *re = dyn_cast<ReadExpr>(top)) {
39  // We memoized so can just add to list without worrying about
40  // repeats.
41  results.push_back(re);
42 
43  if (!isa<ConstantExpr>(re->index) &&
44  visited.insert(re->index).second)
45  stack.push_back(re->index);
46 
47  if (visitUpdates) {
48  // XXX this is probably suboptimal. We want to avoid a potential
49  // explosion traversing update lists which can be quite
50  // long. However, it seems silly to hash all of the update nodes
51  // especially since we memoize all the expr results anyway. So
52  // we take a simple approach of memoizing the results for the
53  // head, which often will be shared among multiple nodes.
54  if (updates.insert(re->updates.head).second) {
55  for (const UpdateNode *un=re->updates.head; un; un=un->next) {
56  if (!isa<ConstantExpr>(un->index) &&
57  visited.insert(un->index).second)
58  stack.push_back(un->index);
59  if (!isa<ConstantExpr>(un->value) &&
60  visited.insert(un->value).second)
61  stack.push_back(un->value);
62  }
63  }
64  }
65  } else if (!isa<ConstantExpr>(top)) {
66  Expr *e = top.get();
67  for (unsigned i=0; i<e->getNumKids(); i++) {
68  ref<Expr> k = e->getKid(i);
69  if (!isa<ConstantExpr>(k) &&
70  visited.insert(k).second)
71  stack.push_back(k);
72  }
73  }
74  }
75 }
76 
78 
79 namespace klee {
80 
82 protected:
83  Action visitRead(const ReadExpr &re) {
84  const UpdateList &ul = re.updates;
85 
86  // XXX should we memo better than what ExprVisitor is doing for us?
87  for (const UpdateNode *un=ul.head; un; un=un->next) {
88  visit(un->index);
89  visit(un->value);
90  }
91 
92  if (ul.root->isSymbolicArray())
93  if (results.insert(ul.root).second)
94  objects.push_back(ul.root);
95 
96  return Action::doChildren();
97  }
98 
99 public:
100  std::set<const Array*> results;
101  std::vector<const Array*> &objects;
102 
103  SymbolicObjectFinder(std::vector<const Array*> &_objects)
104  : objects(_objects) {}
105 };
106 
107 }
108 
109 template<typename InputIterator>
110 void klee::findSymbolicObjects(InputIterator begin,
111  InputIterator end,
112  std::vector<const Array*> &results) {
113  SymbolicObjectFinder of(results);
114  for (; begin!=end; ++begin)
115  of.visit(*begin);
116 }
117 
119  std::vector<const Array*> &results) {
120  findSymbolicObjects(&e, &e+1, results);
121 }
122 
123 typedef std::vector< ref<Expr> >::iterator A;
124 template void klee::findSymbolicObjects<A>(A, A, std::vector<const Array*> &);
125 
126 typedef std::set< ref<Expr> >::iterator B;
127 template void klee::findSymbolicObjects<B>(B, B, std::vector<const Array*> &);
T * get() const
Definition: Ref.h:69
bool isSymbolicArray() const
Definition: Expr.h:641
virtual unsigned getNumKids() const =0
static Action doChildren()
Definition: ExprVisitor.h:39
std::vector< ref< Expr > >::iterator A
Definition: ExprUtil.cpp:123
Action visitRead(const ReadExpr &re)
Definition: ExprUtil.cpp:83
Class representing a complete list of updates into an array.
Definition: Expr.h:655
UpdateList updates
Definition: Expr.h:687
Class representing symbolic expressions.
Definition: Expr.h:88
virtual ref< Expr > getKid(unsigned i) const =0
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
void findReads(ref< Expr > e, bool visitUpdates, std::vector< ref< ReadExpr > > &result)
Definition: ExprUtil.cpp:21
std::set< ref< Expr > >::iterator B
Definition: ExprUtil.cpp:126
std::vector< const Array * > & objects
Definition: ExprUtil.cpp:101
const UpdateNode * next
Definition: Expr.h:577
void findSymbolicObjects(ref< Expr > e, std::vector< const Array * > &results)
Definition: ExprUtil.cpp:118
const Array * root
Definition: Expr.h:659
Class representing a one byte read from an array.
Definition: Expr.h:681
Class representing a byte update of an array.
Definition: Expr.h:569
SymbolicObjectFinder(std::vector< const Array * > &_objects)
Definition: ExprUtil.cpp:103
std::set< const Array * > results
Definition: ExprUtil.cpp:100
std::tr1::unordered_set< ref< Expr >, klee::util::ExprHash, klee::util::ExprCmp > ExprHashSet
Definition: ExprHashMap.h:44
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24