diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-06-04 08:59:53 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-06-04 08:59:53 +0000 |
commit | 92004d6524c7633aa1e014e5b727a39475652dda (patch) | |
tree | e68a45e3aa57b34a33f5f1dfbb496acb8bcebc9a /lib/Core | |
parent | 21fb3bd80309b30ed2223e793003ac4744776dfb (diff) | |
download | klee-92004d6524c7633aa1e014e5b727a39475652dda.tar.gz |
Sink getConstantValue into ConstantExpr.
- Propogate ConstantExpr to various places, or cast as appropriate. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72862 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 74 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/ImpliedValue.cpp | 10 | ||||
-rw-r--r-- | lib/Core/ImpliedValue.h | 3 | ||||
-rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 10 |
5 files changed, 52 insertions, 48 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index aa8681dc..21356af9 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1015,31 +1015,31 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, /* Concretize the given expression, and return a possible constant value. 'reason' is just a documentation string stating the reason for concretization. */ -ref<Expr> Executor::toConstant(ExecutionState &state, - ref<Expr> e, - const char *reason) { +ref<klee::ConstantExpr> +Executor::toConstant(ExecutionState &state, + ref<Expr> e, + const char *reason) { e = state.constraints.simplifyExpr(e); - if (!isa<ConstantExpr>(e)) { - ref<ConstantExpr> value; - bool success = solver->getValue(state, e, value); - assert(success && "FIXME: Unhandled solver failure"); + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) + return CE; + + ref<ConstantExpr> value; + bool success = solver->getValue(state, e, value); + assert(success && "FIXME: Unhandled solver failure"); - std::ostringstream os; - os << "silently concretizing (reason: " << reason << ") expression " << e - << " to value " << value - << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")"; + std::ostringstream os; + os << "silently concretizing (reason: " << reason << ") expression " << e + << " to value " << value + << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")"; - if (AllExternalWarnings) - klee_warning(reason, os.str().c_str()); - else - klee_warning_once(reason, "%s", os.str().c_str()); + if (AllExternalWarnings) + klee_warning(reason, os.str().c_str()); + else + klee_warning_once(reason, "%s", os.str().c_str()); - addConstraint(state, EqExpr::create(e, value)); + addConstraint(state, EqExpr::create(e, value)); - return value; - } else { - return e; - } + return value; } void Executor::executeGetValue(ExecutionState &state, @@ -1909,8 +1909,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::trunc(arg->getConstantValue(), resultType, arg->getWidth()); @@ -1921,8 +1921,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::ext(arg->getConstantValue(), resultType, arg->getWidth()); @@ -1933,8 +1933,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::toUnsignedInt(arg->getConstantValue(), resultType, arg->getWidth()); @@ -1945,8 +1945,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::toSignedInt(arg->getConstantValue(), resultType, arg->getWidth()); @@ -1957,8 +1957,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::UnsignedIntToFP(arg->getConstantValue(), resultType); bindLocal(ki, state, ConstantExpr::alloc(value, resultType)); @@ -1968,8 +1968,8 @@ 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).value, - "floating point"); + ref<ConstantExpr> arg = toConstant(state, eval(ki, 0, state).value, + "floating point"); uint64_t value = floats::SignedIntToFP(arg->getConstantValue(), resultType, arg->getWidth()); @@ -1980,10 +1980,10 @@ 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).value, - "floating point"); - ref<Expr> right = toConstant(state, eval(ki, 1, state).value, - "floating point"); + ref<ConstantExpr> left = toConstant(state, eval(ki, 0, state).value, + "floating point"); + ref<ConstantExpr> right = toConstant(state, eval(ki, 1, state).value, + "floating point"); uint64_t leftVal = left->getConstantValue(); uint64_t rightVal = right->getConstantValue(); @@ -2804,7 +2804,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(cast<ConstantExpr>(address)->getConstantValue(), op); } solver->setTimeout(0); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index ba65cf5a..013d3bb8 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -319,7 +319,8 @@ private: /// should generally be avoided. /// /// \param purpose An identify string to printed in case of concretization. - ref<Expr> toConstant(ExecutionState &state, ref<Expr> e, const char *purpose); + ref<klee::ConstantExpr> toConstant(ExecutionState &state, ref<Expr> e, + const char *purpose); /// Bind a constant value for e to the given target. NOTE: This /// function may fork state if the state has multiple seeds. diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index 6ad0f5d2..e1daca2f 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -30,7 +30,8 @@ static void _getImpliedValue(ref<Expr> e, ImpliedValueList &results) { switch (e->getKind()) { case Expr::Constant: { - assert(value == e->getConstantValue() && "error in implied value calculation"); + assert(value == cast<ConstantExpr>(e)->getConstantValue() && + "error in implied value calculation"); break; } @@ -203,14 +204,15 @@ void ImpliedValue::getImpliedValues(ref<Expr> e, void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, ref<ConstantExpr> value) { std::vector<ref<ReadExpr> > reads; - std::map<ref<ReadExpr>, ref<Expr> > found; + std::map<ref<ReadExpr>, ref<ConstantExpr> > found; ImpliedValueList results; getImpliedValues(e, value, results); for (ImpliedValueList::iterator i = results.begin(), ie = results.end(); i != ie; ++i) { - std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(i->first); + std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = + found.find(i->first); if (it != found.end()) { assert(it->second->getConstantValue() == i->second->getConstantValue() && "I don't think so Scott"); @@ -247,7 +249,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e, ref<ConstantExpr> possible; bool success = S->getValue(Query(assume, var), possible); assert(success && "FIXME: Unhandled solver failure"); - std::map<ref<ReadExpr>, ref<Expr> >::iterator it = found.find(var); + std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = found.find(var); bool res; success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res); assert(success && "FIXME: Unhandled solver failure"); diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h index cbc55dc5..6bdb6c66 100644 --- a/lib/Core/ImpliedValue.h +++ b/lib/Core/ImpliedValue.h @@ -26,7 +26,8 @@ namespace klee { class ReadExpr; class Solver; - typedef std::vector< std::pair<ref<ReadExpr>, ref<Expr> > > ImpliedValueList; + typedef std::vector< std::pair<ref<ReadExpr>, + ref<ConstantExpr> > > ImpliedValueList; namespace ImpliedValue { void getImpliedValues(ref<Expr> e, ref<ConstantExpr> cvalue, diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index ea2594eb..2ee73457 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -419,7 +419,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state, assert(isa<ConstantExpr>(arguments[0]) && "symbolic argument given to klee_under_constrained!"); - unsigned v = arguments[0]->getConstantValue(); + unsigned v = cast<ConstantExpr>(arguments[0])->getConstantValue(); llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n"; if(v) { assert(state.underConstrained == false && @@ -599,14 +599,14 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, } else { ObjectPair op; - if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) { + if (!state.addressSpace.resolveOne(cast<ConstantExpr>(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()); + cast<ConstantExpr>(size)->getConstantValue()); if (!cast<ConstantExpr>(chk)->getConstantValue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", @@ -636,8 +636,8 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state, assert(isa<ConstantExpr>(arguments[1]) && "expect constant size argument to klee_define_fixed_object"); - uint64_t address = arguments[0]->getConstantValue(); - uint64_t size = arguments[1]->getConstantValue(); + uint64_t address = cast<ConstantExpr>(arguments[0])->getConstantValue(); + uint64_t size = cast<ConstantExpr>(arguments[1])->getConstantValue(); MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst); executor.bindObjectInState(state, mo, false); mo->isUserSpecified = true; // XXX hack; |