about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr.h7
-rw-r--r--include/klee/util/Assignment.h2
-rw-r--r--include/klee/util/Ref.h16
-rw-r--r--lib/Core/AddressSpace.cpp4
-rw-r--r--lib/Core/Executor.cpp34
-rw-r--r--lib/Core/ImpliedValue.cpp18
-rw-r--r--lib/Core/Memory.cpp12
-rw-r--r--lib/Core/SeedInfo.cpp2
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp25
-rw-r--r--lib/Core/TimingSolver.cpp6
-rw-r--r--lib/Expr/Constraints.cpp6
-rw-r--r--lib/Expr/Expr.cpp86
-rw-r--r--lib/Expr/ExprEvaluator.cpp6
-rw-r--r--lib/Expr/ExprPPrinter.cpp10
-rw-r--r--lib/Expr/ExprUtil.cpp12
-rw-r--r--lib/Expr/ExprVisitor.cpp6
-rw-r--r--lib/Expr/Parser.cpp2
-rw-r--r--lib/Solver/CexCachingSolver.cpp8
-rw-r--r--lib/Solver/FastCexSolver.cpp10
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp18
-rw-r--r--lib/Solver/Solver.cpp8
22 files changed, 149 insertions, 151 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index ea5f18c9..df55d126 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -12,6 +12,7 @@
 
 #include "Machine.h"
 #include "klee/util/Bits.h"
+#include "klee/util/Ref.h"
 
 #include "llvm/Support/Streams.h"
 #include "llvm/ADT/SmallVector.h"
@@ -188,6 +189,7 @@ public:
 
   ///
 
+  bool isConstant() const { return getKind() == Expr::Constant; }
   uint64_t getConstantValue() const;
 
   /* Static utility methods */
@@ -224,11 +226,6 @@ public:
   static bool isValidKidWidth(unsigned kid, Width w) { return true; }
   static bool needsResultType() { return false; }
 };
-// END class Expr
-
-
-
-#include "klee/util/Ref.h"
 
 struct Expr::CreateArg {
   ref<Expr> expr;
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 54f6b0af..36f4739d 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -90,7 +90,7 @@ namespace klee {
     AssignmentEvaluator v(*this);
     for (; begin!=end; ++begin) {
       ref<Expr> res = v.visit(*begin);
-      if (!res.isConstant() || !res->getConstantValue())
+      if (!res->isConstant() || !res->getConstantValue())
         return false;
     }
     return true;
diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h
index e2421bb0..1a633fb5 100644
--- a/include/klee/util/Ref.h
+++ b/include/klee/util/Ref.h
@@ -10,10 +10,11 @@
 #ifndef KLEE_REF_H
 #define KLEE_REF_H
 
+#include "llvm/Support/Streams.h"
+
 #include <assert.h>
 
-class Expr;
-class ConstantExpr;
+namespace klee {
 
 template<class T>
 class ref {
@@ -68,11 +69,6 @@ public:
     return ptr;
   }
 
-  // method calls for the constant optimization
-  bool isConstant() const {
-    return ptr && ptr->getKind() == Expr::Constant;
-  }
-
   /* The copy assignment operator must also explicitly be defined,
    * despite a redundant template. */
   ref<T> &operator= (const ref<T> &r) {
@@ -116,10 +112,12 @@ public:
 
 template<class T>
 inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) {
-  os << *e.get();
+  os << *e;
   return os;
 }
 
+class Expr;
+
 template<class U>
 U* dyn_ref_cast(ref<Expr> &src) {
   return dynamic_cast<U*>(src.ptr);
@@ -140,4 +138,6 @@ const U* static_ref_cast(const ref<Expr> &src) {
   return static_cast<const U*>(src.ptr);
 }
 
+}
+
 #endif /* KLEE_REF_H */
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 9a9a0235..92d75aa8 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -72,7 +72,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
                               ref<Expr> address,
                               ObjectPair &result,
                               bool &success) {
-  if (address.isConstant()) {
+  if (address->isConstant()) {
     success = resolveOne(address->getConstantValue(), result);
     return true;
   } else {
@@ -163,7 +163,7 @@ bool AddressSpace::resolve(ExecutionState &state,
                            ResolutionList &rl, 
                            unsigned maxResolutions,
                            double timeout) {
-  if (p.isConstant()) {
+  if (p->isConstant()) {
     ObjectPair res;
     if (resolveOne(p->getConstantValue(), res))
       rl.push_back(res);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bb4bcb53..a1687f58 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -663,7 +663,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   bool isSeeding = it != seedMap.end();
 
   if (!isSeeding &&
-      !condition.isConstant() && 
+      !condition->isConstant() && 
       (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
        MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
       statsTracker->elapsed() > 60.) {
@@ -753,7 +753,7 @@ 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->isConstant()) {
         if (res->getConstantValue()) {
           trueSeed = true;
         } else {
@@ -874,7 +874,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 }
 
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
-  if (condition.isConstant()) {
+  if (condition->isConstant()) {
     assert(condition->getConstantValue() &&
            "attempt to add invalid constraint");
     return;
@@ -998,7 +998,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
                              ref<Expr> &e) {
   ref<Expr> result = e;
 
-  if (!e.isConstant()) {
+  if (!e->isConstant()) {
     ref<Expr> value(0);
     bool isTrue = false;
 
@@ -1020,7 +1020,7 @@ ref<Expr> Executor::toConstant(ExecutionState &state,
                                ref<Expr> e,
                                const char *reason) {
   e = state.constraints.simplifyExpr(e);
-  if (!e.isConstant()) {
+  if (!e->isConstant()) {
     ref<Expr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
@@ -1049,7 +1049,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() || e->isConstant()) {
     ref<Expr> value;
     bool success = solver->getValue(state, e, value);
     assert(success && "FIXME: Unhandled solver failure");
@@ -1393,7 +1393,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     BasicBlock *bb = si->getParent();
 
     cond = toUnique(state, cond);
-    if (cond.isConstant()) {
+    if (cond->isConstant()) {
       // Somewhat gross to create these all the time, but fine till we
       // switch to an internal rep.
       ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(),
@@ -2180,7 +2180,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
     }
     index++;
   }
-  assert(constantOffset.isConstant());
+  assert(constantOffset->isConstant());
   kgepi->offset = constantOffset->getConstantValue();
 }
 
@@ -2346,7 +2346,7 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   std::ostringstream info;
   info << "\taddress: " << address << "\n";
   uint64_t example;
-  if (address.isConstant()) {
+  if (address->isConstant()) {
     example = address->getConstantValue();
   } else {
     ref<Expr> value;
@@ -2466,7 +2466,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 (value->isConstant())
           msg << "=" << value;
       }
       msg << ")";
@@ -2521,7 +2521,7 @@ 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 (arg->isConstant()) {
         // XXX kick toMemory functions from here
         static_cast<ConstantExpr*>(arg.get())->toMemory((void*) &args[i]);
       } else {
@@ -2578,7 +2578,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 (!e->isConstant())
     return e;
 
   if (n != 1 && random() %  n)
@@ -2620,7 +2620,7 @@ void Executor::executeAlloc(ExecutionState &state,
                             bool zeroMemory,
                             const ObjectState *reallocFrom) {
   size = toUnique(state, size);
-  if (size.isConstant()) {
+  if (size->isConstant()) {
     MemoryObject *mo = 
       memory->allocate(size->getConstantValue(), isLocal, false, 
                        state.prevPC->inst);
@@ -2793,9 +2793,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   unsigned bytes = Expr::getMinBytesForWidth(type);
 
   if (SimplifySymIndices) {
-    if (!address.isConstant())
+    if (!address->isConstant())
       address = state.constraints.simplifyExpr(address);
-    if (isWrite && !value.isConstant())
+    if (isWrite && !value->isConstant())
       value = state.constraints.simplifyExpr(value);
   }
 
@@ -3175,7 +3175,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");
+  assert(value->isConstant() && "non-constant passed in place of constant");
   
   if (DebugCheckForImpliedValues)
     ImpliedValue::checkForImpliedValues(solver->solver, e, value);
@@ -3186,7 +3186,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
        it != ie; ++it) {
     ReadExpr *re = it->first.get();
     
-    if (re->index.isConstant()) {
+    if (re->index->isConstant()) {
       // FIXME: This is the sole remaining usage of the Array object
       // variable. Kill me.
       const MemoryObject *mo = re->updates.root->object;
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index c73ae4f1..d1037839 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -53,8 +53,8 @@ static void _getImpliedValue(ref<Expr> e,
     // not much to do, could improve with range analysis
     SelectExpr *se = static_ref_cast<SelectExpr>(e);
     
-    if (se->trueExpr.isConstant()) {
-      if (se->falseExpr.isConstant()) {
+    if (se->trueExpr->isConstant()) {
+      if (se->falseExpr->isConstant()) {
         if (se->trueExpr->getConstantValue() != se->falseExpr->getConstantValue()) {
           if (value == se->trueExpr->getConstantValue()) {
             _getImpliedValue(se->cond, 1, results);
@@ -97,7 +97,7 @@ static void _getImpliedValue(ref<Expr> e,
 
   case Expr::Add: { // constants on left
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    if (be->left.isConstant()) {
+    if (be->left->isConstant()) {
       uint64_t nvalue = ints::sub(value,
                                   be->left->getConstantValue(),
                                   be->left->getWidth());
@@ -107,7 +107,7 @@ static void _getImpliedValue(ref<Expr> e,
   }
   case Expr::Sub: { // constants on left
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    if (be->left.isConstant()) {
+    if (be->left->isConstant()) {
       uint64_t nvalue = ints::sub(be->left->getConstantValue(),
                                   value,
                                   be->left->getWidth());
@@ -156,7 +156,7 @@ static void _getImpliedValue(ref<Expr> e,
   }
   case Expr::Xor: { // constants on left
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    if (be->left.isConstant()) {
+    if (be->left->isConstant()) {
       _getImpliedValue(be->right, value ^ be->left->getConstantValue(), results);
     }
     break;
@@ -169,7 +169,7 @@ static void _getImpliedValue(ref<Expr> e,
   case Expr::Eq: {
     EqExpr *ee = static_ref_cast<EqExpr>(e);
     if (value) {
-      if (ee->left.isConstant())
+      if (ee->left->isConstant())
         _getImpliedValue(ee->right, ee->left->getConstantValue(), results);
     } else {
       // look for limited value range, woohoo
@@ -180,7 +180,7 @@ static void _getImpliedValue(ref<Expr> e,
       // expression where the true and false branches are single
       // valued and distinct.
       
-      if (ee->left.isConstant()) {
+      if (ee->left->isConstant()) {
         if (ee->left->getWidth() == Expr::Bool) {
           _getImpliedValue(ee->right, !ee->left->getConstantValue(), results);
         }
@@ -197,13 +197,13 @@ static void _getImpliedValue(ref<Expr> e,
 void ImpliedValue::getImpliedValues(ref<Expr> e, 
                                     ref<Expr> value, 
                                     ImpliedValueList &results) {
-  assert(value.isConstant() && "non-constant in place of constant");
+  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");
+  assert(value->isConstant() && "non-constant in place of constant");
 
   std::vector<ref<ReadExpr> > reads;
   std::map<ref<ReadExpr>, ref<Expr> > found;
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index e03254a5..de48651b 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -301,7 +301,7 @@ ref<Expr> ObjectState::read8(unsigned offset) const {
 }
 
 ref<Expr> ObjectState::read8(ref<Expr> offset) const {
-  assert(!offset.isConstant() && "constant offset passed to symbolic read8");
+  assert(!offset->isConstant() && "constant offset passed to symbolic read8");
   unsigned base, size;
   fastRangeCheckOffset(offset, &base, &size);
   flushRangeForRead(base, size);
@@ -328,7 +328,7 @@ void ObjectState::write8(unsigned offset, uint8_t value) {
 
 void ObjectState::write8(unsigned offset, ref<Expr> value) {
   // can happen when ExtractExpr special cases
-  if (value.isConstant()) {
+  if (value->isConstant()) {
     write8(offset, (uint8_t) value->getConstantValue());
   } else {
     setKnownSymbolic(offset, value.get());
@@ -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(!offset->isConstant() && "constant offset passed to symbolic write8");
   unsigned base, size;
   fastRangeCheckOffset(offset, &base, &size);
   flushRangeForWrite(base, size);
@@ -358,7 +358,7 @@ void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
 /***/
 
 ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
-  if (offset.isConstant()) {
+  if (offset->isConstant()) {
     return read((unsigned) offset->getConstantValue(), width);
   } else { 
     switch (width) {
@@ -547,7 +547,7 @@ ref<Expr> ObjectState::read64(ref<Expr> offset) const {
 
 void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
-  if (offset.isConstant()) {
+  if (offset->isConstant()) {
     write(offset->getConstantValue(), value);
   } else {
     switch(w) {
@@ -563,7 +563,7 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
 
 void ObjectState::write(unsigned offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
-  if (value.isConstant()) {
+  if (value->isConstant()) {
     uint64_t val = value->getConstantValue();
     switch(w) {
     case  Expr::Bool:
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index bb6496ac..30377ee4 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -77,7 +77,7 @@ 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()) {
+    if (re->index->isConstant()) {
       unsigned index = (unsigned) re->index->getConstantValue();
       directReads.insert(std::make_pair(re->updates.root, index));
     }
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 594a6518..b2e5d277 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -176,7 +176,7 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
                                                         ref<Expr> address) {
   ObjectPair op;
   address = executor.toUnique(state, address);
-  assert(address.isConstant() && "symbolic string arg to intrinsic");  
+  assert(address->isConstant() && "symbolic string arg to intrinsic");  
   if (!state.addressSpace.resolveOne(address->getConstantValue(), op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
   bool res;
@@ -195,7 +195,7 @@ 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(cur->isConstant() && 
            "hit symbolic char while reading concrete string");
     buf[i] = cur->getConstantValue();
   }
@@ -375,7 +375,7 @@ void SpecialFunctionHandler::handleIsSymbolic(ExecutionState &state,
   assert(arguments.size()==1 && "invalid number of arguments to klee_is_symbolic");
 
   executor.bindLocal(target, state, 
-                     ConstantExpr::create(!arguments[0].isConstant(), Expr::Int32));
+                     ConstantExpr::create(!arguments[0]->isConstant(), Expr::Int32));
 }
 
 void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
@@ -414,7 +414,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
   // XXX should type check args
   assert(arguments.size()==1 &&
          "invalid number of arguments to klee_under_constrained().");
-  assert(arguments[0].isConstant() &&
+  assert(arguments[0]->isConstant() &&
    	 "symbolic argument given to klee_under_constrained!");
 
   unsigned v = arguments[0]->getConstantValue();
@@ -438,7 +438,7 @@ 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 (!value->isConstant()) {
     executor.terminateStateOnError(state, 
                                    "klee_set_forking requires a constant arg",
                                    "user.err");
@@ -476,7 +476,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 (!arguments[1]->isConstant()) {
     // FIXME: Pull into a unique value method?
     ref<Expr> value;
     bool success = executor.solver->getValue(state, arguments[1], value);
@@ -582,14 +582,15 @@ void SpecialFunctionHandler::handleFree(ExecutionState &state,
 }
 
 void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
-                                            KInstruction *target,
-                                            std::vector<ref<Expr> > &arguments) {
+                                                     KInstruction *target,
+                                                     std::vector<ref<Expr> > 
+                                                       &arguments) {
   assert(arguments.size()==2 &&
          "invalid number of arguments to klee_check_memory_access");
 
   ref<Expr> address = executor.toUnique(state, arguments[0]);
   ref<Expr> size = executor.toUnique(state, arguments[1]);
-  if (!address.isConstant() || !size.isConstant()) {
+  if (!address->isConstant() || !size->isConstant()) {
     executor.terminateStateOnError(state, 
                                    "check_memory_access requires constant args",
                                    "user.err");
@@ -604,7 +605,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
                                                       size->getConstantValue());
-      assert(chk.isConstant());
+      assert(chk->isConstant());
       if (!chk->getConstantValue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
@@ -629,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(arguments[0]->isConstant() &&
          "expect constant address argument to klee_define_fixed_object");
-  assert(arguments[1].isConstant() &&
+  assert(arguments[1]->isConstant() &&
          "expect constant size argument to klee_define_fixed_object");
   
   uint64_t address = arguments[0]->getConstantValue();
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 55fa7c8d..9efb77b8 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -25,7 +25,7 @@ using namespace llvm;
 bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
                             Solver::Validity &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr.isConstant()) {
+  if (expr->isConstant()) {
     result = expr->getConstantValue() ? Solver::True : Solver::False;
     return true;
   }
@@ -49,7 +49,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
 bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, 
                               bool &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr.isConstant()) {
+  if (expr->isConstant()) {
     result = expr->getConstantValue() ? true : false;
     return true;
   }
@@ -96,7 +96,7 @@ bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr,
 bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, 
                             ref<Expr> &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr.isConstant()) {
+  if (expr->isConstant()) {
     result = expr;
     return true;
   }
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 472c0aa3..93384060 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -87,7 +87,7 @@ void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
 }
 
 ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
-  if (e.isConstant())
+  if (e->isConstant())
     return e;
 
   std::map< ref<Expr>, ref<Expr> > equalities;
@@ -95,7 +95,7 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
   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()) {
+      if (ee->left->isConstant()) {
         equalities.insert(std::make_pair(ee->right,
                                          ee->left));
       } else {
@@ -135,7 +135,7 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 
   case Expr::Eq: {
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
-    if (be->left.isConstant()) {
+    if (be->left->isConstant()) {
       ExprReplaceVisitor visitor(be->right, be->left);
       rewriteConstraints(visitor);
     }
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 4c6f5e43..9a78f188 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -378,7 +378,7 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
   for (; un; un=un->next) {
     ref<Expr> cond = EqExpr::create(index, un->index);
     
-    if (cond.isConstant()) {
+    if (cond->isConstant()) {
       if (cond->getConstantValue())
         return un->value;
     } else {
@@ -399,18 +399,18 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
   assert(c->getWidth()==Bool && "type mismatch");
   assert(kt==f->getWidth() && "type mismatch");
 
-  if (c.isConstant()) {
+  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->isConstant()) {      
       if (t->getConstantValue()) {
         return OrExpr::create(c, f);
       } else {
         return AndExpr::create(Expr::createNot(c), f);
       }
-    } else if (f.isConstant()) {
+    } else if (f->isConstant()) {
       if (f->getConstantValue()) {
         return OrExpr::create(Expr::createNot(c), t);
       } else {
@@ -485,7 +485,7 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
   
   if (w == kw)
     return expr;
-  else if (expr.isConstant()) {
+  else if (expr->isConstant()) {
     return ConstantExpr::create(ints::trunc(expr->getConstantValue() >> off, w, kw), w);
   } 
   else 
@@ -521,7 +521,7 @@ ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
-    if (e.isConstant()) {
+    if (e->isConstant()) {
       return ConstantExpr::create(ints::zext(e->getConstantValue(), w, kBits),
                                   w);
     }
@@ -537,7 +537,7 @@ ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
-    if (e.isConstant()) {
+    if (e->isConstant()) {
       return ConstantExpr::create(ints::sext(e->getConstantValue(), w, kBits),
                                   w);
     }
@@ -557,7 +557,7 @@ 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");
+  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -567,10 +567,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 && 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
+    } 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 {
@@ -588,16 +588,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 && 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)
+    } 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)
+    } 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)
+    } 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 {
@@ -607,17 +607,17 @@ 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");
+  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
+    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
+    } 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 {
@@ -626,7 +626,7 @@ static ref<Expr> SubExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   }
 }
 static ref<Expr> SubExpr_createPartial(Expr *l, const ref<Expr> &cr) {
-  assert(cr.isConstant() && "non-constant passed in place of constant");
+  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);
@@ -642,16 +642,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 && 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)
+    } 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
+    } 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
+    } 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 {
@@ -661,7 +661,7 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> MulExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
-  assert(cl.isConstant() && "non-constant passed in place of constant");
+  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -689,7 +689,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");
+  assert(cr->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
 
@@ -709,7 +709,7 @@ static ref<Expr> AndExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> OrExpr_createPartial(Expr *l, const ref<Expr> &cr) {
-  assert(cr.isConstant() && "non-constant passed in place of constant");
+  assert(cr->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
 
@@ -729,7 +729,7 @@ static ref<Expr> OrExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
-  assert(cl.isConstant() && "non-constant passed in place of constant");
+  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -812,8 +812,8 @@ 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()) {                              \
+  if (l->isConstant()) {                                \
+    if (r->isConstant()) {                              \
       Expr::Width width = l->getWidth(); \
       uint64_t val = ints::_op(l->getConstantValue(),  \
                                r->getConstantValue(), width);  \
@@ -821,7 +821,7 @@ ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
     } else { \
       return _e_op ## _createPartialR(l, r.get()); \
     } \
-  } else if (r.isConstant()) {             \
+  } else if (r->isConstant()) {             \
     return _e_op ## _createPartial(l.get(), r); \
   } \
   return _e_op ## _create(l.get(), r.get()); \
@@ -830,8 +830,8 @@ ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
 #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()) {                              \
+  if (l->isConstant()) {                                \
+    if (r->isConstant()) {                              \
       Expr::Width width = l->getWidth(); \
       uint64_t val = ints::_op(l->getConstantValue(), \
                                r->getConstantValue(), width);  \
@@ -858,8 +858,8 @@ 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()) {                              \
+  if (l->isConstant()) {                                \
+    if (r->isConstant()) {                              \
       Expr::Width width = l->getWidth(); \
       uint64_t val = ints::_op(l->getConstantValue(), \
                                r->getConstantValue(), width);  \
@@ -872,8 +872,8 @@ ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &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()) {                              \
+  if (l->isConstant()) {                                \
+    if (r->isConstant()) {                              \
       Expr::Width width = l->getWidth(); \
       uint64_t val = ints::_op(l->getConstantValue(), \
                                r->getConstantValue(), width);  \
@@ -881,7 +881,7 @@ ref<Expr>  _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
     } else { \
       return partialR(l, r.get()); \
     } \
-  } else if (r.isConstant()) {                  \
+  } else if (r->isConstant()) {                  \
     return partialL(l.get(), r); \
   } else { \
     return _e_op ## _create(l.get(), r.get()); \
@@ -904,7 +904,7 @@ static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 /// returns the initial equality expression. 
 static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl, 
 				  ReadExpr *rd) {
-  assert(cl.isConstant() && "constant expression required");
+  assert(cl->isConstant() && "constant expression required");
   assert(rd->getKind() == Expr::Read && "read expression required");
   
   uint64_t ct = cl->getConstantValue();
@@ -926,7 +926,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 
       ref<Expr> idx = un->index;
       ref<Expr> val = un->value;
-      if (!idx.isConstant() || !val.isConstant()) {
+      if (!idx->isConstant() || !val->isConstant()) {
 	all_const = false;
 	//llvm::cerr << "Idx or val not constant\n";
 	break;
@@ -973,7 +973,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 
 
 static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {  
-  assert(cl.isConstant() && "non-constant passed in place of constant");
+  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width width = cl->getWidth();
 
@@ -988,7 +988,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
         const EqExpr *ree = static_ref_cast<EqExpr>(r);
 
         // eliminate double negation
-        if (ree->left.isConstant() &&
+        if (ree->left->isConstant() &&
             ree->left->getWidth()==Expr::Bool) {
           assert(!ree->left->getConstantValue());
           return ree->right;
@@ -1029,14 +1029,14 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
     }
   } else if (rk==Expr::Add) {
     const AddExpr *ae = static_ref_cast<AddExpr>(r);
-    if (ae->left.isConstant()) {
+    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()) {
+    if (se->left->isConstant()) {
       // c0 = c1 - b => c1 - c0 = b
       return EqExpr_createPartialR(SubExpr::create(se->left, cl),
                                    se->right.get());
@@ -1076,7 +1076,7 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (t == Expr::Bool) { // !l && r
     return AndExpr::create(Expr::createNot(l), r);
   } else {
-    if (r.isConstant()) {      
+    if (r->isConstant()) {      
       uint64_t value = r->getConstantValue();
       if (value <= 8) {
         ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 0c04a538..038fe8b8 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -16,7 +16,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
   for (const UpdateNode *un=ul.head; un; un=un->next) {
     ref<Expr> ui = visit(un->index);
     
-    if (ui.isConstant()) {
+    if (ui->isConstant()) {
       if (ui->getConstantValue() == index)
         return Action::changeTo(visit(un->value));
     } else {
@@ -36,7 +36,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
 ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);
   
-  if (v.isConstant()) {
+  if (v->isConstant()) {
     return evalRead(re.updates, v->getConstantValue());
   } else {
     return Action::doChildren();
@@ -50,7 +50,7 @@ ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
   ref<Expr> kids[2] = { visit(e.left),
                         visit(e.right) };
 
-  if (kids[1].isConstant() && !kids[1]->getConstantValue())
+  if (kids[1]->isConstant() && !kids[1]->getConstantValue())
     kids[1] = e.right;
 
   if (kids[0]!=e.left || kids[1]!=e.right) {
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 08809684..da4f45f9 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 e->isConstant() || 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 (!e->isConstant()) {
       if (couldPrint.insert(e).second) {
         Expr *ep = e.get();
         for (unsigned i=0; i<ep->getNumKids(); i++)
@@ -208,7 +208,7 @@ class PPrinter : public ExprPPrinter {
       print(un->value, PC);
       //PC << ')';
       
-      nextShouldBreak = !(un->index.isConstant() && un->value.isConstant());
+      nextShouldBreak = !(un->index->isConstant() && un->value->isConstant());
     }
 
     if (openedList)
@@ -324,7 +324,7 @@ public:
   }
 
   void printConst(const ref<Expr> &e, PrintContext &PC, bool printWidth) {
-    assert(e.isConstant());
+    assert(e->isConstant());
 
     if (e->getWidth() == Expr::Bool)
       PC << (e->getConstantValue() ? "true" : "false");
@@ -343,7 +343,7 @@ public:
   }
 
   void print(const ref<Expr> &e, PrintContext &PC, bool printConstWidth=false) {
-    if (e.isConstant()) 
+    if (e->isConstant()) 
       printConst(e, PC, printConstWidth);
     else {
       std::map<ref<Expr>, unsigned>::iterator it = bindings.find(e);
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index f74b519f..192c18a5 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 (!e->isConstant()) {
     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 (!re->index->isConstant() &&
           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 (!un->index->isConstant() &&
                 visited.insert(un->index).second)
               stack.push_back(un->index);
-            if (!un->value.isConstant() &&
+            if (!un->value->isConstant() &&
                 visited.insert(un->value).second)
               stack.push_back(un->value);
           }
         }
       }
-    } else if (!top.isConstant()) {
+    } 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() &&
+        if (!k->isConstant() &&
             visited.insert(k).second)
           stack.push_back(k);
       }
diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp
index b15cdffa..5e9d0a81 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 || e->isConstant()) {
     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 (e->isConstant()) {    
     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 (!e->isConstant()) {
         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 70c1cc76..5f666269 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -929,7 +929,7 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
   if (!OffsetExpr.isValid() || !Child.isValid())
     return ConstantExpr::alloc(0, ResTy);
 
-  assert(OffsetExpr.get().isConstant() && "ParseNumber returned non-constant.");
+  assert(OffsetExpr.get()->isConstant() && "ParseNumber returned non-constant.");
   unsigned Offset = (unsigned) OffsetExpr.get()->getConstantValue();
 
   if (Offset + ResTy > Child.get()->getWidth()) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index db15632b..546d81fd 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -138,7 +138,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
                                         Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg.isConstant()) {
+  if (neg->isConstant()) {
     if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
@@ -153,7 +153,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg.isConstant()) {
+  if (neg->isConstant()) {
     if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
@@ -217,7 +217,7 @@ 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(q->isConstant() && "assignment evaluation did not result in constant");
 
   if (q->getConstantValue()) {
     if (!getAssignment(query, a))
@@ -268,7 +268,7 @@ bool CexCachingSolver::computeValue(const Query& query,
     return false;
   assert(a && "computeValue() must have assignment");
   result = a->evaluate(query.expr);  
-  assert(result.isConstant() && 
+  assert(result->isConstant() && 
          "assignment evaluation did not result in constant");
   return true;
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 88f34c99..ee46be4f 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -416,7 +416,7 @@ public:
 
       // XXX we need to respect the version here and object state chain
 
-      if (re->index.isConstant() && 
+      if (re->index->isConstant() && 
           re->index->getConstantValue() < array->size) {
         CexValueData &cvd = cod.values[re->index->getConstantValue()];
         CexValueData tmp = cvd.set_intersection(range);
@@ -613,7 +613,7 @@ public:
     case Expr::Eq: {
       BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
       if (range.isFixed()) {
-        if (be->left.isConstant()) {
+        if (be->left->isConstant()) {
           uint64_t value = be->left->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
@@ -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 (!v->isConstant()) 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 (value->isConstant()) {
     result = value;
     return true;
   } else {
@@ -939,7 +939,7 @@ FastCexSolver::computeInitialValues(const Query& query,
                                   ConstantExpr::create(i,
                                                        kMachinePointerType)));
       
-      if (value.isConstant()) {
+      if (value->isConstant()) {
         data.push_back(value->getConstantValue());
       } else {
         // FIXME: When does this happen?
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 18e5c84d..4e004fd8 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -97,7 +97,7 @@ public:
       if (re->updates.isRooted) {
         const Array *array = re->updates.root;
         if (!wholeObjects.count(array)) {
-          if (re->index.isConstant()) {
+          if (re->index->isConstant()) {
             DenseSet<unsigned> &dis = elements[array];
             dis.add((unsigned) re->index->getConstantValue());
           } else {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 1d27c655..d1f7360c 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 || e->isConstant()) {
     return constructActual(e, width_out);
   } else {
     ExprHashMap< std::pair<ExprHandle, unsigned> >::iterator it = 
@@ -555,7 +555,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (me->left.isConstant()) {
+    if (me->left->isConstant()) {
       return constructMulByConstant(right, *width_out, 
                                     me->left->getConstantValue());
     } else {
@@ -569,7 +569,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized udiv");
     
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
@@ -591,7 +591,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
  
       if (optimizeDivides) {
@@ -611,7 +611,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized urem");
     
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
@@ -710,7 +710,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(se->left, width_out);
     assert(*width_out!=1 && "uncanonicalized shl");
 
-    if (se->right.isConstant()) {
+    if (se->right->isConstant()) {
       return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
     } else {
       int shiftWidth;
@@ -725,7 +725,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
-    if (lse->right.isConstant()) {
+    if (lse->right->isConstant()) {
       return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
     } else {
       int shiftWidth;
@@ -739,7 +739,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ase->left, width_out);
     assert(*width_out!=1 && "uncanonicalized ashr");
     
-    if (ase->right.isConstant()) {
+    if (ase->right->isConstant()) {
       unsigned shift = (unsigned) ase->right->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
@@ -757,7 +757,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ee->left, width_out);
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
-      if (ee->left.isConstant()) {
+      if (ee->left->isConstant()) {
         assert(!ee->left->getConstantValue() && "uncanonicalized eq");
         return vc_notExpr(vc, right);
       } else {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 8990e3b9..46d6039e 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -56,7 +56,7 @@ bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr.isConstant()) {
+  if (query.expr->isConstant()) {
     result = query.expr->getConstantValue() ? True : False;
     return true;
   }
@@ -82,7 +82,7 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr.isConstant()) {
+  if (query.expr->isConstant()) {
     result = query.expr->getConstantValue() ? true : false;
     return true;
   }
@@ -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 (query.expr->isConstant()) {
     result = query.expr;
     return true;
   }
@@ -151,7 +151,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
     default:
       min = 0, max = 1; break;
     }
-  } else if (e.isConstant()) {
+  } else if (e->isConstant()) {
     min = max = e->getConstantValue();
   } else {
     // binary search for # of useful bits
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 00:11:18 +0000