Start removing uses of Expr::isConstant.

 - These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet,
   changed to use ref<ConstantExpr> when the type is known).


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

18 files changed, 168 insertions, 173 deletions

diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 36f4739d..051a84f9 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -90,7 +90,8 @@ namespace klee {
     AssignmentEvaluator v(*this);
     for (; begin!=end; ++begin) {
       ref<Expr> res = v.visit(*begin);
-      if (!res->isConstant() || !res->getConstantValue())
+      ConstantExpr *CE = dyn_cast<ConstantExpr>(res);
+      if (!CE || !CE->getConstantValue())
         return false;
     }
     return true;
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 92d75aa8..a4a65bd9 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -72,8 +72,8 @@ bool AddressSpace::resolveOne(ExecutionState &state,
                               ref<Expr> address,
                               ObjectPair &result,
                               bool &success) {
-  if (address->isConstant()) {
-    success = resolveOne(address->getConstantValue(), result);
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
+    success = resolveOne(CE->getConstantValue(), result);
     return true;
   } else {
     TimerStatIncrementer timer(stats::resolveTime);
@@ -163,9 +163,9 @@ bool AddressSpace::resolve(ExecutionState &state,
                            ResolutionList &rl, 
                            unsigned maxResolutions,
                            double timeout) {
-  if (p->isConstant()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) {
     ObjectPair res;
-    if (resolveOne(p->getConstantValue(), res))
+    if (resolveOne(CE->getConstantValue(), res))
       rl.push_back(res);
     return false;
   } else {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index a1687f58..f567efc6 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -662,8 +662,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     seedMap.find(&current);
   bool isSeeding = it != seedMap.end();
 
-  if (!isSeeding &&
-      !condition->isConstant() && 
+  if (!isSeeding && !isa<ConstantExpr>(condition) && 
       (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
        MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
       statsTracker->elapsed() > 60.) {
@@ -753,8 +752,8 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       bool success = 
         solver->getValue(current, siit->assignment.evaluate(condition), res);
       assert(success && "FIXME: Unhandled solver failure");
-      if (res->isConstant()) {
-        if (res->getConstantValue()) {
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(res)) {
+        if (CE->getConstantValue()) {
           trueSeed = true;
         } else {
           falseSeed = true;
@@ -874,9 +873,8 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 }
 
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
-  if (condition->isConstant()) {
-    assert(condition->getConstantValue() &&
-           "attempt to add invalid constraint");
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(condition)) {
+    assert(CE->getConstantValue() && "attempt to add invalid constraint");
     return;
   }
 
@@ -902,7 +900,8 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
 
   state.addConstraint(condition);
   if (ivcEnabled)
-    doImpliedValueConcretization(state, condition, ConstantExpr::alloc(1, Expr::Bool));
+    doImpliedValueConcretization(state, condition, 
+                                 ConstantExpr::alloc(1, Expr::Bool));
 }
 
 ref<Expr> Executor::evalConstant(Constant *c) {
@@ -998,7 +997,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
                              ref<Expr> &e) {
   ref<Expr> result = e;
 
-  if (!e->isConstant()) {
+  if (!isa<ConstantExpr>(e)) {
     ref<Expr> value(0);
     bool isTrue = false;
 
@@ -1020,7 +1019,7 @@ ref<Expr> Executor::toConstant(ExecutionState &state,
                                ref<Expr> e,
                                const char *reason) {
   e = state.constraints.simplifyExpr(e);
-  if (!e->isConstant()) {
+  if (!isa<ConstantExpr>(e)) {
     ref<Expr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
@@ -1049,7 +1048,7 @@ void Executor::executeGetValue(ExecutionState &state,
   e = state.constraints.simplifyExpr(e);
   std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
     seedMap.find(&state);
-  if (it==seedMap.end() || e->isConstant()) {
+  if (it==seedMap.end() || isa<ConstantExpr>(e)) {
     ref<Expr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
@@ -1393,11 +1392,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     BasicBlock *bb = si->getParent();
 
     cond = toUnique(state, cond);
-    if (cond->isConstant()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
       // Somewhat gross to create these all the time, but fine till we
       // switch to an internal rep.
       ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(),
-                                         cond->getConstantValue());
+                                         CE->getConstantValue());
       unsigned index = si->findCaseValue(ci);
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
@@ -2180,8 +2179,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
     }
     index++;
   }
-  assert(constantOffset->isConstant());
-  kgepi->offset = constantOffset->getConstantValue();
+  kgepi->offset = cast<ConstantExpr>(constantOffset)->getConstantValue();
 }
 
 void Executor::bindModuleConstants() {
@@ -2346,8 +2344,8 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   std::ostringstream info;
   info << "\taddress: " << address << "\n";
   uint64_t example;
-  if (address->isConstant()) {
-    example = address->getConstantValue();
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(address)) {
+    example = CE->getConstantValue();
   } else {
     ref<Expr> value;
     bool success = solver->getValue(state, address, value);
@@ -2466,7 +2464,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
         msg << ai->getName();
         // XXX should go through function
         ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; 
-        if (value->isConstant())
+        if (isa<ConstantExpr>(value))
           msg << "=" << value;
       }
       msg << ")";
@@ -2521,9 +2519,9 @@ void Executor::callExternalFunction(ExecutionState &state,
       static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
     } else {
       ref<Expr> arg = toUnique(state, *ai);
-      if (arg->isConstant()) {
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(arg)) {
         // XXX kick toMemory functions from here
-        static_cast<ConstantExpr*>(arg.get())->toMemory((void*) &args[i]);
+        CE->toMemory((void*) &args[i]);
       } else {
         std::string msg = "external call with symbolic argument: " + function->getName();
         terminateStateOnExecError(state, msg);
@@ -2578,7 +2576,7 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
     return e;
 
   // right now, we don't replace symbolics (is there any reason too?)
-  if (!e->isConstant())
+  if (!isa<ConstantExpr>(e))
     return e;
 
   if (n != 1 && random() %  n)
@@ -2620,9 +2618,9 @@ void Executor::executeAlloc(ExecutionState &state,
                             bool zeroMemory,
                             const ObjectState *reallocFrom) {
   size = toUnique(state, size);
-  if (size->isConstant()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(size)) {
     MemoryObject *mo = 
-      memory->allocate(size->getConstantValue(), isLocal, false, 
+      memory->allocate(CE->getConstantValue(), isLocal, false, 
                        state.prevPC->inst);
     if (!mo) {
       bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
@@ -2793,9 +2791,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   unsigned bytes = Expr::getMinBytesForWidth(type);
 
   if (SimplifySymIndices) {
-    if (!address->isConstant())
+    if (!isa<ConstantExpr>(address))
       address = state.constraints.simplifyExpr(address);
-    if (isWrite && !value->isConstant())
+    if (isWrite && !isa<ConstantExpr>(value))
       value = state.constraints.simplifyExpr(value);
   }
 
@@ -3174,9 +3172,7 @@ void Executor::getCoveredLines(const ExecutionState &state,
 
 void Executor::doImpliedValueConcretization(ExecutionState &state,
                                             ref<Expr> e,
-                                            ref<Expr> value) {
-  assert(value->isConstant() && "non-constant passed in place of constant");
-  
+                                            ref<ConstantExpr> value) {
   if (DebugCheckForImpliedValues)
     ImpliedValue::checkForImpliedValues(solver->solver, e, value);
 
@@ -3186,7 +3182,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
        it != ie; ++it) {
     ReadExpr *re = it->first.get();
     
-    if (re->index->isConstant()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
       // FIXME: This is the sole remaining usage of the Array object
       // variable. Kill me.
       const MemoryObject *mo = re->updates.root->object;
@@ -3197,9 +3193,10 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
         // in other cases we would like to concretize the outstanding
         // reads, but we have no facility for that yet)
       } else {
-        assert(!os->readOnly && "not possible? read only object with static read?");
+        assert(!os->readOnly && 
+               "not possible? read only object with static read?");
         ObjectState *wos = state.addressSpace.getWriteable(mo, os);
-        wos->write(re->index->getConstantValue(), it->second);
+        wos->write(CE->getConstantValue(), it->second);
       }
     }
   }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 2619e786..ba65cf5a 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -362,7 +362,7 @@ private:
 
   void doImpliedValueConcretization(ExecutionState &state,
                                     ref<Expr> e,
-                                    ref<Expr> value);
+                                    ref<ConstantExpr> value);
 
   /// Add a timer to be executed periodically.
   ///
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 8ebc0aef..dfb91344 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -195,16 +195,13 @@ static void _getImpliedValue(ref<Expr> e,
 }
     
 void ImpliedValue::getImpliedValues(ref<Expr> e, 
-                                    ref<Expr> value, 
+                                    ref<ConstantExpr> value, 
                                     ImpliedValueList &results) {
-  assert(value->isConstant() && "non-constant in place of constant");
   _getImpliedValue(e, value->getConstantValue(), results);
 }
 
 void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, 
-                                         ref<Expr> value) {
-  assert(value->isConstant() && "non-constant in place of constant");
-
+                                         ref<ConstantExpr> value) {
   std::vector<ref<ReadExpr> > reads;
   std::map<ref<ReadExpr>, ref<Expr> > found;
   ImpliedValueList results;
diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h
index 51ec6e9b..cbc55dc5 100644
--- a/lib/Core/ImpliedValue.h
+++ b/lib/Core/ImpliedValue.h
@@ -29,8 +29,10 @@ namespace klee {
   typedef std::vector< std::pair<ref<ReadExpr>, ref<Expr> > > ImpliedValueList;
   
   namespace ImpliedValue {        
-    void getImpliedValues(ref<Expr> e, ref<Expr> cvalue, ImpliedValueList &result);
-    void checkForImpliedValues(Solver *S, ref<Expr> e, ref<Expr> cvalue);    
+    void getImpliedValues(ref<Expr> e, ref<ConstantExpr> cvalue, 
+                          ImpliedValueList &result);
+    void checkForImpliedValues(Solver *S, ref<Expr> e, 
+                               ref<ConstantExpr> cvalue);    
   }
 
 }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index de48651b..b4c433b1 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -339,7 +339,7 @@ void ObjectState::write8(unsigned offset, ref<Expr> value) {
 }
 
 void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
-  assert(!offset->isConstant() && "constant offset passed to symbolic write8");
+  assert(!isa<ConstantExpr>(offset) && "constant offset passed to symbolic write8");
   unsigned base, size;
   fastRangeCheckOffset(offset, &base, &size);
   flushRangeForWrite(base, size);
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 30377ee4..62b71e87 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -77,9 +77,9 @@ void SeedInfo::patchSeed(const ExecutionState &state,
   for (std::vector< ref<ReadExpr> >::iterator it = reads.begin(), 
          ie = reads.end(); it != ie; ++it) {
     ReadExpr *re = it->get();
-    if (re->index->isConstant()) {
-      unsigned index = (unsigned) re->index->getConstantValue();
-      directReads.insert(std::make_pair(re->updates.root, index));
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+      directReads.insert(std::make_pair(re->updates.root, 
+                                        (unsigned) CE->getConstantValue()));
     }
   }
   
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index b2e5d277..e1182cf0 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -172,11 +172,12 @@ bool SpecialFunctionHandler::handle(ExecutionState &state,
 /****/
 
 // reads a concrete string from memory
-std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, 
-                                                        ref<Expr> address) {
+std::string 
+SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, 
+                                            ref<Expr> addressExpr) {
   ObjectPair op;
-  address = executor.toUnique(state, address);
-  assert(address->isConstant() && "symbolic string arg to intrinsic");  
+  addressExpr = executor.toUnique(state, addressExpr);
+  ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
   if (!state.addressSpace.resolveOne(address->getConstantValue(), op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
   bool res;
@@ -195,9 +196,9 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   for (i = 0; i < mo->size - 1; i++) {
     ref<Expr> cur = os->read8(i);
     cur = executor.toUnique(state, cur);
-    assert(cur->isConstant() && 
+    assert(isa<ConstantExpr>(cur) && 
            "hit symbolic char while reading concrete string");
-    buf[i] = cur->getConstantValue();
+    buf[i] = cast<ConstantExpr>(cur)->getConstantValue();
   }
   buf[i] = 0;
   
@@ -438,12 +439,12 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
          "invalid number of arguments to klee_set_forking");
   ref<Expr> value = executor.toUnique(state, arguments[0]);
   
-  if (!value->isConstant()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
+    state.forkDisabled = !CE->getConstantValue();
+  } else {
     executor.terminateStateOnError(state, 
                                    "klee_set_forking requires a constant arg",
                                    "user.err");
-  } else {
-    state.forkDisabled = !value->getConstantValue();
   }
 }
 
@@ -476,7 +477,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
 
   std::string msg_str = readStringAtAddress(state, arguments[0]);
   llvm::cerr << msg_str << ":" << arguments[1];
-  if (!arguments[1]->isConstant()) {
+  if (!isa<ConstantExpr>(arguments[1])) {
     // FIXME: Pull into a unique value method?
     ref<Expr> value;
     bool success = executor.solver->getValue(state, arguments[1], value);
@@ -590,7 +591,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
 
   ref<Expr> address = executor.toUnique(state, arguments[0]);
   ref<Expr> size = executor.toUnique(state, arguments[1]);
-  if (!address->isConstant() || !size->isConstant()) {
+  if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) {
     executor.terminateStateOnError(state, 
                                    "check_memory_access requires constant args",
                                    "user.err");
@@ -605,8 +606,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
                                                       size->getConstantValue());
-      assert(chk->isConstant());
-      if (!chk->getConstantValue()) {
+      if (!cast<ConstantExpr>(chk)->getConstantValue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
                                        "ptr.err",
@@ -630,9 +630,9 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
                                                      std::vector<ref<Expr> > &arguments) {
   assert(arguments.size()==2 &&
          "invalid number of arguments to klee_define_fixed_object");
-  assert(arguments[0]->isConstant() &&
+  assert(isa<ConstantExpr>(arguments[0]) &&
          "expect constant address argument to klee_define_fixed_object");
-  assert(arguments[1]->isConstant() &&
+  assert(isa<ConstantExpr>(arguments[1]) &&
          "expect constant size argument to klee_define_fixed_object");
   
   uint64_t address = arguments[0]->getConstantValue();
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 6cd15be7..0a174179 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -551,13 +551,12 @@ ref<Expr> SExtExpr::create(const ref<Expr> &e, Width 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> EqExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr);
+static ref<Expr> AndExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r);
+static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r);
+static ref<Expr> XorExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r);
 
-static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
-  assert(cl->isConstant() && "non-constant passed in place of constant");
+static ref<Expr> AddExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -567,10 +566,10 @@ static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     return r;
   } else {
     Expr::Kind rk = r->getKind();
-    if (rk==Expr::Add && r->getKid(0)->isConstant()) { // A + (B+c) == (A+B) + c
+    if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // 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
+    } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // A + (B-c) == (A+B) - c
       return SubExpr::create(AddExpr::create(cl, r->getKid(0)),
                              r->getKid(1));
     } else {
@@ -578,7 +577,7 @@ static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     }
   }
 }
-static ref<Expr> AddExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+static ref<Expr> AddExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   return AddExpr_createPartialR(cr, l);
 }
 static ref<Expr> AddExpr_create(Expr *l, Expr *r) {
@@ -588,16 +587,16 @@ static ref<Expr> AddExpr_create(Expr *l, Expr *r) {
     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)
+    if (lk==Expr::Add && isa<ConstantExpr>(l->getKid(0))) { // (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)
+    } else if (lk==Expr::Sub && isa<ConstantExpr>(l->getKid(0))) { // (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)
+    } else if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // 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)
+    } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // a + (k-b) = k+(a-b)
       return AddExpr::create(r->getKid(0),
                              SubExpr::create(l, r->getKid(1)));
     } else {
@@ -606,8 +605,7 @@ static ref<Expr> AddExpr_create(Expr *l, Expr *r) {
   }  
 }
 
-static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
-  assert(cl->isConstant() && "non-constant passed in place of constant");
+static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   Expr::Width type = cl->getWidth();
 
   if (type==Expr::Bool) {
@@ -625,7 +623,7 @@ static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     }
   }
 }
-static ref<Expr> SubExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+static ref<Expr> SubExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   assert(cr->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
@@ -642,16 +640,16 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
     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)
+    if (lk==Expr::Add && isa<ConstantExpr>(l->getKid(0))) { // (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)
+    } else if (lk==Expr::Sub && isa<ConstantExpr>(l->getKid(0))) { // (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
+    } else if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // 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
+    } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // a - (k-b) = (a+b) - k
       return SubExpr::create(AddExpr::create(l, r->getKid(1)),
                              r->getKid(0));
     } else {
@@ -660,7 +658,7 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
   }  
 }
 
-static ref<Expr> MulExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+static ref<Expr> MulExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
@@ -675,7 +673,7 @@ static ref<Expr> MulExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     return MulExpr::alloc(cl, r);
   }
 }
-static ref<Expr> MulExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+static ref<Expr> MulExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   return MulExpr_createPartialR(cr, l);
 }
 static ref<Expr> MulExpr_create(Expr *l, Expr *r) {
@@ -688,8 +686,7 @@ static ref<Expr> MulExpr_create(Expr *l, Expr *r) {
   }
 }
 
-static ref<Expr> AndExpr_createPartial(Expr *l, const ref<Expr> &cr) {
-  assert(cr->isConstant() && "non-constant passed in place of constant");
+static ref<Expr> AndExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
 
@@ -701,15 +698,14 @@ static ref<Expr> AndExpr_createPartial(Expr *l, const ref<Expr> &cr) {
     return AndExpr::alloc(l, cr);
   }
 }
-static ref<Expr> AndExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+static ref<Expr> AndExpr_createPartialR(const ref<ConstantExpr> &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");
+static ref<Expr> OrExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
 
@@ -721,15 +717,14 @@ static ref<Expr> OrExpr_createPartial(Expr *l, const ref<Expr> &cr) {
     return OrExpr::alloc(l, cr);
   }
 }
-static ref<Expr> OrExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
+static ref<Expr> OrExpr_createPartialR(const ref<ConstantExpr> &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");
+static ref<Expr> XorExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -746,7 +741,7 @@ static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   }
 }
 
-static ref<Expr> XorExpr_createPartial(Expr *l, const ref<Expr> &cr) {
+static ref<Expr> XorExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
   return XorExpr_createPartialR(cr, l);
 }
 static ref<Expr> XorExpr_create(Expr *l, Expr *r) {
@@ -811,34 +806,34 @@ static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &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()); \
+  assert(l->getWidth()==r->getWidth() && "type mismatch");              \
+  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) {                   \
+    if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {                 \
+      Expr::Width width = l->getWidth();                                \
+      uint64_t val = ints::_op(cl->getConstantValue(),                  \
+                               cr->getConstantValue(), width);          \
+      return ConstantExpr::create(val, width);                          \
+    } else {                                                            \
+      return _e_op ## _createPartialR(cl, r.get());                     \
+    }                                                                   \
+  } else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {            \
+    return _e_op ## _createPartial(l.get(), cr);                        \
+  }                                                                     \
+  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);                    \
+  assert(l->getWidth()==r->getWidth() && "type mismatch");          \
+  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) {               \
+    if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {             \
+      Expr::Width width = l->getWidth();                            \
+      uint64_t val = ints::_op(cl->getConstantValue(),              \
+                               cr->getConstantValue(), width);      \
+      return ConstantExpr::create(val, width);                      \
+    }                                                               \
+  }                                                                 \
+  return _e_op ## _create(l, r);                                    \
 }
 
 BCREATE_R(AddExpr, add, AddExpr_createPartial, AddExpr_createPartialR)
@@ -857,35 +852,35 @@ 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);                    \
+  assert(l->getWidth()==r->getWidth() && "type mismatch");              \
+  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) {                   \
+    if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {                 \
+      Expr::Width width = cl->getWidth();                               \
+      uint64_t val = ints::_op(cl->getConstantValue(),                  \
+                               cr->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()); \
-  } \
+ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) {    \
+  assert(l->getWidth()==r->getWidth() && "type mismatch");             \
+  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) {                  \
+    if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {                \
+      Expr::Width width = cl->getWidth();                              \
+      uint64_t val = ints::_op(cl->getConstantValue(),                 \
+                               cr->getConstantValue(), width);         \
+      return ConstantExpr::create(val, Expr::Bool);                    \
+    } else {                                                           \
+      return partialR(cl, r.get());                                    \
+    }                                                                  \
+  } else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) {           \
+    return partialL(l.get(), cr);                                      \
+  } else {                                                             \
+    return _e_op ## _create(l.get(), r.get());                         \
+  }                                                                    \
 }
   
 
@@ -972,7 +967,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 }
 
 
-static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {  
+static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {  
   assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width width = cl->getWidth();
@@ -1031,14 +1026,16 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     const AddExpr *ae = cast<AddExpr>(r);
     if (ae->left->isConstant()) {
       // c0 = c1 + b => c0 - c1 = b
-      return EqExpr_createPartialR(SubExpr::create(cl, ae->left),
+      return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(cl, 
+                                                                      ae->left)),
                                    ae->right.get());
     }
   } else if (rk==Expr::Sub) {
     const SubExpr *se = cast<SubExpr>(r);
     if (se->left->isConstant()) {
       // c0 = c1 - b => c1 - c0 = b
-      return EqExpr_createPartialR(SubExpr::create(se->left, cl),
+      return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(se->left, 
+                                                                      cl)),
                                    se->right.get());
     }
   } else if (rk == Expr::Read && ConstArrayOpt) {
@@ -1048,7 +1045,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   return EqExpr_create(cl, r);
 }
 
-static ref<Expr> EqExpr_createPartial(Expr *l, const ref<Expr> &cr) {  
+static ref<Expr> EqExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {  
   return EqExpr_createPartialR(cr, l);
 }
   
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index e26568d9..94c0ac17 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -100,7 +100,7 @@ class PPrinter : public ExprPPrinter {
   }
 
   bool isVerySimple(const ref<Expr> &e) { 
-    return e->isConstant() || bindings.find(e)!=bindings.end();
+    return isa<ConstantExpr>(e) || bindings.find(e)!=bindings.end();
   }
 
   bool isVerySimpleUpdate(const UpdateNode *un) {
@@ -143,7 +143,7 @@ class PPrinter : public ExprPPrinter {
   }
 
   void scan1(const ref<Expr> &e) {
-    if (!e->isConstant()) {
+    if (!isa<ConstantExpr>(e)) {
       if (couldPrint.insert(e).second) {
         Expr *ep = e.get();
         for (unsigned i=0; i<ep->getNumKids(); i++)
@@ -208,7 +208,8 @@ class PPrinter : public ExprPPrinter {
       print(un->value, PC);
       //PC << ')';
       
-      nextShouldBreak = !(un->index->isConstant() && un->value->isConstant());
+      nextShouldBreak = !(isa<ConstantExpr>(un->index) && 
+                          isa<ConstantExpr>(un->value));
     }
 
     if (openedList)
@@ -367,9 +368,8 @@ public:
     print(e, PC);
   }
 
-  void printConst(const ref<Expr> &e, PrintContext &PC, bool printWidth) {
-    assert(e->isConstant());
-
+  void printConst(const ref<ConstantExpr> &e, PrintContext &PC, 
+                  bool printWidth) {
     if (e->getWidth() == Expr::Bool)
       PC << (e->getConstantValue() ? "true" : "false");
     else {
@@ -387,8 +387,8 @@ public:
   }
 
   void print(const ref<Expr> &e, PrintContext &PC, bool printConstWidth=false) {
-    if (e->isConstant()) 
-      printConst(e, PC, printConstWidth);
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+      printConst(CE, PC, printConstWidth);
     else {
       std::map<ref<Expr>, unsigned>::iterator it = bindings.find(e);
       if (it!=bindings.end()) {
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 780398f0..0c150a51 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -26,7 +26,7 @@ void klee::findReads(ref<Expr> e,
   ExprHashSet visited;
   std::set<const UpdateNode *> updates;
   
-  if (!e->isConstant()) {
+  if (!isa<ConstantExpr>(e)) {
     visited.insert(e);
     stack.push_back(e);
   }
@@ -40,7 +40,7 @@ void klee::findReads(ref<Expr> e,
       // repeats.
       results.push_back(re);
 
-      if (!re->index->isConstant() &&
+      if (!isa<ConstantExpr>(re->index) &&
           visited.insert(re->index).second)
         stack.push_back(re->index);
       
@@ -53,20 +53,20 @@ void klee::findReads(ref<Expr> e,
         // 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() &&
+            if (!isa<ConstantExpr>(un->index) &&
                 visited.insert(un->index).second)
               stack.push_back(un->index);
-            if (!un->value->isConstant() &&
+            if (!isa<ConstantExpr>(un->value) &&
                 visited.insert(un->value).second)
               stack.push_back(un->value);
           }
         }
       }
-    } else if (!top->isConstant()) {
+    } else if (!isa<ConstantExpr>(top)) {
       Expr *e = top.get();
       for (unsigned i=0; i<e->getNumKids(); i++) {
         ref<Expr> k = e->getKid(i);
-        if (!k->isConstant() &&
+        if (!isa<ConstantExpr>(k) &&
             visited.insert(k).second)
           stack.push_back(k);
       }
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
index 5e9d0a81..c81199d7 100644
--- a/lib/Expr/ExprVisitor.cpp
+++ b/lib/Expr/ExprVisitor.cpp
@@ -22,7 +22,7 @@ namespace {
 using namespace klee;
 
 ref<Expr> ExprVisitor::visit(const ref<Expr> &e) {
-  if (!UseVisitorHash || e->isConstant()) {
+  if (!UseVisitorHash || isa<ConstantExpr>(e)) {
     return visitActual(e);
   } else {
     visited_ty::iterator it = visited.find(e);
@@ -38,7 +38,7 @@ ref<Expr> ExprVisitor::visit(const ref<Expr> &e) {
 }
 
 ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
-  if (e->isConstant()) {    
+  if (isa<ConstantExpr>(e)) {    
     return e;
   } else {
     Expr &ep = *e.get();
@@ -106,7 +106,7 @@ ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
         if (recursive)
           e = visit(e);
       }
-      if (!e->isConstant()) {
+      if (!isa<ConstantExpr>(e)) {
         res = visitExprPost(*e.get());
         if (res.kind==Action::ChangeTo)
           e = res.argument;
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 1808ca7b..c0cc05d5 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -947,8 +947,8 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
   if (!OffsetExpr.isValid() || !Child.isValid())
     return ConstantExpr::alloc(0, ResTy);
 
-  assert(OffsetExpr.get()->isConstant() && "ParseNumber returned non-constant.");
-  unsigned Offset = (unsigned) OffsetExpr.get()->getConstantValue();
+  unsigned Offset = 
+    (unsigned) cast<ConstantExpr>(OffsetExpr.get())->getConstantValue();
 
   if (Offset + ResTy > Child.get()->getWidth()) {
     Error("extract out-of-range of child expression.", Name);
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 546d81fd..49db74e8 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -217,7 +217,8 @@ bool CexCachingSolver::computeValidity(const Query& query,
     return false;
   assert(a && "computeValidity() must have assignment");
   ref<Expr> q = a->evaluate(query.expr);
-  assert(q->isConstant() && "assignment evaluation did not result in constant");
+  assert(isa<ConstantExpr>(q) && 
+         "assignment evaluation did not result in constant");
 
   if (q->getConstantValue()) {
     if (!getAssignment(query, a))
@@ -268,7 +269,7 @@ bool CexCachingSolver::computeValue(const Query& query,
     return false;
   assert(a && "computeValue() must have assignment");
   result = a->evaluate(query.expr);  
-  assert(result->isConstant() && 
+  assert(isa<ConstantExpr>(result) && 
          "assignment evaluation did not result in constant");
   return true;
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index cc0068ca..a0d943d3 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -729,7 +729,7 @@ public:
   bool exprMustBeValue(ref<Expr> e, uint64_t value) {
     CexConstifier cc(objectValues);
     ref<Expr> v = cc.visit(e);
-    if (!v->isConstant()) return false;
+    if (!isa<ConstantExpr>(v)) return false;
     // XXX reenable once all reads and vars are fixed
     //    assert(v.isConstant() && "not all values have been fixed");
     return v->getConstantValue() == value;
@@ -886,7 +886,7 @@ bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) {
   CexConstifier cc(cd.objectValues);
   ref<Expr> value = cc.visit(query.expr);
 
-  if (value->isConstant()) {
+  if (isa<ConstantExpr>(value)) {
     result = value;
     return true;
   } else {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ee5b777b..00fd8e4a 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -419,7 +419,7 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
 /** if *width_out!=1 then result is a bitvector,
     otherwise it is a bool */
 ExprHandle STPBuilder::construct(ref<Expr> e, int *width_out) {
-  if (!UseConstructHash || e->isConstant()) {
+  if (!UseConstructHash || isa<ConstantExpr>(e)) {
     return constructActual(e, width_out);
   } else {
     ExprHashMap< std::pair<ExprHandle, unsigned> >::iterator it = 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 46d6039e..6cbf6ac0 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -112,7 +112,7 @@ bool Solver::mayBeFalse(const Query& query, bool &result) {
 
 bool Solver::getValue(const Query& query, ref<Expr> &result) {
   // Maintain invariants implementation expect.
-  if (query.expr->isConstant()) {
+  if (isa<ConstantExpr>(query.expr)) {
     result = query.expr;
     return true;
   }