diff options
-rw-r--r-- | include/klee/Expr.h | 2 | ||||
-rw-r--r-- | lib/Core/AddressSpace.cpp | 4 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 19 | ||||
-rw-r--r-- | lib/Core/Executor.h | 6 | ||||
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 136 | ||||
-rw-r--r-- | lib/Core/Memory.h | 4 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 5 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 2 | ||||
-rw-r--r-- | lib/Expr/ExprEvaluator.cpp | 4 |
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(); } |