Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

10 files changed, 3922 insertions, 0 deletions

diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
new file mode 100644
index 00000000..e9c376f4
--- /dev/null
+++ b/lib/Expr/Constraints.cpp
@@ -0,0 +1,155 @@
+//===-- Constraints.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/Constraints.h"
+
+#include "klee/util/ExprPPrinter.h"
+#include "klee/util/ExprVisitor.h"
+
+#include <iostream>
+#include <map>
+
+using namespace klee;
+
+class ExprReplaceVisitor : public ExprVisitor {
+private:
+  ref<Expr> src, dst;
+
+public:
+  ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {}
+
+  Action visitExpr(const Expr &e) {
+    if (e == *src.get()) {
+      return Action::changeTo(dst);
+    } else {
+      return Action::doChildren();
+    }
+  }
+
+  Action visitExprPost(const Expr &e) {
+    if (e == *src.get()) {
+      return Action::changeTo(dst);
+    } else {
+      return Action::doChildren();
+    }
+  }
+};
+
+class ExprReplaceVisitor2 : public ExprVisitor {
+private:
+  const std::map< ref<Expr>, ref<Expr> > &replacements;
+
+public:
+  ExprReplaceVisitor2(const std::map< ref<Expr>, ref<Expr> > &_replacements) 
+    : ExprVisitor(true),
+      replacements(_replacements) {}
+
+  Action visitExprPost(const Expr &e) {
+    std::map< ref<Expr>, ref<Expr> >::const_iterator it =
+      replacements.find(ref<Expr>((Expr*) &e));
+    if (it!=replacements.end()) {
+      return Action::changeTo(it->second);
+    } else {
+      return Action::doChildren();
+    }
+  }
+};
+
+bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
+  ConstraintManager::constraints_ty old;
+  bool changed = false;
+
+  constraints.swap(old);
+  for (ConstraintManager::constraints_ty::iterator 
+         it = old.begin(), ie = old.end(); it != ie; ++it) {
+    ref<Expr> &ce = *it;
+    ref<Expr> e = visitor.visit(ce);
+
+    if (e!=ce) {
+      addConstraintInternal(e); // enable further reductions
+      changed = true;
+    } else {
+      constraints.push_back(ce);
+    }
+  }
+
+  return changed;
+}
+
+void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
+  // XXX 
+}
+
+ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
+  if (e.isConstant())
+    return e;
+
+  std::map< ref<Expr>, ref<Expr> > equalities;
+  
+  for (ConstraintManager::constraints_ty::const_iterator 
+         it = constraints.begin(), ie = constraints.end(); it != ie; ++it) {
+    if (const EqExpr *ee = dyn_ref_cast<EqExpr>(*it)) {
+      if (ee->left.isConstant()) {
+        equalities.insert(std::make_pair(ee->right,
+                                         ee->left));
+      } else {
+        equalities.insert(std::make_pair(*it,
+                                         ref<Expr>(1,Expr::Bool)));
+      }
+    } else {
+      equalities.insert(std::make_pair(*it,
+                                       ref<Expr>(1,Expr::Bool)));
+    }
+  }
+
+  return ExprReplaceVisitor2(equalities).visit(e);
+}
+
+void ConstraintManager::addConstraintInternal(ref<Expr> e) {
+  // rewrite any known equalities 
+
+  // XXX should profile the effects of this and the overhead.
+  // traversing the constraints looking for equalities is hardly the
+  // slowest thing we do, but it is probably nicer to have a
+  // ConstraintSet ADT which efficiently remembers obvious patterns
+  // (byte-constant comparison).
+
+  switch (e.getKind()) {
+  case Expr::Constant:
+    assert(e.getConstantValue() && "attempt to add invalid (false) constraint");
+    break;
+    
+    // split to enable finer grained independence and other optimizations
+  case Expr::And: {
+    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    addConstraintInternal(be->left);
+    addConstraintInternal(be->right);
+    break;
+  }
+
+  case Expr::Eq: {
+    BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+    if (be->left.isConstant()) {
+      ExprReplaceVisitor visitor(be->right, be->left);
+      rewriteConstraints(visitor);
+    }
+    constraints.push_back(e);
+    break;
+  }
+    
+  default:
+    constraints.push_back(e);
+    break;
+  }
+}
+
+void ConstraintManager::addConstraint(ref<Expr> e) {
+  e = simplifyExpr(e);
+  addConstraintInternal(e);
+}
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
new file mode 100644
index 00000000..55b9a0a4
--- /dev/null
+++ b/lib/Expr/Expr.cpp
@@ -0,0 +1,1122 @@
+//===-- Expr.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/Expr.h"
+
+
+#include "klee/Machine.h"
+// FIXME: This shouldn't be here.
+//#include "klee/Memory.h"
+#include "llvm/Type.h"
+#include "llvm/DerivedTypes.h"
+#include "llvm/Support/CommandLine.h"
+#include "llvm/Support/Streams.h"
+// FIXME: We shouldn't need this once fast constant support moves into
+// Core. If we need to do arithmetic, we probably want to use APInt.
+#include "klee/Internal/Support/IntEvaluation.h"
+
+#include "klee/util/ExprPPrinter.h"
+
+using namespace klee;
+using namespace llvm;
+
+namespace {
+  cl::opt<bool>
+  ConstArrayOpt("const-array-opt",
+	 cl::init(false),
+	 cl::desc("Enable various optimizations involving all-constant arrays."));
+}
+
+/***/
+
+unsigned Expr::count = 0;
+
+ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
+  UpdateList ul(array, true, 0);
+
+  switch (w) {
+  case Expr::Bool: 
+    return ZExtExpr::create(ReadExpr::create(ul, 
+                                             ref<Expr>(0,kMachinePointerType)),
+                            Expr::Bool);
+  case Expr::Int8: 
+    return ReadExpr::create(ul, 
+                            ref<Expr>(0,kMachinePointerType));
+  case Expr::Int16: 
+    return ConcatExpr::create(ReadExpr::create(ul, 
+                                               ref<Expr>(1,kMachinePointerType)),
+                              ReadExpr::create(ul, 
+                                               ref<Expr>(0,kMachinePointerType)));
+  case Expr::Int32: 
+    return ConcatExpr::create4(ReadExpr::create(ul, 
+                                                ref<Expr>(3,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(2,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(1,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(0,kMachinePointerType)));
+  case Expr::Int64: 
+    return ConcatExpr::create8(ReadExpr::create(ul, 
+                                                ref<Expr>(7,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(6,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(5,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(4,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(3,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(2,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(1,kMachinePointerType)),
+                               ReadExpr::create(ul, 
+                                                ref<Expr>(0,kMachinePointerType)));
+  default: assert(0 && "invalid width");
+  }
+}
+
+// returns 0 if b is structurally equal to *this
+int Expr::compare(const Expr &b) const {
+  if (this == &b) return 0;
+
+  Kind ak = getKind(), bk = b.getKind();
+  if (ak!=bk)
+    return (ak < bk) ? -1 : 1;
+
+  if (hashValue != b.hashValue) 
+    return (hashValue < b.hashValue) ? -1 : 1;
+
+  if (int res = compareContents(b)) 
+    return res;
+
+  unsigned aN = getNumKids();
+  for (unsigned i=0; i<aN; i++)
+    if (int res = getKid(i).compare(b.getKid(i)))
+      return res;
+
+  return 0;
+}
+
+void Expr::printKind(std::ostream &os, Kind k) {
+  switch(k) {
+#define X(C) case C: os << #C; break
+    X(Constant);
+    X(NotOptimized);
+    X(Read);
+    X(Select);
+    X(Concat);
+    X(Extract);
+    X(ZExt);
+    X(SExt);
+    X(Add);
+    X(Sub);
+    X(Mul);
+    X(UDiv);
+    X(SDiv);
+    X(URem);
+    X(SRem);
+    X(And);
+    X(Or);
+    X(Xor);
+    X(Shl);
+    X(LShr);
+    X(AShr);
+    X(Eq);
+    X(Ne);
+    X(Ult);
+    X(Ule);
+    X(Ugt);
+    X(Uge);
+    X(Slt);
+    X(Sle);
+    X(Sgt);
+    X(Sge);
+#undef X
+  default:
+    assert(0 && "invalid kind");
+    }
+}
+
+////////
+//
+// Simple hash functions for various kinds of Exprs
+//
+///////
+
+unsigned Expr::computeHash() {
+  unsigned res = getKind() * Expr::MAGIC_HASH_CONSTANT;
+
+  int n = getNumKids();
+  for (int i = 0; i < n; i++) {
+    res <<= 1;
+    res ^= getKid(i).hash() * Expr::MAGIC_HASH_CONSTANT;
+  }
+  
+  hashValue = res;
+  return hashValue;
+}
+
+unsigned ConstantExpr::computeHash() {
+  hashValue = Expr::hashConstant(asUInt64, width);
+  return hashValue;
+}
+
+unsigned CastExpr::computeHash() {
+  unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT;
+  hashValue = res ^ src.hash() * Expr::MAGIC_HASH_CONSTANT;
+  return hashValue;
+}
+
+unsigned ExtractExpr::computeHash() {
+  unsigned res = offset * Expr::MAGIC_HASH_CONSTANT;
+  res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT;
+  hashValue = res ^ expr.hash() * Expr::MAGIC_HASH_CONSTANT;
+  return hashValue;
+}
+
+unsigned ReadExpr::computeHash() {
+  unsigned res = index.hash() * Expr::MAGIC_HASH_CONSTANT;
+  res ^= updates.hash();
+  hashValue = res;
+  return hashValue;
+}
+
+uint64_t Expr::getConstantValue() const {
+  assert(getKind() == Constant);
+  return static_cast<const ConstantExpr*>(this)->asUInt64;
+}
+
+ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
+  unsigned numArgs = args.size();
+  
+  switch(k) {
+    case NotOptimized:
+      assert(numArgs == 1 && args[0].isExpr() &&
+             "invalid args array for given opcode");
+      return NotOptimizedExpr::create(args[0].expr);
+      
+    case Select:
+      assert(numArgs == 3 && args[0].isExpr() &&
+             args[1].isExpr() && args[2].isExpr() &&
+             "invalid args array for Select opcode");
+      return SelectExpr::create(args[0].expr,
+                                args[1].expr,
+                                args[2].expr);
+
+    case Concat: {
+      assert(numArgs == 2 && args[0].isExpr() && args[1].isExpr() && 
+             "invalid args array for Concat opcode");
+      
+      return ConcatExpr::create(args[0].expr, args[1].expr);
+    }
+      
+#define CAST_EXPR_CASE(T)                                    \
+      case T:                                                \
+        assert(numArgs == 2 &&				     \
+               args[0].isExpr() && args[1].isWidth() &&      \
+               "invalid args array for given opcode");       \
+      return T ## Expr::create(args[0].expr, args[1].width); \
+      
+#define BINARY_EXPR_CASE(T)                                 \
+      case T:                                               \
+        assert(numArgs == 2 &&                              \
+               args[0].isExpr() && args[1].isExpr() &&      \
+               "invalid args array for given opcode");      \
+      return T ## Expr::create(args[0].expr, args[1].expr); \
+
+      CAST_EXPR_CASE(ZExt);
+      CAST_EXPR_CASE(SExt);
+      
+      BINARY_EXPR_CASE(Add);
+      BINARY_EXPR_CASE(Sub);
+      BINARY_EXPR_CASE(Mul);
+      BINARY_EXPR_CASE(UDiv);
+      BINARY_EXPR_CASE(SDiv);
+      BINARY_EXPR_CASE(URem);
+      BINARY_EXPR_CASE(SRem);
+      BINARY_EXPR_CASE(And);
+      BINARY_EXPR_CASE(Or);
+      BINARY_EXPR_CASE(Xor);
+      BINARY_EXPR_CASE(Shl);
+      BINARY_EXPR_CASE(LShr);
+      BINARY_EXPR_CASE(AShr);
+      
+      BINARY_EXPR_CASE(Eq);
+      BINARY_EXPR_CASE(Ne);
+      BINARY_EXPR_CASE(Ult);
+      BINARY_EXPR_CASE(Ule);
+      BINARY_EXPR_CASE(Ugt);
+      BINARY_EXPR_CASE(Uge);
+      BINARY_EXPR_CASE(Slt);
+      BINARY_EXPR_CASE(Sle);
+      BINARY_EXPR_CASE(Sgt);
+      BINARY_EXPR_CASE(Sge);
+
+    case Constant:
+    case Extract:
+    case Read:
+    default:
+      assert(0 && "invalid kind");
+  }
+
+}
+
+
+void Expr::printWidth(std::ostream &os, Width width) {
+  switch(width) {
+  case Expr::Bool: os << "Expr::Bool"; break;
+  case Expr::Int8: os << "Expr::Int8"; break;
+  case Expr::Int16: os << "Expr::Int16"; break;
+  case Expr::Int32: os << "Expr::Int32"; break;
+  case Expr::Int64: os << "Expr::Int64"; break;
+  default: os << "<invalid type: " << (unsigned) width << ">";
+  }
+}
+
+Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
+  switch (t->getTypeID()) {
+  case llvm::Type::IntegerTyID: {
+    Width w = cast<IntegerType>(t)->getBitWidth();
+
+    // should remove this limitation soon
+    if (w == 1 || w == 8 || w == 16 || w == 32 || w == 64)
+      return w;
+    else {
+      assert(0 && "XXX arbitrary bit widths unsupported");
+      abort();
+    }
+  }
+  case llvm::Type::FloatTyID: return Expr::Int32;
+  case llvm::Type::DoubleTyID: return Expr::Int64;
+  case llvm::Type::X86_FP80TyID: return Expr::Int64; // XXX: needs to be fixed
+  case llvm::Type::PointerTyID: return kMachinePointerType;
+  default:
+    cerr << "non-primitive type argument to Expr::getTypeForLLVMType()\n";
+    abort();
+  }
+}
+
+ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
+  return OrExpr::create(Expr::createNot(hyp), conc);
+}
+
+ref<Expr> Expr::createIsZero(ref<Expr> e) {
+  return EqExpr::create(e, ConstantExpr::create(0, e.getWidth()));
+}
+
+ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
+  return ZExtExpr::create(e, kMachinePointerType);
+}
+
+ref<Expr> Expr::createNot(ref<Expr> e) {
+  return createIsZero(e);
+}
+
+ref<Expr> Expr::createPointer(uint64_t v) {
+  return ConstantExpr::create(v, kMachinePointerType);
+}
+
+Expr* Expr::createConstant(uint64_t val, Width w) {
+  Expr *r = new ConstantExpr(val, w);
+  r->computeHash();
+  return r;
+}
+
+void Expr::print(std::ostream &os) const {
+  const ref<Expr> tmp((Expr*)this);
+  ExprPPrinter::printOne(os, "", tmp);
+}
+
+/***/
+
+ref<ConstantExpr> ConstantExpr::fromMemory(void *address, Width width) {
+  switch (width) {
+  case  Expr::Bool: return ConstantExpr::create(*(( uint8_t*) address), width);
+  case  Expr::Int8: return ConstantExpr::create(*(( uint8_t*) address), width);
+  case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width);
+  case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width);
+  case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width);
+  default: assert(0 && "invalid type");
+  }
+}
+
+void ConstantExpr::toMemory(void *address) {
+  switch (width) {
+  case  Expr::Bool: *(( uint8_t*) address) = asUInt64; break;
+  case  Expr::Int8: *(( uint8_t*) address) = asUInt64; break;
+  case Expr::Int16: *((uint16_t*) address) = asUInt64; break;
+  case Expr::Int32: *((uint32_t*) address) = asUInt64; break;
+  case Expr::Int64: *((uint64_t*) address) = asUInt64; break;
+  default: assert(0 && "invalid type");
+  }
+}
+
+/***/
+
+ref<Expr>  NotOptimizedExpr::create(ref<Expr> src) {
+  return NotOptimizedExpr::alloc(src);
+}
+
+ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
+  // rollback index when possible... 
+
+  // XXX this doesn't really belong here... there are basically two
+  // cases, one is rebuild, where we want to optimistically try various
+  // optimizations when the index has changed, and the other is 
+  // initial creation, where we expect the ObjectState to have constructed
+  // a smart UpdateList so it is not worth rescanning.
+
+  const UpdateNode *un = ul.head;
+  for (; un; un=un->next) {
+    ref<Expr> cond = EqExpr::create(index, un->index);
+    
+    if (cond.isConstant()) {
+      if (cond.getConstantValue())
+        return un->value;
+    } else {
+      break;
+    }
+  }
+
+  return ReadExpr::alloc(ul, index);
+}
+
+int ReadExpr::compareContents(const Expr &b) const { 
+  return updates.compare(static_cast<const ReadExpr&>(b).updates);
+}
+
+ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
+  Expr::Width kt = t.getWidth();
+
+  assert(c.getWidth()==Bool && "type mismatch");
+  assert(kt==f.getWidth() && "type mismatch");
+
+  if (c.isConstant()) {
+    return c.getConstantValue() ? t : f;
+  } else if (t==f) {
+    return t;
+  } else if (kt==Expr::Bool) { // c ? t : f  <=> (c and t) or (not c and f)
+    if (t.isConstant()) {      
+      if (t.getConstantValue()) {
+        return OrExpr::create(c, f);
+      } else {
+        return AndExpr::create(Expr::createNot(c), f);
+      }
+    } else if (f.isConstant()) {
+      if (f.getConstantValue()) {
+        return OrExpr::create(Expr::createNot(c), t);
+      } else {
+        return AndExpr::create(c, t);
+      }
+    }
+  }
+  
+  return SelectExpr::alloc(c, t, f);
+}
+
+/***/
+
+
+ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  Expr::Width w = l.getWidth() + r.getWidth();
+  
+  /* Constant folding */
+  if (l.getKind() == Expr::Constant && r.getKind() == Expr::Constant) {
+    // XXX: should fix this constant limitation soon
+    assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
+    
+    uint64_t res = (l.getConstantValue() << r.getWidth()) + r.getConstantValue();
+    return ConstantExpr::create(res, w);
+  }
+
+  // Merge contiguous Extracts
+  if (l.getKind() == Expr::Extract && r.getKind() == Expr::Extract) {
+    const ExtractExpr* ee_left = static_ref_cast<ExtractExpr>(l);
+    const ExtractExpr* ee_right = static_ref_cast<ExtractExpr>(r);
+    if (ee_left->expr == ee_right->expr &&
+	ee_right->offset + ee_right->width == ee_left->offset) {
+      return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
+    }
+  }
+
+  return ConcatExpr::alloc(l, r);
+}
+
+/// Shortcut to concat N kids.  The chain returned is unbalanced to the right
+ref<Expr> ConcatExpr::createN(unsigned n_kids, const ref<Expr> kids[]) {
+  assert(n_kids > 0);
+  if (n_kids == 1)
+    return kids[0];
+  
+  ref<Expr> r = ConcatExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  for (int i=n_kids-3; i>=0; i--)
+    r = ConcatExpr::create(kids[i], r);
+  return r;
+}
+
+/// Shortcut to concat 4 kids.  The chain returned is unbalanced to the right
+ref<Expr> ConcatExpr::create4(const ref<Expr> &kid1, const ref<Expr> &kid2,
+				     const ref<Expr> &kid3, const ref<Expr> &kid4) {
+  return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, kid4)));
+}
+
+/// Shortcut to concat 8 kids.  The chain returned is unbalanced to the right
+ref<Expr> ConcatExpr::create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
+			      const ref<Expr> &kid3, const ref<Expr> &kid4,
+			      const ref<Expr> &kid5, const ref<Expr> &kid6,
+			      const ref<Expr> &kid7, const ref<Expr> &kid8) {
+  return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, 
+			      ConcatExpr::create(kid4, ConcatExpr::create4(kid5, kid6, kid7, kid8)))));
+}
+
+/***/
+
+ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
+  unsigned kw = expr.getWidth();
+  assert(w > 0 && off + w <= kw && "invalid extract");
+  
+  if (w == kw)
+    return expr;
+  else if (expr.isConstant()) {
+    return ConstantExpr::create(ints::trunc(expr.getConstantValue() >> off, w, kw), w);
+  } 
+  else 
+    // Extract(Concat)
+    if (ConcatExpr *ce = dyn_ref_cast<ConcatExpr>(expr)) {
+      // if the extract skips the right side of the concat
+      if (off >= ce->getRight().getWidth())
+	return ExtractExpr::create(ce->getLeft(), off - ce->getRight().getWidth(), w);
+      
+      // if the extract skips the left side of the concat
+      if (off + w <= ce->getRight().getWidth())
+	return ExtractExpr::create(ce->getRight(), off, w);
+
+      // E(C(x,y)) = C(E(x), E(y))
+      return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1).getWidth() + off),
+				ExtractExpr::create(ce->getKid(1), off, ce->getKid(1).getWidth() - off));
+    }
+  
+  return ExtractExpr::alloc(expr, off, w);
+}
+
+
+ref<Expr> ExtractExpr::createByteOff(ref<Expr> expr, unsigned offset, Width bits) {
+  return ExtractExpr::create(expr, 8*offset, bits);
+}
+
+/***/
+
+ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
+  unsigned kBits = e.getWidth();
+  if (w == kBits) {
+    return e;
+  } else if (w < kBits) { // trunc
+    return ExtractExpr::createByteOff(e, 0, w);
+  } else {
+    if (e.isConstant()) {
+      return ConstantExpr::create(ints::zext(e.getConstantValue(), w, kBits),
+                                  w);
+    }
+    
+    return ZExtExpr::alloc(e, w);
+  }
+}
+
+ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
+  unsigned kBits = e.getWidth();
+  if (w == kBits) {
+    return e;
+  } else if (w < kBits) { // trunc
+    return ExtractExpr::createByteOff(e, 0, w);
+  } else {
+    if (e.isConstant()) {
+      return ConstantExpr::create(ints::sext(e.getConstantValue(), w, kBits),
+                                  w);
+    }
+    
+    return SExtExpr::alloc(e, w);
+  }
+}
+
+/***/
+
+static ref<Expr> AndExpr_create(Expr *l, Expr *r);
+static ref<Expr> XorExpr_create(Expr *l, Expr *r);
+
+static ref<Expr> EqExpr_createPartial(Expr *l, const ref<Expr> &cr);
+static ref<Expr> AndExpr_createPartialR(const ref<Expr> &cl, Expr *r);
+static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r);
+static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r);
+
+static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  assert(cl.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cl.getConstantValue();
+  Expr::Width type = cl.getWidth();
+
+  if (type==Expr::Bool) {
+    return XorExpr_createPartialR(cl, r);
+  } else if (!value) {
+    return r;
+  } else {
+    Expr::Kind rk = r->getKind();
+    if (rk==Expr::Add && r->getKid(0).isConstant()) { // A + (B+c) == (A+B) + c
+      return AddExpr::create(AddExpr::create(cl, r->getKid(0)),
+                             r->getKid(1));
+    } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // A + (B-c) == (A+B) - c
+      return SubExpr::create(AddExpr::create(cl, r->getKid(0)),
+                             r->getKid(1));
+    } else {
+      return AddExpr::alloc(cl, r);
+    }
+  }
+}
+static ref<Expr> AddExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  return AddExpr_createPartialR(cr, l);
+}
+static ref<Expr> AddExpr_create(Expr *l, Expr *r) {
+  Expr::Width type = l->getWidth();
+
+  if (type == Expr::Bool) {
+    return XorExpr_create(l, r);
+  } else {
+    Expr::Kind lk = l->getKind(), rk = r->getKind();
+    if (lk==Expr::Add && l->getKid(0).isConstant()) { // (k+a)+b = k+(a+b)
+      return AddExpr::create(l->getKid(0),
+                             AddExpr::create(l->getKid(1), r));
+    } else if (lk==Expr::Sub && l->getKid(0).isConstant()) { // (k-a)+b = k+(b-a)
+      return AddExpr::create(l->getKid(0),
+                             SubExpr::create(r, l->getKid(1)));
+    } else if (rk==Expr::Add && r->getKid(0).isConstant()) { // a + (k+b) = k+(a+b)
+      return AddExpr::create(r->getKid(0),
+                             AddExpr::create(l, r->getKid(1)));
+    } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // a + (k-b) = k+(a-b)
+      return AddExpr::create(r->getKid(0),
+                             SubExpr::create(l, r->getKid(1)));
+    } else {
+      return AddExpr::alloc(l, r);
+    }
+  }  
+}
+
+static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  assert(cl.isConstant() && "non-constant passed in place of constant");
+  Expr::Width type = cl.getWidth();
+
+  if (type==Expr::Bool) {
+    return XorExpr_createPartialR(cl, r);
+  } else {
+    Expr::Kind rk = r->getKind();
+    if (rk==Expr::Add && r->getKid(0).isConstant()) { // A - (B+c) == (A-B) - c
+      return SubExpr::create(SubExpr::create(cl, r->getKid(0)),
+                             r->getKid(1));
+    } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // A - (B-c) == (A-B) + c
+      return AddExpr::create(SubExpr::create(cl, r->getKid(0)),
+                             r->getKid(1));
+    } else {
+      return SubExpr::alloc(cl, r);
+    }
+  }
+}
+static ref<Expr> SubExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  assert(cr.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cr.getConstantValue();
+  Expr::Width width = cr.getWidth();
+  uint64_t nvalue = ints::sub(0, value, width);
+
+  return AddExpr_createPartial(l, ConstantExpr::create(nvalue, width));
+}
+static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
+  Expr::Width type = l->getWidth();
+
+  if (type == Expr::Bool) {
+    return XorExpr_create(l, r);
+  } else if (*l==*r) {
+    return ref<Expr>(0, type);
+  } else {
+    Expr::Kind lk = l->getKind(), rk = r->getKind();
+    if (lk==Expr::Add && l->getKid(0).isConstant()) { // (k+a)-b = k+(a-b)
+      return AddExpr::create(l->getKid(0),
+                             SubExpr::create(l->getKid(1), r));
+    } else if (lk==Expr::Sub && l->getKid(0).isConstant()) { // (k-a)-b = k-(a+b)
+      return SubExpr::create(l->getKid(0),
+                             AddExpr::create(l->getKid(1), r));
+    } else if (rk==Expr::Add && r->getKid(0).isConstant()) { // a - (k+b) = (a-c) - k
+      return SubExpr::create(SubExpr::create(l, r->getKid(1)),
+                             r->getKid(0));
+    } else if (rk==Expr::Sub && r->getKid(0).isConstant()) { // a - (k-b) = (a+b) - k
+      return SubExpr::create(AddExpr::create(l, r->getKid(1)),
+                             r->getKid(0));
+    } else {
+      return SubExpr::alloc(l, r);
+    }
+  }  
+}
+
+static ref<Expr> MulExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  assert(cl.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cl.getConstantValue();
+  Expr::Width type = cl.getWidth();
+
+  if (type == Expr::Bool) {
+    return AndExpr_createPartialR(cl, r);
+  } else if (value == 1) {
+    return r;
+  } else if (!value) {
+    return cl;
+  } else {
+    return MulExpr::alloc(cl, r);
+  }
+}
+static ref<Expr> MulExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  return MulExpr_createPartialR(cr, l);
+}
+static ref<Expr> MulExpr_create(Expr *l, Expr *r) {
+  Expr::Width type = l->getWidth();
+  
+  if (type == Expr::Bool) {
+    return AndExpr::alloc(l, r);
+  } else {
+    return MulExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> AndExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  assert(cr.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cr.getConstantValue();
+  Expr::Width width = cr.getWidth();;
+
+  if (value==ints::sext(1, width, 1)) {
+    return l;
+  } else if (!value) {
+    return cr;
+  } else {
+    return AndExpr::alloc(l, cr);
+  }
+}
+static ref<Expr> AndExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  return AndExpr_createPartial(r, cl);
+}
+static ref<Expr> AndExpr_create(Expr *l, Expr *r) {
+  return AndExpr::alloc(l, r);
+}
+
+static ref<Expr> OrExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  assert(cr.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cr.getConstantValue();
+  Expr::Width width = cr.getWidth();
+
+  if (value == ints::sext(1, width, 1)) {
+    return cr;
+  } else if (!value) {
+    return l;
+  } else {
+    return OrExpr::alloc(l, cr);
+  }
+}
+static ref<Expr> OrExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  return OrExpr_createPartial(r, cl);
+}
+static ref<Expr> OrExpr_create(Expr *l, Expr *r) {
+  return OrExpr::alloc(l, r);
+}
+
+static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+  assert(cl.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cl.getConstantValue();
+  Expr::Width type = cl.getWidth();
+
+  if (type==Expr::Bool) {
+    if (value) {
+      return EqExpr_createPartial(r, ConstantExpr::create(0, Expr::Bool));
+    } else {
+      return r;
+    }
+  } else if (!value) {
+    return r;
+  } else {
+    return XorExpr::alloc(cl, r);
+  }
+}
+
+static ref<Expr> XorExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+  return XorExpr_createPartialR(cr, l);
+}
+static ref<Expr> XorExpr_create(Expr *l, Expr *r) {
+  return XorExpr::alloc(l, r);
+}
+
+static ref<Expr> UDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // r must be 1
+    return l;
+  } else{
+    return UDivExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> SDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // r must be 1
+    return l;
+  } else{
+    return SDivExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> URemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // r must be 1
+    return ConstantExpr::create(0, Expr::Bool);
+  } else{
+    return URemExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // r must be 1
+    return ConstantExpr::create(0, Expr::Bool);
+  } else{
+    return SRemExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // l & !r
+    return AndExpr::create(l, Expr::createNot(r));
+  } else{
+    return ShlExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // l & !r
+    return AndExpr::create(l, Expr::createNot(r));
+  } else{
+    return LShrExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // l
+    return l;
+  } else{
+    return AShrExpr::alloc(l, r);
+  }
+}
+
+#define BCREATE_R(_e_op, _op, partialL, partialR) \
+ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
+  assert(l.getWidth()==r.getWidth() && "type mismatch"); \
+  if (l.isConstant()) {                                \
+    if (r.isConstant()) {                              \
+      Expr::Width width = l.getWidth(); \
+      uint64_t val = ints::_op(l.getConstantValue(),  \
+                               r.getConstantValue(), width);  \
+      return ConstantExpr::create(val, width); \
+    } else { \
+      return _e_op ## _createPartialR(l, r.get()); \
+    } \
+  } else if (r.isConstant()) {             \
+    return _e_op ## _createPartial(l.get(), r); \
+  } \
+  return _e_op ## _create(l.get(), r.get()); \
+}
+
+#define BCREATE(_e_op, _op) \
+ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
+  assert(l.getWidth()==r.getWidth() && "type mismatch"); \
+  if (l.isConstant()) {                                \
+    if (r.isConstant()) {                              \
+      Expr::Width width = l.getWidth(); \
+      uint64_t val = ints::_op(l.getConstantValue(), \
+                               r.getConstantValue(), width);  \
+      return ConstantExpr::create(val, width); \
+    } \
+  } \
+  return _e_op ## _create(l, r);                    \
+}
+
+BCREATE_R(AddExpr, add, AddExpr_createPartial, AddExpr_createPartialR)
+BCREATE_R(SubExpr, sub, SubExpr_createPartial, SubExpr_createPartialR)
+BCREATE_R(MulExpr, mul, MulExpr_createPartial, MulExpr_createPartialR)
+BCREATE_R(AndExpr, land, AndExpr_createPartial, AndExpr_createPartialR)
+BCREATE_R(OrExpr, lor, OrExpr_createPartial, OrExpr_createPartialR)
+BCREATE_R(XorExpr, lxor, XorExpr_createPartial, XorExpr_createPartialR)
+BCREATE(UDivExpr, udiv)
+BCREATE(SDivExpr, sdiv)
+BCREATE(URemExpr, urem)
+BCREATE(SRemExpr, srem)
+BCREATE(ShlExpr, shl)
+BCREATE(LShrExpr, lshr)
+BCREATE(AShrExpr, ashr)
+
+#define CMPCREATE(_e_op, _op) \
+ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
+  assert(l.getWidth()==r.getWidth() && "type mismatch"); \
+  if (l.isConstant()) {                                \
+    if (r.isConstant()) {                              \
+      Expr::Width width = l.getWidth(); \
+      uint64_t val = ints::_op(l.getConstantValue(), \
+                               r.getConstantValue(), width);  \
+      return ConstantExpr::create(val, Expr::Bool); \
+    } \
+  } \
+  return _e_op ## _create(l, r);                    \
+}
+
+#define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \
+ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
+  assert(l.getWidth()==r.getWidth() && "type mismatch"); \
+  if (l.isConstant()) {                                \
+    if (r.isConstant()) {                              \
+      Expr::Width width = l.getWidth(); \
+      uint64_t val = ints::_op(l.getConstantValue(), \
+                               r.getConstantValue(), width);  \
+      return ConstantExpr::create(val, Expr::Bool); \
+    } else { \
+      return partialR(l, r.get()); \
+    } \
+  } else if (r.isConstant()) {                  \
+    return partialL(l.get(), r); \
+  } else { \
+    return _e_op ## _create(l.get(), r.get()); \
+  } \
+}
+  
+
+static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l == r) {
+    return ref<Expr>(1, Expr::Bool);
+  } else {
+    return EqExpr::alloc(l, r);
+  }
+}
+
+
+/// Tries to optimize EqExpr cl == rd, where cl is a ConstantExpr and
+/// rd a ReadExpr.  If rd is a read into an all-constant array,
+/// returns a disjunction of equalities on the index.  Otherwise,
+/// returns the initial equality expression. 
+static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl, 
+				  ReadExpr *rd) {
+  assert(cl.isConstant() && "constant expression required");
+  assert(rd->getKind() == Expr::Read && "read expression required");
+  
+  uint64_t ct = cl.getConstantValue();
+  ref<Expr> first_idx_match;
+
+  // number of positions in the array that contain value ct
+  unsigned matches = 0;
+
+  //llvm::cerr << "Size updates/root: " << rd->updates.getSize() << " / " << (rd->updates.root)->size << "\n";
+
+  // for now, just assume standard "flushing" of a concrete array,
+  // where the concrete array has one update for each index, in order
+  bool all_const = true;
+  if (rd->updates.getSize() == rd->updates.root->size) {
+    unsigned k = rd->updates.getSize();
+    for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
+      assert(k > 0);
+      k--;
+
+      ref<Expr> idx = un->index;
+      ref<Expr> val = un->value;
+      if (!idx.isConstant() || !val.isConstant()) {
+	all_const = false;
+	//llvm::cerr << "Idx or val not constant\n";
+	break;
+      }
+      else {
+	if (idx.getConstantValue() != k) {
+	  all_const = false;
+	  //llvm::cerr << "Wrong constant\n";
+	  break;
+	}
+	if (val.getConstantValue() == ct) {
+	  matches++;
+	  if (matches == 1)
+	    first_idx_match = un->index;
+	}
+      }
+    }
+  }
+  else all_const = false;
+  
+  if (all_const && matches <= 100) {
+    // apply optimization
+    //llvm::cerr << "\n\n=== Applying const array optimization ===\n\n";
+
+    if (matches == 0)
+      return ref<Expr>(0, Expr::Bool);
+
+    ref<Expr> res = EqExpr::create(first_idx_match, rd->index);
+    if (matches == 1)
+      return res;
+    
+    for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
+      if (un->index != first_idx_match && un->value.getConstantValue() == ct) {
+	ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
+	res = OrExpr::create(curr_eq, res);
+      }
+    }
+    
+    return res;
+  }
+
+  return EqExpr_create(cl, ref<Expr>(rd));
+}
+
+
+static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {  
+  assert(cl.isConstant() && "non-constant passed in place of constant");
+  uint64_t value = cl.getConstantValue();
+  Expr::Width width = cl.getWidth();
+
+  Expr::Kind rk = r->getKind();
+  if (width == Expr::Bool) {
+    if (value) {
+      return r;
+    } else {
+      // 0 != ...
+      
+      if (rk == Expr::Eq) {
+        const EqExpr *ree = static_ref_cast<EqExpr>(r);
+
+        // eliminate double negation
+        if (ree->left.isConstant() &&
+            ree->left.getWidth()==Expr::Bool) {
+          assert(!ree->left.getConstantValue());
+          return ree->right;
+        }
+      } else if (rk == Expr::Or) {
+        const OrExpr *roe = static_ref_cast<OrExpr>(r);
+
+        // transform not(or(a,b)) to and(not a, not b)
+        return AndExpr::create(Expr::createNot(roe->left),
+                               Expr::createNot(roe->right));
+      }
+    }
+  } else if (rk == Expr::SExt) {
+    // (sext(a,T)==c) == (a==c)
+    const SExtExpr *see = static_ref_cast<SExtExpr>(r);
+    Expr::Width fromBits = see->src.getWidth();
+    uint64_t trunc = bits64::truncateToNBits(value, fromBits);
+
+    // pathological check, make sure it is possible to
+    // sext to this value *from any value*
+    if (value == ints::sext(trunc, width, fromBits)) {
+      return EqExpr::create(see->src, ConstantExpr::create(trunc, fromBits));
+    } else {
+      return ConstantExpr::create(0, Expr::Bool);
+    }
+  } else if (rk == Expr::ZExt) {
+    // (zext(a,T)==c) == (a==c)
+    const ZExtExpr *zee = static_ref_cast<ZExtExpr>(r);
+    Expr::Width fromBits = zee->src.getWidth();
+    uint64_t trunc = bits64::truncateToNBits(value, fromBits);
+    
+    // pathological check, make sure it is possible to
+    // zext to this value *from any value*
+    if (value == ints::zext(trunc, width, fromBits)) {
+      return EqExpr::create(zee->src, ConstantExpr::create(trunc, fromBits));
+    } else {
+      return ConstantExpr::create(0, Expr::Bool);
+    }
+  } else if (rk==Expr::Add) {
+    const AddExpr *ae = static_ref_cast<AddExpr>(r);
+    if (ae->left.isConstant()) {
+      // c0 = c1 + b => c0 - c1 = b
+      return EqExpr_createPartialR(SubExpr::create(cl, ae->left),
+                                   ae->right.get());
+    }
+  } else if (rk==Expr::Sub) {
+    const SubExpr *se = static_ref_cast<SubExpr>(r);
+    if (se->left.isConstant()) {
+      // c0 = c1 - b => c1 - c0 = b
+      return EqExpr_createPartialR(SubExpr::create(se->left, cl),
+                                   se->right.get());
+    }
+  } else if (rk == Expr::Read && ConstArrayOpt) {
+    return TryConstArrayOpt(cl, static_cast<ReadExpr*>(r));
+  }
+    
+  return EqExpr_create(cl, r);
+}
+
+static ref<Expr> EqExpr_createPartial(Expr *l, const ref<Expr> &cr) {  
+  return EqExpr_createPartialR(cr, l);
+}
+  
+ref<Expr> NeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  return EqExpr::create(ConstantExpr::create(0, Expr::Bool),
+                        EqExpr::create(l, r));
+}
+
+ref<Expr> UgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  return UltExpr::create(r, l);
+}
+ref<Expr> UgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  return UleExpr::create(r, l);
+}
+
+ref<Expr> SgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  return SltExpr::create(r, l);
+}
+ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
+  return SleExpr::create(r, l);
+}
+
+static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  Expr::Width t = l.getWidth();
+  if (t == Expr::Bool) { // !l && r
+    return AndExpr::create(Expr::createNot(l), r);
+  } else {
+    if (r.isConstant()) {      
+      uint64_t value = r.getConstantValue();
+      if (value <= 8) {
+        ref<Expr> res(0,Expr::Bool);
+        for (unsigned i=0; i<value; i++) {
+          res = OrExpr::create(EqExpr::create(l, ref<Expr>(i,t)), res);
+        }
+        //        llvm::cerr << l << "<" << r << "  <=>  " << res << "\n";
+        return res;
+      }
+    }
+    return UltExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // !(l && !r)
+    return OrExpr::create(Expr::createNot(l), r);
+  } else {
+    return UleExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // l && !r
+    return AndExpr::create(l, Expr::createNot(r));
+  } else {
+    return SltExpr::alloc(l, r);
+  }
+}
+
+static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
+  if (l.getWidth() == Expr::Bool) { // !(!l && r)
+    return OrExpr::create(l, Expr::createNot(r));
+  } else {
+    return SleExpr::alloc(l, r);
+  }
+}
+
+CMPCREATE_T(EqExpr, eq, EqExpr, EqExpr_createPartial, EqExpr_createPartialR)
+CMPCREATE(UltExpr, ult)
+CMPCREATE(UleExpr, ule)
+CMPCREATE(SltExpr, slt)
+CMPCREATE(SleExpr, sle)
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
new file mode 100644
index 00000000..102387e1
--- /dev/null
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -0,0 +1,74 @@
+//===-- ExprEvaluator.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/ExprEvaluator.h"
+
+using namespace klee;
+
+ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
+                                            unsigned index) {
+  for (const UpdateNode *un=ul.head; un; un=un->next) {
+    ref<Expr> ui = visit(un->index);
+    
+    if (ui.isConstant()) {
+      if (ui.getConstantValue() == index)
+        return Action::changeTo(visit(un->value));
+    } else {
+      // update index is unknown, so may or may not be index, we
+      // cannot guarantee value. we can rewrite to read at this
+      // version though (mostly for debugging).
+      
+      UpdateList fwd(ul.root, un, 0);
+      return Action::changeTo(ReadExpr::create(fwd, 
+                                               ref<Expr>(index,Expr::Int32)));
+    }
+  }
+  
+  return Action::changeTo(getInitialValue(*ul.root, index));
+}
+
+ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
+  ref<Expr> v = visit(re.index);
+  
+  if (v.isConstant()) {
+    return evalRead(re.updates, v.getConstantValue());
+  } else {
+    return Action::doChildren();
+  }
+}
+
+// we need to check for div by zero during partial evaluation,
+// if this occurs then simply ignore the 0 divisor and use the
+// original expression.
+ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
+  ref<Expr> kids[2] = { visit(e.left),
+                        visit(e.right) };
+
+  if (kids[1].isConstant() && !kids[1].getConstantValue())
+    kids[1] = e.right;
+
+  if (kids[0]!=e.left || kids[1]!=e.right) {
+    return Action::changeTo(e.rebuild(kids));
+  } else {
+    return Action::skipChildren();
+  }
+}
+
+ExprVisitor::Action ExprEvaluator::visitUDiv(const UDivExpr &e) { 
+  return protectedDivOperation(e); 
+}
+ExprVisitor::Action ExprEvaluator::visitSDiv(const SDivExpr &e) { 
+  return protectedDivOperation(e); 
+}
+ExprVisitor::Action ExprEvaluator::visitURem(const URemExpr &e) { 
+  return protectedDivOperation(e); 
+}
+ExprVisitor::Action ExprEvaluator::visitSRem(const SRemExpr &e) { 
+  return protectedDivOperation(e); 
+}
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
new file mode 100644
index 00000000..dc7f4f64
--- /dev/null
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -0,0 +1,478 @@
+//===-- ExprPPrinter.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/ExprPPrinter.h"
+
+#include "klee/Constraints.h"
+
+#include "llvm/Support/CommandLine.h"
+
+#include <map>
+#include <vector>
+#include <iostream>
+#include <sstream>
+#include <iomanip>
+
+using namespace klee;
+
+namespace {
+  llvm::cl::opt<bool>
+  PCWidthAsArg("pc-width-as-arg", llvm::cl::init(true));
+
+  llvm::cl::opt<bool>
+  PCAllWidths("pc-all-widths", llvm::cl::init(false));
+
+  llvm::cl::opt<bool>
+  PCPrefixWidth("pc-prefix-width", llvm::cl::init(true));
+
+  llvm::cl::opt<bool>
+  PCMultibyteReads("pc-multibyte-reads", llvm::cl::init(true));
+
+  llvm::cl::opt<bool>
+  PCAllConstWidths("pc-all-const-widths",  llvm::cl::init(false));
+}
+
+/// PrintContext - Helper class for storing extra information for
+/// the pretty printer.
+class PrintContext {
+private:
+  std::ostream &os;
+  std::stringstream ss;
+  std::string newline;
+
+public:
+  /// Number of characters on the current line.
+  unsigned pos;
+
+public:
+  PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void breakLine(unsigned indent=0) {
+    os << newline;
+    if (indent)
+      os << std::setw(indent) << ' ';
+    pos = indent;
+  }
+
+  /// write - Output a string to the stream and update the
+  /// position. The stream should not have any newlines.
+  void write(const std::string &s) {
+    os << s;
+    pos += s.length();
+  }
+
+  template <typename T>
+  PrintContext &operator<<(T elt) {
+    ss.str("");
+    ss << elt;
+    write(ss.str());
+    return *this;
+  }
+};
+
+class PPrinter : public ExprPPrinter {
+  std::map<ref<Expr>, unsigned> bindings;
+  std::map<const UpdateNode*, unsigned> updateBindings;
+  std::set< ref<Expr> > couldPrint, shouldPrint;
+  std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
+  std::ostream &os;
+  unsigned counter;
+  unsigned updateCounter;
+  bool hasScan;
+  std::string newline;
+
+  /// shouldPrintWidth - Predicate for whether this expression should
+  /// be printed with its width.
+  bool shouldPrintWidth(ref<Expr> e) {
+    if (PCAllWidths)
+      return true;
+    return e.getWidth() != Expr::Bool;
+  }
+
+  bool isVerySimple(const ref<Expr> &e) { 
+    return e.isConstant() || bindings.find(e)!=bindings.end();
+  }
+
+  bool isVerySimpleUpdate(const UpdateNode *un) {
+    return !un || updateBindings.find(un)!=updateBindings.end();
+  }
+
+
+  // document me!
+  bool isSimple(const ref<Expr> &e) { 
+    if (isVerySimple(e)) {
+      return true;
+    } else if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e)) {
+      return isVerySimple(re->index) && isVerySimpleUpdate(re->updates.head);
+    } else {
+      Expr *ep = e.get();
+      for (unsigned i=0; i<ep->getNumKids(); i++)
+        if (!isVerySimple(ep->getKid(i)))
+          return false;
+      return true;
+    }
+  }
+
+  bool hasSimpleKids(const Expr *ep) {
+      for (unsigned i=0; i<ep->getNumKids(); i++)
+        if (!isSimple(ep->getKid(i)))
+          return false;
+      return true;
+  }
+  
+  void scanUpdate(const UpdateNode *un) {
+    if (un) {
+      if (couldPrintUpdates.insert(un).second) {
+        scanUpdate(un->next);
+        scan1(un->index);
+        scan1(un->value);
+      } else {
+        shouldPrintUpdates.insert(un);
+      }
+    }
+  }
+
+  void scan1(const ref<Expr> &e) {
+    if (!e.isConstant()) {
+      if (couldPrint.insert(e).second) {
+        Expr *ep = e.get();
+        for (unsigned i=0; i<ep->getNumKids(); i++)
+          scan1(ep->getKid(i));
+        if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e)) 
+          scanUpdate(re->updates.head);
+      } else {
+        shouldPrint.insert(e);
+      }
+    }
+  }
+
+  void printUpdateList(const UpdateList &updates, PrintContext &PC) {
+    const UpdateNode *head = updates.head;
+
+    // Special case empty list.
+    if (!head) {
+      if (updates.isRooted) {
+        PC << "arr" << updates.root->id;
+      } else {
+        PC << "[]";
+      }
+      return;
+    }
+
+    // FIXME: Explain this breaking policy.
+    bool openedList = false, nextShouldBreak = false;
+    unsigned outerIndent = PC.pos;
+    unsigned middleIndent = 0;
+    for (const UpdateNode *un = head; un; un = un->next) {      
+      // We are done if we hit the cache.
+      std::map<const UpdateNode*, unsigned>::iterator it = 
+        updateBindings.find(un);
+      if (it!=updateBindings.end()) {
+        if (openedList)
+          PC << "] @ ";
+        PC << "U" << it->second;
+        return;
+      } else if (!hasScan || shouldPrintUpdates.count(un)) {
+        if (openedList)
+          PC << "] @";
+        if (un != head)
+          PC.breakLine(outerIndent);
+        PC << "U" << updateCounter << ":"; 
+        updateBindings.insert(std::make_pair(un, updateCounter++));
+        openedList = nextShouldBreak = false;
+     }
+    
+      if (!openedList) {
+        openedList = 1;
+        PC << '[';
+        middleIndent = PC.pos;
+      } else {
+        PC << ',';
+        printSeparator(PC, !nextShouldBreak, middleIndent);
+      }
+      //PC << "(=";
+      //unsigned innerIndent = PC.pos;
+      print(un->index, PC);
+      //printSeparator(PC, isSimple(un->index), innerIndent);
+      PC << "=";
+      print(un->value, PC);
+      //PC << ')';
+      
+      nextShouldBreak = !(un->index.isConstant() && un->value.isConstant());
+    }
+
+    if (openedList)
+      PC << ']';
+
+    if (updates.isRooted)
+      PC << " @ arr" << updates.root->id;
+  }
+
+  void printWidth(PrintContext &PC, ref<Expr> e) {
+    if (!shouldPrintWidth(e))
+      return;
+
+    if (PCWidthAsArg) {
+      PC << ' ';
+      if (PCPrefixWidth)
+        PC << 'w';
+    }
+
+    PC << e.getWidth();
+  }
+
+  /// hasOrderedReads - True iff all children are reads with
+  /// consecutive offsets according to the given \arg stride.
+  bool hasOrderedReads(const Expr *ep, int stride) {
+    const ReadExpr *base = dyn_ref_cast<ReadExpr>(ep->getKid(0));
+    if (!base)
+      return false;
+
+    // Get stride expr in proper index width.
+    Expr::Width idxWidth = base->index.getWidth();
+    ref<Expr> strideExpr(stride, idxWidth), offset(0, idxWidth);
+    for (unsigned i=1; i<ep->getNumKids(); ++i) {
+      const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
+      if (!re) 
+        return false;
+
+      // Check if the index follows the stride. 
+      // FIXME: How aggressive should this be simplified. The
+      // canonicalizing builder is probably the right choice, but this
+      // is yet another area where we would really prefer it to be
+      // global or else use static methods.
+      offset = AddExpr::create(offset, strideExpr);
+      if (SubExpr::create(re->index, base->index) != offset)
+        return false;
+    }
+
+    return true;
+  }
+
+  /// hasAllByteReads - True iff all children are byte level reads.
+  bool hasAllByteReads(const Expr *ep) {
+    for (unsigned i=0; i<ep->getNumKids(); ++i) {
+      const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
+      if (!re || re->getWidth() != Expr::Int8)
+        return false;
+    }
+    return true;
+  }
+
+  void printRead(const ReadExpr *re, PrintContext &PC, unsigned indent) {
+    print(re->index, PC);
+    printSeparator(PC, isVerySimple(re->index), indent);
+    printUpdateList(re->updates, PC);
+  }
+
+  void printExtract(const ExtractExpr *ee, PrintContext &PC, unsigned indent) {
+    PC << ee->offset << ' ';
+    print(ee->expr, PC);
+  }
+
+  void printExpr(const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false) {
+    bool simple = hasSimpleKids(ep);
+    
+    print(ep->getKid(0), PC);
+    for (unsigned i=1; i<ep->getNumKids(); i++) {
+      printSeparator(PC, simple, indent);
+      print(ep->getKid(i), PC, printConstWidth);
+    }
+  }
+
+public:
+  PPrinter(std::ostream &_os) : os(_os), newline("\n") {
+    reset();
+  }
+
+  void setNewline(const std::string &_newline) {
+    newline = _newline;
+  }
+
+  void reset() {
+    counter = 0;
+    updateCounter = 0;
+    hasScan = false;
+    bindings.clear();
+    updateBindings.clear();
+    couldPrint.clear();
+    shouldPrint.clear();
+    couldPrintUpdates.clear();
+    shouldPrintUpdates.clear();
+  }
+
+  void scan(const ref<Expr> &e) {
+    hasScan = true;
+    scan1(e);
+  }
+
+  void print(const ref<Expr> &e, unsigned level=0) {
+    PrintContext PC(os);
+    PC.pos = level;
+    print(e, PC);
+  }
+
+  void printConst(const ref<Expr> &e, PrintContext &PC, bool printWidth) {
+    assert(e.isConstant());
+
+    if (e.getWidth() == Expr::Bool)
+      PC << (e.getConstantValue() ? "true" : "false");
+    else {
+      if (PCAllConstWidths)
+	printWidth = true;
+    
+      if (printWidth)
+	PC << "(w" << e.getWidth() << " ";
+
+      PC << e.getConstantValue();
+
+      if (printWidth)
+	PC << ")";
+    }    
+  }
+
+  void print(const ref<Expr> &e, PrintContext &PC, bool printConstWidth=false) {
+    if (e.isConstant()) 
+      printConst(e, PC, printConstWidth);
+    else {
+      std::map<ref<Expr>, unsigned>::iterator it = bindings.find(e);
+      if (it!=bindings.end()) {
+        PC << 'N' << it->second;
+      } else {
+        if (!hasScan || shouldPrint.count(e)) {
+          PC << 'N' << counter << ':';
+          bindings.insert(std::make_pair(e, counter++));
+        }
+
+        // Detect Not.
+        // FIXME: This should be in common code.
+        if (const EqExpr *ee = dyn_ref_cast<EqExpr>(e)) {
+          if (ee->left == ref<Expr>(false, Expr::Bool)) {
+            PC << "(Not";
+            printWidth(PC, e);
+            PC << ' ';
+            // FIXME: This is a boom if right is a constant.
+            print(ee->right, PC);
+            PC << ')';
+            return;
+          }
+        }
+
+        // Detect multibyte reads.
+        // FIXME: Hrm. One problem with doing this is that we are
+        // masking the sharing of the indices which aren't
+        // visible. Need to think if this matters... probably not
+        // because if they are offset reads then its either constant,
+        // or they are (base + offset) and base will get printed with
+        // a declaration.
+        if (PCMultibyteReads && e.getKind() == Expr::Concat) {
+          const Expr *ep = e.get();
+          if (hasAllByteReads(ep)) {
+            bool isMSB = hasOrderedReads(ep, 1);
+            if (isMSB || hasOrderedReads(ep, -1)) {
+              PC << "(Read" << (isMSB ? "MSB" : "LSB");
+              printWidth(PC, e);
+              PC << ' ';
+              unsigned firstIdx = isMSB ? 0 : ep->getNumKids()-1;
+              printRead(static_ref_cast<ReadExpr>(ep->getKid(firstIdx)), 
+                        PC, PC.pos);
+              PC << ')';
+              return;
+            }
+          }
+        }
+
+	PC << '(' << e.getKind();
+        printWidth(PC, e);
+        PC << ' ';
+
+        // Indent at first argument and dispatch to appropriate print
+        // routine for exprs which require special handling.
+        unsigned indent = PC.pos;
+        if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e)) {
+          printRead(re, PC, indent);
+        } else if (const ExtractExpr *ee = dyn_ref_cast<ExtractExpr>(e)) {
+          printExtract(ee, PC, indent);
+        } else if (e.getKind() == Expr::Concat || e.getKind() == Expr::SExt)
+	  printExpr(e.get(), PC, indent, true);
+	else
+          printExpr(e.get(), PC, indent);	
+        PC << ")";
+      }
+    }
+  }
+
+  /* Public utility functions */
+
+  void printSeparator(PrintContext &PC, bool simple, unsigned indent) {
+    if (simple) {
+      PC << ' ';
+    } else {
+      PC.breakLine(indent);
+    }
+  }
+};
+
+ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) {
+  return new PPrinter(os);
+}
+
+void ExprPPrinter::printOne(std::ostream &os,
+                            const char *message, 
+                            const ref<Expr> &e) {
+  PPrinter p(os);
+  p.scan(e);
+
+  // FIXME: Need to figure out what to do here. Probably print as a
+  // "forward declaration" with whatever syntax we pick for that.
+  PrintContext PC(os);
+  PC << message << ": ";
+  p.print(e, PC);
+  PC.breakLine();
+}
+
+void ExprPPrinter::printConstraints(std::ostream &os,
+                                    const ConstraintManager &constraints) {
+  printQuery(os, constraints, ref<Expr>(false, Expr::Bool));
+}
+
+void ExprPPrinter::printQuery(std::ostream &os,
+                              const ConstraintManager &constraints,
+                              const ref<Expr> &q) {
+  PPrinter p(os);
+  
+  for (ConstraintManager::const_iterator it = constraints.begin(),
+         ie = constraints.end(); it != ie; ++it)
+    p.scan(*it);
+  p.scan(q);
+
+  PrintContext PC(os);
+  PC << "(query [";
+  
+  // Ident at constraint list;
+  unsigned indent = PC.pos;
+  for (ConstraintManager::const_iterator it = constraints.begin(),
+         ie = constraints.end(); it != ie;) {
+    p.print(*it, PC);
+    ++it;
+    if (it != ie)
+      PC.breakLine(indent);
+  }
+  PC << ']';
+
+  p.printSeparator(PC, constraints.empty(), indent-1);
+  p.print(q, PC);
+
+  PC << ')';
+  PC.breakLine();
+}
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*> &);
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
new file mode 100644
index 00000000..b15cdffa
--- /dev/null
+++ b/lib/Expr/ExprVisitor.cpp
@@ -0,0 +1,253 @@
+//===-- ExprVisitor.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/Expr.h"
+#include "klee/util/ExprVisitor.h"
+
+#include "llvm/Support/CommandLine.h"
+
+namespace {
+  llvm::cl::opt<bool>
+  UseVisitorHash("use-visitor-hash", 
+                 llvm::cl::desc("Use hash-consing during expr visitation."),
+                 llvm::cl::init(true));
+}
+
+using namespace klee;
+
+ref<Expr> ExprVisitor::visit(const ref<Expr> &e) {
+  if (!UseVisitorHash || e.isConstant()) {
+    return visitActual(e);
+  } else {
+    visited_ty::iterator it = visited.find(e);
+
+    if (it!=visited.end()) {
+      return it->second;
+    } else {
+      ref<Expr> res = visitActual(e);
+      visited.insert(std::make_pair(e, res));
+      return res;
+    }
+  }
+}
+
+ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
+  if (e.isConstant()) {    
+    return e;
+  } else {
+    Expr &ep = *e.get();
+
+    Action res = visitExpr(ep);
+    switch(res.kind) {
+    case Action::DoChildren:
+      // continue with normal action
+      break;
+    case Action::SkipChildren:
+      return e;
+    case Action::ChangeTo:
+      return res.argument;
+    }
+
+    switch(ep.getKind()) {
+    case Expr::NotOptimized: res = visitNotOptimized(static_cast<NotOptimizedExpr&>(ep)); break;
+    case Expr::Read: res = visitRead(static_cast<ReadExpr&>(ep)); break;
+    case Expr::Select: res = visitSelect(static_cast<SelectExpr&>(ep)); break;
+    case Expr::Concat: res = visitConcat(static_cast<ConcatExpr&>(ep)); break;
+    case Expr::Extract: res = visitExtract(static_cast<ExtractExpr&>(ep)); break;
+    case Expr::ZExt: res = visitZExt(static_cast<ZExtExpr&>(ep)); break;
+    case Expr::SExt: res = visitSExt(static_cast<SExtExpr&>(ep)); break;
+    case Expr::Add: res = visitAdd(static_cast<AddExpr&>(ep)); break;
+    case Expr::Sub: res = visitSub(static_cast<SubExpr&>(ep)); break;
+    case Expr::Mul: res = visitMul(static_cast<MulExpr&>(ep)); break;
+    case Expr::UDiv: res = visitUDiv(static_cast<UDivExpr&>(ep)); break;
+    case Expr::SDiv: res = visitSDiv(static_cast<SDivExpr&>(ep)); break;
+    case Expr::URem: res = visitURem(static_cast<URemExpr&>(ep)); break;
+    case Expr::SRem: res = visitSRem(static_cast<SRemExpr&>(ep)); break;
+    case Expr::And: res = visitAnd(static_cast<AndExpr&>(ep)); break;
+    case Expr::Or: res = visitOr(static_cast<OrExpr&>(ep)); break;
+    case Expr::Xor: res = visitXor(static_cast<XorExpr&>(ep)); break;
+    case Expr::Shl: res = visitShl(static_cast<ShlExpr&>(ep)); break;
+    case Expr::LShr: res = visitLShr(static_cast<LShrExpr&>(ep)); break;
+    case Expr::AShr: res = visitAShr(static_cast<AShrExpr&>(ep)); break;
+    case Expr::Eq: res = visitEq(static_cast<EqExpr&>(ep)); break;
+    case Expr::Ne: res = visitNe(static_cast<NeExpr&>(ep)); break;
+    case Expr::Ult: res = visitUlt(static_cast<UltExpr&>(ep)); break;
+    case Expr::Ule: res = visitUle(static_cast<UleExpr&>(ep)); break;
+    case Expr::Ugt: res = visitUgt(static_cast<UgtExpr&>(ep)); break;
+    case Expr::Uge: res = visitUge(static_cast<UgeExpr&>(ep)); break;
+    case Expr::Slt: res = visitSlt(static_cast<SltExpr&>(ep)); break;
+    case Expr::Sle: res = visitSle(static_cast<SleExpr&>(ep)); break;
+    case Expr::Sgt: res = visitSgt(static_cast<SgtExpr&>(ep)); break;
+    case Expr::Sge: res = visitSge(static_cast<SgeExpr&>(ep)); break;
+    case Expr::Constant:
+    default:
+      assert(0 && "invalid expression kind");
+    }
+
+    switch(res.kind) {
+    case Action::DoChildren: {  
+      bool rebuild = false;
+      ref<Expr> e(&ep), kids[8];
+      unsigned count = ep.getNumKids();
+      for (unsigned i=0; i<count; i++) {
+        ref<Expr> kid = ep.getKid(i);
+        kids[i] = visit(kid);
+        if (kids[i] != kid)
+          rebuild = true;
+      }
+      if (rebuild) {
+        e = ep.rebuild(kids);
+        if (recursive)
+          e = visit(e);
+      }
+      if (!e.isConstant()) {
+        res = visitExprPost(*e.get());
+        if (res.kind==Action::ChangeTo)
+          e = res.argument;
+      }
+      return e;
+    }
+    case Action::SkipChildren:
+      return e;
+    case Action::ChangeTo:
+      return res.argument;
+    default:
+      assert(0 && "invalid kind");
+    }
+  }
+}
+
+ExprVisitor::Action ExprVisitor::visitExpr(const Expr&) {
+  return Action::doChildren();
+}
+
+ExprVisitor::Action ExprVisitor::visitExprPost(const Expr&) {
+  return Action::skipChildren();
+}
+
+ExprVisitor::Action ExprVisitor::visitNotOptimized(const NotOptimizedExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitRead(const ReadExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSelect(const SelectExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitConcat(const ConcatExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitExtract(const ExtractExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitZExt(const ZExtExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSExt(const SExtExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitAdd(const AddExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSub(const SubExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitMul(const MulExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitUDiv(const UDivExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSDiv(const SDivExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitURem(const URemExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSRem(const SRemExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitAnd(const AndExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitOr(const OrExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitXor(const XorExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitShl(const ShlExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitLShr(const LShrExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitAShr(const AShrExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitEq(const EqExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitNe(const NeExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitUlt(const UltExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitUle(const UleExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitUgt(const UgtExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitUge(const UgeExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSlt(const SltExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSle(const SleExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSgt(const SgtExpr&) {
+  return Action::doChildren(); 
+}
+
+ExprVisitor::Action ExprVisitor::visitSge(const SgeExpr&) {
+  return Action::doChildren(); 
+}
+
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
new file mode 100644
index 00000000..77e25f62
--- /dev/null
+++ b/lib/Expr/Lexer.cpp
@@ -0,0 +1,261 @@
+//===-- Lexer.cpp ---------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "expr/Lexer.h"
+
+#include "llvm/Support/MemoryBuffer.h"
+#include "llvm/Support/Streams.h"
+
+#include <iomanip>
+#include <iostream>
+#include <string.h>
+
+using namespace llvm;
+using namespace klee;
+using namespace klee::expr;
+
+///
+
+const char *Token::getKindName() const {
+  switch (kind) {
+  default:
+  case Unknown:    return "Unknown";
+  case Arrow:      return "Arrow";
+  case At:         return "At";
+  case Colon:      return "Colon";
+  case Comma:      return "Comma";
+  case Comment:    return "Comment";
+  case EndOfFile:  return "EndOfFile";
+  case Equals:     return "Equals";
+  case Identifier: return "Identifier";
+  case KWFalse:    return "KWFalse";
+  case KWQuery:    return "KWQuery";
+  case KWReserved: return "KWReserved";
+  case KWTrue:     return "KWTrue";
+  case KWWidth:    return "KWWidth";
+  case LBrace:     return "LBrace";
+  case LParen:     return "LParen";
+  case LSquare:    return "LSquare";
+  case Number:     return "Number";
+  case RBrace:     return "RBrace";
+  case RParen:     return "RParen";
+  case RSquare:    return "RSquare";
+  case Semicolon:  return "Semicolon";
+  }
+}
+
+void Token::dump() {
+  llvm::cerr << "(Token \"" << getKindName() << "\" "
+             << (void*) start << " " << length << " "
+             << line << " " << column << ")";
+}
+
+///
+
+static inline bool isInternalIdentifierChar(int Char) {
+  return isalnum(Char) || Char == '_' || Char == '.';
+}
+
+Lexer::Lexer(const llvm::MemoryBuffer *MB) 
+  : BufferPos(MB->getBufferStart()), BufferEnd(MB->getBufferEnd()), 
+    LineNumber(1), ColumnNumber(0) {
+}
+
+Lexer::~Lexer() {
+}
+
+int Lexer::PeekNextChar() {
+  if (BufferPos == BufferEnd)
+    return -1;
+  return *BufferPos;
+}
+
+int Lexer::GetNextChar() {
+  if (BufferPos == BufferEnd)
+    return -1;
+
+  // Handle DOS/Mac newlines here, by stripping duplicates and by
+  // returning '\n' for both.
+  char Result = *BufferPos++;
+  if (Result == '\n' || Result == '\r') {
+    if (BufferPos != BufferEnd && *BufferPos == ('\n' + '\r' - Result))
+      ++BufferPos;
+    Result = '\n';
+  }
+
+  if (Result == '\n') {
+    ++LineNumber;
+    ColumnNumber = 0;
+  } else {
+    ++ColumnNumber;
+  }
+
+  return Result;
+}
+
+Token &Lexer::SetTokenKind(Token &Result, Token::Kind k) {
+  Result.kind = k;
+  Result.length = BufferPos - Result.start;
+  return Result;
+}
+
+static bool isReservedKW(const char *Str, unsigned N) {
+    unsigned i;
+
+  // Check for i[0-9]+
+  if (N>1 && Str[0] == 'i') {
+    for (i=1; i<N; ++i)
+      if (!isdigit(Str[i]))
+        break;
+    if (i==N)
+      return true;
+  }
+
+  // Check for fp[0-9]+([.].*)?$
+  if (N>3 && Str[0]=='f' && Str[1]=='p' && isdigit(Str[2])) {
+    for (i=3; i<N; ++i)
+      if (!isdigit(Str[i]))
+        break;
+    if (i==N || Str[i]=='.')
+      return true;
+  }
+  
+  return false;
+}
+static bool isWidthKW(const char *Str, unsigned N) {
+  if (N<2 || Str[0] != 'w')
+    return false;
+  for (unsigned i=1; i<N; ++i)
+    if (!isdigit(Str[i]))
+      return false;
+  return true;
+}
+Token &Lexer::SetIdentifierTokenKind(Token &Result) {
+  unsigned Length = BufferPos - Result.start;
+  switch (Length) {
+  case 3:
+    if (memcmp("def", Result.start, 3) == 0)
+      return SetTokenKind(Result, Token::KWReserved);
+    if (memcmp("var", Result.start, 3) == 0)
+      return SetTokenKind(Result, Token::KWReserved);
+    break;
+
+  case 4:
+    if (memcmp("true", Result.start, 4) == 0)
+      return SetTokenKind(Result, Token::KWTrue);
+    break;
+
+  case 5:
+    if (memcmp("array", Result.start, 5) == 0)
+      return SetTokenKind(Result, Token::KWReserved);
+    if (memcmp("false", Result.start, 5) == 0)
+      return SetTokenKind(Result, Token::KWFalse);
+    if (memcmp("query", Result.start, 5) == 0)
+      return SetTokenKind(Result, Token::KWQuery);
+    break;      
+    
+  case 6:
+    if (memcmp("define", Result.start, 6) == 0)
+      return SetTokenKind(Result, Token::KWReserved);
+    break;
+
+  case 7:
+    if (memcmp("declare", Result.start, 7) == 0)
+      return SetTokenKind(Result, Token::KWReserved);
+    break;
+  }
+
+  if (isReservedKW(Result.start, Length))
+    return SetTokenKind(Result, Token::KWReserved);
+  if (isWidthKW(Result.start, Length))
+    return SetTokenKind(Result, Token::KWWidth);
+
+  return SetTokenKind(Result, Token::Identifier);
+}
+
+void Lexer::SkipToEndOfLine() {
+  for (;;) {
+    int Char = GetNextChar();
+    if (Char == -1 || Char =='\n')
+      break;
+  }
+}
+
+Token &Lexer::LexNumber(Token &Result) {
+  while (isalnum(PeekNextChar()) || PeekNextChar()=='_')
+    GetNextChar();
+  return SetTokenKind(Result, Token::Number);
+}
+
+Token &Lexer::LexIdentifier(Token &Result) {
+  while (isInternalIdentifierChar(PeekNextChar()))
+    GetNextChar();
+
+  // Recognize keywords specially.
+  return SetIdentifierTokenKind(Result);
+}
+
+Token &Lexer::Lex(Token &Result) {
+  Result.kind = Token::Unknown;
+  Result.length = 0;
+  Result.start = BufferPos;
+  
+  // Skip whitespace.
+  while (isspace(PeekNextChar()))
+    GetNextChar();
+
+  Result.start = BufferPos;
+  Result.line = LineNumber;
+  Result.column = ColumnNumber;
+  int Char = GetNextChar();
+  switch (Char) {
+  case -1:  return SetTokenKind(Result, Token::EndOfFile);
+    
+  case '(': return SetTokenKind(Result, Token::LParen);
+  case ')': return SetTokenKind(Result, Token::RParen);
+  case ',': return SetTokenKind(Result, Token::Comma);
+  case ':': return SetTokenKind(Result, Token::Colon);
+  case ';': return SetTokenKind(Result, Token::Semicolon);
+  case '=': return SetTokenKind(Result, Token::Equals);
+  case '@': return SetTokenKind(Result, Token::At);
+  case '[': return SetTokenKind(Result, Token::LSquare);
+  case ']': return SetTokenKind(Result, Token::RSquare);
+  case '{': return SetTokenKind(Result, Token::LBrace);
+  case '}': return SetTokenKind(Result, Token::RBrace);
+
+  case '#':
+    SkipToEndOfLine();
+    return SetTokenKind(Result, Token::Comment);
+
+  case '+': {
+    if (isdigit(PeekNextChar()))
+      return LexNumber(Result);
+    else
+      return SetTokenKind(Result, Token::Unknown);
+  }
+
+  case '-': {
+    int Next = PeekNextChar();
+    if (Next == '>')
+      return GetNextChar(), SetTokenKind(Result, Token::Arrow);
+    else if (isdigit(Next))
+      return LexNumber(Result);
+    else
+      return SetTokenKind(Result, Token::Unknown);
+    break;
+  }
+
+  default:
+    if (isdigit(Char))
+      return LexNumber(Result);
+    else if (isalpha(Char) || Char == '_')
+      return LexIdentifier(Result);
+    return SetTokenKind(Result, Token::Unknown);
+  }
+}
diff --git a/lib/Expr/Makefile b/lib/Expr/Makefile
new file mode 100644
index 00000000..b80569b3
--- /dev/null
+++ b/lib/Expr/Makefile
@@ -0,0 +1,16 @@
+#===-- lib/Expr/Makefile -----------------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+LIBRARYNAME=kleaverExpr
+DONT_BUILD_RELINKED=1
+BUILD_ARCHIVE=1
+
+include $(LEVEL)/Makefile.common
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
new file mode 100644
index 00000000..f5708384
--- /dev/null
+++ b/lib/Expr/Parser.cpp
@@ -0,0 +1,1310 @@
+//===-- Parser.cpp --------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "expr/Parser.h"
+
+#include "expr/Lexer.h"
+
+#include "klee/Constraints.h"
+#include "klee/Solver.h"
+#include "klee/util/ExprPPrinter.h"
+
+#include "llvm/ADT/APInt.h"
+#include "llvm/Support/MemoryBuffer.h"
+#include "llvm/Support/Streams.h"
+
+#include <cassert>
+#include <iostream>
+#include <map>
+
+using namespace llvm;
+using namespace klee;
+using namespace klee::expr;
+
+namespace {
+  /// ParseResult - Represent a possibly invalid parse result.
+  template<typename T>
+  struct ParseResult {
+    bool IsValid;
+    T Value;
+
+  public:
+    ParseResult() : IsValid(false) {}
+    ParseResult(T _Value) : IsValid(true), Value(_Value) {}
+    ParseResult(bool _IsValid, T _Value) : IsValid(_IsValid), Value(_Value) {}
+
+    bool isValid() { 
+      return IsValid; 
+    }
+    T get() { 
+      assert(IsValid && "get() on invalid ParseResult!");
+      return Value; 
+    }
+  };
+  
+  typedef ParseResult<Decl*> DeclResult;
+  typedef ParseResult<ExprHandle> ExprResult;
+  typedef ParseResult<Expr::Width> TypeResult;
+  typedef ParseResult<VersionHandle> VersionResult;
+
+  /// NumberOrExprResult - Represent a number or expression. This is used to
+  /// wrap an expression production which may be a number, but for
+  /// which the type width is unknown.
+  class NumberOrExprResult {
+    Token AsNumber;
+    ExprResult AsExpr;
+    bool IsNumber;
+
+  public:
+    NumberOrExprResult() : IsNumber(false) {}
+    explicit NumberOrExprResult(Token _AsNumber) : AsNumber(_AsNumber),
+                                                   IsNumber(true) {}
+    explicit NumberOrExprResult(ExprResult _AsExpr) : AsExpr(_AsExpr),
+                                                      IsNumber(false) {}
+    
+    bool isNumber() const { return IsNumber; }
+    const Token &getNumber() const { 
+      assert(IsNumber && "Invalid accessor call.");
+      return AsNumber; 
+    }
+    const ExprResult &getExpr() const {
+      assert(!IsNumber && "Invalid accessor call.");
+      return AsExpr;
+    }
+  };
+
+  /// ParserImpl - Parser implementation.
+  class ParserImpl : public Parser {
+    typedef std::map<const std::string, const Identifier*> IdentifierTabTy;
+    typedef std::map<const Identifier*, ExprHandle> ExprSymTabTy;
+    typedef std::map<const Identifier*, VersionHandle> VersionSymTabTy;
+
+    const std::string Filename;
+    const MemoryBuffer *TheMemoryBuffer;
+    Lexer TheLexer;
+    unsigned MaxErrors;
+    unsigned NumErrors;
+
+    // FIXME: Use LLVM symbol tables?
+    IdentifierTabTy IdentifierTab;
+
+    std::map<const Identifier*, const ArrayDecl*> ArraySymTab;
+    ExprSymTabTy ExprSymTab;
+    VersionSymTabTy VersionSymTab;
+
+    /// Tok - The currently lexed token.
+    Token Tok;
+
+    /// ParenLevel - The current depth of matched '(' tokens. 
+    unsigned ParenLevel;
+    /// SquareLevel - The current depth of matched '[' tokens.
+    unsigned SquareLevel;
+
+    /* Core parsing functionality */
+    
+    const Identifier *GetOrCreateIdentifier(const Token &Tok);
+
+    void GetNextNonCommentToken() {
+      do {
+        TheLexer.Lex(Tok);
+      } while (Tok.kind == Token::Comment);
+    }
+
+    /// ConsumeToken - Consume the current 'peek token' and lex the next one.
+    void ConsumeToken() {
+      assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen);
+      GetNextNonCommentToken();
+    }
+
+    /// ConsumeExpectedToken - Check that the current token is of the
+    /// expected kind and consume it.
+    void ConsumeExpectedToken(Token::Kind k) {
+      assert(Tok.kind == k && "Unexpected token!");
+      GetNextNonCommentToken();
+    }
+
+    void ConsumeLParen() {
+      ++ParenLevel;
+      ConsumeExpectedToken(Token::LParen);
+    }
+
+    void ConsumeRParen() {
+      if (ParenLevel) // Cannot go below zero.
+        --ParenLevel;
+      ConsumeExpectedToken(Token::RParen);
+    }
+
+    void ConsumeLSquare() {
+      ++SquareLevel;
+      ConsumeExpectedToken(Token::LSquare);
+    }
+
+    void ConsumeRSquare() {
+      if (SquareLevel) // Cannot go below zero.
+        --SquareLevel;
+      ConsumeExpectedToken(Token::RSquare);
+    }
+
+    void ConsumeAnyToken() {
+      switch (Tok.kind) {
+      case Token::LParen: return ConsumeLParen();
+      case Token::RParen: return ConsumeRParen();
+      case Token::LSquare: return ConsumeLSquare();
+      case Token::RSquare: return ConsumeRSquare();
+      default: 
+        return ConsumeToken();
+      }
+    }
+
+    /* Utility functions */
+
+    /// SkipUntilRParen - Scan forward to the next token following an
+    /// rparen at the given level, or EOF, whichever is first.
+    void SkipUntilRParen(unsigned Level) {
+      // FIXME: I keep wavering on whether it is an error to call this
+      // with the current token an rparen. In most cases this should
+      // have been handled differently (error reported,
+      // whatever). Audit & resolve.
+      assert(Level <= ParenLevel && 
+             "Refusing to skip until rparen at higher level.");
+      while (Tok.kind != Token::EndOfFile) {
+        if (Tok.kind == Token::RParen && ParenLevel == Level) {
+          ConsumeRParen();
+          break;
+        }
+        ConsumeAnyToken();
+      }
+    }
+
+    /// SkipUntilRParen - Scan forward until reaching an rparen token
+    /// at the current level (or EOF).
+    void SkipUntilRParen() {
+      SkipUntilRParen(ParenLevel);
+    }
+    
+    /// ExpectRParen - Utility method to close an sexp. This expects to
+    /// eat an rparen, and emits a diagnostic and skips to the next one
+    /// (or EOF) if it cannot.
+    void ExpectRParen(const char *Msg) {
+      if (Tok.kind == Token::EndOfFile) {
+        // FIXME: Combine with Msg
+        Error("expected ')' but found end-of-file.", Tok);
+      } else if (Tok.kind != Token::RParen) {
+        Error(Msg, Tok);
+        SkipUntilRParen();
+      } else {
+        ConsumeRParen();
+      }
+    }
+
+    /// SkipUntilRSquare - Scan forward to the next token following an
+    /// rsquare at the given level, or EOF, whichever is first.
+    void SkipUntilRSquare(unsigned Level) {
+      // FIXME: I keep wavering on whether it is an error to call this
+      // with the current token an rparen. In most cases this should
+      // have been handled differently (error reported,
+      // whatever). Audit & resolve.
+      assert(Level <= ParenLevel && 
+             "Refusing to skip until rparen at higher level.");
+      while (Tok.kind != Token::EndOfFile) {
+        if (Tok.kind == Token::RSquare && ParenLevel == Level) {
+          ConsumeRSquare();
+          break;
+        }
+        ConsumeAnyToken();
+      }
+    }
+
+    /// SkipUntilRSquare - Scan forward until reaching an rsquare token
+    /// at the current level (or EOF).
+    void SkipUntilRSquare() {
+      SkipUntilRSquare(ParenLevel);
+    }
+    
+    /// ExpectRSquare - Utility method to close an array. This expects
+    /// to eat an rparen, and emits a diagnostic and skips to the next
+    /// one (or EOF) if it cannot.
+    void ExpectRSquare(const char *Msg) {
+      if (Tok.kind == Token::EndOfFile) {
+        // FIXME: Combine with Msg
+        Error("expected ']' but found end-of-file.", Tok);
+      } else if (Tok.kind != Token::RSquare) {
+        Error(Msg, Tok);
+        SkipUntilRSquare();
+      } else {
+        ConsumeRSquare();
+      }
+    }
+
+    /*** Grammar productions ****/
+
+    /* Top level decls */
+
+    DeclResult ParseArrayDecl();
+    DeclResult ParseExprVarDecl();
+    DeclResult ParseVersionVarDecl();
+    DeclResult ParseCommandDecl();
+
+    /* Commands */
+
+    DeclResult ParseQueryCommand();
+
+    /* Etc. */
+
+    NumberOrExprResult ParseNumberOrExpr();
+
+    ExprResult ParseExpr(TypeResult ExpectedType);
+    ExprResult ParseParenExpr(TypeResult ExpectedType);
+    ExprResult ParseUnaryParenExpr(const Token &Name,
+                                   unsigned Kind, bool IsFixed,
+                                   Expr::Width ResTy);
+    ExprResult ParseBinaryParenExpr(const Token &Name,
+                                    unsigned Kind, bool IsFixed,
+                                    Expr::Width ResTy);
+    ExprResult ParseSelectParenExpr(const Token &Name, Expr::Width ResTy);
+    ExprResult ParseConcatParenExpr(const Token &Name, Expr::Width ResTy);
+    ExprResult ParseExtractParenExpr(const Token &Name, Expr::Width ResTy);
+    ExprResult ParseAnyReadParenExpr(const Token &Name,
+                                     unsigned Kind,
+                                     Expr::Width ResTy);
+    void ParseMatchedBinaryArgs(const Token &Name, 
+                                TypeResult ExpectType,
+                                ExprResult &LHS, ExprResult &RHS);
+    ExprResult ParseNumber(Expr::Width Width);
+    ExprResult ParseNumberToken(Expr::Width Width, const Token &Tok);
+
+    VersionResult ParseVersionSpecifier();
+    VersionResult ParseVersion();
+
+    TypeResult ParseTypeSpecifier();
+
+    /*** Diagnostics ***/
+    
+    void Error(const char *Message, const Token &At);
+    void Error(const char *Message) { Error(Message, Tok); }
+
+  public:
+    ParserImpl(const std::string _Filename,
+               const MemoryBuffer *MB) : Filename(_Filename),
+                                         TheMemoryBuffer(MB),
+                                         TheLexer(MB),
+                                         MaxErrors(~0u),
+                                         NumErrors(0) {}
+
+    /// Initialize - Initialize the parsing state. This must be called
+    /// prior to the start of parsing.
+    void Initialize() {
+      ParenLevel = SquareLevel = 0;
+
+      ConsumeAnyToken();
+    }
+
+    /* Parser interface implementation */
+
+    virtual Decl *ParseTopLevelDecl();
+
+    virtual void SetMaxErrors(unsigned N) {
+      MaxErrors = N;
+    }
+
+    virtual unsigned GetNumErrors() const {
+      return NumErrors; 
+    }
+  };
+}
+
+const Identifier *ParserImpl::GetOrCreateIdentifier(const Token &Tok) {
+  // FIXME: Make not horribly inefficient please.
+  assert(Tok.kind == Token::Identifier && "Expected only identifier tokens.");
+  std::string Name(Tok.start, Tok.length);
+  IdentifierTabTy::iterator it = IdentifierTab.find(Name);
+  if (it != IdentifierTab.end())
+    return it->second;
+
+  Identifier *I = new Identifier(Name);
+  IdentifierTab.insert(std::make_pair(Name, I));
+
+  return I;
+}
+
+Decl *ParserImpl::ParseTopLevelDecl() {
+  // Repeat until success or EOF.
+  while (Tok.kind != Token::EndOfFile) {
+    // Only handle commands for now.
+    if (Tok.kind == Token::LParen) {
+      DeclResult Res = ParseCommandDecl();
+      if (Res.isValid())
+        return Res.get();
+    } else {
+      Error("expected '(' token.");
+      ConsumeAnyToken();
+    }
+  }
+
+  return 0;
+}
+
+/// ParseCommandDecl - Parse a command declaration. The lexer should
+/// be positioned at the opening '('.
+///
+/// command = '(' name ... ')'
+DeclResult ParserImpl::ParseCommandDecl() {
+  ConsumeLParen();
+
+  if (!Tok.isKeyword()) {
+    Error("malformed command.");
+    SkipUntilRParen();
+    return DeclResult();
+  }
+
+  switch (Tok.kind) {
+  case Token::KWQuery:
+    return ParseQueryCommand();
+
+  default:
+    Error("malformed command (unexpected keyword).");
+    SkipUntilRParen();
+    return DeclResult();
+  }
+}
+
+/// ParseQueryCommand - Parse query command. The lexer should be
+/// positioned at the 'query' keyword.
+/// 
+/// 'query' expressions-list expression [expression-list [array-list]]
+DeclResult ParserImpl::ParseQueryCommand() {
+  // FIXME: We need a command for this. Or something.
+  ExprSymTab.clear();
+  VersionSymTab.clear();
+
+  std::vector<ExprHandle> Constraints;
+  ConsumeExpectedToken(Token::KWQuery);
+  if (Tok.kind != Token::LSquare) {
+    Error("malformed query, expected constraint list.");
+    SkipUntilRParen();
+    return DeclResult();
+  }
+
+  ConsumeExpectedToken(Token::LSquare);
+  // FIXME: Should avoid reading past unbalanced parens here.
+  while (Tok.kind != Token::RSquare) {
+    if (Tok.kind == Token::EndOfFile) {
+      Error("unexpected end of file.");
+      return new QueryCommand(Constraints.begin(), Constraints.end(),
+                              ref<Expr>(false, Expr::Bool));
+    }
+
+    ExprResult Res = ParseExpr(TypeResult(Expr::Bool));
+    if (Res.isValid())
+      Constraints.push_back(Res.get());
+  }
+
+  ConsumeRSquare();
+
+  ExprResult Res = ParseExpr(TypeResult());
+  if (!Res.isValid()) // Error emitted by ParseExpr.
+    Res = ExprResult(ref<Expr>(0, Expr::Bool));
+
+  ExpectRParen("unexpected argument to 'query'.");  
+  return new QueryCommand(Constraints.begin(), Constraints.end(),
+                          Res.get());
+}
+
+/// ParseNumberOrExpr - Parse an expression whose type cannot be
+/// predicted.
+NumberOrExprResult ParserImpl::ParseNumberOrExpr() {
+  if (Tok.kind == Token::Number){ 
+    Token Num = Tok;
+    ConsumeToken();
+    return NumberOrExprResult(Num);
+  } else {
+    return NumberOrExprResult(ParseExpr(TypeResult()));
+  }
+}
+
+/// ParseExpr - Parse an expression with the given \arg
+/// ExpectedType. \arg ExpectedType can be invalid if the type cannot
+/// be inferred from the context.
+///
+/// expr = false | true
+/// expr = <constant>
+/// expr = <identifier>
+/// expr = [<identifier>:] paren-expr
+ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
+  // FIXME: Is it right to need to do this here?
+  if (Tok.kind == Token::EndOfFile) {
+    Error("unexpected end of file.");
+    return ExprResult();
+  }
+
+  if (Tok.kind == Token::KWFalse || Tok.kind == Token::KWTrue) {
+    bool Value = Tok.kind == Token::KWTrue;
+    ConsumeToken();
+    return ExprResult(ref<Expr>(Value, Expr::Bool));
+  }
+  
+  if (Tok.kind == Token::Number) {
+    if (!ExpectedType.isValid()) {
+      Error("cannot infer type of number.");
+      ConsumeToken();
+      return ExprResult();
+    }
+    
+    return ParseNumber(ExpectedType.get());
+  }
+
+  const Identifier *Label = 0;
+  if (Tok.kind == Token::Identifier) {
+    Token LTok = Tok;
+    Label = GetOrCreateIdentifier(Tok);
+    ConsumeToken();
+
+    if (Tok.kind != Token::Colon) {
+      ExprSymTabTy::iterator it = ExprSymTab.find(Label);
+
+      if (it == ExprSymTab.end()) {
+        Error("invalid expression label reference.", LTok);
+        return ExprResult();
+      }
+
+      return it->second;
+    }
+
+    ConsumeToken();
+    if (ExprSymTab.count(Label)) {
+      Error("duplicate expression label definition.", LTok);
+      Label = 0;
+    }
+  }
+
+  Token Start = Tok;
+  ExprResult Res = ParseParenExpr(ExpectedType);
+  if (!Res.isValid()) {
+    // If we know the type, define the identifier just so we don't get
+    // use-of-undef errors. 
+    // FIXME: Maybe we should let the symbol table map to invalid
+    // entries?
+    if (Label && ExpectedType.isValid())
+      ExprSymTab.insert(std::make_pair(Label, 
+                                       ref<Expr>(0, ExpectedType.get())));
+    return Res;
+  } else if (ExpectedType.isValid()) {
+    // Type check result.    
+    if (Res.get().getWidth() != ExpectedType.get()) {
+      // FIXME: Need more info, and range
+      Error("expression has incorrect type.", Start);
+      return ExprResult();
+    }
+  }
+
+  if (Label)
+    ExprSymTab.insert(std::make_pair(Label, Res.get()));
+  return Res;
+}
+
+// Additional kinds for macro forms.
+enum MacroKind {
+  eMacroKind_Not = Expr::LastKind + 1,     // false == x
+  eMacroKind_Neg,                          // 0 - x
+  eMacroKind_ReadLSB,                      // Multibyte read
+  eMacroKind_ReadMSB,                      // Multibyte write
+  eMacroKind_Concat,                       // Magic concatenation syntax
+  eMacroKind_LastMacroKind = eMacroKind_ReadMSB
+};
+
+/// LookupExprInfo - Return information on the named token, if it is
+/// recognized.
+///
+/// \param Kind [out] - The Expr::Kind or MacroKind of the identifier.
+/// \param IsFixed [out] - True if the given kinds result and
+/// (expression) arguments are all of the same width.
+/// \param NumArgs [out] - The number of expression arguments for this
+/// kind. -1 indicates the kind is variadic or has non-expression
+/// arguments.
+/// \return True if the token is a valid kind or macro name.
+static bool LookupExprInfo(const Token &Tok, unsigned &Kind, 
+                           bool &IsFixed, int &NumArgs) {
+#define SetOK(kind, isfixed, numargs) (Kind=kind, IsFixed=isfixed,\
+                                       NumArgs=numargs, true)
+  assert(Tok.kind == Token::Identifier && "Unexpected token.");
+  
+  switch (Tok.length) {
+  case 2:
+    if (memcmp(Tok.start, "Eq", 2) == 0)
+      return SetOK(Expr::Eq, false, 2);
+    if (memcmp(Tok.start, "Ne", 2) == 0)
+      return SetOK(Expr::Ne, false, 2);
+
+    if (memcmp(Tok.start, "Or", 2) == 0)
+      return SetOK(Expr::Or, true, 2);
+    break;
+
+  case 3:
+    if (memcmp(Tok.start, "Add", 3) == 0)
+      return SetOK(Expr::Add, true, 2);
+    if (memcmp(Tok.start, "Sub", 3) == 0)
+      return SetOK(Expr::Sub, true, 2);
+    if (memcmp(Tok.start, "Mul", 3) == 0)
+      return SetOK(Expr::Mul, true, 2);
+
+    if (memcmp(Tok.start, "And", 3) == 0)
+      return SetOK(Expr::And, true, 2);
+    if (memcmp(Tok.start, "Shl", 3) == 0)
+      return SetOK(Expr::Shl, true, 2);
+    if (memcmp(Tok.start, "Xor", 3) == 0)
+      return SetOK(Expr::Xor, true, 2);
+
+    if (memcmp(Tok.start, "Not", 3) == 0)
+      return SetOK(eMacroKind_Not, true, 1);
+    if (memcmp(Tok.start, "Neg", 3) == 0)
+      return SetOK(eMacroKind_Neg, true, 1);
+    if (memcmp(Tok.start, "Ult", 3) == 0)
+      return SetOK(Expr::Ult, false, 2);
+    if (memcmp(Tok.start, "Ule", 3) == 0)
+      return SetOK(Expr::Ule, false, 2);
+    if (memcmp(Tok.start, "Ugt", 3) == 0)
+      return SetOK(Expr::Ugt, false, 2);
+    if (memcmp(Tok.start, "Uge", 3) == 0)
+      return SetOK(Expr::Uge, false, 2);
+    if (memcmp(Tok.start, "Slt", 3) == 0)
+      return SetOK(Expr::Slt, false, 2);
+    if (memcmp(Tok.start, "Sle", 3) == 0)
+      return SetOK(Expr::Sle, false, 2);
+    if (memcmp(Tok.start, "Sgt", 3) == 0)
+      return SetOK(Expr::Sgt, false, 2);
+    if (memcmp(Tok.start, "Sge", 3) == 0)
+      return SetOK(Expr::Sge, false, 2);
+    break;
+
+  case 4:
+    if (memcmp(Tok.start, "Read", 4) == 0)
+      return SetOK(Expr::Read, true, -1);
+    if (memcmp(Tok.start, "AShr", 4) == 0)
+      return SetOK(Expr::AShr, true, 2);
+    if (memcmp(Tok.start, "LShr", 4) == 0)
+      return SetOK(Expr::LShr, true, 2);
+
+    if (memcmp(Tok.start, "UDiv", 4) == 0)
+      return SetOK(Expr::UDiv, true, 2);
+    if (memcmp(Tok.start, "SDiv", 4) == 0)
+      return SetOK(Expr::SDiv, true, 2);
+    if (memcmp(Tok.start, "URem", 4) == 0)
+      return SetOK(Expr::URem, true, 2);
+    if (memcmp(Tok.start, "SRem", 4) == 0)
+      return SetOK(Expr::SRem, true, 2);
+    
+    if (memcmp(Tok.start, "SExt", 4) == 0)
+      return SetOK(Expr::SExt, false, 1);
+    if (memcmp(Tok.start, "ZExt", 4) == 0)
+      return SetOK(Expr::ZExt, false, 1);
+    break;
+    
+  case 6:
+    if (memcmp(Tok.start, "Concat", 6) == 0)
+      return SetOK(eMacroKind_Concat, false, -1); 
+    if (memcmp(Tok.start, "Select", 6) == 0)
+      return SetOK(Expr::Select, false, 3);
+    break;
+    
+  case 7:
+    if (memcmp(Tok.start, "Extract", 7) == 0)
+      return SetOK(Expr::Extract, false, -1);
+    if (memcmp(Tok.start, "ReadLSB", 7) == 0)
+      return SetOK(eMacroKind_ReadLSB, true, -1);
+    if (memcmp(Tok.start, "ReadMSB", 7) == 0)
+      return SetOK(eMacroKind_ReadMSB, true, -1);
+    break;
+  }
+
+  return false;
+#undef SetOK
+}
+
+/// ParseParenExpr - Parse a parenthesized expression with the given
+/// \arg ExpectedType. \arg ExpectedType can be invalid if the type
+/// cannot be inferred from the context.
+///
+/// paren-expr = '(' type number ')'
+/// paren-expr = '(' identifier [type] expr+ ')
+/// paren-expr = '(' ('Read' | 'ReadMSB' | 'ReadLSB') type expr update-list ')'
+ExprResult ParserImpl::ParseParenExpr(TypeResult FIXME_UNUSED) {
+  if (Tok.kind != Token::LParen) {
+    Error("unexpected token.");
+    ConsumeAnyToken();
+    return ExprResult();
+  }
+
+  ConsumeLParen();
+  
+  // Check for coercion case (w32 11).
+  if (Tok.kind == Token::KWWidth) {
+    TypeResult ExpectedType = ParseTypeSpecifier();
+
+    if (Tok.kind != Token::Number) {
+      Error("coercion can only apply to a number.");
+      SkipUntilRParen();
+      return ExprResult();
+    }
+    
+    // Make sure this was a type specifier we support.
+    ExprResult Res;
+    if (ExpectedType.isValid()) 
+      Res = ParseNumber(ExpectedType.get());
+    else
+      ConsumeToken();
+
+    ExpectRParen("unexpected argument in coercion.");  
+    return Res;
+  }
+  
+  if (Tok.kind != Token::Identifier) {
+    Error("unexpected token, expected expression.");
+    SkipUntilRParen();
+    return ExprResult();
+  }
+
+  Token Name = Tok;
+  ConsumeToken();
+
+  // FIXME: Use invalid type (i.e. width==0)?
+  Token TypeTok = Tok;
+  bool HasType = TypeTok.kind == Token::KWWidth;
+  TypeResult Type = HasType ? ParseTypeSpecifier() : Expr::Bool;
+
+  // FIXME: For now just skip to rparen on error. It might be nice
+  // to try and actually parse the child nodes though for error
+  // messages & better recovery?
+  if (!Type.isValid()) {
+    SkipUntilRParen();
+    return ExprResult();
+  }
+  Expr::Width ResTy = Type.get();
+
+  unsigned ExprKind;
+  bool IsFixed;
+  int NumArgs;
+  if (!LookupExprInfo(Name, ExprKind, IsFixed, NumArgs)) {
+    // FIXME: For now just skip to rparen on error. It might be nice
+    // to try and actually parse the child nodes though for error
+    // messages & better recovery?
+    Error("unknown expression kind.", Name);
+    SkipUntilRParen();
+    return ExprResult();
+  }
+
+  // See if we have to parse this form specially.
+  if (NumArgs == -1) {
+    switch (ExprKind) {
+    case eMacroKind_Concat:
+      return ParseConcatParenExpr(Name, ResTy);
+
+    case Expr::Extract:
+      return ParseExtractParenExpr(Name, ResTy);
+
+    case eMacroKind_ReadLSB:
+    case eMacroKind_ReadMSB:
+    case Expr::Read:
+      return ParseAnyReadParenExpr(Name, ExprKind, ResTy);
+
+    default:
+      Error("internal error, unimplemented special form.", Name);
+      SkipUntilRParen();
+      return ExprResult(ref<Expr>(0, ResTy));
+    }
+  }
+
+  switch (NumArgs) {
+  case 1:
+    return ParseUnaryParenExpr(Name, ExprKind, IsFixed, ResTy);
+  case 2:
+    return ParseBinaryParenExpr(Name, ExprKind, IsFixed, ResTy);
+  case 3:
+    if (ExprKind == Expr::Select)
+      return ParseSelectParenExpr(Name, ResTy);
+  default:
+    assert(0 && "Invalid argument kind (number of args).");
+    return ExprResult();
+  }
+}
+
+ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
+                                           unsigned Kind, bool IsFixed,
+                                           Expr::Width ResTy) {
+  if (Tok.kind == Token::RParen) {
+    Error("unexpected end of arguments.", Name);
+    ConsumeRParen();
+    return ref<Expr>(0, ResTy);
+  }
+
+  ExprResult Arg = ParseExpr(IsFixed ? ResTy : TypeResult());
+  if (!Arg.isValid())
+    Arg = ref<Expr>(0, ResTy);
+
+  ExpectRParen("unexpected argument in unary expression.");  
+  ExprHandle E = Arg.get();
+  switch (Kind) {
+  case eMacroKind_Not:
+    return EqExpr::alloc(ref<Expr>(0, E.getWidth()), E);
+  case eMacroKind_Neg:
+    return SubExpr::alloc(ref<Expr>(0, E.getWidth()), E);
+  case Expr::SExt:
+    // FIXME: Type check arguments.
+    return SExtExpr::alloc(E, ResTy);
+  case Expr::ZExt:
+    // FIXME: Type check arguments.
+    return ZExtExpr::alloc(E, ResTy);
+  default:
+    Error("internal error, unhandled kind.", Name);
+    return ref<Expr>(0, ResTy);
+  }
+}
+
+/// ParseMatchedBinaryArgs - Parse a pair of arguments who are
+/// expected to be of the same type. Upon return, if both LHS and RHS
+/// are valid then they are guaranteed to have the same type.
+///
+/// Name - The name token of the expression, for diagnostics.
+/// ExpectType - The expected type of the arguments, if known.
+void ParserImpl::ParseMatchedBinaryArgs(const Token &Name, 
+                                        TypeResult ExpectType,
+                                        ExprResult &LHS, ExprResult &RHS) {
+  if (Tok.kind == Token::RParen) {
+    Error("unexpected end of arguments.", Name);
+    ConsumeRParen();
+    return;
+  }
+
+  // Avoid NumberOrExprResult overhead and give more precise
+  // diagnostics when we know the type.
+  if (ExpectType.isValid()) {
+    LHS = ParseExpr(ExpectType);
+    if (Tok.kind == Token::RParen) {
+      Error("unexpected end of arguments.", Name);
+      ConsumeRParen();
+      return;
+    }
+    RHS = ParseExpr(ExpectType);
+  } else {
+    NumberOrExprResult LHS_NOE = ParseNumberOrExpr();
+
+    if (Tok.kind == Token::RParen) {
+      Error("unexpected end of arguments.", Name);
+      ConsumeRParen();
+      return;
+    }
+
+    if (LHS_NOE.isNumber()) {
+      NumberOrExprResult RHS_NOE = ParseNumberOrExpr();
+      
+      if (RHS_NOE.isNumber()) {
+        Error("ambiguous arguments to expression.", Name);
+      } else {
+        RHS = RHS_NOE.getExpr();
+        if (RHS.isValid())
+          LHS = ParseNumberToken(RHS.get().getWidth(), LHS_NOE.getNumber());
+      }
+    } else {
+      LHS = LHS_NOE.getExpr();
+      if (!LHS.isValid()) {
+        // FIXME: Should suppress ambiguity warnings here.
+        RHS = ParseExpr(TypeResult());
+      } else {
+        RHS = ParseExpr(LHS.get().getWidth());
+      }
+    }
+  }
+
+  ExpectRParen("unexpected argument to expression.");
+}
+
+ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
+                                           unsigned Kind, bool IsFixed,
+                                           Expr::Width ResTy) {
+  ExprResult LHS, RHS;
+  ParseMatchedBinaryArgs(Name, IsFixed ? TypeResult(ResTy) : TypeResult(), 
+                         LHS, RHS);
+  if (!LHS.isValid() || !RHS.isValid())
+    return ref<Expr>(0, ResTy);
+
+  ref<Expr> LHS_E = LHS.get(), RHS_E = RHS.get();
+  assert(LHS_E.getWidth() == RHS_E.getWidth() && "Mismatched types!");
+
+  switch (Kind) {    
+  case Expr::Add: return AddExpr::alloc(LHS_E, RHS_E);
+  case Expr::Sub: return SubExpr::alloc(LHS_E, RHS_E);
+  case Expr::Mul: return MulExpr::alloc(LHS_E, RHS_E);
+  case Expr::UDiv: return UDivExpr::alloc(LHS_E, RHS_E);
+  case Expr::SDiv: return SDivExpr::alloc(LHS_E, RHS_E);
+  case Expr::URem: return URemExpr::alloc(LHS_E, RHS_E);
+  case Expr::SRem: return SRemExpr::alloc(LHS_E, RHS_E);
+
+  case Expr::AShr: return AShrExpr::alloc(LHS_E, RHS_E);
+  case Expr::LShr: return LShrExpr::alloc(LHS_E, RHS_E);
+  case Expr::Shl: return AndExpr::alloc(LHS_E, RHS_E);
+
+  case Expr::And: return AndExpr::alloc(LHS_E, RHS_E);
+  case Expr::Or:  return OrExpr::alloc(LHS_E, RHS_E);
+  case Expr::Xor: return XorExpr::alloc(LHS_E, RHS_E);
+
+  case Expr::Eq:  return EqExpr::alloc(LHS_E, RHS_E);
+  case Expr::Ne:  return NeExpr::alloc(LHS_E, RHS_E);
+  case Expr::Ult: return UltExpr::alloc(LHS_E, RHS_E);
+  case Expr::Ule: return UleExpr::alloc(LHS_E, RHS_E);
+  case Expr::Ugt: return UgtExpr::alloc(LHS_E, RHS_E);
+  case Expr::Uge: return UgeExpr::alloc(LHS_E, RHS_E);
+  case Expr::Slt: return SltExpr::alloc(LHS_E, RHS_E);
+  case Expr::Sle: return SleExpr::alloc(LHS_E, RHS_E);
+  case Expr::Sgt: return SgtExpr::alloc(LHS_E, RHS_E);
+  case Expr::Sge: return SgeExpr::alloc(LHS_E, RHS_E);
+  default:
+    Error("FIXME: unhandled kind.", Name);
+    return ref<Expr>(0, ResTy);
+  }  
+}
+
+ExprResult ParserImpl::ParseSelectParenExpr(const Token &Name, 
+                                            Expr::Width ResTy) {
+  // FIXME: Why does this need to be here?
+  if (Tok.kind == Token::RParen) {
+    Error("unexpected end of arguments.", Name);
+    ConsumeRParen();
+    return ref<Expr>(0, ResTy);
+  }
+
+  ExprResult Cond = ParseExpr(Expr::Bool);
+  ExprResult LHS, RHS;
+  ParseMatchedBinaryArgs(Name, ResTy, LHS, RHS);
+  if (!Cond.isValid() || !LHS.isValid() || !RHS.isValid())
+    return ref<Expr>(0, ResTy);
+  return SelectExpr::alloc(Cond.get(), LHS.get(), RHS.get());
+}
+
+
+// need to decide if we want to allow n-ary Concat expressions in the
+// language
+ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
+                                            Expr::Width ResTy) {
+  std::vector<ExprHandle> Kids;
+  
+  unsigned Width = 0;
+  while (Tok.kind != Token::RParen) {
+    ExprResult E = ParseExpr(TypeResult());
+
+    // Skip to end of expr on error.
+    if (!E.isValid()) {
+      SkipUntilRParen();
+      return ref<Expr>(0, ResTy);
+    }
+    
+    Kids.push_back(E.get());
+    Width += E.get().getWidth();
+  }
+  
+  ConsumeRParen();
+
+  if (Width != ResTy) {
+    Error("concat does not match expected result size.");
+    return ref<Expr>(0, ResTy);
+  }
+
+  return ConcatExpr::createN(Kids.size(), &Kids[0]);
+}
+
+ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
+                                             Expr::Width ResTy) {
+  // FIXME: Pull out parse constant integer expression.
+  ExprResult OffsetExpr = ParseNumber(Expr::Int32);
+  ExprResult Child = ParseExpr(TypeResult());
+
+  ExpectRParen("unexpected argument to expression.");
+
+  if (!OffsetExpr.isValid() || !Child.isValid())
+    return ref<Expr>(0, ResTy);
+
+  assert(OffsetExpr.get().isConstant() && "ParseNumber returned non-constant.");
+  unsigned Offset = (unsigned) OffsetExpr.get().getConstantValue();
+
+  if (Offset + ResTy > Child.get().getWidth()) {
+    Error("extract out-of-range of child expression.", Name);
+    return ref<Expr>(0, ResTy);
+  }
+
+  return ExtractExpr::alloc(Child.get(), Offset, ResTy);
+}
+
+ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
+                                             unsigned Kind,
+                                             Expr::Width ResTy) {
+  NumberOrExprResult Index = ParseNumberOrExpr();
+  VersionResult Array = ParseVersionSpecifier();
+  ExpectRParen("unexpected argument in read expression.");
+  
+  if (!Array.isValid())
+    return ref<Expr>(0, ResTy);
+
+  // FIXME: Need generic way to get array width. Needs to work with
+  // anonymous arrays.
+  Expr::Width ArrayDomainType = Expr::Int32;
+  Expr::Width ArrayRangeType = Expr::Int8;
+
+  // Coerce number to correct type.
+  ExprResult IndexExpr;
+  if (Index.isNumber())
+    IndexExpr = ParseNumberToken(ArrayDomainType, Index.getNumber());
+  else
+    IndexExpr = Index.getExpr();
+  
+  if (!IndexExpr.isValid())
+    return ref<Expr>(0, ResTy);
+  else if (IndexExpr.get().getWidth() != ArrayDomainType) {
+    Error("index width does not match array domain.");
+    return ref<Expr>(0, ResTy);
+  }
+
+  // FIXME: Check range width.
+
+  switch (Kind) {
+  default:
+    assert(0 && "Invalid kind.");
+    return ref<Expr>(0, ResTy);
+  case eMacroKind_ReadLSB:
+  case eMacroKind_ReadMSB: {
+    unsigned NumReads = ResTy / ArrayRangeType;
+    if (ResTy != NumReads*ArrayRangeType) {
+      Error("invalid ordered read (not multiple of range type).", Name);
+      return ref<Expr>(0, ResTy);
+    }
+    std::vector<ExprHandle> Kids;
+    Kids.reserve(NumReads);
+    ExprHandle Index = IndexExpr.get();
+    for (unsigned i=0; i<NumReads; ++i) {
+      // FIXME: using folding here
+      ExprHandle OffsetIndex = AddExpr::create(IndexExpr.get(),
+                                               ref<Expr>(i, ArrayDomainType));
+      Kids.push_back(ReadExpr::alloc(Array.get(), OffsetIndex));
+    }
+    if (Kind == eMacroKind_ReadLSB)
+      std::reverse(Kids.begin(), Kids.end());
+    return ConcatExpr::createN(NumReads, &Kids[0]);
+  }
+  case Expr::Read:
+    return ReadExpr::alloc(Array.get(), IndexExpr.get());
+  }
+}
+
+/// version-specifier = <identifier>
+/// version-specifier = [<identifier>:] [ version ]
+VersionResult ParserImpl::ParseVersionSpecifier() {
+  const Identifier *Label = 0;
+  if (Tok.kind == Token::Identifier) {
+    Token LTok = Tok;
+    Label = GetOrCreateIdentifier(Tok);
+    ConsumeToken();
+
+    // FIXME: hack: add array declarations and ditch this.
+    if (memcmp(Label->Name.c_str(), "arr", 3) == 0) {
+      // Declare or create array.
+      const ArrayDecl *&A = ArraySymTab[Label];
+      if (!A) {
+        //        Array = new ArrayDecl(Label, 0, 32, 8);
+        unsigned id = atoi(&Label->Name.c_str()[3]);
+        Array *root = new Array(0, id, 0);
+        // Create update list mapping of name -> array.
+        VersionSymTab.insert(std::make_pair(Label,
+                                            UpdateList(root, true, NULL)));
+      }
+    }
+
+    if (Tok.kind != Token::Colon) {
+      VersionSymTabTy::iterator it = VersionSymTab.find(Label);
+      
+      if (it == VersionSymTab.end()) {
+        Error("invalid update list label reference.", LTok);
+        return VersionResult(false,
+                             UpdateList(0, true, NULL));
+      }
+
+      return it->second;
+    }
+
+    ConsumeToken();
+    if (VersionSymTab.count(Label)) {
+      Error("duplicate update list label definition.", LTok);
+      Label = 0;
+    }
+  }
+
+  Token Start = Tok;
+  VersionResult Res = ParseVersion();
+  // Define update list to avoid use-of-undef errors.
+  if (!Res.isValid())
+    Res = VersionResult(false,
+                        UpdateList(0, true, NULL));
+  
+  if (Label)
+    VersionSymTab.insert(std::make_pair(Label, Res.get()));
+  return Res;
+}
+
+/// version - '[' update-list? ']' ['@' version-specifier]
+/// update-list - empty
+/// update-list - lhs '=' rhs [',' update-list]
+VersionResult ParserImpl::ParseVersion() {
+  if (Tok.kind != Token::LSquare)
+    return VersionResult(false, UpdateList(0, false, NULL));
+  
+  std::vector< std::pair<NumberOrExprResult, NumberOrExprResult> > Writes;
+  ConsumeLSquare();
+  for (;;) {
+    // FIXME: Type check exprs.
+
+    // FIXME: We need to do this (the above) anyway just to handle
+    // implicit constants correctly.
+    NumberOrExprResult LHS = ParseNumberOrExpr();
+    
+    if (Tok.kind != Token::Equals) {
+      Error("expected '='.", Tok);
+      break;
+    }
+    
+    ConsumeToken();
+    NumberOrExprResult RHS = ParseNumberOrExpr();
+
+    Writes.push_back(std::make_pair(LHS, RHS));
+    
+    if (Tok.kind == Token::Comma)
+      ConsumeToken();
+    else
+      break;
+  }
+  ExpectRSquare("expected close of update list");
+
+  VersionHandle Base(0, false, NULL);
+
+  // Anonymous array case.
+  if (Tok.kind != Token::At) { 
+    Array *root = new Array(0, 0, 0);
+    Base = UpdateList(root, false, NULL);
+  } else {
+    ConsumeToken();
+
+    VersionResult BaseRes = ParseVersionSpecifier();
+    if (!BaseRes.isValid())
+      return BaseRes;
+
+    Base = BaseRes.get();
+  }
+
+  Expr::Width ArrayDomainType = Expr::Int32;
+  Expr::Width ArrayRangeType = Expr::Int8;
+
+  for (std::vector< std::pair<NumberOrExprResult, NumberOrExprResult> >::reverse_iterator
+         it = Writes.rbegin(), ie = Writes.rend(); it != ie; ++it) {
+    ExprResult LHS, RHS;
+    // FIXME: This can be factored into common helper for coercing a
+    // NumberOrExpr into an Expr.
+    if (it->first.isNumber()) {
+      LHS = ParseNumberToken(ArrayDomainType, it->first.getNumber());
+    } else {
+      LHS = it->first.getExpr(); 
+      if (LHS.isValid() && LHS.get().getWidth() != ArrayDomainType) {
+        // FIXME: bad token location. We should maybe try and know the
+        // array up-front?
+        Error("invalid value in write index (doesn't match domain).", Tok);
+        LHS = ExprResult();
+      }
+    }
+
+    if (it->second.isNumber()) {
+      RHS = ParseNumberToken(ArrayRangeType, it->second.getNumber());
+    } else {
+      RHS = it->second.getExpr();
+      if (RHS.isValid() && RHS.get().getWidth() != ArrayRangeType) {
+        // FIXME: bad token location. We should maybe try and know the
+        // array up-front?
+        Error("invalid value in write assignment (doesn't match range).", Tok);
+        RHS = ExprResult();
+      }
+    }
+    
+    if (LHS.isValid() && RHS.isValid())
+      Base.extend(LHS.get(), RHS.get());
+  }
+
+  return Base;
+}
+
+/// ParseNumber - Parse a number of the given type.
+ExprResult ParserImpl::ParseNumber(Expr::Width Type) {
+  ExprResult Res = ParseNumberToken(Type, Tok);
+  ConsumeExpectedToken(Token::Number);
+  return Res;
+}
+
+/// ParseNumberToken - Parse a number of the given type from the given
+/// token.
+ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
+  const char *S = Tok.start;
+  unsigned N = Tok.length;
+  unsigned Radix = 10, RadixBits = 4;
+  bool HasMinus = false;
+
+  // Detect +/- (a number token cannot have both).
+  if (S[0] == '+') {
+    ++S;
+    --N;
+  } else if (S[0] == '-') {
+    HasMinus = true;
+    ++S;
+    --N;
+  }
+
+  // Detect 0[box].
+  if ((Tok.length >= 2 && S[0] == '0') &&
+      (S[1] == 'b' || S[1] == 'o' || S[1] == 'x')) {
+    if (S[1] == 'b') {
+      Radix = 2; 
+      RadixBits = 1;
+    } else if (S[1] == 'o') {
+      Radix = 8;
+      RadixBits = 3;
+    } else {
+      Radix = 16;
+      RadixBits = 4;
+    }
+    S += 2;
+    N -= 2;
+
+    // Diagnose 0[box] with no trailing digits.
+    if (!N) {
+      Error("invalid numeric token (no digits).", Tok);
+      return ref<Expr>(0, Type);
+    }
+  }
+
+  // This is a simple but slow way to handle overflow.
+  APInt Val(std::max(64U, RadixBits * N), 0);
+  APInt RadixVal(Val.getBitWidth(), Radix);
+  APInt DigitVal(Val.getBitWidth(), 0);
+  for (unsigned i=0; i<N; ++i) {
+    unsigned Digit, Char = S[i];
+    
+    if (Char == '_')
+      continue;
+    
+    if ('0' <= Char && Char <= '9')
+      Digit = Char - '0';
+    else if ('a' <= Char && Char <= 'z')
+      Digit = Char - 'a' + 10;
+    else if ('A' <= Char && Char <= 'Z')
+      Digit = Char - 'A' + 10;
+    else {
+      Error("invalid character in numeric token.", Tok);
+      return ref<Expr>(0, Type);
+    }
+
+    if (Digit >= Radix) {
+      Error("invalid character in numeric token (out of range).", Tok);
+      return ref<Expr>(0, Type);
+    }
+
+    DigitVal = Digit;
+    Val = Val * RadixVal + DigitVal;
+  }
+
+  // FIXME: Actually do the check for overflow.
+  if (HasMinus)
+    Val = -Val;
+
+  return ExprResult(ref<Expr>(Val.trunc(Type).getZExtValue(), Type));
+}
+
+/// ParseTypeSpecifier - Parse a type specifier.
+///
+/// type = w[0-9]+
+TypeResult ParserImpl::ParseTypeSpecifier() {
+  assert(Tok.kind == Token::KWWidth && "Unexpected token.");
+
+  // FIXME: Need APInt technically.
+  Token TypeTok = Tok;
+  int width = atoi(std::string(Tok.start+1,Tok.length-1).c_str());
+  ConsumeToken();
+
+  // FIXME: We should impose some sort of maximum just for sanity?
+  return TypeResult(width);
+}
+
+void ParserImpl::Error(const char *Message, const Token &At) {
+  ++NumErrors;
+  if (MaxErrors && NumErrors >= MaxErrors)
+    return;
+
+  llvm::cerr << Filename 
+             << ":" << At.line << ":" << At.column 
+             << ": error: " << Message << "\n";
+
+  // Skip carat diagnostics on EOF token.
+  if (At.kind == Token::EndOfFile)
+    return;
+  
+  // Simple caret style diagnostics.
+  const char *LineBegin = At.start, *LineEnd = At.start,
+    *BufferBegin = TheMemoryBuffer->getBufferStart(),
+    *BufferEnd = TheMemoryBuffer->getBufferEnd();
+
+  // Run line pointers forward and back.
+  while (LineBegin > BufferBegin && 
+         LineBegin[-1] != '\r' && LineBegin[-1] != '\n')
+    --LineBegin;
+  while (LineEnd < BufferEnd && 
+         LineEnd[0] != '\r' && LineEnd[0] != '\n')
+    ++LineEnd;
+
+  // Show the line.
+  llvm::cerr << std::string(LineBegin, LineEnd) << "\n";
+
+  // Show the caret or squiggly, making sure to print back spaces the
+  // same.
+  for (const char *S=LineBegin; S != At.start; ++S)
+    llvm::cerr << (isspace(*S) ? *S : ' ');
+  if (At.length > 1) {
+    for (unsigned i=0; i<At.length; ++i)
+      llvm::cerr << '~';
+  } else
+    llvm::cerr << '^';
+  llvm::cerr << '\n';
+}
+
+// AST API
+// FIXME: Move out of parser.
+
+Decl::Decl() {}
+
+void QueryCommand::dump() {
+  // FIXME: This is masking the difference between an actual query and
+  // a query decl.
+  ExprPPrinter::printQuery(std::cerr, 
+                           ConstraintManager(Constraints), 
+                           Query);
+}
+
+// Public parser API
+
+Parser::Parser() {
+}
+
+Parser::~Parser() {
+}
+
+Parser *Parser::Create(const std::string Filename,
+                       const MemoryBuffer *MB) {
+  ParserImpl *P = new ParserImpl(Filename, MB);
+  P->Initialize();
+  return P;
+}
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
new file mode 100644
index 00000000..b2ceeaf1
--- /dev/null
+++ b/lib/Expr/Updates.cpp
@@ -0,0 +1,126 @@
+//===-- Updates.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/Expr.h"
+
+#include <cassert>
+
+using namespace klee;
+
+///
+
+UpdateNode::UpdateNode(const UpdateNode *_next, 
+                       const ref<Expr> &_index, 
+                       const ref<Expr> &_value) 
+  : refCount(0),
+    stpArray(0),
+    next(_next),
+    index(_index),
+    value(_value) {
+  assert(_value.getWidth() == Expr::Int8 && "Update value should be 8-bit wide.");
+  computeHash();
+  if (next) {
+    ++next->refCount;
+    size = 1 + next->size;
+  }
+  else size = 1;
+}
+
+extern "C" void vc_DeleteExpr(void*);
+
+UpdateNode::~UpdateNode() {
+  // XXX gross
+  if (stpArray)
+    ::vc_DeleteExpr(stpArray);
+}
+
+int UpdateNode::compare(const UpdateNode &b) const {
+  if (int i = index.compare(b.index)) 
+    return i;
+  return value.compare(b.value);
+}
+
+unsigned UpdateNode::computeHash() {
+  hashValue = index.hash() ^ value.hash();
+  if (next)
+    hashValue ^= next->hash();
+  return hashValue;
+}
+
+///
+
+UpdateList::UpdateList(const Array *_root, bool _isRooted,
+                       const UpdateNode *_head)
+  : root(_root),
+    head(_head),
+    isRooted(_isRooted) {
+  if (head) ++head->refCount;
+}
+
+UpdateList::UpdateList(const UpdateList &b)
+  : root(b.root),
+    head(b.head),
+    isRooted(b.isRooted) {
+  if (head) ++head->refCount;
+}
+
+UpdateList::~UpdateList() {
+  // We need to be careful and avoid recursion here. We do this in
+  // cooperation with the private dtor of UpdateNode which does not
+  // recursively free its tail.
+  while (head && --head->refCount==0) {
+    const UpdateNode *n = head->next;
+    delete head;
+    head = n;
+  }
+}
+
+UpdateList &UpdateList::operator=(const UpdateList &b) {
+  if (b.head) ++b.head->refCount;
+  if (head && --head->refCount==0) delete head;
+  root = b.root;
+  head = b.head;
+  isRooted = b.isRooted;
+  return *this;
+}
+
+void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) {
+  if (head) --head->refCount;
+  head = new UpdateNode(head, index, value);
+  ++head->refCount;
+}
+
+int UpdateList::compare(const UpdateList &b) const {
+  // use object id to increase determinism
+  if (root->id != b.root->id) 
+    return root->id < b.root->id ? -1 : 1;
+  
+  if (getSize() < b.getSize()) return -1;
+  else if (getSize() > b.getSize()) return 1;    
+
+  // XXX build comparison into update, make fast
+  const UpdateNode *an=head, *bn=b.head;
+  for (; an && bn; an=an->next,bn=bn->next) {
+    if (an==bn) { // exploit shared list structure
+      return 0;
+    } else {
+      if (int res = an->compare(*bn))
+        return res;
+    }
+  }
+  assert(!an && !bn);
+  return 0;
+}
+
+unsigned UpdateList::hash() const {
+  unsigned res = root->id * Expr::MAGIC_HASH_CONSTANT;
+  if (head)
+    res ^= head->hash();
+  return res;
+}