Use ConstantExpr::alloc instead of ref<Expr> directly

 - The "constant optimization" embedded inside ref<Expr> is going away.

 - No functionality change.


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

22 files changed, 133 insertions, 172 deletions

diff --git a/Makefile b/Makefile
index db11c416..2c3ab72b 100644
--- a/Makefile
+++ b/Makefile
@@ -33,7 +33,7 @@ doxygen:
 .PHONY: cscope.files
 cscope.files:
 	find \
-          lib include stp tools runtime examples unittests test www/code-examples \
+          lib include stp tools runtime examples unittests test \
           -name Makefile -or \
           -name \*.in -or \
           -name \*.c -or \
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d16a09bf..cb5423e0 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -238,7 +238,7 @@ struct Expr::CreateArg {
   ref<Expr> expr;
   Width width;
   
-  CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {}
+  CreateArg(Width w = Bool) : expr(0), width(w) {}
   CreateArg(ref<Expr> e) : expr(e), width(Expr::InvalidWidth) {}
   
   bool isExpr() { return !isWidth(); }
@@ -328,12 +328,12 @@ public:
   static ref<ConstantExpr> fromMemory(void *address, Width w);
   void toMemory(void *address);
 
-  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
+  static ref<Expr> alloc(uint64_t v, Width w) {
     // constructs an "optimized" ConstantExpr
     return ref<ConstantExpr>(v, w);
   }
   
-  static ref<ConstantExpr> create(uint64_t v, Width w) {
+  static ref<Expr> create(uint64_t v, Width w) {
     assert(v == bits64::truncateToNBits(v, w) &&
            "invalid constant");
     return alloc(v, w);
diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h
index b090d2d9..212ab760 100644
--- a/include/klee/Internal/Support/QueryLog.h
+++ b/include/klee/Internal/Support/QueryLog.h
@@ -35,7 +35,7 @@ namespace klee {
     std::vector<const Array*> objects;
     
   public:
-    QueryLogEntry() : query(0,Expr::Bool) {}
+    QueryLogEntry() : query(ConstantExpr::alloc(0,Expr::Bool)) {}
     QueryLogEntry(const QueryLogEntry &b);
     QueryLogEntry(const Query &_query, 
                   Type _type,
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index a053050d..1ed8c175 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -35,7 +35,7 @@ namespace klee {
 
     /// withFalse - Return a copy of the query with a false expression.
     Query withFalse() const {
-      return Query(constraints, ref<Expr>(0, Expr::Bool));
+      return Query(constraints, ConstantExpr::alloc(0, Expr::Bool));
     }
 
     /// negateExpr - Return a copy of the query with the expression negated.
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 19f89a03..cb001415 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -69,13 +69,13 @@ namespace klee {
                                         unsigned index) const {
     bindings_ty::const_iterator it = bindings.find(array);
     if (it!=bindings.end() && index<it->second.size()) {
-      return ref<Expr>(it->second[index], Expr::Int8);
+      return ConstantExpr::alloc(it->second[index], Expr::Int8);
     } else {
       if (allowFreeValues) {
         return ReadExpr::create(UpdateList(array, true, 0), 
-                                ref<Expr>(index, Expr::Int32));
+                                ConstantExpr::alloc(index, Expr::Int32));
       } else {
-        return ref<Expr>(0, Expr::Int8);
+        return ConstantExpr::alloc(0, Expr::Int8);
       }
     }
   }
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index a70b09cf..f900f137 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -13,48 +13,11 @@
 #include <assert.h>
 
 class Expr;
-class BinaryExpr;
-class CastExpr;
-class CmpExpr;
-
 class ConstantExpr;
-class ReadExpr;
-class UpdateNode;
-class NotOptimizedExpr;
-class ReadExpr;
-class SelectExpr;
-class ConcatExpr;
-class ExtractExpr;
-class ZExtExpr;
-class SExtExpr;
-class AddExpr;
-class SubExpr;
-class MulExpr;
-class UDivExpr;
-class SDivExpr;
-class URemExpr;
-class SRemExpr;
-class AndExpr;
-class OrExpr;
-class XorExpr;
-class ShlExpr;
-class LShrExpr;
-class AShrExpr;
-class EqExpr;
-class NeExpr;
-class UltExpr;
-class UleExpr;
-class UgtExpr;
-class UgeExpr;
-class SltExpr;
-class SleExpr;
-class SgtExpr;
-class SgeExpr;
-class KModule;
-
-  class ExprVisitor;
-  class StackFrame;
-  class ObjectState;
+
+class ExprVisitor;
+class StackFrame;
+class ObjectState;
 
 template<class T>
 class ref {
@@ -91,9 +54,12 @@ private:
   }  
 
   friend class ExprVisitor;
-  friend class Cell;
-  friend class ObjectState;
-  friend class KModule;
+  friend class ConstantExpr;
+
+  // construct from constant
+  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
+    contents.val = val;
+  }
 
 public:
   template<class U> friend class ref;
@@ -107,14 +73,9 @@ public:
     contents.ptr = p;
     inc();
   }
-
-  // construct from constant
-  ref(uint64_t val, Expr::Width w) : constantWidth(w) {
-    contents.val = val;
-  }
   
   // normal copy constructor
-  ref (const ref<T> &r)
+  ref(const ref<T> &r)
     : constantWidth(r.constantWidth), contents(r.contents) {
     inc();
   }
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index dd6d4647..d07b6490 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -247,7 +247,8 @@ bool ExecutionState::merge(const ExecutionState &b) {
   
   // merge stack
 
-  ref<Expr> inA(1, Expr::Bool), inB(1, Expr::Bool);
+  ref<Expr> inA = ConstantExpr::alloc(1, Expr::Bool);
+  ref<Expr> inB = ConstantExpr::alloc(1, Expr::Bool);
   for (std::set< ref<Expr> >::iterator it = aSuffix.begin(), 
          ie = aSuffix.end(); it != ie; ++it)
     inA = AndExpr::create(inA, *it);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9c6d84cd..c3d2fcb4 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -902,7 +902,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
 
   state.addConstraint(condition);
   if (ivcEnabled)
-    doImpliedValueConcretization(state, condition, ref<Expr>(1, Expr::Bool));
+    doImpliedValueConcretization(state, condition, ConstantExpr::alloc(1, Expr::Bool));
 }
 
 ref<Expr> Executor::evalConstant(Constant *c) {
@@ -1268,7 +1268,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     KInstIterator kcaller = state.stack.back().caller;
     Instruction *caller = kcaller ? kcaller->inst : 0;
     bool isVoidReturn = (ri->getNumOperands() == 0);
-    ref<Expr> result(0,Expr::Bool);
+    ref<Expr> result = ConstantExpr::alloc(0, Expr::Bool);
 
     if (WriteTraces) {
       state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki));
@@ -1402,7 +1402,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
       std::map<BasicBlock*, ref<Expr> > targets;
-      ref<Expr> isDefault(1,Expr::Bool);
+      ref<Expr> isDefault = ConstantExpr::alloc(1, Expr::Bool);
       for (unsigned i=1; i<cases; ++i) {
         ref<Expr> value = evalConstant(si->getCaseValue(i));
         ref<Expr> match = EqExpr::create(cond, value);
@@ -1413,7 +1413,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         if (result) {
           std::map<BasicBlock*, ref<Expr> >::iterator it =
             targets.insert(std::make_pair(si->getSuccessor(i),
-                                          ref<Expr>(0,Expr::Bool))).first;
+                                          ConstantExpr::alloc(0, Expr::Bool))).first;
           it->second = OrExpr::create(match, it->second);
         }
       }
@@ -1587,9 +1587,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Arithmetic / logical
 #define FP_CONSTANT_BINOP(op, type, l, r, target, state) \
         bindLocal(target, state, \
-                  ref<Expr>(op(toConstant(state, l, "floating point").getConstantValue(), \
-                               toConstant(state, r, "floating point").getConstantValue(), \
-                               type), type))
+                  ConstantExpr::alloc(op(toConstant(state, l, "floating point").getConstantValue(), \
+                                         toConstant(state, r, "floating point").getConstantValue(), \
+                                         type), type))
   case Instruction::Add: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
     ref<Expr> left = eval(ki, 0, state).value;
@@ -1915,8 +1915,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::trunc(arg.getConstantValue(),
                                    resultType,
                                    arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1928,8 +1927,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::ext(arg.getConstantValue(),
                                  resultType,
                                  arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1941,8 +1939,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
                                            resultType,
                                            arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1954,8 +1951,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::toSignedInt(arg.getConstantValue(),
                                          resultType,
                                          arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1966,8 +1962,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                "floating point");
     uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
                                              resultType);
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -1979,8 +1974,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
                                            resultType,
                                            arg.getWidth());
-    ref<Expr> result(value, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
 
@@ -2088,8 +2082,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       }
     }
 
-    ref<Expr> result(ret, resultType);
-    bindLocal(ki, state, result);
+    bindLocal(ki, state, ConstantExpr::alloc(ret, resultType));
     break;
   }
 
@@ -2630,7 +2623,7 @@ void Executor::executeAlloc(ExecutionState &state,
     MemoryObject *mo = memory->allocate(size.getConstantValue(), isLocal, false,
                                         state.prevPC->inst);
     if (!mo) {
-      bindLocal(target, state, ref<Expr>(0, kMachinePointerType));
+      bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
       ObjectState *os = bindObjectInState(state, mo, isLocal);
       if (zeroMemory) {
@@ -2665,8 +2658,8 @@ void Executor::executeAlloc(ExecutionState &state,
     
     // Try and start with a small example
     while (example.getConstantValue()>128) {
-      ref<Expr> tmp = ref<Expr>(example.getConstantValue() >> 1, 
-                                example.getWidth());
+      ref<Expr> tmp = ConstantExpr::alloc(example.getConstantValue() >> 1, 
+                                          example.getWidth());
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -2693,12 +2686,15 @@ void Executor::executeAlloc(ExecutionState &state,
       } else {
         // See if a *really* big value is possible. If so assume
         // malloc will fail for it, so lets fork and return 0.
-        StatePair hugeSize = fork(*fixedSize.second, 
-                                  UltExpr::create(ref<Expr>(1<<31, Expr::Int32), size), 
-                                  true);
+        StatePair hugeSize = 
+          fork(*fixedSize.second, 
+               UltExpr::create(ConstantExpr::alloc(1<<31, Expr::Int32),
+                               size), 
+               true);
         if (hugeSize.first) {
           klee_message("NOTE: found huge malloc, returing 0");
-          bindLocal(target, *hugeSize.first, ref<Expr>(0,kMachinePointerType));
+          bindLocal(target, *hugeSize.first, 
+                    ConstantExpr::alloc(0, kMachinePointerType));
         }
         
         if (hugeSize.second) {
@@ -3011,7 +3007,7 @@ void Executor::runFunctionAsMain(Function *f,
   assert(kf);
   Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
   if (ai!=ae) {
-    arguments.push_back(ref<Expr>(argc, Expr::Int32));
+    arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
 
     if (++ai!=ae) {
       argvMO = memory->allocate((argc+1+envc+1+1) * kMachinePointerSize, false, true,
@@ -3108,7 +3104,7 @@ void Executor::getConstraintLog(const ExecutionState &state,
                                 std::string &res,
                                 bool asCVC) {
   if (asCVC) {
-    Query query(state.constraints, ref<Expr>(0, Expr::Bool));
+    Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool));
     char *log = solver->stpSolver->getConstraintLog(query);
     res = std::string(log);
     free(log);
@@ -3155,7 +3151,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
     klee_warning("unable to compute initial values (invalid constraints?)!");
     ExprPPrinter::printQuery(std::cerr,
                              state.constraints, 
-                             ref<Expr>(0,Expr::Bool));
+                             ConstantExpr::alloc(0, Expr::Bool));
     return false;
   }
   
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 3b11dd42..62aa45db 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -37,7 +37,7 @@ ref<Expr>
 Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
   const llvm::Type *type = ce->getType();
 
-  ref<Expr> op1(0,Expr::Bool), op2(0,Expr::Bool), op3(0,Expr::Bool);
+  ref<Expr> op1(0), op2(0), op3(0);
   int numOperands = ce->getNumOperands();
 
   if (numOperands > 0) op1 = evalConstant(ce->getOperand(0));
@@ -80,7 +80,7 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
 
       for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce);
            ii != ie; ++ii) {
-        ref<Expr> addend(0, kMachinePointerType);
+        ref<Expr> addend = ConstantExpr::alloc(0, kMachinePointerType);
         
         if (const StructType *st = dyn_cast<StructType>(*ii)) {
           const StructLayout *sl = kmodule->targetData->getStructLayout(st);
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 386c8d80..1de47d0c 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -239,8 +239,9 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
   for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(), 
          ie = reads.end(); i != ie; ++i) {
     ReadExpr *re = i->get();
-    ref<Expr> size = ref<Expr>(re->updates.root->size, kMachinePointerType);
-    assumption.push_back(UltExpr::create(re->index, size));
+    assumption.push_back(UltExpr::create(re->index, 
+                                         ConstantExpr::alloc(re->updates.root->size, 
+                                                             kMachinePointerType)));
   }
 
   ConstraintManager assume(assumption);
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 0f09b162..cfb4ab43 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -118,7 +118,7 @@ public:
 
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
     if (size==0) {
-      return EqExpr::create(offset, ref<Expr>(0, kMachinePointerType));
+      return EqExpr::create(offset, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
       return UltExpr::create(offset, getSizeExpr());
     }
@@ -126,9 +126,9 @@ public:
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
     if (bytes<=size) {
       return UltExpr::create(offset, 
-                             ref<Expr>(size - bytes + 1, kMachinePointerType));
+                             ConstantExpr::alloc(size - bytes + 1, kMachinePointerType));
     } else {
-      return ref<Expr>(0, Expr::Bool);
+      return ConstantExpr::alloc(0, Expr::Bool);
     }
   }
 };
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index e6d88bac..9369dcbc 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -88,12 +88,12 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     unsigned i = it->second;
     ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                      ref<Expr>(i, Expr::Int32));
+                                      ConstantExpr::alloc(i, Expr::Int32));
     
     // If not in bindings then this can't be a violation?
     Assignment::bindings_ty::iterator it2 = assignment.bindings.find(array);
     if (it2 != assignment.bindings.end()) {
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -102,7 +102,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it2->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it2->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
@@ -122,8 +122,8 @@ void SeedInfo::patchSeed(const ExecutionState &state,
     const Array *array = it->first;
     for (unsigned i=0; i<array->size; ++i) {
       ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
-                                        ref<Expr>(i, Expr::Int32));
-      ref<Expr> isSeed = EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8));
+                                        ConstantExpr::alloc(i, Expr::Int32));
+      ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
       bool res;
       bool success = solver->mustBeFalse(tmp, isSeed, res);
       assert(success && "FIXME: Unhandled solver failure");
@@ -132,7 +132,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
         it->second[i] = value.getConstantValue();
-        tmp.addConstraint(EqExpr::create(read, ref<Expr>(it->second[i], Expr::Int8)));
+        tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
       }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 3f7c442e..9f5a2347 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -386,7 +386,7 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
 
   ref<Expr> cond = arguments[1];
   if (cond.getWidth() != Expr::Bool)
-    cond = NeExpr::create(cond, ref<Expr>(0, cond.getWidth()));
+    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond.getWidth()));
 
   Executor::ExactResolutionList rl;
   executor.resolveExact(state, arguments[0], rl, "prefex_cex");
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 70e42836..4c09a1aa 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -130,7 +130,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   sys::Process::GetTimeUsage(now,user,sys);
 
   bool success = solver->getInitialValues(Query(state.constraints,
-                                                ref<Expr>(0, Expr::Bool)), 
+                                                ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
   sys::Process::GetTimeUsage(delta,user,sys);
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index e9c376f4..4c18a3b3 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -100,11 +100,11 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
                                          ee->left));
       } else {
         equalities.insert(std::make_pair(*it,
-                                         ref<Expr>(1,Expr::Bool)));
+                                         ConstantExpr::alloc(1, Expr::Bool)));
       }
     } else {
       equalities.insert(std::make_pair(*it,
-                                       ref<Expr>(1,Expr::Bool)));
+                                       ConstantExpr::alloc(1, Expr::Bool)));
     }
   }
 
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 55b9a0a4..7f20e3fc 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -43,42 +43,42 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   switch (w) {
   case Expr::Bool: 
     return ZExtExpr::create(ReadExpr::create(ul, 
-                                             ref<Expr>(0,kMachinePointerType)),
+                                             ConstantExpr::alloc(0,kMachinePointerType)),
                             Expr::Bool);
   case Expr::Int8: 
     return ReadExpr::create(ul, 
-                            ref<Expr>(0,kMachinePointerType));
+                            ConstantExpr::alloc(0,kMachinePointerType));
   case Expr::Int16: 
     return ConcatExpr::create(ReadExpr::create(ul, 
-                                               ref<Expr>(1,kMachinePointerType)),
+                                               ConstantExpr::alloc(1,kMachinePointerType)),
                               ReadExpr::create(ul, 
-                                               ref<Expr>(0,kMachinePointerType)));
+                                               ConstantExpr::alloc(0,kMachinePointerType)));
   case Expr::Int32: 
     return ConcatExpr::create4(ReadExpr::create(ul, 
-                                                ref<Expr>(3,kMachinePointerType)),
+                                                ConstantExpr::alloc(3,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(2,kMachinePointerType)),
+                                                ConstantExpr::alloc(2,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(1,kMachinePointerType)),
+                                                ConstantExpr::alloc(1,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(0,kMachinePointerType)));
+                                                ConstantExpr::alloc(0,kMachinePointerType)));
   case Expr::Int64: 
     return ConcatExpr::create8(ReadExpr::create(ul, 
-                                                ref<Expr>(7,kMachinePointerType)),
+                                                ConstantExpr::alloc(7,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(6,kMachinePointerType)),
+                                                ConstantExpr::alloc(6,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(5,kMachinePointerType)),
+                                                ConstantExpr::alloc(5,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(4,kMachinePointerType)),
+                                                ConstantExpr::alloc(4,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(3,kMachinePointerType)),
+                                                ConstantExpr::alloc(3,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(2,kMachinePointerType)),
+                                                ConstantExpr::alloc(2,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(1,kMachinePointerType)),
+                                                ConstantExpr::alloc(1,kMachinePointerType)),
                                ReadExpr::create(ul, 
-                                                ref<Expr>(0,kMachinePointerType)));
+                                                ConstantExpr::alloc(0,kMachinePointerType)));
   default: assert(0 && "invalid width");
   }
 }
@@ -639,7 +639,7 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
   if (type == Expr::Bool) {
     return XorExpr_create(l, r);
   } else if (*l==*r) {
-    return ref<Expr>(0, type);
+    return ConstantExpr::alloc(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)
@@ -891,7 +891,7 @@ ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
 
 static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (l == r) {
-    return ref<Expr>(1, Expr::Bool);
+    return ConstantExpr::alloc(1, Expr::Bool);
   } else {
     return EqExpr::alloc(l, r);
   }
@@ -952,7 +952,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
     //llvm::cerr << "\n\n=== Applying const array optimization ===\n\n";
 
     if (matches == 0)
-      return ref<Expr>(0, Expr::Bool);
+      return ConstantExpr::alloc(0, Expr::Bool);
 
     ref<Expr> res = EqExpr::create(first_idx_match, rd->index);
     if (matches == 1)
@@ -1079,11 +1079,11 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
     if (r.isConstant()) {      
       uint64_t value = r.getConstantValue();
       if (value <= 8) {
-        ref<Expr> res(0,Expr::Bool);
+        ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
         for (unsigned i=0; i<value; i++) {
-          res = OrExpr::create(EqExpr::create(l, ref<Expr>(i,t)), res);
+          res = OrExpr::create(EqExpr::create(l, 
+                                              ConstantExpr::alloc(i, t)), res);
         }
-        //        llvm::cerr << l << "<" << r << "  <=>  " << res << "\n";
         return res;
       }
     }
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 102387e1..cf901f0e 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -26,7 +26,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
       
       UpdateList fwd(ul.root, un, 0);
       return Action::changeTo(ReadExpr::create(fwd, 
-                                               ref<Expr>(index,Expr::Int32)));
+                                               ConstantExpr::alloc(index, Expr::Int32)));
     }
   }
   
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index dc7f4f64..fd367f23 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -240,7 +240,8 @@ class PPrinter : public ExprPPrinter {
 
     // Get stride expr in proper index width.
     Expr::Width idxWidth = base->index.getWidth();
-    ref<Expr> strideExpr(stride, idxWidth), offset(0, idxWidth);
+    ref<Expr> strideExpr = ConstantExpr::alloc(stride, idxWidth);
+    ref<Expr> offset = ConstantExpr::alloc(0, idxWidth);
     for (unsigned i=1; i<ep->getNumKids(); ++i) {
       const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
       if (!re) 
@@ -357,7 +358,7 @@ public:
         // 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)) {
+          if (ee->left == ConstantExpr::alloc(false, Expr::Bool)) {
             PC << "(Not";
             printWidth(PC, e);
             PC << ' ';
@@ -443,7 +444,7 @@ void ExprPPrinter::printOne(std::ostream &os,
 
 void ExprPPrinter::printConstraints(std::ostream &os,
                                     const ConstraintManager &constraints) {
-  printQuery(os, constraints, ref<Expr>(false, Expr::Bool));
+  printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
 void ExprPPrinter::printQuery(std::ostream &os,
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index dba089a5..a8ea0a6b 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -398,7 +398,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
     if (Tok.kind == Token::EndOfFile) {
       Error("unexpected end of file.");
       return new QueryCommand(Constraints.begin(), Constraints.end(),
-                              ref<Expr>(false, Expr::Bool));
+                              ConstantExpr::alloc(false, Expr::Bool));
     }
 
     ExprResult Res = ParseExpr(TypeResult(Expr::Bool));
@@ -410,7 +410,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
 
   ExprResult Res = ParseExpr(TypeResult());
   if (!Res.isValid()) // Error emitted by ParseExpr.
-    Res = ExprResult(ref<Expr>(0, Expr::Bool));
+    Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool));
 
   ExpectRParen("unexpected argument to 'query'.");  
   return new QueryCommand(Constraints.begin(), Constraints.end(),
@@ -447,7 +447,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
   if (Tok.kind == Token::KWFalse || Tok.kind == Token::KWTrue) {
     bool Value = Tok.kind == Token::KWTrue;
     ConsumeToken();
-    return ExprResult(ref<Expr>(Value, Expr::Bool));
+    return ExprResult(ConstantExpr::alloc(Value, Expr::Bool));
   }
   
   if (Tok.kind == Token::Number) {
@@ -491,9 +491,10 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
     // 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())));
+    if (Label && ExpectedType.isValid()) {
+      ref<Expr> Value = ConstantExpr::alloc(0, ExpectedType.get());
+      ExprSymTab.insert(std::make_pair(Label, Value));
+    }
     return Res;
   } else if (ExpectedType.isValid()) {
     // Type check result.    
@@ -716,7 +717,7 @@ ExprResult ParserImpl::ParseParenExpr(TypeResult FIXME_UNUSED) {
     default:
       Error("internal error, unimplemented special form.", Name);
       SkipUntilRParen();
-      return ExprResult(ref<Expr>(0, ResTy));
+      return ExprResult(ConstantExpr::alloc(0, ResTy));
     }
   }
 
@@ -740,20 +741,20 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
   if (Tok.kind == Token::RParen) {
     Error("unexpected end of arguments.", Name);
     ConsumeRParen();
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   }
 
   ExprResult Arg = ParseExpr(IsFixed ? ResTy : TypeResult());
   if (!Arg.isValid())
-    Arg = ref<Expr>(0, ResTy);
+    Arg = ConstantExpr::alloc(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);
+    return EqExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
   case eMacroKind_Neg:
-    return SubExpr::alloc(ref<Expr>(0, E.getWidth()), E);
+    return SubExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
   case Expr::SExt:
     // FIXME: Type check arguments.
     return SExtExpr::alloc(E, ResTy);
@@ -762,7 +763,7 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
     return ZExtExpr::alloc(E, ResTy);
   default:
     Error("internal error, unhandled kind.", Name);
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   }
 }
 
@@ -831,7 +832,7 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
   ParseMatchedBinaryArgs(Name, IsFixed ? TypeResult(ResTy) : TypeResult(), 
                          LHS, RHS);
   if (!LHS.isValid() || !RHS.isValid())
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
 
   ref<Expr> LHS_E = LHS.get(), RHS_E = RHS.get();
   assert(LHS_E.getWidth() == RHS_E.getWidth() && "Mismatched types!");
@@ -865,7 +866,7 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
   case Expr::Sge: return SgeExpr::alloc(LHS_E, RHS_E);
   default:
     Error("FIXME: unhandled kind.", Name);
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   }  
 }
 
@@ -875,14 +876,14 @@ ExprResult ParserImpl::ParseSelectParenExpr(const Token &Name,
   if (Tok.kind == Token::RParen) {
     Error("unexpected end of arguments.", Name);
     ConsumeRParen();
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(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 ConstantExpr::alloc(0, ResTy);
   return SelectExpr::alloc(Cond.get(), LHS.get(), RHS.get());
 }
 
@@ -900,7 +901,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
     // Skip to end of expr on error.
     if (!E.isValid()) {
       SkipUntilRParen();
-      return ref<Expr>(0, ResTy);
+      return ConstantExpr::alloc(0, ResTy);
     }
     
     Kids.push_back(E.get());
@@ -911,7 +912,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
 
   if (Width != ResTy) {
     Error("concat does not match expected result size.");
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   }
 
   return ConcatExpr::createN(Kids.size(), &Kids[0]);
@@ -926,14 +927,14 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
   ExpectRParen("unexpected argument to expression.");
 
   if (!OffsetExpr.isValid() || !Child.isValid())
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(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 ConstantExpr::alloc(0, ResTy);
   }
 
   return ExtractExpr::alloc(Child.get(), Offset, ResTy);
@@ -947,7 +948,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
   ExpectRParen("unexpected argument in read expression.");
   
   if (!Array.isValid())
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
 
   // FIXME: Need generic way to get array width. Needs to work with
   // anonymous arrays.
@@ -962,10 +963,10 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
     IndexExpr = Index.getExpr();
   
   if (!IndexExpr.isValid())
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   else if (IndexExpr.get().getWidth() != ArrayDomainType) {
     Error("index width does not match array domain.");
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(0, ResTy);
   }
 
   // FIXME: Check range width.
@@ -973,13 +974,13 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
   switch (Kind) {
   default:
     assert(0 && "Invalid kind.");
-    return ref<Expr>(0, ResTy);
+    return ConstantExpr::alloc(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);
+      return ConstantExpr::alloc(0, ResTy);
     }
     std::vector<ExprHandle> Kids;
     Kids.reserve(NumReads);
@@ -987,7 +988,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
     for (unsigned i=0; i<NumReads; ++i) {
       // FIXME: using folding here
       ExprHandle OffsetIndex = AddExpr::create(IndexExpr.get(),
-                                               ref<Expr>(i, ArrayDomainType));
+                                               ConstantExpr::alloc(i, ArrayDomainType));
       Kids.push_back(ReadExpr::alloc(Array.get(), OffsetIndex));
     }
     if (Kind == eMacroKind_ReadLSB)
@@ -1185,7 +1186,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
     // Diagnose 0[box] with no trailing digits.
     if (!N) {
       Error("invalid numeric token (no digits).", Tok);
-      return ref<Expr>(0, Type);
+      return ConstantExpr::alloc(0, Type);
     }
   }
 
@@ -1207,12 +1208,12 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
       Digit = Char - 'A' + 10;
     else {
       Error("invalid character in numeric token.", Tok);
-      return ref<Expr>(0, Type);
+      return ConstantExpr::alloc(0, Type);
     }
 
     if (Digit >= Radix) {
       Error("invalid character in numeric token (out of range).", Tok);
-      return ref<Expr>(0, Type);
+      return ConstantExpr::alloc(0, Type);
     }
 
     DigitVal = Digit;
@@ -1223,7 +1224,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) {
   if (HasMinus)
     Val = -Val;
 
-  return ExprResult(ref<Expr>(Val.trunc(Type).getZExtValue(), Type));
+  return ExprResult(ConstantExpr::alloc(Val.trunc(Type).getZExtValue(), Type));
 }
 
 /// ParseTypeSpecifier - Parse a type specifier.
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index d2bc27c6..b6f676aa 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -358,11 +358,11 @@ protected:
     
     if (index >= cod.size) {
       return ReadExpr::create(UpdateList(&array, true, 0), 
-                              ref<Expr>(index, Expr::Int32));
+                              ConstantExpr::alloc(index, Expr::Int32));
     } else {
       CexValueData &cvd = cod.values[index];
       assert(cvd.min() == cvd.max() && "value is not fixed");
-      return ref<Expr>(cvd.min(), Expr::Int8);
+      return ConstantExpr::alloc(cvd.min(), Expr::Int8);
     }
   }
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 2a50ae0c..ae378ac1 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -327,8 +327,8 @@ ValidatingSolver::computeInitialValues(const Query& query,
         unsigned char value = values[i][j];
         bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array,
                                                                       true, 0),
-                                                           ref<Expr>(j, Expr::Int32)),
-                                          ref<Expr>(value, Expr::Int8)));
+                                                           ConstantExpr::alloc(j, Expr::Int32)),
+                                          ConstantExpr::alloc(value, Expr::Int8)));
       }
     }
     ConstraintManager tmp(bindings);
@@ -439,7 +439,7 @@ char *STPSolverImpl::getConstraintLog(const Query &query) {
   for (std::vector< ref<Expr> >::const_iterator it = query.constraints.begin(), 
          ie = query.constraints.end(); it != ie; ++it)
     vc_assertFormula(vc, builder->construct(*it));
-  assert(query.expr == ref<Expr>(0, Expr::Bool) &&
+  assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
          "Unexpected expression in query!");
 
   char *buffer;
diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
index 9220c53e..72b37ab2 100644
--- a/unittests/Expr/ExprTest.cpp
+++ b/unittests/Expr/ExprTest.cpp
@@ -22,9 +22,9 @@ ref<Expr> getConstant(int value, Expr::Width width) {
 }
 
 TEST(ExprTest, BasicConstruction) {
-  EXPECT_EQ(ref<Expr>(0, 32),
-            SubExpr::create(ref<Expr>(10, 32),
-                            ref<Expr>(10, 32)));
+  EXPECT_EQ(ConstantExpr::alloc(0, 32),
+            SubExpr::create(ConstantExpr::alloc(10, 32),
+                            ConstantExpr::alloc(10, 32)));
 }
 
 TEST(ExprTest, ConcatExtract) {