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 | |
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')
-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 | ||||
-rw-r--r-- | lib/Expr/Constraints.cpp | 3 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 38 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 7 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 2 |
10 files changed, 78 insertions, 74 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; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 5869a852..8f89f88a 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -122,7 +122,8 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) { switch (e->getKind()) { case Expr::Constant: - assert(e->getConstantValue() && "attempt to add invalid (false) constraint"); + assert(cast<ConstantExpr>(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 f95369f4..c645f37c 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -189,11 +189,6 @@ unsigned ReadExpr::computeHash() { return hashValue; } -uint64_t Expr::getConstantValue() const { - assert(getKind() == Constant); - return static_cast<const ConstantExpr*>(this)->asUInt64; -} - ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) { unsigned numArgs = args.size(); @@ -428,22 +423,26 @@ 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(); - /* Constant folding */ - 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(); - return ConstantExpr::create(res, w); + // Fold concatenation of constants. + // + // FIXME: concat 0 x -> zext x ? + if (ConstantExpr *lCE = dyn_cast<ConstantExpr>(l)) { + if (ConstantExpr *rCE = dyn_cast<ConstantExpr>(r)) { + assert(w <= 64 && "ConcatExpr::create(): don't support concats describing constants greater than 64 bits yet"); + + uint64_t res = (lCE->getConstantValue() << rCE->getWidth()) + + rCE->getConstantValue(); + return ConstantExpr::create(res, w); + } } // Merge contiguous Extracts - if (l->getKind() == Expr::Extract && r->getKind() == Expr::Extract) { - const ExtractExpr* ee_left = cast<ExtractExpr>(l); - const ExtractExpr* ee_right = cast<ExtractExpr>(r); - if (ee_left->expr == ee_right->expr && - ee_right->offset + ee_right->width == ee_left->offset) { - return ExtractExpr::create(ee_left->expr, ee_right->offset, w); + if (ExtractExpr *ee_left = dyn_cast<ExtractExpr>(l)) { + if (ExtractExpr *ee_right = dyn_cast<ExtractExpr>(r)) { + if (ee_left->expr == ee_right->expr && + ee_right->offset + ee_right->width == ee_left->offset) { + return ExtractExpr::create(ee_left->expr, ee_right->offset, w); + } } } @@ -949,7 +948,8 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &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 && + cast<ConstantExpr>(un->value)->getConstantValue() == ct) { ref<Expr> curr_eq = EqExpr::create(un->index, rd->index); res = OrExpr::create(curr_eq, res); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 1eaec4d9..9c233530 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query, assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); - if (q->getConstantValue()) { + if (cast<ConstantExpr>(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 1a1cfe62..6d9c8551 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -730,10 +730,9 @@ public: bool exprMustBeValue(ref<Expr> e, uint64_t value) { CexConstifier cc(objectValues); ref<Expr> v = cc.visit(e); - if (!isa<ConstantExpr>(v)) return false; - // XXX reenable once all reads and vars are fixed - // assert(v.isConstant() && "not all values have been fixed"); - return v->getConstantValue() == value; + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v)) + return CE->getConstantValue() == value; + return false; } }; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 88bdd2b0..5b3fdd60 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -449,7 +449,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { switch (e->getKind()) { case Expr::Constant: { - uint64_t asUInt64 = e->getConstantValue(); + uint64_t asUInt64 = cast<ConstantExpr>(e)->getConstantValue(); *width_out = e->getWidth(); if (*width_out > 64) |