10 files changed, 1113 insertions, 0 deletions
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
new file mode 100644
index 00000000..19f89a03
--- /dev/null
+++ b/include/klee/util/Assignment.h
@@ -0,0 +1,100 @@
+//===-- Assignment.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_UTIL_ASSIGNMENT_H
+#define KLEE_UTIL_ASSIGNMENT_H
+
+#include <map>
+
+#include "klee/util/ExprEvaluator.h"
+
+// FIXME: Rename?
+
+namespace klee {
+  class Array;
+
+  class Assignment {
+  public:
+    typedef std::map<const Array*, std::vector<unsigned char> > bindings_ty;
+
+    bool allowFreeValues;
+    bindings_ty bindings;
+    
+  public:
+    Assignment(bool _allowFreeValues=false) 
+      : allowFreeValues(_allowFreeValues) {}
+    Assignment(std::vector<const Array*> &objects, 
+               std::vector< std::vector<unsigned char> > &values,
+               bool _allowFreeValues=false) 
+      : allowFreeValues(_allowFreeValues){
+      std::vector< std::vector<unsigned char> >::iterator valIt = 
+        values.begin();
+      for (std::vector<const Array*>::iterator it = objects.begin(),
+             ie = objects.end(); it != ie; ++it) {
+        const Array *os = *it;
+        std::vector<unsigned char> &arr = *valIt;
+        bindings.insert(std::make_pair(os, arr));
+        ++valIt;
+      }
+    }
+    
+    ref<Expr> evaluate(const Array *mo, unsigned index) const;
+    ref<Expr> evaluate(ref<Expr> e);
+
+    template<typename InputIterator>
+    bool satisfies(InputIterator begin, InputIterator end);
+  };
+  
+  class AssignmentEvaluator : public ExprEvaluator {
+    const Assignment &a;
+
+  protected:
+    ref<Expr> getInitialValue(const Array &mo, unsigned index) {
+      return a.evaluate(&mo, index);
+    }
+    
+  public:
+    AssignmentEvaluator(const Assignment &_a) : a(_a) {}    
+  };
+
+  /***/
+
+  inline ref<Expr> Assignment::evaluate(const Array *array, 
+                                        unsigned index) const {
+    bindings_ty::const_iterator it = bindings.find(array);
+    if (it!=bindings.end() && index<it->second.size()) {
+      return ref<Expr>(it->second[index], Expr::Int8);
+    } else {
+      if (allowFreeValues) {
+        return ReadExpr::create(UpdateList(array, true, 0), 
+                                ref<Expr>(index, Expr::Int32));
+      } else {
+        return ref<Expr>(0, Expr::Int8);
+      }
+    }
+  }
+
+  inline ref<Expr> Assignment::evaluate(ref<Expr> e) { 
+    AssignmentEvaluator v(*this);
+    return v.visit(e); 
+  }
+
+  template<typename InputIterator>
+  inline bool Assignment::satisfies(InputIterator begin, InputIterator end) {
+    AssignmentEvaluator v(*this);
+    for (; begin!=end; ++begin) {
+      ref<Expr> res = v.visit(*begin);
+      if (!res.isConstant() || !res.getConstantValue())
+        return false;
+    }
+    return true;
+  }
+}
+
+#endif
diff --git a/include/klee/util/BitArray.h b/include/klee/util/BitArray.h
new file mode 100644
index 00000000..6f887600
--- /dev/null
+++ b/include/klee/util/BitArray.h
@@ -0,0 +1,42 @@
+//===-- BitArray.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_UTIL_BITARRAY_H
+#define KLEE_UTIL_BITARRAY_H
+
+namespace klee {
+
+  // XXX would be nice not to have
+  // two allocations here for allocated
+  // BitArrays
+class BitArray {
+private:
+  uint32_t *bits;
+  
+protected:
+  static uint32_t length(unsigned size) { return (size+31)/32; }
+
+public:
+  BitArray(unsigned size, bool value = false) : bits(new uint32_t[length(size)]) {
+    memset(bits, value?0xFF:0, sizeof(*bits)*length(size));
+  }
+  BitArray(const BitArray &b, unsigned size) : bits(new uint32_t[length(size)]) {
+    memcpy(bits, b.bits, sizeof(*bits)*length(size));
+  }
+  ~BitArray() { delete[] bits; }
+
+  bool get(unsigned idx) { return (bool) ((bits[idx/32]>>(idx&0x1F))&1); }
+  void set(unsigned idx) { bits[idx/32] |= 1<<(idx&0x1F); }
+  void unset(unsigned idx) { bits[idx/32] &= ~(1<<(idx&0x1F)); }
+  void set(unsigned idx, bool value) { if (value) set(idx); else unset(idx); }
+};
+
+} // End klee namespace
+
+#endif
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h
new file mode 100644
index 00000000..ffbda09e
--- /dev/null
+++ b/include/klee/util/Bits.h
@@ -0,0 +1,102 @@
+//===-- Bits.h --------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_UTIL_BITS_H
+#define KLEE_UTIL_BITS_H
+
+#include "llvm/Support/DataTypes.h"
+
+namespace klee {
+  namespace bits32 {
+    // @pre(0 <= N <= 32)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline unsigned maxValueOfNBits(unsigned N) {
+      if (N==0)
+        return 0;
+      return ((unsigned) -1) >> (32 - N);
+    }
+
+    // @pre(0 < N <= 32)
+    inline unsigned truncateToNBits(unsigned x, unsigned N) {
+      return x&(((unsigned) -1) >> (32 - N));
+    }
+
+    inline unsigned withoutRightmostBit(unsigned x) {
+      return x&(x-1);
+    }
+
+    inline unsigned isolateRightmostBit(unsigned x) {
+      return x&-x;
+    }
+
+    inline unsigned isPowerOfTwo(unsigned x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre(withoutRightmostBit(x) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(unsigned x) {
+      unsigned res = 0;
+      if (x&0xFFFF0000) res += 16;
+      if (x&0xFF00FF00) res += 8;
+      if (x&0xF0F0F0F0) res += 4;
+      if (x&0xCCCCCCCC) res += 2;
+      if (x&0xAAAAAAAA) res += 1;
+      return res;
+    } 
+
+    inline unsigned indexOfRightmostBit(unsigned x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+
+  namespace bits64 {
+    // @pre(0 <= N <= 32)
+    // @post(retval = max([truncateToNBits(i,N) for i in naturals()]))
+    inline uint64_t maxValueOfNBits(unsigned N) {
+      if (N==0)
+        return 0;
+      return ((uint64_t) (int64_t) -1) >> (64 - N);
+    }
+    
+    // @pre(0 < N <= 64)
+    inline uint64_t truncateToNBits(uint64_t x, unsigned N) {
+      return x&(((uint64_t) (int64_t) -1) >> (64 - N));
+    }
+
+    inline uint64_t withoutRightmostBit(uint64_t x) {
+      return x&(x-1);
+    }
+
+    inline uint64_t isolateRightmostBit(uint64_t x) {
+      return x&-x;
+    }
+
+    inline uint64_t isPowerOfTwo(uint64_t x) {
+      if (x==0) return 0;
+      return !(x&(x-1));
+    }
+
+    // @pre((x&(x-1)) == 0)
+    // @post((1 << retval) == x)
+    inline unsigned indexOfSingleBit(uint64_t x) {
+      unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32)));
+      if (x&((uint64_t) 0xFFFFFFFF << 32))
+	  res += 32;
+      return res;
+    } 
+
+    inline uint64_t indexOfRightmostBit(uint64_t x) {
+      return indexOfSingleBit(isolateRightmostBit(x));
+    }
+  }
+} // End klee namespace
+
+#endif
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
new file mode 100644
index 00000000..be98942d
--- /dev/null
+++ b/include/klee/util/ExprEvaluator.h
@@ -0,0 +1,39 @@
+//===-- ExprEvaluator.h -----------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPREVALUATOR_H
+#define KLEE_EXPREVALUATOR_H
+
+#include "klee/Expr.h"
+#include "klee/util/ExprVisitor.h"
+
+namespace klee {
+  class ExprEvaluator : public ExprVisitor {
+  protected:
+    Action evalRead(const UpdateList &ul, unsigned index);
+    Action visitRead(const ReadExpr &re);
+      
+    Action protectedDivOperation(const BinaryExpr &e);
+    Action visitUDiv(const UDivExpr &e);
+    Action visitSDiv(const SDivExpr &e);
+    Action visitURem(const URemExpr &e);
+    Action visitSRem(const SRemExpr &e);
+      
+  public:
+    ExprEvaluator() {}
+
+    // override to implement evaluation, this function is called to
+    // get the initial value for a symbolic byte. if the value is
+    // unknown then the user can simply return a ReadExpr at version 0
+    // of this MemoryObject.
+    virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
+  };
+}
+
+#endif
diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h
new file mode 100644
index 00000000..d9f95bff
--- /dev/null
+++ b/include/klee/util/ExprHashMap.h
@@ -0,0 +1,48 @@
+//===-- ExprHashMap.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRHASHMAP_H
+#define KLEE_EXPRHASHMAP_H
+
+#include "klee/Expr.h"
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+
+namespace klee {
+
+  namespace util {
+    struct ExprHash  {
+      unsigned operator()(const ref<Expr> e) const {
+        return e.hash();
+      }
+    };
+    
+    struct ExprCmp {
+      bool operator()(const ref<Expr> &a, const ref<Expr> &b) const {
+        return a==b;
+      }
+    };
+  }
+  
+  template<class T> 
+  class ExprHashMap : 
+
+    public std::tr1::unordered_map<ref<Expr>,
+				   T,
+				   klee::util::ExprHash,
+				   klee::util::ExprCmp> {
+  };
+  
+  typedef std::tr1::unordered_set<ref<Expr>,
+				  klee::util::ExprHash,
+				  klee::util::ExprCmp> ExprHashSet;
+
+}
+
+#endif
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
new file mode 100644
index 00000000..a1961e2b
--- /dev/null
+++ b/include/klee/util/ExprPPrinter.h
@@ -0,0 +1,58 @@
+//===-- ExprPPrinter.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRPPRINTER_H
+#define KLEE_EXPRPPRINTER_H
+
+#include "klee/Expr.h"
+
+namespace klee {
+  class ConstraintManager;
+
+  class ExprPPrinter {
+  protected:
+    ExprPPrinter() {}
+    
+  public:
+    static ExprPPrinter *create(std::ostream &os);
+
+    virtual ~ExprPPrinter() {}
+
+    virtual void setNewline(const std::string &newline) = 0;
+    virtual void reset() = 0;
+    virtual void scan(const ref<Expr> &e) = 0;
+    virtual void print(const ref<Expr> &e, unsigned indent=0) = 0;
+
+    // utility methods
+
+    template<class Container>
+    void scan(Container c) {
+      scan(c.begin(), c.end());
+    }
+
+    template<class InputIterator>
+    void scan(InputIterator it, InputIterator end) {
+      for (; it!=end; ++it)
+        scan(*it);
+    }
+
+    static void printOne(std::ostream &os, const char *message, 
+                         const ref<Expr> &e);
+
+    static void printConstraints(std::ostream &os,
+                                 const ConstraintManager &constraints);
+
+    static void printQuery(std::ostream &os,
+                           const ConstraintManager &constraints,
+                           const ref<Expr> &q);
+  };
+
+}
+
+#endif
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
new file mode 100644
index 00000000..3729b5c2
--- /dev/null
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -0,0 +1,283 @@
+//===-- ExprRangeEvaluator.h ------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRRANGEEVALUATOR_H
+#define KLEE_EXPRRANGEEVALUATOR_H
+
+#include "klee/Expr.h"
+#include "klee/util/Bits.h"
+
+namespace klee {
+
+/*
+class ValueType {
+public:
+  ValueType(); // empty range
+  ValueType(uint64_t value);
+  ValueType(uint64_t min, uint64_t max);
+  
+  bool mustEqual(const uint64_t b);
+  bool mustEqual(const ValueType &b);
+  bool mayEqual(const uint64_t b);  
+  bool mayEqual(const ValueType &b);
+
+  bool isFullRange(unsigned width);
+
+  ValueType set_union(ValueType &);
+  ValueType set_intersection(ValueType &);
+  ValueType set_difference(ValueType &);
+
+  ValueType binaryAnd(ValueType &);
+  ValueType binaryOr(ValueType &);
+  ValueType binaryXor(ValueType &);
+  ValueType concat(ValueType &, unsigned width);
+  ValueType add(ValueType &, unsigned width);
+  ValueType sub(ValueType &, unsigned width);
+  ValueType mul(ValueType &, unsigned width);
+  ValueType udiv(ValueType &, unsigned width);
+  ValueType sdiv(ValueType &, unsigned width);
+  ValueType urem(ValueType &, unsigned width);
+  ValueType srem(ValueType &, unsigned width);
+
+  uint64_t min();
+  uint64_t max();
+  int64_t minSigned(unsigned width);
+  int64_t maxSigned(unsigned width);
+}
+*/
+
+template<class T>
+class ExprRangeEvaluator {
+protected:
+  virtual T getInitialReadRange(const Array &os, T index) = 0;
+
+  T evalRead(const UpdateList &ul, T index);
+
+public:
+  ExprRangeEvaluator() {}
+  virtual ~ExprRangeEvaluator() {}
+
+  T evaluate(const ref<Expr> &e);
+};
+
+template<class T>
+T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
+                                  T index) {
+  T res;
+
+  for (const UpdateNode *un=ul.head; un; un=un->next) {
+    T ui = evaluate(un->index);
+
+    if (ui.mustEqual(index)) {
+      return res.set_union(evaluate(un->value));
+    } else if (ui.mayEqual(index)) {
+      res = res.set_union(evaluate(un->value));
+      if (res.isFullRange(8)) {
+        return res;
+      } 
+    }
+  }
+
+  return res.set_union(getInitialReadRange(*ul.root, index));
+}
+
+template<class T>
+T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) {
+  switch (e.getKind()) {
+  case Expr::Constant:
+    return T(e.getConstantValue());
+
+  case Expr::NotOptimized: 
+    break;
+
+  case Expr::Read: {
+    const ReadExpr *re = static_ref_cast<const ReadExpr>(e);
+    T index = evaluate(re->index);
+
+    assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read");
+
+    return evalRead(re->updates, index);
+  }
+
+  case Expr::Select: {
+    const SelectExpr *se = static_ref_cast<const SelectExpr>(e);
+    T cond = evaluate(se->cond);
+      
+    if (cond.mustEqual(1)) {
+      return evaluate(se->trueExpr);
+    } else if (cond.mustEqual(0)) {
+      return evaluate(se->falseExpr);
+    } else {
+      return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr));
+    }
+  }
+
+    // XXX these should be unrolled to ensure nice inline
+  case Expr::Concat: {
+    const Expr *ep = e.get();
+    T res(0);
+    for (unsigned i=0; i<ep->getNumKids(); i++)
+      res = res.concat(evaluate(ep->getKid(i)),8);
+    return res;
+  }
+
+    // Arithmetic
+
+  case Expr::Add: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).add(evaluate(be->right), width);
+  }
+  case Expr::Sub: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).sub(evaluate(be->right), width);
+  }
+  case Expr::Mul: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).mul(evaluate(be->right), width);
+  }
+  case Expr::UDiv: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).udiv(evaluate(be->right), width);
+  }
+  case Expr::SDiv: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).sdiv(evaluate(be->right), width);
+  }
+  case Expr::URem: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).urem(evaluate(be->right), width);
+  }
+  case Expr::SRem: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    unsigned width = be->left.getWidth();
+    return evaluate(be->left).srem(evaluate(be->right), width);
+  }
+
+    // Binary
+
+  case Expr::And: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryAnd(evaluate(be->right));
+  }
+  case Expr::Or: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryOr(evaluate(be->right));
+  }
+  case Expr::Xor: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    return evaluate(be->left).binaryXor(evaluate(be->right));
+  }
+  case Expr::Shl: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).shl(evaluate(be->right), width);
+    break;
+  }
+  case Expr::LShr: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).lshr(evaluate(be->right), width);
+    break;
+  }
+  case Expr::AShr: {
+    //    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    //    unsigned width = be->left.getWidth();
+    //    return evaluate(be->left).ashr(evaluate(be->right), width);
+    break;
+  }
+
+    // Comparison
+
+  case Expr::Eq: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.mustEqual(right)) {
+      return T(1);
+    } else if (!left.mayEqual(right)) {
+      return T(0);
+    }
+    break;
+  }
+
+  case Expr::Ult: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.max() < right.min()) {
+      return T(1);
+    } else if (left.min() >= right.max()) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Ule: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+      
+    if (left.max() <= right.min()) {
+      return T(1);
+    } else if (left.min() > right.max()) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Slt: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+    unsigned bits = be->left.getWidth();
+
+    if (left.maxSigned(bits) < right.minSigned(bits)) {
+      return T(1);
+    } else if (left.minSigned(bits) >= right.maxSigned(bits)) {
+      return T(0);
+    }
+    break;
+  }
+  case Expr::Sle: {
+    const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e);
+    T left = evaluate(be->left);
+    T right = evaluate(be->right);
+    unsigned bits = be->left.getWidth();
+      
+    if (left.maxSigned(bits) <= right.minSigned(bits)) {
+      return T(1);
+    } else if (left.minSigned(bits) > right.maxSigned(bits)) {
+      return T(0);
+    }
+    break;
+  }
+
+  case Expr::Ne:
+  case Expr::Ugt:
+  case Expr::Uge:
+  case Expr::Sgt:
+  case Expr::Sge:
+    assert(0 && "invalid expressions (uncanonicalized)");
+
+  default:
+    break;
+  }
+
+  return T(0, bits64::maxValueOfNBits(e.getWidth()));
+}
+
+}
+
+#endif
diff --git a/include/klee/util/ExprUtil.h b/include/klee/util/ExprUtil.h
new file mode 100644
index 00000000..a81c299f
--- /dev/null
+++ b/include/klee/util/ExprUtil.h
@@ -0,0 +1,43 @@
+//===-- ExprUtil.h ----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRUTIL_H
+#define KLEE_EXPRUTIL_H
+
+#include <vector>
+
+namespace klee {
+  class Array;
+  class Expr;
+  class ReadExpr;
+  template<typename T> class ref;
+
+  /// Find all ReadExprs used in the expression DAG. If visitUpdates
+  /// is true then this will including those reachable by traversing
+  /// update lists. Note that this may be slow and return a large
+  /// number of results.
+  void findReads(ref<Expr> e, 
+                 bool visitUpdates,
+                 std::vector< ref<ReadExpr> > &result);
+  
+  /// Return a list of all unique symbolic objects referenced by the given
+  /// expression.
+  void findSymbolicObjects(ref<Expr> e,
+                           std::vector<const Array*> &results);
+
+  /// Return a list of all unique symbolic objects referenced by the
+  /// given expression range.
+  template<typename InputIterator>
+  void findSymbolicObjects(InputIterator begin, 
+                           InputIterator end,
+                           std::vector<const Array*> &results);
+
+}
+
+#endif
diff --git a/include/klee/util/ExprVisitor.h b/include/klee/util/ExprVisitor.h
new file mode 100644
index 00000000..8f8617e3
--- /dev/null
+++ b/include/klee/util/ExprVisitor.h
@@ -0,0 +1,95 @@
+//===-- ExprVisitor.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRVISITOR_H
+#define KLEE_EXPRVISITOR_H
+
+#include "ExprHashMap.h"
+
+namespace klee {
+  class ExprVisitor {
+  protected:
+    // typed variant, but non-virtual for efficiency
+    class Action {
+    public:
+      enum Kind { SkipChildren, DoChildren, ChangeTo };
+
+    private:
+      //      Action() {}
+      Action(Kind _kind) 
+        : kind(_kind), argument(0,Expr::Bool) {}
+      Action(Kind _kind, const ref<Expr> &_argument) 
+        : kind(_kind), argument(_argument) {}
+
+      friend class ExprVisitor;
+
+    public:
+      Kind kind;
+      ref<Expr> argument;
+
+      static Action changeTo(const ref<Expr> &expr) { return Action(ChangeTo,expr); }
+      static Action doChildren() { return Action(DoChildren); }
+      static Action skipChildren() { return Action(SkipChildren); }
+    };
+
+  protected:
+    explicit
+    ExprVisitor(bool _recursive=false) : recursive(_recursive) {}
+    virtual ~ExprVisitor() {}
+
+    virtual Action visitExpr(const Expr&);
+    virtual Action visitExprPost(const Expr&);
+
+    virtual Action visitNotOptimized(const NotOptimizedExpr&);
+    virtual Action visitRead(const ReadExpr&);
+    virtual Action visitSelect(const SelectExpr&);
+    virtual Action visitConcat(const ConcatExpr&);
+    virtual Action visitExtract(const ExtractExpr&);
+    virtual Action visitZExt(const ZExtExpr&);
+    virtual Action visitSExt(const SExtExpr&);
+    virtual Action visitAdd(const AddExpr&);
+    virtual Action visitSub(const SubExpr&);
+    virtual Action visitMul(const MulExpr&);
+    virtual Action visitUDiv(const UDivExpr&);
+    virtual Action visitSDiv(const SDivExpr&);
+    virtual Action visitURem(const URemExpr&);
+    virtual Action visitSRem(const SRemExpr&);
+    virtual Action visitAnd(const AndExpr&);
+    virtual Action visitOr(const OrExpr&);
+    virtual Action visitXor(const XorExpr&);
+    virtual Action visitShl(const ShlExpr&);
+    virtual Action visitLShr(const LShrExpr&);
+    virtual Action visitAShr(const AShrExpr&);
+    virtual Action visitEq(const EqExpr&);
+    virtual Action visitNe(const NeExpr&);
+    virtual Action visitUlt(const UltExpr&);
+    virtual Action visitUle(const UleExpr&);
+    virtual Action visitUgt(const UgtExpr&);
+    virtual Action visitUge(const UgeExpr&);
+    virtual Action visitSlt(const SltExpr&);
+    virtual Action visitSle(const SleExpr&);
+    virtual Action visitSgt(const SgtExpr&);
+    virtual Action visitSge(const SgeExpr&);
+
+  private:
+    typedef ExprHashMap< ref<Expr> > visited_ty;
+    visited_ty visited;
+    bool recursive;
+
+    ref<Expr> visitActual(const ref<Expr> &e);
+    
+  public:
+    // apply the visitor to the expression and return a possibly
+    // modified new expression.
+    ref<Expr> visit(const ref<Expr> &e);
+  };
+
+}
+
+#endif
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
new file mode 100644
index 00000000..a70b09cf
--- /dev/null
+++ b/include/klee/util/Ref.h
@@ -0,0 +1,303 @@
+//===-- Ref.h ---------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_REF_H
+#define KLEE_REF_H
+
+#include <assert.h>
+
+class Expr;
+class BinaryExpr;
+class CastExpr;
+class CmpExpr;
+
+class ConstantExpr;
+class ReadExpr;
+class UpdateNode;
+class NotOptimizedExpr;
+class ReadExpr;
+class SelectExpr;
+class ConcatExpr;
+class ExtractExpr;
+class ZExtExpr;
+class SExtExpr;
+class AddExpr;
+class SubExpr;
+class MulExpr;
+class UDivExpr;
+class SDivExpr;
+class URemExpr;
+class SRemExpr;
+class AndExpr;
+class OrExpr;
+class XorExpr;
+class ShlExpr;
+class LShrExpr;
+class AShrExpr;
+class EqExpr;
+class NeExpr;
+class UltExpr;
+class UleExpr;
+class UgtExpr;
+class UgeExpr;
+class SltExpr;
+class SleExpr;
+class SgtExpr;
+class SgeExpr;
+class KModule;
+
+  class ExprVisitor;
+  class StackFrame;
+  class ObjectState;
+
+template<class T>
+class ref {
+public:
+  // default constructor: create a NULL reference
+  ref() : constantWidth(Expr::InvalidWidth) {
+    contents.ptr = 0;
+  }
+
+private:
+  // if NotConstant, not this ref is not a constant.
+  // otherwise, it's the width of the constant.
+  Expr::Width constantWidth;
+  static const Expr::Width NotConstant = (Expr::Width) 0;
+  
+  union {
+    T *ptr;
+    uint64_t val;
+  } contents;
+  
+  void inc() {
+    if (constantWidth == NotConstant &&
+        contents.ptr) {
+      contents.ptr->refCount++;
+    }
+  }
+  
+  void dec() {
+    if (constantWidth == NotConstant &&
+        contents.ptr &&
+        --contents.ptr->refCount == 0) {
+      delete contents.ptr;
+    }
+  }  
+
+  friend class ExprVisitor;
+  friend class Cell;
+  friend class ObjectState;
+  friend class KModule;
+
+public:
+  template<class U> friend class ref;
+  template<class U> friend U* dyn_ref_cast(ref &src);
+  template<class U> friend const U* dyn_ref_cast(const ref &src);
+  template<class U> friend U* static_ref_cast(ref &src);
+  template<class U> friend const U* static_ref_cast(const ref &src);
+
+  // constructor from pointer
+  ref(T *p) : constantWidth(NotConstant) {
+    contents.ptr = p;
+    inc();
+  }
+
+  // construct from constant
+  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+    contents.val = val;
+  }
+  
+  // normal copy constructor
+  ref (const ref<T> &r)
+    : constantWidth(r.constantWidth), contents(r.contents) {
+    inc();
+  }
+  
+  // conversion constructor
+  template<class U>
+  ref (const ref<U> &r) {
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+  }
+  
+  // pointer operations
+  T *get () {
+    // demand(constantWidth == NotConstant, "deref of constant");
+
+    // allocate 
+    if (constantWidth != NotConstant) {
+      contents.ptr = dynamic_cast<T*>(Expr::createConstant(contents.val, constantWidth));
+      assert(contents.ptr && "error with lazy constant initialization");
+      constantWidth = NotConstant;
+      
+      inc();
+    }
+    return contents.ptr;
+  }
+
+  T *get () const {
+    assert(constantWidth == NotConstant && "deref of constant");
+    return contents.ptr;
+  }
+
+  // method calls for the constant optimization
+  bool isConstant() const {
+    if (constantWidth != NotConstant) {
+      return true;
+    } else if (contents.ptr) {
+      return contents.ptr->getKind() == Expr::Constant;
+    } else {
+      return false; // should never happen, but nice check
+    }
+  }
+
+  uint64_t getConstantValue() const {
+    if (constantWidth) {
+      return contents.val;
+    } else {
+      return contents.ptr->getConstantValue();
+    }
+  }
+
+  unsigned hash() const {
+    if (constantWidth) {
+      return Expr::hashConstant(contents.val, constantWidth);
+    } else {
+      return contents.ptr->hash();
+    }
+  }
+
+  unsigned computeHash() const {
+    if (isConstant()) {
+      return Expr::hashConstant(contents.val, constantWidth);
+    } else {
+      return contents.ptr->computeHash();
+    }
+  }
+
+  void rehash() const {
+    if (!isConstant())
+      contents.ptr->computeHash();
+  }
+  
+  Expr::Width getWidth() const {
+    if (constantWidth != NotConstant)
+      return constantWidth;
+    return contents.ptr->getWidth();
+  }
+
+  Expr::Kind getKind() const {
+    if (constantWidth != NotConstant)
+      return Expr::Constant;
+    return contents.ptr->getKind();
+  }
+
+  unsigned getNumKids() const {
+    if (constantWidth != NotConstant)
+      return 0;
+    return contents.ptr->getNumKids();
+  }
+
+  ref<Expr> getKid(unsigned k) {
+    if (constantWidth != NotConstant)
+      return 0;
+    return contents.ptr->getKid(k);
+  }
+
+  ~ref () { dec (); }
+
+  /* The copy assignment operator must also explicitly be defined,
+   * despite a redundant template. */
+  ref<T> &operator= (const ref<T> &r) {
+    dec();
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+    
+    return *this;
+  }
+  
+  template<class U> ref<T> &operator= (const ref<U> &r) {
+    dec();
+    constantWidth = r.constantWidth;
+    contents.val = r.contents.val;
+    inc();
+    
+    return *this;
+  }
+
+  bool isNull() const { return !constantWidth && !contents.ptr; }
+
+  // assumes non-null arguments
+  int compare(const ref &rhs) const {
+    Expr::Kind ak = getKind(), bk = rhs.getKind();
+    if (ak!=bk) 
+      return (ak < bk) ? -1 : 1;
+    if (ak==Expr::Constant) {
+      Expr::Width at = getWidth(), bt = rhs.getWidth();
+      if (at!=bt) 
+        return (at < bt) ? -1 : 1;
+      uint64_t av = getConstantValue(), bv = rhs.getConstantValue();
+      if (av<bv) {
+        return -1;
+      } else if (av>bv) {
+        return 1;
+      } else {
+        return 0;
+      }
+    } else {
+      return get()->compare(*rhs.get());
+    }
+  }
+
+  // assumes non-null arguments
+  bool operator<(const ref &rhs) const { return compare(rhs)<0; }
+  bool operator==(const ref &rhs) const { return compare(rhs)==0; }
+  bool operator!=(const ref &rhs) const { return compare(rhs)!=0; }
+};
+
+
+template<class T>
+inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
+  if (e.isConstant()) {
+    os << e.getConstantValue();
+  } else {
+    os << *e.get();
+  }
+  return os;
+}
+
+template<class U>
+U* dyn_ref_cast(ref<Expr> &src) {
+  if (src.constantWidth != ref<Expr>::NotConstant)
+    return 0;
+    
+  return dynamic_cast<U*>(src.contents.ptr);
+}
+
+template<class U>
+const U* dyn_ref_cast(const ref<Expr> &src) {
+  if (src.constantWidth != ref<Expr>::NotConstant)
+    return 0;
+    
+  return dynamic_cast<const U*>(src.contents.ptr);
+}
+
+template<class U>
+U* static_ref_cast(ref<Expr> &src) {
+  return static_cast<U*>(src.contents.ptr);
+}
+
+template<class U>
+const U* static_ref_cast(const ref<Expr> &src) {
+  return static_cast<const U*>(src.contents.ptr);
+}
+
+#endif /* KLEE_REF_H */