about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-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
-rw-r--r--lib/Expr/Constraints.cpp4
-rw-r--r--lib/Expr/Expr.cpp156
-rw-r--r--lib/Expr/ExprEvaluator.cpp6
-rw-r--r--lib/Expr/ExprPPrinter.cpp20
-rw-r--r--lib/Expr/Parser.cpp24
-rw-r--r--lib/Expr/Updates.cpp5
-rw-r--r--lib/Solver/CachingSolver.cpp4
-rw-r--r--lib/Solver/CexCachingSolver.cpp6
-rw-r--r--lib/Solver/FastCexSolver.cpp22
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp24
-rw-r--r--lib/Solver/Solver.cpp16
19 files changed, 235 insertions, 234 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;
   }
 
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 4c18a3b3..472c0aa3 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -120,9 +120,9 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
   // ConstraintSet ADT which efficiently remembers obvious patterns
   // (byte-constant comparison).
 
-  switch (e.getKind()) {
+  switch (e->getKind()) {
   case Expr::Constant:
-    assert(e.getConstantValue() && "attempt to add invalid (false) constraint");
+    assert(e->getConstantValue() && "attempt to add invalid (false) constraint");
     break;
     
     // split to enable finer grained independence and other optimizations
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 6e70e6f2..4c6f5e43 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -157,7 +157,7 @@ unsigned Expr::computeHash() {
   int n = getNumKids();
   for (int i = 0; i < n; i++) {
     res <<= 1;
-    res ^= getKid(i).hash() * Expr::MAGIC_HASH_CONSTANT;
+    res ^= getKid(i)->hash() * Expr::MAGIC_HASH_CONSTANT;
   }
   
   hashValue = res;
@@ -171,19 +171,19 @@ unsigned ConstantExpr::computeHash() {
 
 unsigned CastExpr::computeHash() {
   unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT;
-  hashValue = res ^ src.hash() * Expr::MAGIC_HASH_CONSTANT;
+  hashValue = res ^ src->hash() * Expr::MAGIC_HASH_CONSTANT;
   return hashValue;
 }
 
 unsigned ExtractExpr::computeHash() {
   unsigned res = offset * Expr::MAGIC_HASH_CONSTANT;
   res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT;
-  hashValue = res ^ expr.hash() * Expr::MAGIC_HASH_CONSTANT;
+  hashValue = res ^ expr->hash() * Expr::MAGIC_HASH_CONSTANT;
   return hashValue;
 }
 
 unsigned ReadExpr::computeHash() {
-  unsigned res = index.hash() * Expr::MAGIC_HASH_CONSTANT;
+  unsigned res = index->hash() * Expr::MAGIC_HASH_CONSTANT;
   res ^= updates.hash();
   hashValue = res;
   return hashValue;
@@ -309,7 +309,7 @@ ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
 }
 
 ref<Expr> Expr::createIsZero(ref<Expr> e) {
-  return EqExpr::create(e, ConstantExpr::create(0, e.getWidth()));
+  return EqExpr::create(e, ConstantExpr::create(0, e->getWidth()));
 }
 
 ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
@@ -379,7 +379,7 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
     ref<Expr> cond = EqExpr::create(index, un->index);
     
     if (cond.isConstant()) {
-      if (cond.getConstantValue())
+      if (cond->getConstantValue())
         return un->value;
     } else {
       break;
@@ -394,24 +394,24 @@ int ReadExpr::compareContents(const Expr &b) const {
 }
 
 ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
-  Expr::Width kt = t.getWidth();
+  Expr::Width kt = t->getWidth();
 
-  assert(c.getWidth()==Bool && "type mismatch");
-  assert(kt==f.getWidth() && "type mismatch");
+  assert(c->getWidth()==Bool && "type mismatch");
+  assert(kt==f->getWidth() && "type mismatch");
 
   if (c.isConstant()) {
-    return c.getConstantValue() ? t : f;
+    return c->getConstantValue() ? t : f;
   } else if (t==f) {
     return t;
   } else if (kt==Expr::Bool) { // c ? t : f  <=> (c and t) or (not c and f)
     if (t.isConstant()) {      
-      if (t.getConstantValue()) {
+      if (t->getConstantValue()) {
         return OrExpr::create(c, f);
       } else {
         return AndExpr::create(Expr::createNot(c), f);
       }
     } else if (f.isConstant()) {
-      if (f.getConstantValue()) {
+      if (f->getConstantValue()) {
         return OrExpr::create(Expr::createNot(c), t);
       } else {
         return AndExpr::create(c, t);
@@ -426,19 +426,19 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
 
 
 ref<Expr> ConcatExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
-  Expr::Width w = l.getWidth() + r.getWidth();
+  Expr::Width w = l->getWidth() + r->getWidth();
   
   /* Constant folding */
-  if (l.getKind() == Expr::Constant && r.getKind() == Expr::Constant) {
+  if (l->getKind() == Expr::Constant && r->getKind() == Expr::Constant) {
     // XXX: should fix this constant limitation soon
     assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet");
     
-    uint64_t res = (l.getConstantValue() << r.getWidth()) + r.getConstantValue();
+    uint64_t res = (l->getConstantValue() << r->getWidth()) + r->getConstantValue();
     return ConstantExpr::create(res, w);
   }
 
   // Merge contiguous Extracts
-  if (l.getKind() == Expr::Extract && r.getKind() == Expr::Extract) {
+  if (l->getKind() == Expr::Extract && r->getKind() == Expr::Extract) {
     const ExtractExpr* ee_left = static_ref_cast<ExtractExpr>(l);
     const ExtractExpr* ee_right = static_ref_cast<ExtractExpr>(r);
     if (ee_left->expr == ee_right->expr &&
@@ -480,28 +480,28 @@ ref<Expr> ConcatExpr::create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
 /***/
 
 ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
-  unsigned kw = expr.getWidth();
+  unsigned kw = expr->getWidth();
   assert(w > 0 && off + w <= kw && "invalid extract");
   
   if (w == kw)
     return expr;
   else if (expr.isConstant()) {
-    return ConstantExpr::create(ints::trunc(expr.getConstantValue() >> off, w, kw), w);
+    return ConstantExpr::create(ints::trunc(expr->getConstantValue() >> off, w, kw), w);
   } 
   else 
     // Extract(Concat)
     if (ConcatExpr *ce = dyn_ref_cast<ConcatExpr>(expr)) {
       // if the extract skips the right side of the concat
-      if (off >= ce->getRight().getWidth())
-	return ExtractExpr::create(ce->getLeft(), off - ce->getRight().getWidth(), w);
+      if (off >= ce->getRight()->getWidth())
+	return ExtractExpr::create(ce->getLeft(), off - ce->getRight()->getWidth(), w);
       
       // if the extract skips the left side of the concat
-      if (off + w <= ce->getRight().getWidth())
+      if (off + w <= ce->getRight()->getWidth())
 	return ExtractExpr::create(ce->getRight(), off, w);
 
       // E(C(x,y)) = C(E(x), E(y))
-      return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1).getWidth() + off),
-				ExtractExpr::create(ce->getKid(1), off, ce->getKid(1).getWidth() - off));
+      return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1)->getWidth() + off),
+				ExtractExpr::create(ce->getKid(1), off, ce->getKid(1)->getWidth() - off));
     }
   
   return ExtractExpr::alloc(expr, off, w);
@@ -515,14 +515,14 @@ ref<Expr> ExtractExpr::createByteOff(ref<Expr> expr, unsigned offset, Width bits
 /***/
 
 ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
-  unsigned kBits = e.getWidth();
+  unsigned kBits = e->getWidth();
   if (w == kBits) {
     return e;
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
     if (e.isConstant()) {
-      return ConstantExpr::create(ints::zext(e.getConstantValue(), w, kBits),
+      return ConstantExpr::create(ints::zext(e->getConstantValue(), w, kBits),
                                   w);
     }
     
@@ -531,14 +531,14 @@ ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
 }
 
 ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
-  unsigned kBits = e.getWidth();
+  unsigned kBits = e->getWidth();
   if (w == kBits) {
     return e;
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
     if (e.isConstant()) {
-      return ConstantExpr::create(ints::sext(e.getConstantValue(), w, kBits),
+      return ConstantExpr::create(ints::sext(e->getConstantValue(), w, kBits),
                                   w);
     }
     
@@ -558,8 +558,8 @@ static ref<Expr> XorExpr_createPartialR(const ref<Expr> &cl, Expr *r);
 
 static ref<Expr> AddExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   assert(cl.isConstant() && "non-constant passed in place of constant");
-  uint64_t value = cl.getConstantValue();
-  Expr::Width type = cl.getWidth();
+  uint64_t value = cl->getConstantValue();
+  Expr::Width type = cl->getWidth();
 
   if (type==Expr::Bool) {
     return XorExpr_createPartialR(cl, r);
@@ -608,7 +608,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");
-  Expr::Width type = cl.getWidth();
+  Expr::Width type = cl->getWidth();
 
   if (type==Expr::Bool) {
     return XorExpr_createPartialR(cl, r);
@@ -627,8 +627,8 @@ 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");
-  uint64_t value = cr.getConstantValue();
-  Expr::Width width = cr.getWidth();
+  uint64_t value = cr->getConstantValue();
+  Expr::Width width = cr->getWidth();
   uint64_t nvalue = ints::sub(0, value, width);
 
   return AddExpr_createPartial(l, ConstantExpr::create(nvalue, width));
@@ -662,8 +662,8 @@ 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");
-  uint64_t value = cl.getConstantValue();
-  Expr::Width type = cl.getWidth();
+  uint64_t value = cl->getConstantValue();
+  Expr::Width type = cl->getWidth();
 
   if (type == Expr::Bool) {
     return AndExpr_createPartialR(cl, r);
@@ -690,8 +690,8 @@ 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");
-  uint64_t value = cr.getConstantValue();
-  Expr::Width width = cr.getWidth();;
+  uint64_t value = cr->getConstantValue();
+  Expr::Width width = cr->getWidth();
 
   if (value==ints::sext(1, width, 1)) {
     return l;
@@ -710,8 +710,8 @@ 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");
-  uint64_t value = cr.getConstantValue();
-  Expr::Width width = cr.getWidth();
+  uint64_t value = cr->getConstantValue();
+  Expr::Width width = cr->getWidth();
 
   if (value == ints::sext(1, width, 1)) {
     return cr;
@@ -730,8 +730,8 @@ 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");
-  uint64_t value = cl.getConstantValue();
-  Expr::Width type = cl.getWidth();
+  uint64_t value = cl->getConstantValue();
+  Expr::Width type = cl->getWidth();
 
   if (type==Expr::Bool) {
     if (value) {
@@ -754,7 +754,7 @@ static ref<Expr> XorExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> UDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // r must be 1
+  if (l->getWidth() == Expr::Bool) { // r must be 1
     return l;
   } else{
     return UDivExpr::alloc(l, r);
@@ -762,7 +762,7 @@ static ref<Expr> UDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> SDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // r must be 1
+  if (l->getWidth() == Expr::Bool) { // r must be 1
     return l;
   } else{
     return SDivExpr::alloc(l, r);
@@ -770,7 +770,7 @@ static ref<Expr> SDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> URemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // r must be 1
+  if (l->getWidth() == Expr::Bool) { // r must be 1
     return ConstantExpr::create(0, Expr::Bool);
   } else{
     return URemExpr::alloc(l, r);
@@ -778,7 +778,7 @@ static ref<Expr> URemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // r must be 1
+  if (l->getWidth() == Expr::Bool) { // r must be 1
     return ConstantExpr::create(0, Expr::Bool);
   } else{
     return SRemExpr::alloc(l, r);
@@ -786,7 +786,7 @@ static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // l & !r
+  if (l->getWidth() == Expr::Bool) { // l & !r
     return AndExpr::create(l, Expr::createNot(r));
   } else{
     return ShlExpr::alloc(l, r);
@@ -794,7 +794,7 @@ static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // l & !r
+  if (l->getWidth() == Expr::Bool) { // l & !r
     return AndExpr::create(l, Expr::createNot(r));
   } else{
     return LShrExpr::alloc(l, r);
@@ -802,7 +802,7 @@ static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // l
+  if (l->getWidth() == Expr::Bool) { // l
     return l;
   } else{
     return AShrExpr::alloc(l, r);
@@ -811,12 +811,12 @@ 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"); \
+  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);  \
+      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()); \
@@ -829,12 +829,12 @@ 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"); \
+  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);  \
+      Expr::Width width = l->getWidth(); \
+      uint64_t val = ints::_op(l->getConstantValue(), \
+                               r->getConstantValue(), width);  \
       return ConstantExpr::create(val, width); \
     } \
   } \
@@ -857,12 +857,12 @@ 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"); \
+  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);  \
+      Expr::Width width = l->getWidth(); \
+      uint64_t val = ints::_op(l->getConstantValue(), \
+                               r->getConstantValue(), width);  \
       return ConstantExpr::create(val, Expr::Bool); \
     } \
   } \
@@ -871,12 +871,12 @@ 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"); \
+  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);  \
+      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()); \
@@ -907,7 +907,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
   assert(cl.isConstant() && "constant expression required");
   assert(rd->getKind() == Expr::Read && "read expression required");
   
-  uint64_t ct = cl.getConstantValue();
+  uint64_t ct = cl->getConstantValue();
   ref<Expr> first_idx_match;
 
   // number of positions in the array that contain value ct
@@ -932,12 +932,12 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 	break;
       }
       else {
-	if (idx.getConstantValue() != k) {
+	if (idx->getConstantValue() != k) {
 	  all_const = false;
 	  //llvm::cerr << "Wrong constant\n";
 	  break;
 	}
-	if (val.getConstantValue() == ct) {
+	if (val->getConstantValue() == ct) {
 	  matches++;
 	  if (matches == 1)
 	    first_idx_match = un->index;
@@ -959,7 +959,7 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
       return res;
     
     for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
-      if (un->index != first_idx_match && un->value.getConstantValue() == ct) {
+      if (un->index != first_idx_match && un->value->getConstantValue() == ct) {
 	ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
 	res = OrExpr::create(curr_eq, res);
       }
@@ -974,8 +974,8 @@ 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");
-  uint64_t value = cl.getConstantValue();
-  Expr::Width width = cl.getWidth();
+  uint64_t value = cl->getConstantValue();
+  Expr::Width width = cl->getWidth();
 
   Expr::Kind rk = r->getKind();
   if (width == Expr::Bool) {
@@ -989,8 +989,8 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
 
         // eliminate double negation
         if (ree->left.isConstant() &&
-            ree->left.getWidth()==Expr::Bool) {
-          assert(!ree->left.getConstantValue());
+            ree->left->getWidth()==Expr::Bool) {
+          assert(!ree->left->getConstantValue());
           return ree->right;
         }
       } else if (rk == Expr::Or) {
@@ -1004,7 +1004,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   } else if (rk == Expr::SExt) {
     // (sext(a,T)==c) == (a==c)
     const SExtExpr *see = static_ref_cast<SExtExpr>(r);
-    Expr::Width fromBits = see->src.getWidth();
+    Expr::Width fromBits = see->src->getWidth();
     uint64_t trunc = bits64::truncateToNBits(value, fromBits);
 
     // pathological check, make sure it is possible to
@@ -1017,7 +1017,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<Expr> &cl, Expr *r) {
   } else if (rk == Expr::ZExt) {
     // (zext(a,T)==c) == (a==c)
     const ZExtExpr *zee = static_ref_cast<ZExtExpr>(r);
-    Expr::Width fromBits = zee->src.getWidth();
+    Expr::Width fromBits = zee->src->getWidth();
     uint64_t trunc = bits64::truncateToNBits(value, fromBits);
     
     // pathological check, make sure it is possible to
@@ -1072,12 +1072,12 @@ ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  Expr::Width t = l.getWidth();
+  Expr::Width t = l->getWidth();
   if (t == Expr::Bool) { // !l && r
     return AndExpr::create(Expr::createNot(l), r);
   } else {
     if (r.isConstant()) {      
-      uint64_t value = r.getConstantValue();
+      uint64_t value = r->getConstantValue();
       if (value <= 8) {
         ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
         for (unsigned i=0; i<value; i++) {
@@ -1092,7 +1092,7 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // !(l && !r)
+  if (l->getWidth() == Expr::Bool) { // !(l && !r)
     return OrExpr::create(Expr::createNot(l), r);
   } else {
     return UleExpr::alloc(l, r);
@@ -1100,7 +1100,7 @@ static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // l && !r
+  if (l->getWidth() == Expr::Bool) { // l && !r
     return AndExpr::create(l, Expr::createNot(r));
   } else {
     return SltExpr::alloc(l, r);
@@ -1108,7 +1108,7 @@ static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 }
 
 static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
-  if (l.getWidth() == Expr::Bool) { // !(!l && r)
+  if (l->getWidth() == Expr::Bool) { // !(!l && r)
     return OrExpr::create(l, Expr::createNot(r));
   } else {
     return SleExpr::alloc(l, r);
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index cf901f0e..0c04a538 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -17,7 +17,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
     ref<Expr> ui = visit(un->index);
     
     if (ui.isConstant()) {
-      if (ui.getConstantValue() == index)
+      if (ui->getConstantValue() == index)
         return Action::changeTo(visit(un->value));
     } else {
       // update index is unknown, so may or may not be index, we
@@ -37,7 +37,7 @@ ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);
   
   if (v.isConstant()) {
-    return evalRead(re.updates, v.getConstantValue());
+    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 fd367f23..08809684 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -96,7 +96,7 @@ class PPrinter : public ExprPPrinter {
   bool shouldPrintWidth(ref<Expr> e) {
     if (PCAllWidths)
       return true;
-    return e.getWidth() != Expr::Bool;
+    return e->getWidth() != Expr::Bool;
   }
 
   bool isVerySimple(const ref<Expr> &e) { 
@@ -228,7 +228,7 @@ class PPrinter : public ExprPPrinter {
         PC << 'w';
     }
 
-    PC << e.getWidth();
+    PC << e->getWidth();
   }
 
   /// hasOrderedReads - True iff all children are reads with
@@ -239,7 +239,7 @@ class PPrinter : public ExprPPrinter {
       return false;
 
     // Get stride expr in proper index width.
-    Expr::Width idxWidth = base->index.getWidth();
+    Expr::Width idxWidth = base->index->getWidth();
     ref<Expr> strideExpr = ConstantExpr::alloc(stride, idxWidth);
     ref<Expr> offset = ConstantExpr::alloc(0, idxWidth);
     for (unsigned i=1; i<ep->getNumKids(); ++i) {
@@ -326,16 +326,16 @@ public:
   void printConst(const ref<Expr> &e, PrintContext &PC, bool printWidth) {
     assert(e.isConstant());
 
-    if (e.getWidth() == Expr::Bool)
-      PC << (e.getConstantValue() ? "true" : "false");
+    if (e->getWidth() == Expr::Bool)
+      PC << (e->getConstantValue() ? "true" : "false");
     else {
       if (PCAllConstWidths)
 	printWidth = true;
     
       if (printWidth)
-	PC << "(w" << e.getWidth() << " ";
+	PC << "(w" << e->getWidth() << " ";
 
-      PC << e.getConstantValue();
+      PC << e->getConstantValue();
 
       if (printWidth)
 	PC << ")";
@@ -376,7 +376,7 @@ public:
         // because if they are offset reads then its either constant,
         // or they are (base + offset) and base will get printed with
         // a declaration.
-        if (PCMultibyteReads && e.getKind() == Expr::Concat) {
+        if (PCMultibyteReads && e->getKind() == Expr::Concat) {
           const Expr *ep = e.get();
           if (hasAllByteReads(ep)) {
             bool isMSB = hasOrderedReads(ep, 1);
@@ -393,7 +393,7 @@ public:
           }
         }
 
-	PC << '(' << e.getKind();
+	PC << '(' << e->getKind();
         printWidth(PC, e);
         PC << ' ';
 
@@ -404,7 +404,7 @@ public:
           printRead(re, PC, indent);
         } else if (const ExtractExpr *ee = dyn_ref_cast<ExtractExpr>(e)) {
           printExtract(ee, PC, indent);
-        } else if (e.getKind() == Expr::Concat || e.getKind() == Expr::SExt)
+        } else if (e->getKind() == Expr::Concat || e->getKind() == Expr::SExt)
 	  printExpr(e.get(), PC, indent, true);
 	else
           printExpr(e.get(), PC, indent);	
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index a8ea0a6b..70c1cc76 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -498,7 +498,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) {
     return Res;
   } else if (ExpectedType.isValid()) {
     // Type check result.    
-    if (Res.get().getWidth() != ExpectedType.get()) {
+    if (Res.get()->getWidth() != ExpectedType.get()) {
       // FIXME: Need more info, and range
       Error("expression has incorrect type.", Start);
       return ExprResult();
@@ -752,9 +752,9 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name,
   ExprHandle E = Arg.get();
   switch (Kind) {
   case eMacroKind_Not:
-    return EqExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
+    return EqExpr::alloc(ConstantExpr::alloc(0, E->getWidth()), E);
   case eMacroKind_Neg:
-    return SubExpr::alloc(ConstantExpr::alloc(0, E.getWidth()), E);
+    return SubExpr::alloc(ConstantExpr::alloc(0, E->getWidth()), E);
   case Expr::SExt:
     // FIXME: Type check arguments.
     return SExtExpr::alloc(E, ResTy);
@@ -809,7 +809,7 @@ void ParserImpl::ParseMatchedBinaryArgs(const Token &Name,
       } else {
         RHS = RHS_NOE.getExpr();
         if (RHS.isValid())
-          LHS = ParseNumberToken(RHS.get().getWidth(), LHS_NOE.getNumber());
+          LHS = ParseNumberToken(RHS.get()->getWidth(), LHS_NOE.getNumber());
       }
     } else {
       LHS = LHS_NOE.getExpr();
@@ -817,7 +817,7 @@ void ParserImpl::ParseMatchedBinaryArgs(const Token &Name,
         // FIXME: Should suppress ambiguity warnings here.
         RHS = ParseExpr(TypeResult());
       } else {
-        RHS = ParseExpr(LHS.get().getWidth());
+        RHS = ParseExpr(LHS.get()->getWidth());
       }
     }
   }
@@ -835,7 +835,7 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name,
     return ConstantExpr::alloc(0, ResTy);
 
   ref<Expr> LHS_E = LHS.get(), RHS_E = RHS.get();
-  assert(LHS_E.getWidth() == RHS_E.getWidth() && "Mismatched types!");
+  assert(LHS_E->getWidth() == RHS_E->getWidth() && "Mismatched types!");
 
   switch (Kind) {    
   case Expr::Add: return AddExpr::alloc(LHS_E, RHS_E);
@@ -905,7 +905,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
     }
     
     Kids.push_back(E.get());
-    Width += E.get().getWidth();
+    Width += E.get()->getWidth();
   }
   
   ConsumeRParen();
@@ -930,9 +930,9 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
     return ConstantExpr::alloc(0, ResTy);
 
   assert(OffsetExpr.get().isConstant() && "ParseNumber returned non-constant.");
-  unsigned Offset = (unsigned) OffsetExpr.get().getConstantValue();
+  unsigned Offset = (unsigned) OffsetExpr.get()->getConstantValue();
 
-  if (Offset + ResTy > Child.get().getWidth()) {
+  if (Offset + ResTy > Child.get()->getWidth()) {
     Error("extract out-of-range of child expression.", Name);
     return ConstantExpr::alloc(0, ResTy);
   }
@@ -964,7 +964,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
   
   if (!IndexExpr.isValid())
     return ConstantExpr::alloc(0, ResTy);
-  else if (IndexExpr.get().getWidth() != ArrayDomainType) {
+  else if (IndexExpr.get()->getWidth() != ArrayDomainType) {
     Error("index width does not match array domain.");
     return ConstantExpr::alloc(0, ResTy);
   }
@@ -1115,7 +1115,7 @@ VersionResult ParserImpl::ParseVersion() {
       LHS = ParseNumberToken(ArrayDomainType, it->first.getNumber());
     } else {
       LHS = it->first.getExpr(); 
-      if (LHS.isValid() && LHS.get().getWidth() != ArrayDomainType) {
+      if (LHS.isValid() && LHS.get()->getWidth() != ArrayDomainType) {
         // FIXME: bad token location. We should maybe try and know the
         // array up-front?
         Error("invalid value in write index (doesn't match domain).", Tok);
@@ -1127,7 +1127,7 @@ VersionResult ParserImpl::ParseVersion() {
       RHS = ParseNumberToken(ArrayRangeType, it->second.getNumber());
     } else {
       RHS = it->second.getExpr();
-      if (RHS.isValid() && RHS.get().getWidth() != ArrayRangeType) {
+      if (RHS.isValid() && RHS.get()->getWidth() != ArrayRangeType) {
         // FIXME: bad token location. We should maybe try and know the
         // array up-front?
         Error("invalid value in write assignment (doesn't match range).", Tok);
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index b2ceeaf1..7c3f41d4 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -23,7 +23,8 @@ UpdateNode::UpdateNode(const UpdateNode *_next,
     next(_next),
     index(_index),
     value(_value) {
-  assert(_value.getWidth() == Expr::Int8 && "Update value should be 8-bit wide.");
+  assert(_value->getWidth() == Expr::Int8 && 
+         "Update value should be 8-bit wide.");
   computeHash();
   if (next) {
     ++next->refCount;
@@ -47,7 +48,7 @@ int UpdateNode::compare(const UpdateNode &b) const {
 }
 
 unsigned UpdateNode::computeHash() {
-  hashValue = index.hash() ^ value.hash();
+  hashValue = index->hash() ^ value->hash();
   if (next)
     hashValue ^= next->hash();
   return hashValue;
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 517e133b..d353e485 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -49,11 +49,11 @@ private:
   
   struct CacheEntryHash {
     unsigned operator()(const CacheEntry &ce) const {
-      unsigned result = ce.query.hash();
+      unsigned result = ce.query->hash();
       
       for (ConstraintManager::constraint_iterator it = ce.constraints.begin();
            it != ce.constraints.end(); ++it)
-        result ^= it->hash();
+        result ^= (*it)->hash();
       
       return result;
     }
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 79bc985d..db15632b 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -139,7 +139,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
   if (neg.isConstant()) {
-    if (!neg.getConstantValue()) {
+    if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -154,7 +154,7 @@ 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.getConstantValue()) {
+    if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -219,7 +219,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   ref<Expr> q = a->evaluate(query.expr);
   assert(q.isConstant() && "assignment evaluation did not result in constant");
 
-  if (q.getConstantValue()) {
+  if (q->getConstantValue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index b6f676aa..88f34c99 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -398,7 +398,7 @@ public:
 #ifdef LOG
     //    *theLog << "force: " << e << " to " << range << "\n";
 #endif
-    switch (e.getKind()) {
+    switch (e->getKind()) {
     case Expr::Constant: {
       // rather a pity if the constant isn't in the range, but how can
       // we use this?
@@ -417,8 +417,8 @@ public:
       // XXX we need to respect the version here and object state chain
 
       if (re->index.isConstant() && 
-          re->index.getConstantValue() < array->size) {
-        CexValueData &cvd = cod.values[re->index.getConstantValue()];
+          re->index->getConstantValue() < array->size) {
+        CexValueData &cvd = cod.values[re->index->getConstantValue()];
         CexValueData tmp = cvd.set_intersection(range);
         
         if (tmp.isEmpty()) {
@@ -522,7 +522,7 @@ public:
       // possible input range.
     case Expr::ZExt: {
       CastExpr *ce = static_ref_cast<CastExpr>(e);
-      unsigned inBits = ce->src.getWidth();
+      unsigned inBits = ce->src->getWidth();
       ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits)));
       forceExprToRange(ce->src, input);
       break;
@@ -531,7 +531,7 @@ public:
       // minus the impossible values. This is nicer since it is a single interval.
     case Expr::SExt: {
       CastExpr *ce = static_ref_cast<CastExpr>(e);
-      unsigned inBits = ce->src.getWidth();
+      unsigned inBits = ce->src->getWidth();
       unsigned outBits = ce->width;
       ValueRange output = range.set_difference(ValueRange(1<<(inBits-1),
                                                           (bits64::maxValueOfNBits(outBits)-
@@ -614,7 +614,7 @@ public:
       BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
       if (range.isFixed()) {
         if (be->left.isConstant()) {
-          uint64_t value = be->left.getConstantValue();
+          uint64_t value = be->left->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
           } else {
@@ -622,7 +622,7 @@ public:
               forceExprToRange(be->right, 
                                CexValueData(1,
                                             ints::sext(1, 
-                                                       be->right.getWidth(),
+                                                       be->right->getWidth(),
                                                        1)));
             } else {
               // XXX heuristic / lossy, could be better to pick larger range?
@@ -645,7 +645,7 @@ public:
         ValueRange left = evalRangeForExpr(be->left);
         ValueRange right = evalRangeForExpr(be->right);
 
-        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
 
         // XXX should deal with overflow (can lead to empty range)
 
@@ -678,7 +678,7 @@ public:
 
         // XXX should deal with overflow (can lead to empty range)
 
-        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
         if (left.isFixed()) {
           if (range.min()) {
             forceExprToRange(be->right, CexValueData(left.min(), maxValue));
@@ -732,7 +732,7 @@ public:
     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;
+    return v->getConstantValue() == value;
   }
 };
 
@@ -940,7 +940,7 @@ FastCexSolver::computeInitialValues(const Query& query,
                                                        kMachinePointerType)));
       
       if (value.isConstant()) {
-        data.push_back(value.getConstantValue());
+        data.push_back(value->getConstantValue());
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index c966aff6..18e5c84d 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -99,7 +99,7 @@ public:
         if (!wholeObjects.count(array)) {
           if (re->index.isConstant()) {
             DenseSet<unsigned> &dis = elements[array];
-            dis.add((unsigned) re->index.getConstantValue());
+            dis.add((unsigned) re->index->getConstantValue());
           } else {
             elements_ty::iterator it2 = elements.find(array);
             if (it2!=elements.end())
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index a1b6e99a..1d27c655 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -447,11 +447,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   ++stats::queryConstructs;
 
-  switch(e.getKind()) {
-
+  switch (e->getKind()) {
   case Expr::Constant: {
-    uint64_t asUInt64 = e.getConstantValue();
-    *width_out = e.getWidth();
+    uint64_t asUInt64 = e->getConstantValue();
+    *width_out = e->getWidth();
 
     if (*width_out > 64)
       assert(0 && "constructActual: width > 64");
@@ -557,7 +556,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized mul");
 
     if (me->left.isConstant()) {
-      return constructMulByConstant(right, *width_out, me->left.getConstantValue());
+      return constructMulByConstant(right, *width_out, 
+                                    me->left->getConstantValue());
     } else {
       ExprHandle left = construct(me->left, width_out);
       return vc_bvMultExpr(vc, *width_out, left, right);
@@ -570,7 +570,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized udiv");
     
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
         return bvRightShift(left,
@@ -592,7 +592,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
  
       if (optimizeDivides) {
 	if (*width_out == 32) //only works for 32-bit division
@@ -612,7 +612,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized urem");
     
     if (de->right.isConstant()) {
-      uint64_t divisor = de->right.getConstantValue();
+      uint64_t divisor = de->right->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
         unsigned bits = bits64::indexOfSingleBit(divisor);
@@ -711,7 +711,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized shl");
 
     if (se->right.isConstant()) {
-      return bvLeftShift(left, se->right.getConstantValue(), getShiftBits(*width_out));
+      return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
@@ -726,7 +726,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized lshr");
 
     if (lse->right.isConstant()) {
-      return bvRightShift(left, (unsigned) lse->right.getConstantValue(), shiftBits);
+      return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
@@ -740,7 +740,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized ashr");
     
     if (ase->right.isConstant()) {
-      unsigned shift = (unsigned) ase->right.getConstantValue();
+      unsigned shift = (unsigned) ase->right->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
     } else {
@@ -758,7 +758,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
       if (ee->left.isConstant()) {
-        assert(!ee->left.getConstantValue() && "uncanonicalized eq");
+        assert(!ee->left->getConstantValue() && "uncanonicalized eq");
         return vc_notExpr(vc, right);
       } else {
         return vc_iffExpr(vc, left, right);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index ae378ac1..8990e3b9 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -53,11 +53,11 @@ SolverImpl::~SolverImpl() {
 }
 
 bool Solver::evaluate(const Query& query, Validity &result) {
-  assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
+  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
-  // Maintain invariants implementation expect.
+  // Maintain invariants implementations expect.
   if (query.expr.isConstant()) {
-    result = query.expr.getConstantValue() ? True : False;
+    result = query.expr->getConstantValue() ? True : False;
     return true;
   }
 
@@ -79,11 +79,11 @@ bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
 }
 
 bool Solver::mustBeTrue(const Query& query, bool &result) {
-  assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
+  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
-  // Maintain invariants implementation expect.
+  // Maintain invariants implementations expect.
   if (query.expr.isConstant()) {
-    result = query.expr.getConstantValue() ? true : false;
+    result = query.expr->getConstantValue() ? true : false;
     return true;
   }
 
@@ -136,7 +136,7 @@ Solver::getInitialValues(const Query& query,
 
 std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
   ref<Expr> e = query.expr;
-  Expr::Width width = e.getWidth();
+  Expr::Width width = e->getWidth();
   uint64_t min, max;
 
   if (width==1) {
@@ -152,7 +152,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
       min = 0, max = 1; break;
     }
   } else if (e.isConstant()) {
-    min = max = e.getConstantValue();
+    min = max = e->getConstantValue();
   } else {
     // binary search for # of useful bits
     uint64_t lo=0, hi=width, mid, bits=0;
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-23 09:08:00 +0000