From b9c0914f3d27e04e3335760b7fd13c5e9953103d Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 4 Jun 2009 00:49:34 +0000 Subject: Move isConstant from ref<> to Expr:: - Ref.h is now freestanding. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8 --- include/klee/Expr.h | 7 +-- include/klee/util/Assignment.h | 2 +- include/klee/util/Ref.h | 16 +++---- lib/Core/AddressSpace.cpp | 4 +- lib/Core/Executor.cpp | 34 +++++++-------- lib/Core/ImpliedValue.cpp | 18 ++++---- lib/Core/Memory.cpp | 12 +++--- lib/Core/SeedInfo.cpp | 2 +- lib/Core/SpecialFunctionHandler.cpp | 25 +++++------ lib/Core/TimingSolver.cpp | 6 +-- lib/Expr/Constraints.cpp | 6 +-- lib/Expr/Expr.cpp | 86 ++++++++++++++++++------------------- lib/Expr/ExprEvaluator.cpp | 6 +-- lib/Expr/ExprPPrinter.cpp | 10 ++--- lib/Expr/ExprUtil.cpp | 12 +++--- lib/Expr/ExprVisitor.cpp | 6 +-- lib/Expr/Parser.cpp | 2 +- lib/Solver/CexCachingSolver.cpp | 8 ++-- lib/Solver/FastCexSolver.cpp | 10 ++--- lib/Solver/IndependentSolver.cpp | 2 +- lib/Solver/STPBuilder.cpp | 18 ++++---- lib/Solver/Solver.cpp | 8 ++-- 22 files changed, 149 insertions(+), 151 deletions(-) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index ea5f18c9..df55d126 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -12,6 +12,7 @@ #include "Machine.h" #include "klee/util/Bits.h" +#include "klee/util/Ref.h" #include "llvm/Support/Streams.h" #include "llvm/ADT/SmallVector.h" @@ -188,6 +189,7 @@ public: /// + bool isConstant() const { return getKind() == Expr::Constant; } uint64_t getConstantValue() const; /* Static utility methods */ @@ -224,11 +226,6 @@ public: static bool isValidKidWidth(unsigned kid, Width w) { return true; } static bool needsResultType() { return false; } }; -// END class Expr - - - -#include "klee/util/Ref.h" struct Expr::CreateArg { ref expr; diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 54f6b0af..36f4739d 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -90,7 +90,7 @@ namespace klee { AssignmentEvaluator v(*this); for (; begin!=end; ++begin) { ref res = v.visit(*begin); - if (!res.isConstant() || !res->getConstantValue()) + if (!res->isConstant() || !res->getConstantValue()) return false; } return true; diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h index e2421bb0..1a633fb5 100644 --- a/include/klee/util/Ref.h +++ b/include/klee/util/Ref.h @@ -10,10 +10,11 @@ #ifndef KLEE_REF_H #define KLEE_REF_H +#include "llvm/Support/Streams.h" + #include -class Expr; -class ConstantExpr; +namespace klee { template class ref { @@ -68,11 +69,6 @@ public: return ptr; } - // method calls for the constant optimization - bool isConstant() const { - return ptr && ptr->getKind() == Expr::Constant; - } - /* The copy assignment operator must also explicitly be defined, * despite a redundant template. */ ref &operator= (const ref &r) { @@ -116,10 +112,12 @@ public: template inline std::ostream &operator<<(std::ostream &os, const ref &e) { - os << *e.get(); + os << *e; return os; } +class Expr; + template U* dyn_ref_cast(ref &src) { return dynamic_cast(src.ptr); @@ -140,4 +138,6 @@ const U* static_ref_cast(const ref &src) { return static_cast(src.ptr); } +} + #endif /* KLEE_REF_H */ diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 9a9a0235..92d75aa8 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -72,7 +72,7 @@ bool AddressSpace::resolveOne(ExecutionState &state, ref address, ObjectPair &result, bool &success) { - if (address.isConstant()) { + if (address->isConstant()) { success = resolveOne(address->getConstantValue(), result); return true; } else { @@ -163,7 +163,7 @@ bool AddressSpace::resolve(ExecutionState &state, ResolutionList &rl, unsigned maxResolutions, double timeout) { - if (p.isConstant()) { + if (p->isConstant()) { ObjectPair res; if (resolveOne(p->getConstantValue(), res)) rl.push_back(res); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index bb4bcb53..a1687f58 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -663,7 +663,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { bool isSeeding = it != seedMap.end(); if (!isSeeding && - !condition.isConstant() && + !condition->isConstant() && (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. || MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) && statsTracker->elapsed() > 60.) { @@ -753,7 +753,7 @@ 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->isConstant()) { if (res->getConstantValue()) { trueSeed = true; } else { @@ -874,7 +874,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { } void Executor::addConstraint(ExecutionState &state, ref condition) { - if (condition.isConstant()) { + if (condition->isConstant()) { assert(condition->getConstantValue() && "attempt to add invalid constraint"); return; @@ -998,7 +998,7 @@ ref Executor::toUnique(const ExecutionState &state, ref &e) { ref result = e; - if (!e.isConstant()) { + if (!e->isConstant()) { ref value(0); bool isTrue = false; @@ -1020,7 +1020,7 @@ ref Executor::toConstant(ExecutionState &state, ref e, const char *reason) { e = state.constraints.simplifyExpr(e); - if (!e.isConstant()) { + if (!e->isConstant()) { ref value; bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); @@ -1049,7 +1049,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() || e->isConstant()) { ref value; bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); @@ -1393,7 +1393,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { BasicBlock *bb = si->getParent(); cond = toUnique(state, cond); - if (cond.isConstant()) { + if (cond->isConstant()) { // Somewhat gross to create these all the time, but fine till we // switch to an internal rep. ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(), @@ -2180,7 +2180,7 @@ void Executor::bindInstructionConstants(KInstruction *KI) { } index++; } - assert(constantOffset.isConstant()); + assert(constantOffset->isConstant()); kgepi->offset = constantOffset->getConstantValue(); } @@ -2346,7 +2346,7 @@ std::string Executor::getAddressInfo(ExecutionState &state, std::ostringstream info; info << "\taddress: " << address << "\n"; uint64_t example; - if (address.isConstant()) { + if (address->isConstant()) { example = address->getConstantValue(); } else { ref value; @@ -2466,7 +2466,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 (value->isConstant()) msg << "=" << value; } msg << ")"; @@ -2521,7 +2521,7 @@ void Executor::callExternalFunction(ExecutionState &state, static_cast(ce.get())->toMemory((void*) &args[i]); } else { ref arg = toUnique(state, *ai); - if (arg.isConstant()) { + if (arg->isConstant()) { // XXX kick toMemory functions from here static_cast(arg.get())->toMemory((void*) &args[i]); } else { @@ -2578,7 +2578,7 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, return e; // right now, we don't replace symbolics (is there any reason too?) - if (!e.isConstant()) + if (!e->isConstant()) return e; if (n != 1 && random() % n) @@ -2620,7 +2620,7 @@ void Executor::executeAlloc(ExecutionState &state, bool zeroMemory, const ObjectState *reallocFrom) { size = toUnique(state, size); - if (size.isConstant()) { + if (size->isConstant()) { MemoryObject *mo = memory->allocate(size->getConstantValue(), isLocal, false, state.prevPC->inst); @@ -2793,9 +2793,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, unsigned bytes = Expr::getMinBytesForWidth(type); if (SimplifySymIndices) { - if (!address.isConstant()) + if (!address->isConstant()) address = state.constraints.simplifyExpr(address); - if (isWrite && !value.isConstant()) + if (isWrite && !value->isConstant()) value = state.constraints.simplifyExpr(value); } @@ -3175,7 +3175,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"); + assert(value->isConstant() && "non-constant passed in place of constant"); if (DebugCheckForImpliedValues) ImpliedValue::checkForImpliedValues(solver->solver, e, value); @@ -3186,7 +3186,7 @@ void Executor::doImpliedValueConcretization(ExecutionState &state, it != ie; ++it) { ReadExpr *re = it->first.get(); - if (re->index.isConstant()) { + if (re->index->isConstant()) { // FIXME: This is the sole remaining usage of the Array object // variable. Kill me. const MemoryObject *mo = re->updates.root->object; diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index c73ae4f1..d1037839 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -53,8 +53,8 @@ static void _getImpliedValue(ref e, // not much to do, could improve with range analysis SelectExpr *se = static_ref_cast(e); - if (se->trueExpr.isConstant()) { - if (se->falseExpr.isConstant()) { + if (se->trueExpr->isConstant()) { + if (se->falseExpr->isConstant()) { if (se->trueExpr->getConstantValue() != se->falseExpr->getConstantValue()) { if (value == se->trueExpr->getConstantValue()) { _getImpliedValue(se->cond, 1, results); @@ -97,7 +97,7 @@ static void _getImpliedValue(ref e, case Expr::Add: { // constants on left BinaryExpr *be = static_ref_cast(e); - if (be->left.isConstant()) { + if (be->left->isConstant()) { uint64_t nvalue = ints::sub(value, be->left->getConstantValue(), be->left->getWidth()); @@ -107,7 +107,7 @@ static void _getImpliedValue(ref e, } case Expr::Sub: { // constants on left BinaryExpr *be = static_ref_cast(e); - if (be->left.isConstant()) { + if (be->left->isConstant()) { uint64_t nvalue = ints::sub(be->left->getConstantValue(), value, be->left->getWidth()); @@ -156,7 +156,7 @@ static void _getImpliedValue(ref e, } case Expr::Xor: { // constants on left BinaryExpr *be = static_ref_cast(e); - if (be->left.isConstant()) { + if (be->left->isConstant()) { _getImpliedValue(be->right, value ^ be->left->getConstantValue(), results); } break; @@ -169,7 +169,7 @@ static void _getImpliedValue(ref e, case Expr::Eq: { EqExpr *ee = static_ref_cast(e); if (value) { - if (ee->left.isConstant()) + if (ee->left->isConstant()) _getImpliedValue(ee->right, ee->left->getConstantValue(), results); } else { // look for limited value range, woohoo @@ -180,7 +180,7 @@ static void _getImpliedValue(ref e, // expression where the true and false branches are single // valued and distinct. - if (ee->left.isConstant()) { + if (ee->left->isConstant()) { if (ee->left->getWidth() == Expr::Bool) { _getImpliedValue(ee->right, !ee->left->getConstantValue(), results); } @@ -197,13 +197,13 @@ static void _getImpliedValue(ref e, void ImpliedValue::getImpliedValues(ref e, ref value, ImpliedValueList &results) { - assert(value.isConstant() && "non-constant in place of constant"); + 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"); + assert(value->isConstant() && "non-constant in place of constant"); std::vector > reads; std::map, ref > found; diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index e03254a5..de48651b 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -301,7 +301,7 @@ ref ObjectState::read8(unsigned offset) const { } ref ObjectState::read8(ref offset) const { - assert(!offset.isConstant() && "constant offset passed to symbolic read8"); + assert(!offset->isConstant() && "constant offset passed to symbolic read8"); unsigned base, size; fastRangeCheckOffset(offset, &base, &size); flushRangeForRead(base, size); @@ -328,7 +328,7 @@ void ObjectState::write8(unsigned offset, uint8_t value) { void ObjectState::write8(unsigned offset, ref value) { // can happen when ExtractExpr special cases - if (value.isConstant()) { + if (value->isConstant()) { write8(offset, (uint8_t) value->getConstantValue()); } else { setKnownSymbolic(offset, value.get()); @@ -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(!offset->isConstant() && "constant offset passed to symbolic write8"); unsigned base, size; fastRangeCheckOffset(offset, &base, &size); flushRangeForWrite(base, size); @@ -358,7 +358,7 @@ void ObjectState::write8(ref offset, ref value) { /***/ ref ObjectState::read(ref offset, Expr::Width width) const { - if (offset.isConstant()) { + if (offset->isConstant()) { return read((unsigned) offset->getConstantValue(), width); } else { switch (width) { @@ -547,7 +547,7 @@ ref ObjectState::read64(ref offset) const { void ObjectState::write(ref offset, ref value) { Expr::Width w = value->getWidth(); - if (offset.isConstant()) { + if (offset->isConstant()) { write(offset->getConstantValue(), value); } else { switch(w) { @@ -563,7 +563,7 @@ void ObjectState::write(ref offset, ref value) { void ObjectState::write(unsigned offset, ref value) { Expr::Width w = value->getWidth(); - if (value.isConstant()) { + if (value->isConstant()) { uint64_t val = value->getConstantValue(); switch(w) { case Expr::Bool: diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index bb6496ac..30377ee4 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -77,7 +77,7 @@ 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()) { + if (re->index->isConstant()) { unsigned index = (unsigned) re->index->getConstantValue(); directReads.insert(std::make_pair(re->updates.root, index)); } diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 594a6518..b2e5d277 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -176,7 +176,7 @@ std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ref address) { ObjectPair op; address = executor.toUnique(state, address); - assert(address.isConstant() && "symbolic string arg to intrinsic"); + assert(address->isConstant() && "symbolic string arg to intrinsic"); if (!state.addressSpace.resolveOne(address->getConstantValue(), op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); bool res; @@ -195,7 +195,7 @@ 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(cur->isConstant() && "hit symbolic char while reading concrete string"); buf[i] = cur->getConstantValue(); } @@ -375,7 +375,7 @@ void SpecialFunctionHandler::handleIsSymbolic(ExecutionState &state, assert(arguments.size()==1 && "invalid number of arguments to klee_is_symbolic"); executor.bindLocal(target, state, - ConstantExpr::create(!arguments[0].isConstant(), Expr::Int32)); + ConstantExpr::create(!arguments[0]->isConstant(), Expr::Int32)); } void SpecialFunctionHandler::handlePreferCex(ExecutionState &state, @@ -414,7 +414,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state, // XXX should type check args assert(arguments.size()==1 && "invalid number of arguments to klee_under_constrained()."); - assert(arguments[0].isConstant() && + assert(arguments[0]->isConstant() && "symbolic argument given to klee_under_constrained!"); unsigned v = arguments[0]->getConstantValue(); @@ -438,7 +438,7 @@ void SpecialFunctionHandler::handleSetForking(ExecutionState &state, "invalid number of arguments to klee_set_forking"); ref value = executor.toUnique(state, arguments[0]); - if (!value.isConstant()) { + if (!value->isConstant()) { executor.terminateStateOnError(state, "klee_set_forking requires a constant arg", "user.err"); @@ -476,7 +476,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 (!arguments[1]->isConstant()) { // FIXME: Pull into a unique value method? ref value; bool success = executor.solver->getValue(state, arguments[1], value); @@ -582,14 +582,15 @@ void SpecialFunctionHandler::handleFree(ExecutionState &state, } void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, - KInstruction *target, - std::vector > &arguments) { + KInstruction *target, + std::vector > + &arguments) { assert(arguments.size()==2 && "invalid number of arguments to klee_check_memory_access"); ref address = executor.toUnique(state, arguments[0]); ref size = executor.toUnique(state, arguments[1]); - if (!address.isConstant() || !size.isConstant()) { + if (!address->isConstant() || !size->isConstant()) { executor.terminateStateOnError(state, "check_memory_access requires constant args", "user.err"); @@ -604,7 +605,7 @@ void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state, } else { ref chk = op.first->getBoundsCheckPointer(address, size->getConstantValue()); - assert(chk.isConstant()); + assert(chk->isConstant()); if (!chk->getConstantValue()) { executor.terminateStateOnError(state, "check_memory_access: memory error", @@ -629,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(arguments[0]->isConstant() && "expect constant address argument to klee_define_fixed_object"); - assert(arguments[1].isConstant() && + assert(arguments[1]->isConstant() && "expect constant size argument to klee_define_fixed_object"); uint64_t address = arguments[0]->getConstantValue(); diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 55fa7c8d..9efb77b8 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -25,7 +25,7 @@ using namespace llvm; bool TimingSolver::evaluate(const ExecutionState& state, ref expr, Solver::Validity &result) { // Fast path, to avoid timer and OS overhead. - if (expr.isConstant()) { + if (expr->isConstant()) { result = expr->getConstantValue() ? Solver::True : Solver::False; return true; } @@ -49,7 +49,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref expr, bool TimingSolver::mustBeTrue(const ExecutionState& state, ref expr, bool &result) { // Fast path, to avoid timer and OS overhead. - if (expr.isConstant()) { + if (expr->isConstant()) { result = expr->getConstantValue() ? true : false; return true; } @@ -96,7 +96,7 @@ bool TimingSolver::mayBeFalse(const ExecutionState& state, ref expr, bool TimingSolver::getValue(const ExecutionState& state, ref expr, ref &result) { // Fast path, to avoid timer and OS overhead. - if (expr.isConstant()) { + if (expr->isConstant()) { result = expr; return true; } diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 472c0aa3..93384060 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -87,7 +87,7 @@ void ConstraintManager::simplifyForValidConstraint(ref e) { } ref ConstraintManager::simplifyExpr(ref e) const { - if (e.isConstant()) + if (e->isConstant()) return e; std::map< ref, ref > equalities; @@ -95,7 +95,7 @@ ref ConstraintManager::simplifyExpr(ref e) const { for (ConstraintManager::constraints_ty::const_iterator it = constraints.begin(), ie = constraints.end(); it != ie; ++it) { if (const EqExpr *ee = dyn_ref_cast(*it)) { - if (ee->left.isConstant()) { + if (ee->left->isConstant()) { equalities.insert(std::make_pair(ee->right, ee->left)); } else { @@ -135,7 +135,7 @@ void ConstraintManager::addConstraintInternal(ref e) { case Expr::Eq: { BinaryExpr *be = static_ref_cast(e); - if (be->left.isConstant()) { + if (be->left->isConstant()) { ExprReplaceVisitor visitor(be->right, be->left); rewriteConstraints(visitor); } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 4c6f5e43..9a78f188 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -378,7 +378,7 @@ ref ReadExpr::create(const UpdateList &ul, ref index) { for (; un; un=un->next) { ref cond = EqExpr::create(index, un->index); - if (cond.isConstant()) { + if (cond->isConstant()) { if (cond->getConstantValue()) return un->value; } else { @@ -399,18 +399,18 @@ ref SelectExpr::create(ref c, ref t, ref f) { assert(c->getWidth()==Bool && "type mismatch"); assert(kt==f->getWidth() && "type mismatch"); - if (c.isConstant()) { + if (c->isConstant()) { return c->getConstantValue() ? t : f; } else if (t==f) { return t; } else if (kt==Expr::Bool) { // c ? t : f <=> (c and t) or (not c and f) - if (t.isConstant()) { + if (t->isConstant()) { if (t->getConstantValue()) { return OrExpr::create(c, f); } else { return AndExpr::create(Expr::createNot(c), f); } - } else if (f.isConstant()) { + } else if (f->isConstant()) { if (f->getConstantValue()) { return OrExpr::create(Expr::createNot(c), t); } else { @@ -485,7 +485,7 @@ ref ExtractExpr::create(ref expr, unsigned off, Width w) { if (w == kw) return expr; - else if (expr.isConstant()) { + else if (expr->isConstant()) { return ConstantExpr::create(ints::trunc(expr->getConstantValue() >> off, w, kw), w); } else @@ -521,7 +521,7 @@ ref ZExtExpr::create(const ref &e, Width w) { } else if (w < kBits) { // trunc return ExtractExpr::createByteOff(e, 0, w); } else { - if (e.isConstant()) { + if (e->isConstant()) { return ConstantExpr::create(ints::zext(e->getConstantValue(), w, kBits), w); } @@ -537,7 +537,7 @@ ref SExtExpr::create(const ref &e, Width w) { } else if (w < kBits) { // trunc return ExtractExpr::createByteOff(e, 0, w); } else { - if (e.isConstant()) { + if (e->isConstant()) { return ConstantExpr::create(ints::sext(e->getConstantValue(), w, kBits), w); } @@ -557,7 +557,7 @@ 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"); + assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -567,10 +567,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 && r->getKid(0)->isConstant()) { // 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 && r->getKid(0)->isConstant()) { // A + (B-c) == (A+B) - c return SubExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); } else { @@ -588,16 +588,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 && l->getKid(0)->isConstant()) { // (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 && l->getKid(0)->isConstant()) { // (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 && r->getKid(0)->isConstant()) { // 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 && r->getKid(0)->isConstant()) { // a + (k-b) = k+(a-b) return AddExpr::create(r->getKid(0), SubExpr::create(l, r->getKid(1))); } else { @@ -607,17 +607,17 @@ 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"); + assert(cl->isConstant() && "non-constant passed in place of constant"); Expr::Width type = cl->getWidth(); if (type==Expr::Bool) { return XorExpr_createPartialR(cl, 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 && r->getKid(0)->isConstant()) { // A - (B+c) == (A-B) - c return SubExpr::create(SubExpr::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 && r->getKid(0)->isConstant()) { // A - (B-c) == (A-B) + c return AddExpr::create(SubExpr::create(cl, r->getKid(0)), r->getKid(1)); } else { @@ -626,7 +626,7 @@ static ref SubExpr_createPartialR(const ref &cl, Expr *r) { } } static ref SubExpr_createPartial(Expr *l, const ref &cr) { - assert(cr.isConstant() && "non-constant passed in place of constant"); + assert(cr->isConstant() && "non-constant passed in place of constant"); uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); uint64_t nvalue = ints::sub(0, value, width); @@ -642,16 +642,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 && l->getKid(0)->isConstant()) { // (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 && l->getKid(0)->isConstant()) { // (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 && r->getKid(0)->isConstant()) { // 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 && r->getKid(0)->isConstant()) { // a - (k-b) = (a+b) - k return SubExpr::create(AddExpr::create(l, r->getKid(1)), r->getKid(0)); } else { @@ -661,7 +661,7 @@ static ref SubExpr_create(Expr *l, Expr *r) { } static ref MulExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl.isConstant() && "non-constant passed in place of constant"); + assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -689,7 +689,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"); + assert(cr->isConstant() && "non-constant passed in place of constant"); uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); @@ -709,7 +709,7 @@ static ref AndExpr_create(Expr *l, Expr *r) { } static ref OrExpr_createPartial(Expr *l, const ref &cr) { - assert(cr.isConstant() && "non-constant passed in place of constant"); + assert(cr->isConstant() && "non-constant passed in place of constant"); uint64_t value = cr->getConstantValue(); Expr::Width width = cr->getWidth(); @@ -729,7 +729,7 @@ static ref OrExpr_create(Expr *l, Expr *r) { } static ref XorExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl.isConstant() && "non-constant passed in place of constant"); + assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width type = cl->getWidth(); @@ -812,8 +812,8 @@ 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()) { \ + if (l->isConstant()) { \ + if (r->isConstant()) { \ Expr::Width width = l->getWidth(); \ uint64_t val = ints::_op(l->getConstantValue(), \ r->getConstantValue(), width); \ @@ -821,7 +821,7 @@ ref _e_op ::create(const ref &l, const ref &r) { \ } else { \ return _e_op ## _createPartialR(l, r.get()); \ } \ - } else if (r.isConstant()) { \ + } else if (r->isConstant()) { \ return _e_op ## _createPartial(l.get(), r); \ } \ return _e_op ## _create(l.get(), r.get()); \ @@ -830,8 +830,8 @@ ref _e_op ::create(const ref &l, const ref &r) { \ #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()) { \ + if (l->isConstant()) { \ + if (r->isConstant()) { \ Expr::Width width = l->getWidth(); \ uint64_t val = ints::_op(l->getConstantValue(), \ r->getConstantValue(), width); \ @@ -858,8 +858,8 @@ 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()) { \ + if (l->isConstant()) { \ + if (r->isConstant()) { \ Expr::Width width = l->getWidth(); \ uint64_t val = ints::_op(l->getConstantValue(), \ r->getConstantValue(), width); \ @@ -872,8 +872,8 @@ ref _e_op ::create(const ref &l, const ref &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()) { \ + if (l->isConstant()) { \ + if (r->isConstant()) { \ Expr::Width width = l->getWidth(); \ uint64_t val = ints::_op(l->getConstantValue(), \ r->getConstantValue(), width); \ @@ -881,7 +881,7 @@ ref _e_op ::create(const ref &l, const ref &r) { \ } else { \ return partialR(l, r.get()); \ } \ - } else if (r.isConstant()) { \ + } else if (r->isConstant()) { \ return partialL(l.get(), r); \ } else { \ return _e_op ## _create(l.get(), r.get()); \ @@ -904,7 +904,7 @@ static ref EqExpr_create(const ref &l, const ref &r) { /// returns the initial equality expression. static ref TryConstArrayOpt(const ref &cl, ReadExpr *rd) { - assert(cl.isConstant() && "constant expression required"); + assert(cl->isConstant() && "constant expression required"); assert(rd->getKind() == Expr::Read && "read expression required"); uint64_t ct = cl->getConstantValue(); @@ -926,7 +926,7 @@ static ref TryConstArrayOpt(const ref &cl, ref idx = un->index; ref val = un->value; - if (!idx.isConstant() || !val.isConstant()) { + if (!idx->isConstant() || !val->isConstant()) { all_const = false; //llvm::cerr << "Idx or val not constant\n"; break; @@ -973,7 +973,7 @@ static ref TryConstArrayOpt(const ref &cl, static ref EqExpr_createPartialR(const ref &cl, Expr *r) { - assert(cl.isConstant() && "non-constant passed in place of constant"); + assert(cl->isConstant() && "non-constant passed in place of constant"); uint64_t value = cl->getConstantValue(); Expr::Width width = cl->getWidth(); @@ -988,7 +988,7 @@ static ref EqExpr_createPartialR(const ref &cl, Expr *r) { const EqExpr *ree = static_ref_cast(r); // eliminate double negation - if (ree->left.isConstant() && + if (ree->left->isConstant() && ree->left->getWidth()==Expr::Bool) { assert(!ree->left->getConstantValue()); return ree->right; @@ -1029,14 +1029,14 @@ static ref EqExpr_createPartialR(const ref &cl, Expr *r) { } } else if (rk==Expr::Add) { const AddExpr *ae = static_ref_cast(r); - if (ae->left.isConstant()) { + if (ae->left->isConstant()) { // c0 = c1 + b => c0 - c1 = b return EqExpr_createPartialR(SubExpr::create(cl, ae->left), ae->right.get()); } } else if (rk==Expr::Sub) { const SubExpr *se = static_ref_cast(r); - if (se->left.isConstant()) { + if (se->left->isConstant()) { // c0 = c1 - b => c1 - c0 = b return EqExpr_createPartialR(SubExpr::create(se->left, cl), se->right.get()); @@ -1076,7 +1076,7 @@ static ref UltExpr_create(const ref &l, const ref &r) { if (t == Expr::Bool) { // !l && r return AndExpr::create(Expr::createNot(l), r); } else { - if (r.isConstant()) { + if (r->isConstant()) { uint64_t value = r->getConstantValue(); if (value <= 8) { ref res = ConstantExpr::alloc(0, Expr::Bool); diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp index 0c04a538..038fe8b8 100644 --- a/lib/Expr/ExprEvaluator.cpp +++ b/lib/Expr/ExprEvaluator.cpp @@ -16,7 +16,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul, for (const UpdateNode *un=ul.head; un; un=un->next) { ref ui = visit(un->index); - if (ui.isConstant()) { + if (ui->isConstant()) { if (ui->getConstantValue() == index) return Action::changeTo(visit(un->value)); } else { @@ -36,7 +36,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul, ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) { ref v = visit(re.index); - if (v.isConstant()) { + if (v->isConstant()) { return evalRead(re.updates, v->getConstantValue()); } else { return Action::doChildren(); @@ -50,7 +50,7 @@ ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) { ref kids[2] = { visit(e.left), visit(e.right) }; - if (kids[1].isConstant() && !kids[1]->getConstantValue()) + if (kids[1]->isConstant() && !kids[1]->getConstantValue()) kids[1] = e.right; if (kids[0]!=e.left || kids[1]!=e.right) { diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 08809684..da4f45f9 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 e->isConstant() || 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 (!e->isConstant()) { if (couldPrint.insert(e).second) { Expr *ep = e.get(); for (unsigned i=0; igetNumKids(); i++) @@ -208,7 +208,7 @@ class PPrinter : public ExprPPrinter { print(un->value, PC); //PC << ')'; - nextShouldBreak = !(un->index.isConstant() && un->value.isConstant()); + nextShouldBreak = !(un->index->isConstant() && un->value->isConstant()); } if (openedList) @@ -324,7 +324,7 @@ public: } void printConst(const ref &e, PrintContext &PC, bool printWidth) { - assert(e.isConstant()); + assert(e->isConstant()); if (e->getWidth() == Expr::Bool) PC << (e->getConstantValue() ? "true" : "false"); @@ -343,7 +343,7 @@ public: } void print(const ref &e, PrintContext &PC, bool printConstWidth=false) { - if (e.isConstant()) + if (e->isConstant()) printConst(e, PC, printConstWidth); else { std::map, unsigned>::iterator it = bindings.find(e); diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index f74b519f..192c18a5 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 (!e->isConstant()) { 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 (!re->index->isConstant() && 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 (!un->index->isConstant() && visited.insert(un->index).second) stack.push_back(un->index); - if (!un->value.isConstant() && + if (!un->value->isConstant() && visited.insert(un->value).second) stack.push_back(un->value); } } } - } else if (!top.isConstant()) { + } else if (!top->isConstant()) { Expr *e = top.get(); for (unsigned i=0; igetNumKids(); i++) { ref k = e->getKid(i); - if (!k.isConstant() && + if (!k->isConstant() && visited.insert(k).second) stack.push_back(k); } diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index b15cdffa..5e9d0a81 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 || e->isConstant()) { 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 (e->isConstant()) { 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 (!e->isConstant()) { 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 70c1cc76..5f666269 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -929,7 +929,7 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name, if (!OffsetExpr.isValid() || !Child.isValid()) return ConstantExpr::alloc(0, ResTy); - assert(OffsetExpr.get().isConstant() && "ParseNumber returned non-constant."); + assert(OffsetExpr.get()->isConstant() && "ParseNumber returned non-constant."); unsigned Offset = (unsigned) OffsetExpr.get()->getConstantValue(); if (Offset + ResTy > Child.get()->getWidth()) { diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index db15632b..546d81fd 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -138,7 +138,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query, Assignment *&result) { KeyType key(query.constraints.begin(), query.constraints.end()); ref neg = Expr::createNot(query.expr); - if (neg.isConstant()) { + if (neg->isConstant()) { if (!neg->getConstantValue()) { result = (Assignment*) 0; return true; @@ -153,7 +153,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query, bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) { KeyType key(query.constraints.begin(), query.constraints.end()); ref neg = Expr::createNot(query.expr); - if (neg.isConstant()) { + if (neg->isConstant()) { if (!neg->getConstantValue()) { result = (Assignment*) 0; return true; @@ -217,7 +217,7 @@ 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(q->isConstant() && "assignment evaluation did not result in constant"); if (q->getConstantValue()) { if (!getAssignment(query, a)) @@ -268,7 +268,7 @@ bool CexCachingSolver::computeValue(const Query& query, return false; assert(a && "computeValue() must have assignment"); result = a->evaluate(query.expr); - assert(result.isConstant() && + assert(result->isConstant() && "assignment evaluation did not result in constant"); return true; } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 88f34c99..ee46be4f 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -416,7 +416,7 @@ public: // XXX we need to respect the version here and object state chain - if (re->index.isConstant() && + if (re->index->isConstant() && re->index->getConstantValue() < array->size) { CexValueData &cvd = cod.values[re->index->getConstantValue()]; CexValueData tmp = cvd.set_intersection(range); @@ -613,7 +613,7 @@ public: case Expr::Eq: { BinaryExpr *be = static_ref_cast(e); if (range.isFixed()) { - if (be->left.isConstant()) { + if (be->left->isConstant()) { uint64_t value = be->left->getConstantValue(); if (range.min()) { forceExprToValue(be->right, value); @@ -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 (!v->isConstant()) 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 (value->isConstant()) { result = value; return true; } else { @@ -939,7 +939,7 @@ FastCexSolver::computeInitialValues(const Query& query, ConstantExpr::create(i, kMachinePointerType))); - if (value.isConstant()) { + if (value->isConstant()) { data.push_back(value->getConstantValue()); } else { // FIXME: When does this happen? diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 18e5c84d..4e004fd8 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -97,7 +97,7 @@ public: if (re->updates.isRooted) { const Array *array = re->updates.root; if (!wholeObjects.count(array)) { - if (re->index.isConstant()) { + if (re->index->isConstant()) { DenseSet &dis = elements[array]; dis.add((unsigned) re->index->getConstantValue()); } else { diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 1d27c655..d1f7360c 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 || e->isConstant()) { return constructActual(e, width_out); } else { ExprHashMap< std::pair >::iterator it = @@ -555,7 +555,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle right = construct(me->right, width_out); assert(*width_out!=1 && "uncanonicalized mul"); - if (me->left.isConstant()) { + if (me->left->isConstant()) { return constructMulByConstant(right, *width_out, me->left->getConstantValue()); } else { @@ -569,7 +569,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(de->left, width_out); assert(*width_out!=1 && "uncanonicalized udiv"); - if (de->right.isConstant()) { + if (de->right->isConstant()) { uint64_t divisor = de->right->getConstantValue(); if (bits64::isPowerOfTwo(divisor)) { @@ -591,7 +591,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(de->left, width_out); assert(*width_out!=1 && "uncanonicalized sdiv"); - if (de->right.isConstant()) { + if (de->right->isConstant()) { uint64_t divisor = de->right->getConstantValue(); if (optimizeDivides) { @@ -611,7 +611,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(de->left, width_out); assert(*width_out!=1 && "uncanonicalized urem"); - if (de->right.isConstant()) { + if (de->right->isConstant()) { uint64_t divisor = de->right->getConstantValue(); if (bits64::isPowerOfTwo(divisor)) { @@ -710,7 +710,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(se->left, width_out); assert(*width_out!=1 && "uncanonicalized shl"); - if (se->right.isConstant()) { + if (se->right->isConstant()) { return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out)); } else { int shiftWidth; @@ -725,7 +725,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { unsigned shiftBits = getShiftBits(*width_out); assert(*width_out!=1 && "uncanonicalized lshr"); - if (lse->right.isConstant()) { + if (lse->right->isConstant()) { return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits); } else { int shiftWidth; @@ -739,7 +739,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(ase->left, width_out); assert(*width_out!=1 && "uncanonicalized ashr"); - if (ase->right.isConstant()) { + if (ase->right->isConstant()) { unsigned shift = (unsigned) ase->right->getConstantValue(); ExprHandle signedBool = bvBoolExtract(left, *width_out-1); return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out)); @@ -757,7 +757,7 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ExprHandle left = construct(ee->left, width_out); ExprHandle right = construct(ee->right, width_out); if (*width_out==1) { - if (ee->left.isConstant()) { + if (ee->left->isConstant()) { assert(!ee->left->getConstantValue() && "uncanonicalized eq"); return vc_notExpr(vc, right); } else { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 8990e3b9..46d6039e 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -56,7 +56,7 @@ bool Solver::evaluate(const Query& query, Validity &result) { assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); // Maintain invariants implementations expect. - if (query.expr.isConstant()) { + if (query.expr->isConstant()) { result = query.expr->getConstantValue() ? True : False; return true; } @@ -82,7 +82,7 @@ bool Solver::mustBeTrue(const Query& query, bool &result) { assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); // Maintain invariants implementations expect. - if (query.expr.isConstant()) { + if (query.expr->isConstant()) { result = query.expr->getConstantValue() ? true : false; return true; } @@ -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 (query.expr->isConstant()) { result = query.expr; return true; } @@ -151,7 +151,7 @@ std::pair< ref, ref > Solver::getRange(const Query& query) { default: min = 0, max = 1; break; } - } else if (e.isConstant()) { + } else if (e->isConstant()) { min = max = e->getConstantValue(); } else { // binary search for # of useful bits -- cgit 1.4.1