From 44e3d58b59099f5fd0e6f88893ce431171b3fef6 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 4 Jun 2009 08:08:21 +0000 Subject: Start removing uses of Expr::isConstant. - These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet, changed to use ref when the type is known). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72857 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/util/Assignment.h | 3 +- lib/Core/AddressSpace.cpp | 8 +- lib/Core/Executor.cpp | 59 ++++++------- lib/Core/Executor.h | 2 +- lib/Core/ImpliedValue.cpp | 7 +- lib/Core/ImpliedValue.h | 6 +- lib/Core/Memory.cpp | 2 +- lib/Core/SeedInfo.cpp | 6 +- lib/Core/SpecialFunctionHandler.cpp | 30 +++---- lib/Expr/Expr.cpp | 167 ++++++++++++++++++------------------ lib/Expr/ExprPPrinter.cpp | 16 ++-- lib/Expr/ExprUtil.cpp | 12 +-- lib/Expr/ExprVisitor.cpp | 6 +- lib/Expr/Parser.cpp | 4 +- lib/Solver/CexCachingSolver.cpp | 5 +- lib/Solver/FastCexSolver.cpp | 4 +- lib/Solver/STPBuilder.cpp | 2 +- lib/Solver/Solver.cpp | 2 +- 18 files changed, 168 insertions(+), 173 deletions(-) diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 36f4739d..051a84f9 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -90,7 +90,8 @@ namespace klee { AssignmentEvaluator v(*this); for (; begin!=end; ++begin) { ref res = v.visit(*begin); - if (!res->isConstant() || !res->getConstantValue()) + ConstantExpr *CE = dyn_cast(res); + if (!CE || !CE->getConstantValue()) return false; } return true; diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 92d75aa8..a4a65bd9 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -72,8 +72,8 @@ bool AddressSpace::resolveOne(ExecutionState &state, ref address, ObjectPair &result, bool &success) { - if (address->isConstant()) { - success = resolveOne(address->getConstantValue(), result); + if (ConstantExpr *CE = dyn_cast(address)) { + success = resolveOne(CE->getConstantValue(), result); return true; } else { TimerStatIncrementer timer(stats::resolveTime); @@ -163,9 +163,9 @@ bool AddressSpace::resolve(ExecutionState &state, ResolutionList &rl, unsigned maxResolutions, double timeout) { - if (p->isConstant()) { + if (ConstantExpr *CE = dyn_cast(p)) { ObjectPair res; - if (resolveOne(p->getConstantValue(), res)) + if (resolveOne(CE->getConstantValue(), res)) rl.push_back(res); return false; } else { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a1687f58..f567efc6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -662,8 +662,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { seedMap.find(¤t); bool isSeeding = it != seedMap.end(); - if (!isSeeding && - !condition->isConstant() && + if (!isSeeding && !isa(condition) && (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. || MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) && statsTracker->elapsed() > 60.) { @@ -753,8 +752,8 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { bool success = solver->getValue(current, siit->assignment.evaluate(condition), res); assert(success && "FIXME: Unhandled solver failure"); - if (res->isConstant()) { - if (res->getConstantValue()) { + if (ConstantExpr *CE = dyn_cast(res)) { + if (CE->getConstantValue()) { trueSeed = true; } else { falseSeed = true; @@ -874,9 +873,8 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { } void Executor::addConstraint(ExecutionState &state, ref condition) { - if (condition->isConstant()) { - assert(condition->getConstantValue() && - "attempt to add invalid constraint"); + if (ConstantExpr *CE = dyn_cast(condition)) { + assert(CE->getConstantValue() && "attempt to add invalid constraint"); return; } @@ -902,7 +900,8 @@ void Executor::addConstraint(ExecutionState &state, ref condition) { state.addConstraint(condition); if (ivcEnabled) - doImpliedValueConcretization(state, condition, ConstantExpr::alloc(1, Expr::Bool)); + doImpliedValueConcretization(state, condition, + ConstantExpr::alloc(1, Expr::Bool)); } ref Executor::evalConstant(Constant *c) { @@ -998,7 +997,7 @@ ref Executor::toUnique(const ExecutionState &state, ref &e) { ref result = e; - if (!e->isConstant()) { + if (!isa(e)) { ref value(0); bool isTrue = false; @@ -1020,7 +1019,7 @@ ref Executor::toConstant(ExecutionState &state, ref e, const char *reason) { e = state.constraints.simplifyExpr(e); - if (!e->isConstant()) { + if (!isa(e)) { ref value; bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); @@ -1049,7 +1048,7 @@ void Executor::executeGetValue(ExecutionState &state, e = state.constraints.simplifyExpr(e); std::map< ExecutionState*, std::vector >::iterator it = seedMap.find(&state); - if (it==seedMap.end() || e->isConstant()) { + if (it==seedMap.end() || isa(e)) { ref value; bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); @@ -1393,11 +1392,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { BasicBlock *bb = si->getParent(); cond = toUnique(state, cond); - if (cond->isConstant()) { + if (ConstantExpr *CE = dyn_cast(cond)) { // Somewhat gross to create these all the time, but fine till we // switch to an internal rep. ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(), - cond->getConstantValue()); + CE->getConstantValue()); unsigned index = si->findCaseValue(ci); transferToBasicBlock(si->getSuccessor(index), si->getParent(), state); } else { @@ -2180,8 +2179,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) { } index++; } - assert(constantOffset->isConstant()); - kgepi->offset = constantOffset->getConstantValue(); + kgepi->offset = cast(constantOffset)->getConstantValue(); } void Executor::bindModuleConstants() { @@ -2346,8 +2344,8 @@ std::string Executor::getAddressInfo(ExecutionState &state, std::ostringstream info; info << "\taddress: " << address << "\n"; uint64_t example; - if (address->isConstant()) { - example = address->getConstantValue(); + if (ConstantExpr *CE = dyn_cast(address)) { + example = CE->getConstantValue(); } else { ref value; bool success = solver->getValue(state, address, value); @@ -2466,7 +2464,7 @@ void Executor::terminateStateOnError(ExecutionState &state, msg << ai->getName(); // XXX should go through function ref value = sf.locals[sf.kf->getArgRegister(index++)].value; - if (value->isConstant()) + if (isa(value)) msg << "=" << value; } msg << ")"; @@ -2521,9 +2519,9 @@ void Executor::callExternalFunction(ExecutionState &state, static_cast(ce.get())->toMemory((void*) &args[i]); } else { ref arg = toUnique(state, *ai); - if (arg->isConstant()) { + if (ConstantExpr *CE = dyn_cast(arg)) { // XXX kick toMemory functions from here - static_cast(arg.get())->toMemory((void*) &args[i]); + CE->toMemory((void*) &args[i]); } else { std::string msg = "external call with symbolic argument: " + function->getName(); terminateStateOnExecError(state, msg); @@ -2578,7 +2576,7 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, return e; // right now, we don't replace symbolics (is there any reason too?) - if (!e->isConstant()) + if (!isa(e)) return e; if (n != 1 && random() % n) @@ -2620,9 +2618,9 @@ void Executor::executeAlloc(ExecutionState &state, bool zeroMemory, const ObjectState *reallocFrom) { size = toUnique(state, size); - if (size->isConstant()) { + if (ConstantExpr *CE = dyn_cast(size)) { MemoryObject *mo = - memory->allocate(size->getConstantValue(), isLocal, false, + memory->allocate(CE->getConstantValue(), isLocal, false, state.prevPC->inst); if (!mo) { bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType)); @@ -2793,9 +2791,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, unsigned bytes = Expr::getMinBytesForWidth(type); if (SimplifySymIndices) { - if (!address->isConstant()) + if (!isa(address)) address = state.constraints.simplifyExpr(address); - if (isWrite && !value->isConstant()) + if (isWrite && !isa(value)) value = state.constraints.simplifyExpr(value); } @@ -3174,9 +3172,7 @@ void Executor::getCoveredLines(const ExecutionState &state, void Executor::doImpliedValueConcretization(ExecutionState &state, ref e, - ref value) { - assert(value->isConstant() && "non-constant passed in place of constant"); - + ref value) { if (DebugCheckForImpliedValues) ImpliedValue::checkForImpliedValues(solver->solver, e, value); @@ -3186,7 +3182,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, it != ie; ++it) { ReadExpr *re = it->first.get(); - if (re->index->isConstant()) { + if (ConstantExpr *CE = dyn_cast(re->index)) { // FIXME: This is the sole remaining usage of the Array object // variable. Kill me. const MemoryObject *mo = re->updates.root->object; @@ -3197,9 +3193,10 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, // in other cases we would like to concretize the outstanding // reads, but we have no facility for that yet) } else { - assert(!os->readOnly && "not possible? read only object with static read?"); + assert(!os->readOnly && + "not possible? read only object with static read?"); ObjectState *wos = state.addressSpace.getWriteable(mo, os); - wos->write(re->index->getConstantValue(), it->second); + wos->write(CE->getConstantValue(), it->second); } } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 2619e786..ba65cf5a 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -362,7 +362,7 @@ private: void doImpliedValueConcretization(ExecutionState &state, ref e, - ref value); + ref value); /// Add a timer to be executed periodically. /// diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index 8ebc0aef..dfb91344 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -195,16 +195,13 @@ static void _getImpliedValue(ref e, } void ImpliedValue::getImpliedValues(ref e, - ref value, + ref value, ImpliedValueList &results) { - assert(value->isConstant() && "non-constant in place of constant"); _getImpliedValue(e, value->getConstantValue(), results); } void ImpliedValue::checkForImpliedValues(Solver *S, ref e, - ref value) { - assert(value->isConstant() && "non-constant in place of constant"); - + ref value) { std::vector > reads; std::map, ref > found; ImpliedValueList results; diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h index 51ec6e9b..cbc55dc5 100644 --- a/lib/Core/ImpliedValue.h +++ b/lib/Core/ImpliedValue.h @@ -29,8 +29,10 @@ namespace klee { typedef std::vector< std::pair, ref > > ImpliedValueList; namespace ImpliedValue { - void getImpliedValues(ref e, ref cvalue, ImpliedValueList &result); - void checkForImpliedValues(Solver *S, ref e, ref cvalue); + void getImpliedValues(ref e, ref cvalue, + ImpliedValueList &result); + void checkForImpliedValues(Solver *S, ref e, + ref cvalue); } } diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index de48651b..b4c433b1 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -339,7 +339,7 @@ void ObjectState::write8(unsigned offset, ref value) { } void ObjectState::write8(ref offset, ref value) { - assert(!offset->isConstant() && "constant offset passed to symbolic write8"); + assert(!isa(offset) && "constant offset passed to symbolic write8"); unsigned base, size; fastRangeCheckOffset(offset, &base, &size); flushRangeForWrite(base, size); diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 30377ee4..62b71e87 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -77,9 +77,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, for (std::vector< ref >::iterator it = reads.begin(), ie = reads.end(); it != ie; ++it) { ReadExpr *re = it->get(); - if (re->index->isConstant()) { - unsigned index = (unsigned) re->index->getConstantValue(); - directReads.insert(std::make_pair(re->updates.root, index)); + if (ConstantExpr *CE = dyn_cast(re->index)) { + directReads.insert(std::make_pair(re->updates.root, + (unsigned) CE->getConstantValue())); } } diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index b2e5d277..e1182cf0 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -172,11 +172,12 @@ bool SpecialFunctionHandler::handle(ExecutionState &state, /****/ // reads a concrete string from memory -std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, - ref address) { +std::string +SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, + ref addressExpr) { ObjectPair op; - address = executor.toUnique(state, address); - assert(address->isConstant() && "symbolic string arg to intrinsic"); + addressExpr = executor.toUnique(state, addressExpr); + ref address = cast(addressExpr); if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); bool res; @@ -195,9 +196,9 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, for (i = 0; i < mo->size - 1; i++) { ref cur = os->read8(i); cur = executor.toUnique(state, cur); - assert(cur->isConstant() && + assert(isa(cur) && "hit symbolic char while reading concrete string"); - buf[i] = cur->getConstantValue(); + buf[i] = cast(cur)->getConstantValue(); } buf[i] = 0; @@ -438,12 +439,12 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, "invalid number of arguments to klee_set_forking"); ref value = executor.toUnique(state, arguments[0]); - if (!value->isConstant()) { + if (ConstantExpr *CE = dyn_cast(value)) { + state.forkDisabled = !CE->getConstantValue(); + } else { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", "user.err"); - } else { - state.forkDisabled = !value->getConstantValue(); } } @@ -476,7 +477,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, std::string msg_str = readStringAtAddress(state, arguments[0]); llvm::cerr << msg_str << ":" << arguments[1]; - if (!arguments[1]->isConstant()) { + if (!isa(arguments[1])) { // FIXME: Pull into a unique value method? ref value; bool success = executor.solver->getValue(state, arguments[1], value); @@ -590,7 +591,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, ref address = executor.toUnique(state, arguments[0]); ref size = executor.toUnique(state, arguments[1]); - if (!address->isConstant() || !size->isConstant()) { + if (!isa(address) || !isa(size)) { executor.terminateStateOnError(state, "check_memory_access requires constant args", "user.err"); @@ -605,8 +606,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, } else { ref chk = op.first->getBoundsCheckPointer(address, size->getConstantValue()); - assert(chk->isConstant()); - if (!chk->getConstantValue()) { + if (!cast(chk)->getConstantValue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", "ptr.err", @@ -630,9 +630,9 @@ void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state, std::vector > &arguments) { assert(arguments.size()==2 && "invalid number of arguments to klee_define_fixed_object"); - assert(arguments[0]->isConstant() && + assert(isa(arguments[0]) && "expect constant address argument to klee_define_fixed_object"); - assert(arguments[1]->isConstant() && + assert(isa(arguments[1]) && "expect constant size argument to klee_define_fixed_object"); uint64_t address = arguments[0]->getConstantValue(); diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 6cd15be7..0a174179 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -551,13 +551,12 @@ ref SExtExpr::create(const ref &e, Width w) { static ref AndExpr_create(Expr *l, Expr *r); static ref XorExpr_create(Expr *l, Expr *r); -static ref EqExpr_createPartial(Expr *l, const ref &cr); -static ref AndExpr_createPartialR(const ref &cl, Expr *r); -static ref SubExpr_createPartialR(const ref &cl, Expr *r); -static ref XorExpr_createPartialR(const ref &cl, Expr *r); +static ref EqExpr_createPartial(Expr *l, const ref &cr); +static ref AndExpr_createPartialR(const ref &cl, Expr *r); +static ref SubExpr_createPartialR(const ref &cl, Expr *r); +static ref XorExpr_createPartialR(const ref &cl, Expr *r); -static ref AddExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl->isConstant() && "non-constant passed in place of constant"); +static ref AddExpr_createPartialR(const ref &cl, Expr *r) { uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -567,10 +566,10 @@ static ref AddExpr_createPartialR(const ref &cl, Expr *r) { return r; } else { Expr::Kind rk = r->getKind(); - if (rk==Expr::Add && r->getKid(0)->isConstant()) { // A + (B+c) == (A+B) + c + if (rk==Expr::Add && isa(r->getKid(0))) { // A + (B+c) == (A+B) + c return AddExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); - } else if (rk==Expr::Sub && r->getKid(0)->isConstant()) { // A + (B-c) == (A+B) - c + } else if (rk==Expr::Sub && isa(r->getKid(0))) { // A + (B-c) == (A+B) - c return SubExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); } else { @@ -578,7 +577,7 @@ static ref AddExpr_createPartialR(const ref &cl, Expr *r) { } } } -static ref AddExpr_createPartial(Expr *l, const ref &cr) { +static ref AddExpr_createPartial(Expr *l, const ref &cr) { return AddExpr_createPartialR(cr, l); } static ref AddExpr_create(Expr *l, Expr *r) { @@ -588,16 +587,16 @@ static ref AddExpr_create(Expr *l, Expr *r) { return XorExpr_create(l, r); } else { Expr::Kind lk = l->getKind(), rk = r->getKind(); - if (lk==Expr::Add && l->getKid(0)->isConstant()) { // (k+a)+b = k+(a+b) + if (lk==Expr::Add && isa(l->getKid(0))) { // (k+a)+b = k+(a+b) return AddExpr::create(l->getKid(0), AddExpr::create(l->getKid(1), r)); - } else if (lk==Expr::Sub && l->getKid(0)->isConstant()) { // (k-a)+b = k+(b-a) + } else if (lk==Expr::Sub && isa(l->getKid(0))) { // (k-a)+b = k+(b-a) return AddExpr::create(l->getKid(0), SubExpr::create(r, l->getKid(1))); - } else if (rk==Expr::Add && r->getKid(0)->isConstant()) { // a + (k+b) = k+(a+b) + } else if (rk==Expr::Add && isa(r->getKid(0))) { // a + (k+b) = k+(a+b) return AddExpr::create(r->getKid(0), AddExpr::create(l, r->getKid(1))); - } else if (rk==Expr::Sub && r->getKid(0)->isConstant()) { // a + (k-b) = k+(a-b) + } else if (rk==Expr::Sub && isa(r->getKid(0))) { // a + (k-b) = k+(a-b) return AddExpr::create(r->getKid(0), SubExpr::create(l, r->getKid(1))); } else { @@ -606,8 +605,7 @@ static ref AddExpr_create(Expr *l, Expr *r) { } } -static ref SubExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl->isConstant() && "non-constant passed in place of constant"); +static ref SubExpr_createPartialR(const ref &cl, Expr *r) { Expr::Width type = cl->getWidth(); if (type==Expr::Bool) { @@ -625,7 +623,7 @@ static ref SubExpr_createPartialR(const ref &cl, Expr *r) { } } } -static ref SubExpr_createPartial(Expr *l, const ref &cr) { +static ref SubExpr_createPartial(Expr *l, const ref &cr) { assert(cr->isConstant() && "non-constant passed in place of constant"); uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); @@ -642,16 +640,16 @@ static ref SubExpr_create(Expr *l, Expr *r) { return ConstantExpr::alloc(0, type); } else { Expr::Kind lk = l->getKind(), rk = r->getKind(); - if (lk==Expr::Add && l->getKid(0)->isConstant()) { // (k+a)-b = k+(a-b) + if (lk==Expr::Add && isa(l->getKid(0))) { // (k+a)-b = k+(a-b) return AddExpr::create(l->getKid(0), SubExpr::create(l->getKid(1), r)); - } else if (lk==Expr::Sub && l->getKid(0)->isConstant()) { // (k-a)-b = k-(a+b) + } else if (lk==Expr::Sub && isa(l->getKid(0))) { // (k-a)-b = k-(a+b) return SubExpr::create(l->getKid(0), AddExpr::create(l->getKid(1), r)); - } else if (rk==Expr::Add && r->getKid(0)->isConstant()) { // a - (k+b) = (a-c) - k + } else if (rk==Expr::Add && isa(r->getKid(0))) { // a - (k+b) = (a-c) - k return SubExpr::create(SubExpr::create(l, r->getKid(1)), r->getKid(0)); - } else if (rk==Expr::Sub && r->getKid(0)->isConstant()) { // a - (k-b) = (a+b) - k + } else if (rk==Expr::Sub && isa(r->getKid(0))) { // a - (k-b) = (a+b) - k return SubExpr::create(AddExpr::create(l, r->getKid(1)), r->getKid(0)); } else { @@ -660,7 +658,7 @@ static ref SubExpr_create(Expr *l, Expr *r) { } } -static ref MulExpr_createPartialR(const ref &cl, Expr *r) { +static ref MulExpr_createPartialR(const ref &cl, Expr *r) { assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -675,7 +673,7 @@ static ref MulExpr_createPartialR(const ref &cl, Expr *r) { return MulExpr::alloc(cl, r); } } -static ref MulExpr_createPartial(Expr *l, const ref &cr) { +static ref MulExpr_createPartial(Expr *l, const ref &cr) { return MulExpr_createPartialR(cr, l); } static ref MulExpr_create(Expr *l, Expr *r) { @@ -688,8 +686,7 @@ static ref MulExpr_create(Expr *l, Expr *r) { } } -static ref AndExpr_createPartial(Expr *l, const ref &cr) { - assert(cr->isConstant() && "non-constant passed in place of constant"); +static ref AndExpr_createPartial(Expr *l, const ref &cr) { uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); @@ -701,15 +698,14 @@ static ref AndExpr_createPartial(Expr *l, const ref &cr) { return AndExpr::alloc(l, cr); } } -static ref AndExpr_createPartialR(const ref &cl, Expr *r) { +static ref AndExpr_createPartialR(const ref &cl, Expr *r) { return AndExpr_createPartial(r, cl); } static ref AndExpr_create(Expr *l, Expr *r) { return AndExpr::alloc(l, r); } -static ref OrExpr_createPartial(Expr *l, const ref &cr) { - assert(cr->isConstant() && "non-constant passed in place of constant"); +static ref OrExpr_createPartial(Expr *l, const ref &cr) { uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); @@ -721,15 +717,14 @@ static ref OrExpr_createPartial(Expr *l, const ref &cr) { return OrExpr::alloc(l, cr); } } -static ref OrExpr_createPartialR(const ref &cl, Expr *r) { +static ref OrExpr_createPartialR(const ref &cl, Expr *r) { return OrExpr_createPartial(r, cl); } static ref OrExpr_create(Expr *l, Expr *r) { return OrExpr::alloc(l, r); } -static ref XorExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl->isConstant() && "non-constant passed in place of constant"); +static ref XorExpr_createPartialR(const ref &cl, Expr *r) { uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -746,7 +741,7 @@ static ref XorExpr_createPartialR(const ref &cl, Expr *r) { } } -static ref XorExpr_createPartial(Expr *l, const ref &cr) { +static ref XorExpr_createPartial(Expr *l, const ref &cr) { return XorExpr_createPartialR(cr, l); } static ref XorExpr_create(Expr *l, Expr *r) { @@ -811,34 +806,34 @@ static ref AShrExpr_create(const ref &l, const ref &r) { #define BCREATE_R(_e_op, _op, partialL, partialR) \ ref _e_op ::create(const ref &l, const ref &r) { \ - assert(l->getWidth()==r->getWidth() && "type mismatch"); \ - if (l->isConstant()) { \ - if (r->isConstant()) { \ - Expr::Width width = l->getWidth(); \ - uint64_t val = ints::_op(l->getConstantValue(), \ - r->getConstantValue(), width); \ - return ConstantExpr::create(val, width); \ - } else { \ - return _e_op ## _createPartialR(l, r.get()); \ - } \ - } else if (r->isConstant()) { \ - return _e_op ## _createPartial(l.get(), r); \ - } \ - return _e_op ## _create(l.get(), r.get()); \ + assert(l->getWidth()==r->getWidth() && "type mismatch"); \ + if (ConstantExpr *cl = dyn_cast(l)) { \ + if (ConstantExpr *cr = dyn_cast(r)) { \ + Expr::Width width = l->getWidth(); \ + uint64_t val = ints::_op(cl->getConstantValue(), \ + cr->getConstantValue(), width); \ + return ConstantExpr::create(val, width); \ + } else { \ + return _e_op ## _createPartialR(cl, r.get()); \ + } \ + } else if (ConstantExpr *cr = dyn_cast(r)) { \ + return _e_op ## _createPartial(l.get(), cr); \ + } \ + return _e_op ## _create(l.get(), r.get()); \ } #define BCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ - assert(l->getWidth()==r->getWidth() && "type mismatch"); \ - if (l->isConstant()) { \ - if (r->isConstant()) { \ - Expr::Width width = l->getWidth(); \ - uint64_t val = ints::_op(l->getConstantValue(), \ - r->getConstantValue(), width); \ - return ConstantExpr::create(val, width); \ - } \ - } \ - return _e_op ## _create(l, r); \ + assert(l->getWidth()==r->getWidth() && "type mismatch"); \ + if (ConstantExpr *cl = dyn_cast(l)) { \ + if (ConstantExpr *cr = dyn_cast(r)) { \ + Expr::Width width = l->getWidth(); \ + uint64_t val = ints::_op(cl->getConstantValue(), \ + cr->getConstantValue(), width); \ + return ConstantExpr::create(val, width); \ + } \ + } \ + return _e_op ## _create(l, r); \ } BCREATE_R(AddExpr, add, AddExpr_createPartial, AddExpr_createPartialR) @@ -857,35 +852,35 @@ BCREATE(AShrExpr, ashr) #define CMPCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ - assert(l->getWidth()==r->getWidth() && "type mismatch"); \ - if (l->isConstant()) { \ - if (r->isConstant()) { \ - Expr::Width width = l->getWidth(); \ - uint64_t val = ints::_op(l->getConstantValue(), \ - r->getConstantValue(), width); \ - return ConstantExpr::create(val, Expr::Bool); \ - } \ - } \ - return _e_op ## _create(l, r); \ + assert(l->getWidth()==r->getWidth() && "type mismatch"); \ + if (ConstantExpr *cl = dyn_cast(l)) { \ + if (ConstantExpr *cr = dyn_cast(r)) { \ + Expr::Width width = cl->getWidth(); \ + uint64_t val = ints::_op(cl->getConstantValue(), \ + cr->getConstantValue(), width); \ + return ConstantExpr::create(val, Expr::Bool); \ + } \ + } \ + return _e_op ## _create(l, r); \ } #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \ -ref _e_op ::create(const ref &l, const ref &r) { \ - assert(l->getWidth()==r->getWidth() && "type mismatch"); \ - if (l->isConstant()) { \ - if (r->isConstant()) { \ - Expr::Width width = l->getWidth(); \ - uint64_t val = ints::_op(l->getConstantValue(), \ - r->getConstantValue(), width); \ - return ConstantExpr::create(val, Expr::Bool); \ - } else { \ - return partialR(l, r.get()); \ - } \ - } else if (r->isConstant()) { \ - return partialL(l.get(), r); \ - } else { \ - return _e_op ## _create(l.get(), r.get()); \ - } \ +ref _e_op ::create(const ref &l, const ref &r) { \ + assert(l->getWidth()==r->getWidth() && "type mismatch"); \ + if (ConstantExpr *cl = dyn_cast(l)) { \ + if (ConstantExpr *cr = dyn_cast(r)) { \ + Expr::Width width = cl->getWidth(); \ + uint64_t val = ints::_op(cl->getConstantValue(), \ + cr->getConstantValue(), width); \ + return ConstantExpr::create(val, Expr::Bool); \ + } else { \ + return partialR(cl, r.get()); \ + } \ + } else if (ConstantExpr *cr = dyn_cast(r)) { \ + return partialL(l.get(), cr); \ + } else { \ + return _e_op ## _create(l.get(), r.get()); \ + } \ } @@ -972,7 +967,7 @@ static ref TryConstArrayOpt(const ref &cl, } -static ref EqExpr_createPartialR(const ref &cl, Expr *r) { +static ref EqExpr_createPartialR(const ref &cl, Expr *r) { assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width width = cl->getWidth(); @@ -1031,14 +1026,16 @@ static ref EqExpr_createPartialR(const ref &cl, Expr *r) { const AddExpr *ae = cast(r); if (ae->left->isConstant()) { // c0 = c1 + b => c0 - c1 = b - return EqExpr_createPartialR(SubExpr::create(cl, ae->left), + return EqExpr_createPartialR(cast(SubExpr::create(cl, + ae->left)), ae->right.get()); } } else if (rk==Expr::Sub) { const SubExpr *se = cast(r); if (se->left->isConstant()) { // c0 = c1 - b => c1 - c0 = b - return EqExpr_createPartialR(SubExpr::create(se->left, cl), + return EqExpr_createPartialR(cast(SubExpr::create(se->left, + cl)), se->right.get()); } } else if (rk == Expr::Read && ConstArrayOpt) { @@ -1048,7 +1045,7 @@ static ref EqExpr_createPartialR(const ref &cl, Expr *r) { return EqExpr_create(cl, r); } -static ref EqExpr_createPartial(Expr *l, const ref &cr) { +static ref EqExpr_createPartial(Expr *l, const ref &cr) { return EqExpr_createPartialR(cr, l); } diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index e26568d9..94c0ac17 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -100,7 +100,7 @@ class PPrinter : public ExprPPrinter { } bool isVerySimple(const ref &e) { - return e->isConstant() || bindings.find(e)!=bindings.end(); + return isa(e) || bindings.find(e)!=bindings.end(); } bool isVerySimpleUpdate(const UpdateNode *un) { @@ -143,7 +143,7 @@ class PPrinter : public ExprPPrinter { } void scan1(const ref &e) { - if (!e->isConstant()) { + if (!isa(e)) { if (couldPrint.insert(e).second) { Expr *ep = e.get(); for (unsigned i=0; igetNumKids(); i++) @@ -208,7 +208,8 @@ class PPrinter : public ExprPPrinter { print(un->value, PC); //PC << ')'; - nextShouldBreak = !(un->index->isConstant() && un->value->isConstant()); + nextShouldBreak = !(isa(un->index) && + isa(un->value)); } if (openedList) @@ -367,9 +368,8 @@ public: print(e, PC); } - void printConst(const ref &e, PrintContext &PC, bool printWidth) { - assert(e->isConstant()); - + void printConst(const ref &e, PrintContext &PC, + bool printWidth) { if (e->getWidth() == Expr::Bool) PC << (e->getConstantValue() ? "true" : "false"); else { @@ -387,8 +387,8 @@ public: } void print(const ref &e, PrintContext &PC, bool printConstWidth=false) { - if (e->isConstant()) - printConst(e, PC, printConstWidth); + if (ConstantExpr *CE = dyn_cast(e)) + printConst(CE, PC, printConstWidth); else { std::map, unsigned>::iterator it = bindings.find(e); if (it!=bindings.end()) { diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 780398f0..0c150a51 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -26,7 +26,7 @@ void klee::findReads(ref e, ExprHashSet visited; std::set updates; - if (!e->isConstant()) { + if (!isa(e)) { visited.insert(e); stack.push_back(e); } @@ -40,7 +40,7 @@ void klee::findReads(ref e, // repeats. results.push_back(re); - if (!re->index->isConstant() && + if (!isa(re->index) && visited.insert(re->index).second) stack.push_back(re->index); @@ -53,20 +53,20 @@ void klee::findReads(ref e, // head, which often will be shared among multiple nodes. if (updates.insert(re->updates.head).second) { for (const UpdateNode *un=re->updates.head; un; un=un->next) { - if (!un->index->isConstant() && + if (!isa(un->index) && visited.insert(un->index).second) stack.push_back(un->index); - if (!un->value->isConstant() && + if (!isa(un->value) && visited.insert(un->value).second) stack.push_back(un->value); } } } - } else if (!top->isConstant()) { + } else if (!isa(top)) { Expr *e = top.get(); for (unsigned i=0; igetNumKids(); i++) { ref k = e->getKid(i); - if (!k->isConstant() && + if (!isa(k) && visited.insert(k).second) stack.push_back(k); } diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index 5e9d0a81..c81199d7 100644 --- a/lib/Expr/ExprVisitor.cpp +++ b/lib/Expr/ExprVisitor.cpp @@ -22,7 +22,7 @@ namespace { using namespace klee; ref ExprVisitor::visit(const ref &e) { - if (!UseVisitorHash || e->isConstant()) { + if (!UseVisitorHash || isa(e)) { return visitActual(e); } else { visited_ty::iterator it = visited.find(e); @@ -38,7 +38,7 @@ ref ExprVisitor::visit(const ref &e) { } ref ExprVisitor::visitActual(const ref &e) { - if (e->isConstant()) { + if (isa(e)) { return e; } else { Expr &ep = *e.get(); @@ -106,7 +106,7 @@ ref ExprVisitor::visitActual(const ref &e) { if (recursive) e = visit(e); } - if (!e->isConstant()) { + if (!isa(e)) { res = visitExprPost(*e.get()); if (res.kind==Action::ChangeTo) e = res.argument; diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 1808ca7b..c0cc05d5 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -947,8 +947,8 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name, if (!OffsetExpr.isValid() || !Child.isValid()) return ConstantExpr::alloc(0, ResTy); - assert(OffsetExpr.get()->isConstant() && "ParseNumber returned non-constant."); - unsigned Offset = (unsigned) OffsetExpr.get()->getConstantValue(); + unsigned Offset = + (unsigned) cast(OffsetExpr.get())->getConstantValue(); if (Offset + ResTy > Child.get()->getWidth()) { Error("extract out-of-range of child expression.", Name); diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 546d81fd..49db74e8 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -217,7 +217,8 @@ bool CexCachingSolver::computeValidity(const Query& query, return false; assert(a && "computeValidity() must have assignment"); ref q = a->evaluate(query.expr); - assert(q->isConstant() && "assignment evaluation did not result in constant"); + assert(isa(q) && + "assignment evaluation did not result in constant"); if (q->getConstantValue()) { if (!getAssignment(query, a)) @@ -268,7 +269,7 @@ bool CexCachingSolver::computeValue(const Query& query, return false; assert(a && "computeValue() must have assignment"); result = a->evaluate(query.expr); - assert(result->isConstant() && + assert(isa(result) && "assignment evaluation did not result in constant"); return true; } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index cc0068ca..a0d943d3 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -729,7 +729,7 @@ public: bool exprMustBeValue(ref e, uint64_t value) { CexConstifier cc(objectValues); ref v = cc.visit(e); - if (!v->isConstant()) return false; + if (!isa(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; @@ -886,7 +886,7 @@ bool FastCexSolver::computeValue(const Query& query, ref &result) { CexConstifier cc(cd.objectValues); ref value = cc.visit(query.expr); - if (value->isConstant()) { + if (isa(value)) { result = value; return true; } else { diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index ee5b777b..00fd8e4a 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -419,7 +419,7 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { /** if *width_out!=1 then result is a bitvector, otherwise it is a bool */ ExprHandle STPBuilder::construct(ref e, int *width_out) { - if (!UseConstructHash || e->isConstant()) { + if (!UseConstructHash || isa(e)) { return constructActual(e, width_out); } else { ExprHashMap< std::pair >::iterator it = diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 46d6039e..6cbf6ac0 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -112,7 +112,7 @@ bool Solver::mayBeFalse(const Query& query, bool &result) { bool Solver::getValue(const Query& query, ref &result) { // Maintain invariants implementation expect. - if (query.expr->isConstant()) { + if (isa(query.expr)) { result = query.expr; return true; } -- cgit 1.4.1