about summary refs log tree commit diff homepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/AddressSpace.cpp8
-rw-r--r--lib/Core/Executor.cpp83
-rw-r--r--lib/Core/ImpliedValue.cpp41
-rw-r--r--lib/Core/Memory.cpp12
-rw-r--r--lib/Core/SeedInfo.cpp6
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp26
-rw-r--r--lib/Core/TimingSolver.cpp4
7 files changed, 90 insertions, 90 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index fb032fd5..9a9a0235 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -73,7 +73,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
                               ObjectPair &result,
                               bool &success) {
   if (address.isConstant()) {
-    success = resolveOne(address.getConstantValue(), result);
+    success = resolveOne(address->getConstantValue(), result);
     return true;
   } else {
     TimerStatIncrementer timer(stats::resolveTime);
@@ -83,7 +83,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
     ref<Expr> cex(0);
     if (!solver->getValue(state, address, cex))
       return false;
-    unsigned example = (unsigned) cex.getConstantValue();
+    unsigned example = (unsigned) cex->getConstantValue();
     MemoryObject hack(example);
     const MemoryMap::value_type *res = objects.lookup_previous(&hack);
     
@@ -165,7 +165,7 @@ bool AddressSpace::resolve(ExecutionState &state,
                            double timeout) {
   if (p.isConstant()) {
     ObjectPair res;
-    if (resolveOne(p.getConstantValue(), res))
+    if (resolveOne(p->getConstantValue(), res))
       rl.push_back(res);
     return false;
   } else {
@@ -190,7 +190,7 @@ bool AddressSpace::resolve(ExecutionState &state,
     ref<Expr> cex(0);
     if (!solver->getValue(state, p, cex))
       return true;
-    unsigned example = (unsigned) cex.getConstantValue();
+    unsigned example = (unsigned) cex->getConstantValue();
     MemoryObject hack(example);
     
     MemoryMap::iterator oi = objects.upper_bound(&hack);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f7c22fe0..bb4bcb53 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -628,7 +628,7 @@ void Executor::branch(ExecutionState &state,
           solver->getValue(state, siit->assignment.evaluate(conditions[i]), 
                            res);
         assert(success && "FIXME: Unhandled solver failure");
-        if (res.getConstantValue())
+        if (res->getConstantValue())
           break;
       }
       
@@ -754,7 +754,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
         solver->getValue(current, siit->assignment.evaluate(condition), res);
       assert(success && "FIXME: Unhandled solver failure");
       if (res.isConstant()) {
-        if (res.getConstantValue()) {
+        if (res->getConstantValue()) {
           trueSeed = true;
         } else {
           falseSeed = true;
@@ -818,7 +818,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.getConstantValue()) {
+        if (res->getConstantValue()) {
           trueSeeds.push_back(*siit);
         } else {
           falseSeeds.push_back(*siit);
@@ -875,7 +875,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
 void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
   if (condition.isConstant()) {
-    assert(condition.getConstantValue() &&
+    assert(condition->getConstantValue() &&
            "attempt to add invalid constraint");
     return;
   }
@@ -1182,7 +1182,7 @@ void Executor::executeCall(ExecutionState &state,
       StackFrame &sf = state.stack.back();
       unsigned size = 0;
       for (unsigned i = funcArgs; i < callingArgs; i++)
-        size += Expr::getMinBytesForWidth(arguments[i].getWidth());
+        size += Expr::getMinBytesForWidth(arguments[i]->getWidth());
 
       MemoryObject *mo = sf.varargs = memory->allocate(size, true, false, 
                                                        state.prevPC->inst);
@@ -1195,7 +1195,7 @@ void Executor::executeCall(ExecutionState &state,
       for (unsigned i = funcArgs; i < callingArgs; i++) {
         // XXX: DRE: i think we bind memory objects here?
         os->write(offset, arguments[i]);
-        offset += Expr::getMinBytesForWidth(arguments[i].getWidth());
+        offset += Expr::getMinBytesForWidth(arguments[i]->getWidth());
       }
     }
 
@@ -1298,7 +1298,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         const Type *t = caller->getType();
         if (t != Type::VoidTy) {
           // may need to do coercion due to bitcasts
-          Expr::Width from = result.getWidth();
+          Expr::Width from = result->getWidth();
           Expr::Width to = Expr::getWidthForLLVMType(t);
             
           if (from != to) {
@@ -1397,7 +1397,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // 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());
+                                         cond->getConstantValue());
       unsigned index = si->findCaseValue(ci);
       transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
     } else {
@@ -1495,7 +1495,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         for (std::vector< ref<Expr> >::iterator
                ai = arguments.begin(), ie = arguments.end();
              ai != ie; ++ai) {
-          Expr::Width to, from = (*ai).getWidth();
+          Expr::Width to, from = (*ai)->getWidth();
             
           if (i<fType->getNumParams()) {
             to = Expr::getWidthForLLVMType(fType->getParamType(i));
@@ -1535,7 +1535,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
         assert(success && "FIXME: Unhandled solver failure");
         StatePair res = fork(*free, EqExpr::create(v, value), true);
         if (res.first) {
-          void *addr = (void*) (unsigned long) value.getConstantValue();
+          void *addr = (void*) (unsigned long) value->getConstantValue();
           std::set<void*>::iterator it = legalFunctions.find(addr);
           if (it != legalFunctions.end()) {
             f = (Function*) addr;
@@ -1587,8 +1587,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Arithmetic / logical
 #define FP_CONSTANT_BINOP(op, type, l, r, target, state) \
         bindLocal(target, state, \
-                  ConstantExpr::alloc(op(toConstant(state, l, "floating point").getConstantValue(), \
-                                         toConstant(state, r, "floating point").getConstantValue(), \
+                  ConstantExpr::alloc(op(toConstant(state, l, "floating point")->getConstantValue(), \
+                                         toConstant(state, r, "floating point")->getConstantValue(), \
                                          type), type))
   case Instruction::Add: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
@@ -1912,9 +1912,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::trunc(arg.getConstantValue(),
+    uint64_t value = floats::trunc(arg->getConstantValue(),
                                    resultType,
-                                   arg.getWidth());
+                                   arg->getWidth());
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
@@ -1924,9 +1924,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::ext(arg.getConstantValue(),
+    uint64_t value = floats::ext(arg->getConstantValue(),
                                  resultType,
-                                 arg.getWidth());
+                                 arg->getWidth());
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
@@ -1936,9 +1936,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
+    uint64_t value = floats::toUnsignedInt(arg->getConstantValue(),
                                            resultType,
-                                           arg.getWidth());
+                                           arg->getWidth());
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
@@ -1948,9 +1948,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::toSignedInt(arg.getConstantValue(),
+    uint64_t value = floats::toSignedInt(arg->getConstantValue(),
                                          resultType,
-                                         arg.getWidth());
+                                         arg->getWidth());
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
@@ -1960,7 +1960,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
+    uint64_t value = floats::UnsignedIntToFP(arg->getConstantValue(),
                                              resultType);
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
@@ -1971,9 +1971,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
     ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
-    uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
+    uint64_t value = floats::SignedIntToFP(arg->getConstantValue(),
                                            resultType,
-                                           arg.getWidth());
+                                           arg->getWidth());
     bindLocal(ki, state, ConstantExpr::alloc(value, resultType));
     break;
   }
@@ -1985,11 +1985,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                  "floating point");
     ref<Expr> right = toConstant(state, eval(ki, 1, state).value,
                                  "floating point");
-    uint64_t leftVal = left.getConstantValue();
-    uint64_t rightVal = right.getConstantValue();
+    uint64_t leftVal = left->getConstantValue();
+    uint64_t rightVal = right->getConstantValue();
  
     //determine whether the operands are NANs
-    unsigned inWidth = left.getWidth();
+    unsigned inWidth = left->getWidth();
     bool leftIsNaN   = floats::isNaN( leftVal,  inWidth );
     bool rightIsNaN  = floats::isNaN( rightVal, inWidth );
 
@@ -2181,7 +2181,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
     index++;
   }
   assert(constantOffset.isConstant());
-  kgepi->offset = constantOffset.getConstantValue();
+  kgepi->offset = constantOffset->getConstantValue();
 }
 
 void Executor::bindModuleConstants() {
@@ -2347,12 +2347,12 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   info << "\taddress: " << address << "\n";
   uint64_t example;
   if (address.isConstant()) {
-    example = address.getConstantValue();
+    example = address->getConstantValue();
   } else {
     ref<Expr> value;
     bool success = solver->getValue(state, address, value);
     assert(success && "FIXME: Unhandled solver failure");
-    example = value.getConstantValue();
+    example = value->getConstantValue();
     info << "\texample: " << example << "\n";
     std::pair< ref<Expr>, ref<Expr> > res = solver->getRange(state, address);
     info << "\trange: [" << res.first << ", " << res.second <<"]\n";
@@ -2587,11 +2587,11 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
   // create a new fresh location, assert it is equal to concrete value in e
   // and return it.
   
-  const MemoryObject *mo = memory->allocate(Expr::getMinBytesForWidth(e.getWidth()), 
-                                            false, false,
-                                            state.prevPC->inst);
+  const MemoryObject *mo =
+    memory->allocate(Expr::getMinBytesForWidth(e->getWidth()), false, false,
+                     state.prevPC->inst);
   assert(mo && "out of memory");
-  ref<Expr> res = Expr::createTempRead(mo->array, e.getWidth());
+  ref<Expr> res = Expr::createTempRead(mo->array, e->getWidth());
   ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
   llvm::cerr << "Making symbolic: " << eq << "\n";
   state.addConstraint(eq);
@@ -2621,8 +2621,9 @@ void Executor::executeAlloc(ExecutionState &state,
                             const ObjectState *reallocFrom) {
   size = toUnique(state, size);
   if (size.isConstant()) {
-    MemoryObject *mo = memory->allocate(size.getConstantValue(), isLocal, false,
-                                        state.prevPC->inst);
+    MemoryObject *mo = 
+      memory->allocate(size->getConstantValue(), isLocal, false, 
+                       state.prevPC->inst);
     if (!mo) {
       bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
     } else {
@@ -2658,9 +2659,9 @@ void Executor::executeAlloc(ExecutionState &state,
     assert(success && "FIXME: Unhandled solver failure");
     
     // Try and start with a small example
-    while (example.getConstantValue()>128) {
-      ref<Expr> tmp = ConstantExpr::alloc(example.getConstantValue() >> 1, 
-                                          example.getWidth());
+    while (example->getConstantValue() > 128) {
+      ref<Expr> tmp = ConstantExpr::alloc(example->getConstantValue() >> 1, 
+                                          example->getWidth());
       bool res;
       bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
       assert(success && "FIXME: Unhandled solver failure");      
@@ -2787,7 +2788,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
                                       ref<Expr> address,
                                       ref<Expr> value /* undef if read */,
                                       KInstruction *target /* undef if write */) {
-  Expr::Width type = (isWrite ? value.getWidth() : 
+  Expr::Width type = (isWrite ? value->getWidth() : 
                      Expr::getWidthForLLVMType(target->inst->getType()));
   unsigned bytes = Expr::getMinBytesForWidth(type);
 
@@ -2804,7 +2805,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   solver->setTimeout(stpTimeout);
   if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
     address = toConstant(state, address, "resolveOne failure");
-    success = state.addressSpace.resolveOne(address.getConstantValue(), op);
+    success = state.addressSpace.resolveOne(address->getConstantValue(), op);
   }
   solver->setTimeout(0);
 
@@ -3198,7 +3199,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state,
       } else {
         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(re->index->getConstantValue(), it->second);
       }
     }
   }
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 1de47d0c..c73ae4f1 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -28,10 +28,9 @@ using namespace klee;
 static void _getImpliedValue(ref<Expr> e,
                              uint64_t value,
                              ImpliedValueList &results) {
-  switch (e.getKind()) {
-    
+  switch (e->getKind()) {
   case Expr::Constant: {
-    assert(value == e.getConstantValue() && "error in implied value calculation");
+    assert(value == e->getConstantValue() && "error in implied value calculation");
     break;
   }
 
@@ -46,7 +45,7 @@ static void _getImpliedValue(ref<Expr> e,
     // would work often enough to be worth the effort.
     ReadExpr *re = static_ref_cast<ReadExpr>(e);
     results.push_back(std::make_pair(re, 
-                                     ConstantExpr::create(value, e.getWidth())));
+                                     ConstantExpr::create(value, e->getWidth())));
     break;
   }
     
@@ -56,11 +55,11 @@ static void _getImpliedValue(ref<Expr> e,
     
     if (se->trueExpr.isConstant()) {
       if (se->falseExpr.isConstant()) {
-        if (se->trueExpr.getConstantValue() != se->falseExpr.getConstantValue()) {
-          if (value == se->trueExpr.getConstantValue()) {
+        if (se->trueExpr->getConstantValue() != se->falseExpr->getConstantValue()) {
+          if (value == se->trueExpr->getConstantValue()) {
             _getImpliedValue(se->cond, 1, results);
           } else {
-            assert(value == se->falseExpr.getConstantValue() &&
+            assert(value == se->falseExpr->getConstantValue() &&
                    "err in implied value calculation");
             _getImpliedValue(se->cond, 0, results);
           }
@@ -72,8 +71,8 @@ static void _getImpliedValue(ref<Expr> e,
 
   case Expr::Concat: {
     ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
-    _getImpliedValue(ce->getKid(0), (value >> ce->getKid(1).getWidth()) & ((1 << ce->getKid(0).getWidth()) - 1), results);
-    _getImpliedValue(ce->getKid(1), value & ((1 << ce->getKid(1).getWidth()) - 1), results);
+    _getImpliedValue(ce->getKid(0), (value >> ce->getKid(1)->getWidth()) & ((1 << ce->getKid(0)->getWidth()) - 1), results);
+    _getImpliedValue(ce->getKid(1), value & ((1 << ce->getKid(1)->getWidth()) - 1), results);
     break;
   }
     
@@ -89,7 +88,7 @@ static void _getImpliedValue(ref<Expr> e,
     CastExpr *ce = static_ref_cast<CastExpr>(e);
     _getImpliedValue(ce->src, 
                      bits64::truncateToNBits(value, 
-					     ce->src.getWidth()),
+					     ce->src->getWidth()),
                      results);
     break;
   }
@@ -100,8 +99,8 @@ static void _getImpliedValue(ref<Expr> e,
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
     if (be->left.isConstant()) {
       uint64_t nvalue = ints::sub(value,
-                                  be->left.getConstantValue(),
-                                  be->left.getWidth());
+                                  be->left->getConstantValue(),
+                                  be->left->getWidth());
       _getImpliedValue(be->right, nvalue, results);
     }
     break;
@@ -109,9 +108,9 @@ static void _getImpliedValue(ref<Expr> e,
   case Expr::Sub: { // constants on left
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
     if (be->left.isConstant()) {
-      uint64_t nvalue = ints::sub(be->left.getConstantValue(),
+      uint64_t nvalue = ints::sub(be->left->getConstantValue(),
                                   value,
-                                  be->left.getWidth());
+                                  be->left->getWidth());
       _getImpliedValue(be->right, nvalue, results);
     }
     break;
@@ -158,7 +157,7 @@ static void _getImpliedValue(ref<Expr> e,
   case Expr::Xor: { // constants on left
     BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
     if (be->left.isConstant()) {
-      _getImpliedValue(be->right, value ^ be->left.getConstantValue(), results);
+      _getImpliedValue(be->right, value ^ be->left->getConstantValue(), results);
     }
     break;
   }
@@ -171,7 +170,7 @@ static void _getImpliedValue(ref<Expr> e,
     EqExpr *ee = static_ref_cast<EqExpr>(e);
     if (value) {
       if (ee->left.isConstant())
-        _getImpliedValue(ee->right, ee->left.getConstantValue(), results);
+        _getImpliedValue(ee->right, ee->left->getConstantValue(), results);
     } else {
       // look for limited value range, woohoo
       //
@@ -182,8 +181,8 @@ static void _getImpliedValue(ref<Expr> e,
       // valued and distinct.
       
       if (ee->left.isConstant()) {
-        if (ee->left.getWidth() == Expr::Bool) {
-          _getImpliedValue(ee->right, !ee->left.getConstantValue(), results);
+        if (ee->left->getWidth() == Expr::Bool) {
+          _getImpliedValue(ee->right, !ee->left->getConstantValue(), results);
         }
       }
     }
@@ -199,7 +198,7 @@ void ImpliedValue::getImpliedValues(ref<Expr> e,
                                     ref<Expr> value, 
                                     ImpliedValueList &results) {
   assert(value.isConstant() && "non-constant in place of constant");
-  _getImpliedValue(e, value.getConstantValue(), results);
+  _getImpliedValue(e, value->getConstantValue(), results);
 }
 
 void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, 
@@ -216,7 +215,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
        i != ie; ++i) {
     std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(i->first);
     if (it != found.end()) {
-      assert(it->second.getConstantValue() == i->second.getConstantValue() &&
+      assert(it->second->getConstantValue() == i->second->getConstantValue() &&
              "I don't think so Scott");
     } else {
       found.insert(std::make_pair(i->first, i->second));
@@ -257,7 +256,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
     assert(success && "FIXME: Unhandled solver failure");    
     if (res) {
       if (it != found.end()) {
-        assert(possible.getConstantValue() == it->second.getConstantValue());
+        assert(possible->getConstantValue() == it->second->getConstantValue());
         found.erase(it);
       }
     } else {
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index cd563551..e03254a5 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -329,7 +329,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()) {
-    write8(offset, (uint8_t) value.getConstantValue());
+    write8(offset, (uint8_t) value->getConstantValue());
   } else {
     setKnownSymbolic(offset, value.get());
       
@@ -359,7 +359,7 @@ void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
 
 ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
   if (offset.isConstant()) {
-    return read((unsigned) offset.getConstantValue(), width);
+    return read((unsigned) offset->getConstantValue(), width);
   } else { 
     switch (width) {
     case  Expr::Bool: return  read1(offset);
@@ -546,9 +546,9 @@ ref<Expr> ObjectState::read64(ref<Expr> offset) const {
 }
 
 void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
-  Expr::Width w = value.getWidth();
+  Expr::Width w = value->getWidth();
   if (offset.isConstant()) {
-    write(offset.getConstantValue(), value);
+    write(offset->getConstantValue(), value);
   } else {
     switch(w) {
     case  Expr::Bool:  write1(offset, value); break;
@@ -562,9 +562,9 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
 }
 
 void ObjectState::write(unsigned offset, ref<Expr> value) {
-  Expr::Width w = value.getWidth();
+  Expr::Width w = value->getWidth();
   if (value.isConstant()) {
-    uint64_t val = value.getConstantValue();
+    uint64_t val = value->getConstantValue();
     switch(w) {
     case  Expr::Bool:
     case  Expr::Int8:  write8(offset, val); break;
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 9369dcbc..bb6496ac 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -78,7 +78,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
          ie = reads.end(); it != ie; ++it) {
     ReadExpr *re = it->get();
     if (re->index.isConstant()) {
-      unsigned index = (unsigned) re->index.getConstantValue();
+      unsigned index = (unsigned) re->index->getConstantValue();
       directReads.insert(std::make_pair(re->updates.root, index));
     }
   }
@@ -101,7 +101,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         ref<Expr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
-        it2->second[i] = value.getConstantValue();
+        it2->second[i] = value->getConstantValue();
         tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it2->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
@@ -131,7 +131,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
         ref<Expr> value;
         bool success = solver->getValue(tmp, read, value);
         assert(success && "FIXME: Unhandled solver failure");            
-        it->second[i] = value.getConstantValue();
+        it->second[i] = value->getConstantValue();
         tmp.addConstraint(EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8)));
       } else {
         tmp.addConstraint(isSeed);
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 9f5a2347..594a6518 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -177,7 +177,7 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
   ObjectPair op;
   address = executor.toUnique(state, address);
   assert(address.isConstant() && "symbolic string arg to intrinsic");  
-  if (!state.addressSpace.resolveOne(address.getConstantValue(), op))
+  if (!state.addressSpace.resolveOne(address->getConstantValue(), op))
     assert(0 && "XXX out of bounds / multiple resolution unhandled");
   bool res;
   assert(executor.solver->mustBeTrue(state, 
@@ -197,7 +197,7 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
     cur = executor.toUnique(state, cur);
     assert(cur.isConstant() && 
            "hit symbolic char while reading concrete string");
-    buf[i] = cur.getConstantValue();
+    buf[i] = cur->getConstantValue();
   }
   buf[i] = 0;
   
@@ -354,8 +354,8 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state,
   
   ref<Expr> e = arguments[0];
   
-  if(e.getWidth() != Expr::Bool)
-    e = NeExpr::create(e, ConstantExpr::create(0, e.getWidth()));
+  if (e->getWidth() != Expr::Bool)
+    e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
   
   bool res;
   bool success = executor.solver->mustBeFalse(state, e, res);
@@ -385,8 +385,8 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
          "invalid number of arguments to klee_prefex_cex");
 
   ref<Expr> cond = arguments[1];
-  if (cond.getWidth() != Expr::Bool)
-    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond.getWidth()));
+  if (cond->getWidth() != Expr::Bool)
+    cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth()));
 
   Executor::ExactResolutionList rl;
   executor.resolveExact(state, arguments[0], rl, "prefex_cex");
@@ -417,7 +417,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
   assert(arguments[0].isConstant() &&
    	 "symbolic argument given to klee_under_constrained!");
 
-  unsigned v = arguments[0].getConstantValue();
+  unsigned v = arguments[0]->getConstantValue();
   llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n";
   if(v) {
     assert(state.underConstrained == false &&
@@ -443,7 +443,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
                                    "klee_set_forking requires a constant arg",
                                    "user.err");
   } else {
-    state.forkDisabled = !value.getConstantValue();
+    state.forkDisabled = !value->getConstantValue();
   }
 }
 
@@ -596,16 +596,16 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
   } else {
     ObjectPair op;
 
-    if (!state.addressSpace.resolveOne(address.getConstantValue(), op)) {
+    if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) {
       executor.terminateStateOnError(state,
                                      "check_memory_access: memory error",
                                      "ptr.err",
                                      executor.getAddressInfo(state, address));
     } else {
       ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
-                                                      size.getConstantValue());
+                                                      size->getConstantValue());
       assert(chk.isConstant());
-      if (!chk.getConstantValue()) {
+      if (!chk->getConstantValue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
                                        "ptr.err",
@@ -634,8 +634,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
   assert(arguments[1].isConstant() &&
          "expect constant size argument to klee_define_fixed_object");
   
-  uint64_t address = arguments[0].getConstantValue();
-  uint64_t size = arguments[1].getConstantValue();
+  uint64_t address = arguments[0]->getConstantValue();
+  uint64_t size = arguments[1]->getConstantValue();
   MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
   executor.bindObjectInState(state, mo, false);
   mo->isUserSpecified = true; // XXX hack;
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 4c09a1aa..55fa7c8d 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -26,7 +26,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
                             Solver::Validity &result) {
   // Fast path, to avoid timer and OS overhead.
   if (expr.isConstant()) {
-    result = expr.getConstantValue() ? Solver::True : Solver::False;
+    result = expr->getConstantValue() ? Solver::True : Solver::False;
     return true;
   }
 
@@ -50,7 +50,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
                               bool &result) {
   // Fast path, to avoid timer and OS overhead.
   if (expr.isConstant()) {
-    result = expr.getConstantValue() ? true : false;
+    result = expr->getConstantValue() ? true : false;
     return true;
   }