1 files changed, 127 insertions, 0 deletions
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
new file mode 100644
index 00000000..f74b519f
--- /dev/null
+++ b/lib/Expr/ExprUtil.cpp
@@ -0,0 +1,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*> &);