about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Expr.h2
-rw-r--r--lib/Core/AddressSpace.cpp4
-rw-r--r--lib/Core/Executor.cpp19
-rw-r--r--lib/Core/Executor.h6
-rw-r--r--lib/Core/ExecutorUtil.cpp136
-rw-r--r--lib/Core/Memory.h4
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp5
-rw-r--r--lib/Expr/Expr.cpp2
-rw-r--r--lib/Expr/ExprEvaluator.cpp4
9 files changed, 88 insertions, 94 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 69f9f1df..92b322f2 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -228,7 +228,7 @@ public:
   /// given object.
   static ref<Expr> createTempRead(const Array *array, Expr::Width w);
   
-  static ref<Expr> createPointer(uint64_t v);
+  static ref<ConstantExpr> createPointer(uint64_t v);
 
   struct CreateArg;
   static ref<Expr> createFromKind(Kind k, std::vector<CreateArg> args);
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 1e683e34..25418c13 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -84,7 +84,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
     ref<ConstantExpr> cex;
     if (!solver->getValue(state, address, cex))
       return false;
-    unsigned example = (unsigned) cex->getConstantValue();
+    uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
     const MemoryMap::value_type *res = objects.lookup_previous(&hack);
     
@@ -191,7 +191,7 @@ bool AddressSpace::resolve(ExecutionState &state,
     ref<ConstantExpr> cex;
     if (!solver->getValue(state, p, cex))
       return true;
-    unsigned example = (unsigned) cex->getConstantValue();
+    uint64_t example = cex->getZExtValue();
     MemoryObject hack(example);
     
     MemoryMap::iterator oi = objects.upper_bound(&hack);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 338744a3..88ced236 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -428,7 +428,7 @@ void Executor::initializeGlobals(ExecutionState &state) {
   // since reading/writing via a function pointer is unsupported anyway.
   for (Module::iterator i = m->begin(), ie = m->end(); i != ie; ++i) {
     Function *f = i;
-    ref<Expr> addr(0);
+    ref<ConstantExpr> addr(0);
 
     // If the symbol has external weak linkage then it is implicitly
     // not defined in this module; if it isn't resolvable then it
@@ -918,7 +918,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
                                  ConstantExpr::alloc(1, Expr::Bool));
 }
 
-ref<Expr> Executor::evalConstant(Constant *c) {
+ref<klee::ConstantExpr> Executor::evalConstant(Constant *c) {
   if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
     return evalConstantExpr(ce);
   } else {
@@ -2196,17 +2196,16 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
     return;
 
   KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(KI);
-  ref<Expr> constantOffset = Expr::createPointer(0);
+  ref<ConstantExpr> constantOffset = ConstantExpr::alloc(0, Expr::Int32);
   unsigned index = 1;
   for (gep_type_iterator ii = gep_type_begin(gepi), ie = gep_type_end(gepi);
        ii != ie; ++ii) {
     if (const StructType *st = dyn_cast<StructType>(*ii)) {
-      const StructLayout *sl = 
-        kmodule->targetData->getStructLayout(st);
+      const StructLayout *sl = kmodule->targetData->getStructLayout(st);
       const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
-      ref<Expr> addend = Expr::createPointer(sl->getElementOffset((unsigned) 
-                                                                  ci->getZExtValue()));
-      constantOffset = AddExpr::create(constantOffset, addend);
+      uint64_t addend = sl->getElementOffset((unsigned) ci->getZExtValue());
+      constantOffset = constantOffset->Add(ConstantExpr::alloc(addend,
+                                                               Expr::Int32));
     } else {
       const SequentialType *st = cast<SequentialType>(*ii);
       unsigned elementSize = 
@@ -2216,14 +2215,14 @@ void Executor::bindInstructionConstants(KInstruction *KI) {
         ref<Expr> index = evalConstant(c);
         ref<Expr> addend = MulExpr::create(Expr::createCoerceToPointerType(index), 
                                            Expr::createPointer(elementSize));
-        constantOffset = AddExpr::create(constantOffset, addend);
+        constantOffset = constantOffset->Add(cast<ConstantExpr>(addend));
       } else {
         kgepi->indices.push_back(std::make_pair(index, elementSize));
       }
     }
     index++;
   }
-  kgepi->offset = cast<ConstantExpr>(constantOffset)->getConstantValue();
+  kgepi->offset = constantOffset->getZExtValue();
 }
 
 void Executor::bindModuleConstants() {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 9cfcf627..88a3db4e 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -132,7 +132,7 @@ private:
 
   /// Map of globals to their bound address. This also includes
   /// globals that have no representative object (i.e. functions).
-  std::map<const llvm::GlobalValue*, ref<Expr> > globalAddresses;
+  std::map<const llvm::GlobalValue*, ref<ConstantExpr> > globalAddresses;
 
   /// The set of legal function addresses, used to validate function
   /// pointers. We use the actual Function* address as the function address.
@@ -307,7 +307,7 @@ private:
                     ExecutionState &state,
                     ref<Expr> value);
 
-  ref<Expr> evalConstantExpr(llvm::ConstantExpr *ce);
+  ref<klee::ConstantExpr> evalConstantExpr(llvm::ConstantExpr *ce);
 
   /// Return a unique constant value for the given expression in the
   /// given state, if it has one (i.e. it provably only has a single
@@ -385,7 +385,7 @@ public:
   }
 
   // XXX should just be moved out to utility module
-  ref<Expr> evalConstant(llvm::Constant *c);
+  ref<klee::ConstantExpr> evalConstant(llvm::Constant *c);
 
   virtual void setPathWriter(TreeStreamWriter *tsw) {
     pathWriter = tsw;
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index a1e030a5..3bb8a0b0 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -33,103 +33,97 @@ using namespace llvm;
 
 namespace klee {
 
-ref<Expr> 
-Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
-  const llvm::Type *type = ce->getType();
-
-  ref<Expr> op1(0), op2(0), op3(0);
-  int numOperands = ce->getNumOperands();
-
-  if (numOperands > 0) op1 = evalConstant(ce->getOperand(0));
-  if (numOperands > 1) op2 = evalConstant(ce->getOperand(1));
-  if (numOperands > 2) op3 = evalConstant(ce->getOperand(2));
-  
-  switch (ce->getOpcode()) {
+  ref<ConstantExpr> Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
+    const llvm::Type *type = ce->getType();
+
+    ref<ConstantExpr> op1(0), op2(0), op3(0);
+    int numOperands = ce->getNumOperands();
+
+    if (numOperands > 0) op1 = evalConstant(ce->getOperand(0));
+    if (numOperands > 1) op2 = evalConstant(ce->getOperand(1));
+    if (numOperands > 2) op3 = evalConstant(ce->getOperand(2));
+
+    switch (ce->getOpcode()) {
     default :
       ce->dump();
       llvm::cerr << "error: unknown ConstantExpr type\n"
                  << "opcode: " << ce->getOpcode() << "\n";
       abort();
 
-    case Instruction::Trunc: return ExtractExpr::createByteOff(op1, 
-							       0,
-							       Expr::getWidthForLLVMType(type));
-    case Instruction::ZExt:  return  ZExtExpr::create(op1, 
-                                                      Expr::getWidthForLLVMType(type));
-    case Instruction::SExt:  return  SExtExpr::create(op1, 
-                                                      Expr::getWidthForLLVMType(type));
-    case Instruction::Add:   return   AddExpr::create(op1, op2);
-    case Instruction::Sub:   return   SubExpr::create(op1, op2);
-    case Instruction::Mul:   return   MulExpr::create(op1, op2);
-    case Instruction::SDiv:  return  SDivExpr::create(op1, op2);
-    case Instruction::UDiv:  return  UDivExpr::create(op1, op2);
-    case Instruction::SRem:  return  SRemExpr::create(op1, op2);
-    case Instruction::URem:  return  URemExpr::create(op1, op2);
-    case Instruction::And:   return   AndExpr::create(op1, op2);
-    case Instruction::Or:    return    OrExpr::create(op1, op2);
-    case Instruction::Xor:   return   XorExpr::create(op1, op2);
-    case Instruction::Shl:   return   ShlExpr::create(op1, op2);
-    case Instruction::LShr:  return  LShrExpr::create(op1, op2);
-    case Instruction::AShr:  return  AShrExpr::create(op1, op2);
+    case Instruction::Trunc: 
+      return op1->Extract(0, Expr::getWidthForLLVMType(type));
+    case Instruction::ZExt:  return op1->ZExt(Expr::getWidthForLLVMType(type));
+    case Instruction::SExt:  return op1->SExt(Expr::getWidthForLLVMType(type));
+    case Instruction::Add:   return op1->Add(op2);
+    case Instruction::Sub:   return op1->Sub(op2);
+    case Instruction::Mul:   return op1->Mul(op2);
+    case Instruction::SDiv:  return op1->SDiv(op2);
+    case Instruction::UDiv:  return op1->UDiv(op2);
+    case Instruction::SRem:  return op1->SRem(op2);
+    case Instruction::URem:  return op1->URem(op2);
+    case Instruction::And:   return op1->And(op2);
+    case Instruction::Or:    return op1->Or(op2);
+    case Instruction::Xor:   return op1->Xor(op2);
+    case Instruction::Shl:   return op1->Shl(op2);
+    case Instruction::LShr:  return op1->LShr(op2);
+    case Instruction::AShr:  return op1->AShr(op2);
     case Instruction::BitCast:  return op1;
 
-    case Instruction::IntToPtr: {
-      return ZExtExpr::create(op1, Expr::getWidthForLLVMType(type));
-    } 
+    case Instruction::IntToPtr:
+      return op1->ZExt(Expr::getWidthForLLVMType(type));
+
+    case Instruction::PtrToInt:
+      return op1->ZExt(Expr::getWidthForLLVMType(type));
 
-    case Instruction::PtrToInt: {
-      return ZExtExpr::create(op1, Expr::getWidthForLLVMType(type));
-    }
-      
     case Instruction::GetElementPtr: {
-      ref<Expr> base = op1;
+      ref<ConstantExpr> base = op1;
 
       for (gep_type_iterator ii = gep_type_begin(ce), ie = gep_type_end(ce);
            ii != ie; ++ii) {
-        ref<Expr> addend = ConstantExpr::alloc(0, kMachinePointerType);
-        
+        ref<ConstantExpr> addend = ConstantExpr::alloc(0, Expr::Int32);
+
         if (const StructType *st = dyn_cast<StructType>(*ii)) {
           const StructLayout *sl = kmodule->targetData->getStructLayout(st);
           const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
-          
-          addend = Expr::createPointer(sl->getElementOffset((unsigned)
-                                                            ci->getZExtValue()));
+
+          addend = ConstantExpr::alloc(sl->getElementOffset((unsigned)
+                                                            ci->getZExtValue()),
+                                       Expr::Int32);
         } else {
           const SequentialType *st = cast<SequentialType>(*ii);
-          ref<Expr> index = evalConstant(cast<Constant>(ii.getOperand()));
-          unsigned elementSize = kmodule->targetData->getTypeStoreSize(st->getElementType());
-          
-          index = Expr::createCoerceToPointerType(index);
-          addend = MulExpr::create(index,
-                                   Expr::createPointer(elementSize));
+          ref<ConstantExpr> index = 
+            evalConstant(cast<Constant>(ii.getOperand()));
+          unsigned elementSize = 
+            kmodule->targetData->getTypeStoreSize(st->getElementType());
+
+          index = index->ZExt(Expr::Int32);
+          addend = index->Mul(ConstantExpr::alloc(elementSize, Expr::Int32));
         }
-        
-        base = AddExpr::create(base, addend);
+
+        base = base->Add(addend);
       }
-      
+
       return base;
     }
       
     case Instruction::ICmp: {
       switch(ce->getPredicate()) {
-        case ICmpInst::ICMP_EQ:  return  EqExpr::create(op1, op2);
-        case ICmpInst::ICMP_NE:  return  NeExpr::create(op1, op2);
-        case ICmpInst::ICMP_UGT: return UgtExpr::create(op1, op2);
-        case ICmpInst::ICMP_UGE: return UgeExpr::create(op1, op2);
-        case ICmpInst::ICMP_ULT: return UltExpr::create(op1, op2);
-        case ICmpInst::ICMP_ULE: return UleExpr::create(op1, op2);
-        case ICmpInst::ICMP_SGT: return SgtExpr::create(op1, op2);
-        case ICmpInst::ICMP_SGE: return SgeExpr::create(op1, op2);
-        case ICmpInst::ICMP_SLT: return SltExpr::create(op1, op2);
-        case ICmpInst::ICMP_SLE: return SleExpr::create(op1, op2);
-        default:
-          assert(0 && "unhandled ICmp predicate");
+      default: assert(0 && "unhandled ICmp predicate");
+      case ICmpInst::ICMP_EQ:  return op1->Eq(op2);
+      case ICmpInst::ICMP_NE:  return op1->Ne(op2);
+      case ICmpInst::ICMP_UGT: return op1->Ugt(op2);
+      case ICmpInst::ICMP_UGE: return op1->Uge(op2);
+      case ICmpInst::ICMP_ULT: return op1->Ult(op2);
+      case ICmpInst::ICMP_ULE: return op1->Ule(op2);
+      case ICmpInst::ICMP_SGT: return op1->Sgt(op2);
+      case ICmpInst::ICMP_SGE: return op1->Sge(op2);
+      case ICmpInst::ICMP_SLT: return op1->Slt(op2);
+      case ICmpInst::ICMP_SLE: return op1->Sle(op2);
       }
     }
-      
-    case Instruction::Select: {
-      return SelectExpr::create(op1, op2, op3);
-    }
+
+    case Instruction::Select:
+      return op1->isTrue() ? op2 : op3;
 
     case Instruction::FAdd:
     case Instruction::FSub:
@@ -144,7 +138,7 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
     case Instruction::FPToSI:
     case Instruction::FCmp:
       assert(0 && "floating point ConstantExprs unsupported");
+    }
   }
-}
 
 }
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index d9849d2e..3d481751 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -99,10 +99,10 @@ public:
     this->name = name;
   }
 
-  ref<Expr> getBaseExpr() const { 
+  ref<ConstantExpr> getBaseExpr() const { 
     return ConstantExpr::create(address, kMachinePointerType);
   }
-  ref<Expr> getSizeExpr() const { 
+  ref<ConstantExpr> getSizeExpr() const { 
     return ConstantExpr::create(size, kMachinePointerType);
   }
   ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 3070da41..db673f15 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -580,8 +580,9 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
                                      "ptr.err",
                                      executor.getAddressInfo(state, address));
     } else {
-      ref<Expr> chk = op.first->getBoundsCheckPointer(address, 
-                                                      cast<ConstantExpr>(size)->getConstantValue());
+      ref<Expr> chk = 
+        op.first->getBoundsCheckPointer(address, 
+                                        cast<ConstantExpr>(size)->getZExtValue());
       if (!chk->isTrue()) {
         executor.terminateStateOnError(state,
                                        "check_memory_access: memory error",
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index fd43018f..7beaa665 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -313,7 +313,7 @@ ref<Expr> Expr::createNot(ref<Expr> e) {
   return createIsZero(e);
 }
 
-ref<Expr> Expr::createPointer(uint64_t v) {
+ref<ConstantExpr> Expr::createPointer(uint64_t v) {
   return ConstantExpr::create(v, kMachinePointerType);
 }
 
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index efb0d658..1a146641 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 (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
-      if (CE->getConstantValue() == index)
+      if (CE->getZExtValue() == index)
         return Action::changeTo(visit(un->value));
     } else {
       // update index is unknown, so may or may not be index, we
@@ -61,7 +61,7 @@ ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);
   
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v)) {
-    return evalRead(re.updates, CE->getConstantValue());
+    return evalRead(re.updates, CE->getZExtValue());
   } else {
     return Action::doChildren();
   }