diff options
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 22 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 2 | ||||
-rw-r--r-- | lib/Solver/STPBuilder.cpp | 24 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 16 |
6 files changed, 37 insertions, 37 deletions
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 517e133b..d353e485 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -49,11 +49,11 @@ private: struct CacheEntryHash { unsigned operator()(const CacheEntry &ce) const { - unsigned result = ce.query.hash(); + unsigned result = ce.query->hash(); for (ConstraintManager::constraint_iterator it = ce.constraints.begin(); it != ce.constraints.end(); ++it) - result ^= it->hash(); + result ^= (*it)->hash(); return result; } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 79bc985d..db15632b 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -139,7 +139,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query, KeyType key(query.constraints.begin(), query.constraints.end()); ref<Expr> neg = Expr::createNot(query.expr); if (neg.isConstant()) { - if (!neg.getConstantValue()) { + if (!neg->getConstantValue()) { result = (Assignment*) 0; return true; } @@ -154,7 +154,7 @@ bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) { KeyType key(query.constraints.begin(), query.constraints.end()); ref<Expr> neg = Expr::createNot(query.expr); if (neg.isConstant()) { - if (!neg.getConstantValue()) { + if (!neg->getConstantValue()) { result = (Assignment*) 0; return true; } @@ -219,7 +219,7 @@ bool CexCachingSolver::computeValidity(const Query& query, ref<Expr> q = a->evaluate(query.expr); assert(q.isConstant() && "assignment evaluation did not result in constant"); - if (q.getConstantValue()) { + if (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 b6f676aa..88f34c99 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -398,7 +398,7 @@ public: #ifdef LOG // *theLog << "force: " << e << " to " << range << "\n"; #endif - switch (e.getKind()) { + switch (e->getKind()) { case Expr::Constant: { // rather a pity if the constant isn't in the range, but how can // we use this? @@ -417,8 +417,8 @@ public: // XXX we need to respect the version here and object state chain if (re->index.isConstant() && - re->index.getConstantValue() < array->size) { - CexValueData &cvd = cod.values[re->index.getConstantValue()]; + re->index->getConstantValue() < array->size) { + CexValueData &cvd = cod.values[re->index->getConstantValue()]; CexValueData tmp = cvd.set_intersection(range); if (tmp.isEmpty()) { @@ -522,7 +522,7 @@ public: // possible input range. case Expr::ZExt: { CastExpr *ce = static_ref_cast<CastExpr>(e); - unsigned inBits = ce->src.getWidth(); + unsigned inBits = ce->src->getWidth(); ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits))); forceExprToRange(ce->src, input); break; @@ -531,7 +531,7 @@ public: // minus the impossible values. This is nicer since it is a single interval. case Expr::SExt: { CastExpr *ce = static_ref_cast<CastExpr>(e); - unsigned inBits = ce->src.getWidth(); + unsigned inBits = ce->src->getWidth(); unsigned outBits = ce->width; ValueRange output = range.set_difference(ValueRange(1<<(inBits-1), (bits64::maxValueOfNBits(outBits)- @@ -614,7 +614,7 @@ public: BinaryExpr *be = static_ref_cast<BinaryExpr>(e); if (range.isFixed()) { if (be->left.isConstant()) { - uint64_t value = be->left.getConstantValue(); + uint64_t value = be->left->getConstantValue(); if (range.min()) { forceExprToValue(be->right, value); } else { @@ -622,7 +622,7 @@ public: forceExprToRange(be->right, CexValueData(1, ints::sext(1, - be->right.getWidth(), + be->right->getWidth(), 1))); } else { // XXX heuristic / lossy, could be better to pick larger range? @@ -645,7 +645,7 @@ public: ValueRange left = evalRangeForExpr(be->left); ValueRange right = evalRangeForExpr(be->right); - uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth()); + uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth()); // XXX should deal with overflow (can lead to empty range) @@ -678,7 +678,7 @@ public: // XXX should deal with overflow (can lead to empty range) - uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth()); + uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth()); if (left.isFixed()) { if (range.min()) { forceExprToRange(be->right, CexValueData(left.min(), maxValue)); @@ -732,7 +732,7 @@ public: 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; + return v->getConstantValue() == value; } }; @@ -940,7 +940,7 @@ FastCexSolver::computeInitialValues(const Query& query, kMachinePointerType))); if (value.isConstant()) { - data.push_back(value.getConstantValue()); + data.push_back(value->getConstantValue()); } else { // FIXME: When does this happen? return false; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index c966aff6..18e5c84d 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -99,7 +99,7 @@ public: if (!wholeObjects.count(array)) { if (re->index.isConstant()) { DenseSet<unsigned> &dis = elements[array]; - dis.add((unsigned) re->index.getConstantValue()); + dis.add((unsigned) re->index->getConstantValue()); } else { elements_ty::iterator it2 = elements.find(array); if (it2!=elements.end()) diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index a1b6e99a..1d27c655 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -447,11 +447,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { ++stats::queryConstructs; - switch(e.getKind()) { - + switch (e->getKind()) { case Expr::Constant: { - uint64_t asUInt64 = e.getConstantValue(); - *width_out = e.getWidth(); + uint64_t asUInt64 = e->getConstantValue(); + *width_out = e->getWidth(); if (*width_out > 64) assert(0 && "constructActual: width > 64"); @@ -557,7 +556,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized mul"); if (me->left.isConstant()) { - return constructMulByConstant(right, *width_out, me->left.getConstantValue()); + return constructMulByConstant(right, *width_out, + me->left->getConstantValue()); } else { ExprHandle left = construct(me->left, width_out); return vc_bvMultExpr(vc, *width_out, left, right); @@ -570,7 +570,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized udiv"); if (de->right.isConstant()) { - uint64_t divisor = de->right.getConstantValue(); + uint64_t divisor = de->right->getConstantValue(); if (bits64::isPowerOfTwo(divisor)) { return bvRightShift(left, @@ -592,7 +592,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized sdiv"); if (de->right.isConstant()) { - uint64_t divisor = de->right.getConstantValue(); + uint64_t divisor = de->right->getConstantValue(); if (optimizeDivides) { if (*width_out == 32) //only works for 32-bit division @@ -612,7 +612,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized urem"); if (de->right.isConstant()) { - uint64_t divisor = de->right.getConstantValue(); + uint64_t divisor = de->right->getConstantValue(); if (bits64::isPowerOfTwo(divisor)) { unsigned bits = bits64::indexOfSingleBit(divisor); @@ -711,7 +711,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized shl"); if (se->right.isConstant()) { - return bvLeftShift(left, se->right.getConstantValue(), getShiftBits(*width_out)); + return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out)); } else { int shiftWidth; ExprHandle amount = construct(se->right, &shiftWidth); @@ -726,7 +726,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized lshr"); if (lse->right.isConstant()) { - return bvRightShift(left, (unsigned) lse->right.getConstantValue(), shiftBits); + return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits); } else { int shiftWidth; ExprHandle amount = construct(lse->right, &shiftWidth); @@ -740,7 +740,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { assert(*width_out!=1 && "uncanonicalized ashr"); if (ase->right.isConstant()) { - unsigned shift = (unsigned) ase->right.getConstantValue(); + unsigned shift = (unsigned) ase->right->getConstantValue(); ExprHandle signedBool = bvBoolExtract(left, *width_out-1); return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out)); } else { @@ -758,7 +758,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) { ExprHandle right = construct(ee->right, width_out); if (*width_out==1) { if (ee->left.isConstant()) { - assert(!ee->left.getConstantValue() && "uncanonicalized eq"); + assert(!ee->left->getConstantValue() && "uncanonicalized eq"); return vc_notExpr(vc, right); } else { return vc_iffExpr(vc, left, right); diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index ae378ac1..8990e3b9 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -53,11 +53,11 @@ SolverImpl::~SolverImpl() { } bool Solver::evaluate(const Query& query, Validity &result) { - assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!"); + assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); - // Maintain invariants implementation expect. + // Maintain invariants implementations expect. if (query.expr.isConstant()) { - result = query.expr.getConstantValue() ? True : False; + result = query.expr->getConstantValue() ? True : False; return true; } @@ -79,11 +79,11 @@ bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) { } bool Solver::mustBeTrue(const Query& query, bool &result) { - assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!"); + assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); - // Maintain invariants implementation expect. + // Maintain invariants implementations expect. if (query.expr.isConstant()) { - result = query.expr.getConstantValue() ? true : false; + result = query.expr->getConstantValue() ? true : false; return true; } @@ -136,7 +136,7 @@ Solver::getInitialValues(const Query& query, std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) { ref<Expr> e = query.expr; - Expr::Width width = e.getWidth(); + Expr::Width width = e->getWidth(); uint64_t min, max; if (width==1) { @@ -152,7 +152,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) { min = 0, max = 1; break; } } else if (e.isConstant()) { - min = max = e.getConstantValue(); + min = max = e->getConstantValue(); } else { // binary search for # of useful bits uint64_t lo=0, hi=width, mid, bits=0; |