From aca72ee7ebadf396d815f6c4983697e76e408268 Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Mon, 1 Jun 2009 15:47:52 +0000
Subject: Modify eval() to return a cell reference instead of its contents.

Add get{Dest,Argument}Cell for computing the cell to store instructions results
and arguments into, respectuvely.

Prep for moving fast path constant evaluation out of the Expr libraary itself.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72692 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Core/Executor.cpp | 184 ++++++++++++++++++++++++--------------------------
 lib/Core/Executor.h   |  23 +++++--
 2 files changed, 108 insertions(+), 99 deletions(-)

(limited to 'lib/Core')

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index df8fdba8..f17b4062 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -968,39 +968,30 @@ ref<Expr> Executor::evalConstant(Constant *c) {
   }
 }
 
-ref<Expr> Executor::eval(KInstruction *ki,
-                         unsigned index,
-                         ExecutionState &state) {
+const Cell& Executor::eval(KInstruction *ki, unsigned index, 
+                           ExecutionState &state) const {
   assert(index < ki->inst->getNumOperands());
   int vnumber = ki->operands[index];
 
   // Determine if this is a constant or not.
   if (vnumber < 0) {
     unsigned index = -vnumber - 2;
-    Cell &c = kmodule->constantTable[index];
-    return c.value;
+    return kmodule->constantTable[index];
   } else {
     unsigned index = vnumber;
     StackFrame &sf = state.stack.back();
-    Cell &c = sf.locals[index];
-    return c.value;
+    return sf.locals[index];
   }
 }
 
 void Executor::bindLocal(KInstruction *target, ExecutionState &state, 
                          ref<Expr> value) {
-  StackFrame &sf = state.stack.back();
-  unsigned reg = target->dest;
-  Cell &c = sf.locals[reg];
-  c.value = value;  
+  getDestCell(state, target).value = value;
 }
 
 void Executor::bindArgument(KFunction *kf, unsigned index, 
                             ExecutionState &state, ref<Expr> value) {
-  StackFrame &sf = state.stack.back();
-  unsigned reg = kf->getArgRegister(index);
-  Cell &c = sf.locals[reg];
-  c.value = value;
+  getArgumentCell(state, kf, index).value = value;
 }
 
 ref<Expr> Executor::toUnique(const ExecutionState &state, 
@@ -1284,7 +1275,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     }
     
     if (!isVoidReturn) {
-      result = eval(ki, 0, state);
+      result = eval(ki, 0, state).value;
     }
     
     if (state.stack.size() <= 1) {
@@ -1364,7 +1355,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       // FIXME: Find a way that we don't have this hidden dependency.
       assert(bi->getCondition() == bi->getOperand(0) &&
              "Wrong operand index!");
-      ref<Expr> cond = eval(ki, 0, state);
+      ref<Expr> cond = eval(ki, 0, state).value;
       Executor::StatePair branches = fork(state, cond, false);
 
       if (WriteTraces) {
@@ -1397,7 +1388,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
   case Instruction::Switch: {
     SwitchInst *si = cast<SwitchInst>(i);
-    ref<Expr> cond = eval(ki, 0, state);
+    ref<Expr> cond = eval(ki, 0, state).value;
     unsigned cases = si->getNumCases();
     BasicBlock *bb = si->getParent();
 
@@ -1481,7 +1472,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     arguments.reserve(numArgs);
 
     for (unsigned j=0; j<numArgs; ++j)
-      arguments.push_back(eval(ki, argStart+j, state));
+      arguments.push_back(eval(ki, argStart+j, state).value);
 
     if (!f) {
       // special case the call with a bitcast case
@@ -1530,7 +1521,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     if (f) {
       executeCall(state, ki, f, arguments);
     } else {
-      ref<Expr> v = eval(ki, 0, state);
+      ref<Expr> v = eval(ki, 0, state).value;
 
       ExecutionState *free = &state;
       bool hasInvalid = false, first = true;
@@ -1571,7 +1562,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     break;
   }
   case Instruction::PHI: {
-    ref<Expr> result = eval(ki, state.incomingBBIndex * 2, state);
+    ref<Expr> result = eval(ki, state.incomingBBIndex * 2, state).value;
     bindLocal(ki, state, result);
     break;
   }
@@ -1581,9 +1572,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     SelectInst *SI = cast<SelectInst>(ki->inst);
     assert(SI->getCondition() == SI->getOperand(0) &&
            "Wrong operand index!");
-    ref<Expr> cond = eval(ki, 0, state);
-    ref<Expr> tExpr = eval(ki, 1, state);
-    ref<Expr> fExpr = eval(ki, 2, state);
+    ref<Expr> cond = eval(ki, 0, state).value;
+    ref<Expr> tExpr = eval(ki, 1, state).value;
+    ref<Expr> fExpr = eval(ki, 2, state).value;
     ref<Expr> result = SelectExpr::create(cond, tExpr, fExpr);
     bindLocal(ki, state, result);
     break;
@@ -1601,8 +1592,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
                                type), type))
   case Instruction::Add: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
 
     if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
       bindLocal(ki, state, AddExpr::create(left, right));
@@ -1616,8 +1607,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
 
   case Instruction::Sub: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
 
     if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
       bindLocal(ki, state, SubExpr::create(left, right));
@@ -1626,13 +1617,16 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       FP_CONSTANT_BINOP(floats::sub, type, left, right, ki, state);
     }
 
+sfdrunk
+airbedandbreakfast
+
     break;
   }
  
   case Instruction::Mul: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
 
     if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
       bindLocal(ki, state, MulExpr::create(left, right));
@@ -1645,80 +1639,80 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
 
   case Instruction::UDiv: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = UDivExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::SDiv: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = SDivExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::URem: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = URemExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
  
   case Instruction::SRem: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = SRemExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::And: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = AndExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::Or: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = OrExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::Xor: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = XorExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::Shl: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = ShlExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::LShr: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = LShrExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
   }
 
   case Instruction::AShr: {
-    ref<Expr> left = eval(ki, 0, state);
-    ref<Expr> right = eval(ki, 1, state);
+    ref<Expr> left = eval(ki, 0, state).value;
+    ref<Expr> right = eval(ki, 1, state).value;
     ref<Expr> result = AShrExpr::create(left, right);
     bindLocal(ki, state, result);
     break;
@@ -1732,80 +1726,80 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
  
     switch(ii->getPredicate()) {
     case ICmpInst::ICMP_EQ: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = EqExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_NE: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = NeExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_UGT: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = UgtExpr::create(left, right);
       bindLocal(ki, state,result);
       break;
     }
 
     case ICmpInst::ICMP_UGE: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = UgeExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_ULT: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = UltExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_ULE: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = UleExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_SGT: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = SgtExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_SGE: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = SgeExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_SLT: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = SltExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
     }
 
     case ICmpInst::ICMP_SLE: {
-      ref<Expr> left = eval(ki, 0, state);
-      ref<Expr> right = eval(ki, 1, state);
+      ref<Expr> left = eval(ki, 0, state).value;
+      ref<Expr> right = eval(ki, 1, state).value;
       ref<Expr> result = SleExpr::create(left, right);
       bindLocal(ki, state, result);
       break;
@@ -1826,7 +1820,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     ref<Expr> size = Expr::createPointer(elementSize);
     if (ai->isArrayAllocation()) {
       // XXX coerce?
-      ref<Expr> count = eval(ki, 0, state);
+      ref<Expr> count = eval(ki, 0, state).value;
       size = MulExpr::create(count, size);
     }
     bool isLocal = i->getOpcode()==Instruction::Alloca;
@@ -1834,31 +1828,31 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     break;
   }
   case Instruction::Free: {
-    executeFree(state, eval(ki, 0, state));
+    executeFree(state, eval(ki, 0, state).value);
     break;
   }
 
   case Instruction::Load: {
-    ref<Expr> base = eval(ki, 0, state);
+    ref<Expr> base = eval(ki, 0, state).value;
     executeMemoryOperation(state, false, base, 0, ki);
     break;
   }
   case Instruction::Store: {
-    ref<Expr> base = eval(ki, 1, state);
-    ref<Expr> value = eval(ki, 0, state);
+    ref<Expr> base = eval(ki, 1, state).value;
+    ref<Expr> value = eval(ki, 0, state).value;
     executeMemoryOperation(state, true, base, value, 0);
     break;
   }
 
   case Instruction::GetElementPtr: {
     KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
-    ref<Expr> base = eval(ki, 0, state);
+    ref<Expr> base = eval(ki, 0, state).value;
 
     for (std::vector< std::pair<unsigned, unsigned> >::iterator 
            it = kgepi->indices.begin(), ie = kgepi->indices.end(); 
          it != ie; ++it) {
       unsigned elementSize = it->second;
-      ref<Expr> index = eval(ki, it->first, state);
+      ref<Expr> index = eval(ki, it->first, state).value;
       base = AddExpr::create(base,
                              MulExpr::create(Expr::createCoerceToPointerType(index),
                                              Expr::createPointer(elementSize)));
@@ -1873,7 +1867,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     // Conversion
   case Instruction::Trunc: {
     CastInst *ci = cast<CastInst>(i);
-    ref<Expr> result = ExtractExpr::createByteOff(eval(ki, 0, state),
+    ref<Expr> result = ExtractExpr::createByteOff(eval(ki, 0, state).value,
 						  0,
 						  Expr::getWidthForLLVMType(ci->getType()));
     bindLocal(ki, state, result);
@@ -1881,14 +1875,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   }
   case Instruction::ZExt: {
     CastInst *ci = cast<CastInst>(i);
-    ref<Expr> result = ZExtExpr::create(eval(ki, 0, state),
+    ref<Expr> result = ZExtExpr::create(eval(ki, 0, state).value,
                                         Expr::getWidthForLLVMType(ci->getType()));
     bindLocal(ki, state, result);
     break;
   }
   case Instruction::SExt: {
     CastInst *ci = cast<CastInst>(i);
-    ref<Expr> result = SExtExpr::create(eval(ki, 0, state),
+    ref<Expr> result = SExtExpr::create(eval(ki, 0, state).value,
                                         Expr::getWidthForLLVMType(ci->getType()));
     bindLocal(ki, state, result);
     break;
@@ -1897,20 +1891,20 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::IntToPtr: {
     CastInst *ci = cast<CastInst>(i);
     Expr::Width pType = Expr::getWidthForLLVMType(ci->getType());
-    ref<Expr> arg = eval(ki, 0, state);
+    ref<Expr> arg = eval(ki, 0, state).value;
     bindLocal(ki, state, ZExtExpr::create(arg, pType));
     break;
   } 
   case Instruction::PtrToInt: {
     CastInst *ci = cast<CastInst>(i);
     Expr::Width iType = Expr::getWidthForLLVMType(ci->getType());
-    ref<Expr> arg = eval(ki, 0, state);
+    ref<Expr> arg = eval(ki, 0, state).value;
     bindLocal(ki, state, ZExtExpr::create(arg, iType));
     break;
   }
 
   case Instruction::BitCast: {
-    ref<Expr> result = eval(ki, 0, state);
+    ref<Expr> result = eval(ki, 0, state).value;
     bindLocal(ki, state, result);
     break;
   }
@@ -1919,7 +1913,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPTrunc: {
     FPTruncInst *fi = cast<FPTruncInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::trunc(arg.getConstantValue(),
                                    resultType,
@@ -1932,7 +1926,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPExt: {
     FPExtInst *fi = cast<FPExtInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::ext(arg.getConstantValue(),
                                  resultType,
@@ -1945,7 +1939,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPToUI: {
     FPToUIInst *fi = cast<FPToUIInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
                                            resultType,
@@ -1958,7 +1952,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FPToSI: {
     FPToSIInst *fi = cast<FPToSIInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::toSignedInt(arg.getConstantValue(),
                                          resultType,
@@ -1971,7 +1965,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::UIToFP: {
     UIToFPInst *fi = cast<UIToFPInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
                                              resultType);
@@ -1983,7 +1977,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::SIToFP: {
     SIToFPInst *fi = cast<SIToFPInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> arg = toConstant(state, eval(ki, 0, state),
+    ref<Expr> arg = toConstant(state, eval(ki, 0, state).value,
                                "floating point");
     uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
                                            resultType,
@@ -1996,9 +1990,9 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FCmp: {
     FCmpInst *fi = cast<FCmpInst>(i);
     Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
-    ref<Expr> left  = toConstant(state, eval(ki, 0, state), 
+    ref<Expr> left  = toConstant(state, eval(ki, 0, state).value, 
                                  "floating point");
-    ref<Expr> right = toConstant(state, eval(ki, 1, state),
+    ref<Expr> right = toConstant(state, eval(ki, 1, state).value,
                                  "floating point");
     uint64_t leftVal = left.getConstantValue();
     uint64_t rightVal = right.getConstantValue();
@@ -2105,8 +2099,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FDiv: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
 
-    ref<Expr> dividend = eval(ki, 0, state);
-    ref<Expr> divisor = eval(ki, 1, state);
+    ref<Expr> dividend = eval(ki, 0, state).value;
+    ref<Expr> divisor = eval(ki, 1, state).value;
     Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
     FP_CONSTANT_BINOP(floats::div, type, dividend, divisor, ki, state);
     break;
@@ -2115,8 +2109,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
   case Instruction::FRem: {
     BinaryOperator *bi = cast<BinaryOperator>(i);
 
-    ref<Expr> dividend = eval(ki, 0, state);
-    ref<Expr> divisor = eval(ki, 1, state);
+    ref<Expr> dividend = eval(ki, 0, state).value;
+    ref<Expr> divisor = eval(ki, 1, state).value;
     Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
     FP_CONSTANT_BINOP(floats::mod, type, dividend, divisor, ki, state);
     break;
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 9fa63a04..852d4cc6 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -15,7 +15,11 @@
 #ifndef KLEE_EXECUTOR_H
 #define KLEE_EXECUTOR_H
 
+#include "klee/ExecutionState.h"
 #include "klee/Interpreter.h"
+#include "klee/Internal/Module/Cell.h"
+#include "klee/Internal/Module/KInstruction.h"
+#include "klee/Internal/Module/KModule.h"
 #include "llvm/Support/CallSite.h"
 #include <vector>
 #include <string>
@@ -38,6 +42,7 @@ namespace llvm {
 }
 
 namespace klee {  
+  class Cell;
   class ExecutionState;
   class ExternalDispatcher;
   class Expr;
@@ -288,10 +293,20 @@ private:
   // Used for testing.
   ref<Expr> replaceReadWithSymbolic(ExecutionState &state, ref<Expr> e);
 
-  ref<Expr> eval(KInstruction *ki,
-                 unsigned index, 
-                 ExecutionState &state);
-  
+  const Cell& eval(KInstruction *ki, unsigned index, 
+                   ExecutionState &state) const;
+
+  Cell& getArgumentCell(ExecutionState &state,
+                        KFunction *kf,
+                        unsigned index) {
+    return state.stack.back().locals[kf->getArgRegister(index)];
+  }
+
+  Cell& getDestCell(ExecutionState &state,
+                    KInstruction *target) {
+    return state.stack.back().locals[target->dest];
+  }
+
   void bindLocal(KInstruction *target, 
                  ExecutionState &state, 
                  ref<Expr> value);
-- 
cgit 1.4.1