diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/FastCexSolver.cpp | 148 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 2 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 2 |
3 files changed, 77 insertions, 75 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index a45a8f17..382774ce 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -440,17 +440,16 @@ public: return *Entry; } - void propogatePossibleValue(ref<Expr> e, uint64_t value) { - propogatePossibleValues(e, CexValueData(value,value)); + void propagatePossibleValue(ref<Expr> e, uint64_t value) { + propagatePossibleValues(e, CexValueData(value, value)); } - void propogateExactValue(ref<Expr> e, uint64_t value) { - propogateExactValues(e, CexValueData(value,value)); + void propagateExactValue(ref<Expr> e, uint64_t value) { + propagateExactValues(e, CexValueData(value, value)); } - void propogatePossibleValues(ref<Expr> e, CexValueData range) { - KLEE_DEBUG(llvm::errs() << "propogate: " << range << " for\n" - << e << "\n"); + void propagatePossibleValues(ref<Expr> e, CexValueData range) { + KLEE_DEBUG(llvm::errs() << "propagate: " << range << " for\n" << e << "\n"); switch (e->getKind()) { case Expr::Constant: @@ -496,9 +495,9 @@ public: ValueRange cond = evalRangeForExpr(se->cond); if (cond.isFixed()) { if (cond.min()) { - propogatePossibleValues(se->trueExpr, range); + propagatePossibleValues(se->trueExpr, range); } else { - propogatePossibleValues(se->falseExpr, range); + propagatePossibleValues(se->falseExpr, range); } } else { // XXX imprecise... we have a choice here. One method is to @@ -523,8 +522,8 @@ public: // one of the ranges happens to already be a subset of the // required range then it may be preferable to force the // condition to that side. - propogatePossibleValues(se->trueExpr, range); - propogatePossibleValues(se->falseExpr, range); + propagatePossibleValues(se->trueExpr, range); + propagatePossibleValues(se->falseExpr, range); } break; } @@ -542,9 +541,9 @@ public: ConcatExpr *ce = cast<ConcatExpr>(e); Expr::Width LSBWidth = ce->getKid(1)->getWidth(); Expr::Width MSBWidth = ce->getKid(1)->getWidth(); - propogatePossibleValues(ce->getKid(0), + propagatePossibleValues(ce->getKid(0), range.extract(LSBWidth, LSBWidth + MSBWidth)); - propogatePossibleValues(ce->getKid(1), range.extract(0, LSBWidth)); + propagatePossibleValues(ce->getKid(1), range.extract(0, LSBWidth)); break; } @@ -565,7 +564,7 @@ public: unsigned inBits = ce->src->getWidth(); ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits))); - propogatePossibleValues(ce->src, input); + propagatePossibleValues(ce->src, input); break; } // For SExt instead of doing the intersection we just take the output @@ -580,7 +579,7 @@ public: (bits64::maxValueOfNBits(outBits) - bits64::maxValueOfNBits(inBits-1)-1))); ValueRange input = output.binaryAnd(bits64::maxValueOfNBits(inBits)); - propogatePossibleValues(ce->src, input); + propagatePossibleValues(ce->src, input); break; } @@ -591,7 +590,7 @@ public: if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) { // FIXME: Don't depend on width. if (CE->getWidth() <= 64) { - // FIXME: Why do we ever propogate empty ranges? It doesn't make + // FIXME: Why do we ever propagate empty ranges? It doesn't make // sense. if (range.isEmpty()) break; @@ -601,7 +600,7 @@ public: CexValueData nrange(ConstantExpr::alloc(range.min(), W)->Sub(CE)->getZExtValue(), ConstantExpr::alloc(range.max(), W)->Sub(CE)->getZExtValue()); if (!nrange.isEmpty()) - propogatePossibleValues(be->right, nrange); + propagatePossibleValues(be->right, nrange); } } break; @@ -620,16 +619,18 @@ public: } else { // XXX heuristic, which order - propogatePossibleValue(be->left, 0); + propagatePossibleValue(be->left, 0); left = evalRangeForExpr(be->left); // see if that worked if (!left.mustEqual(1)) - propogatePossibleValue(be->right, 0); + propagatePossibleValue(be->right, 0); } } else { - if (!left.mustEqual(1)) propogatePossibleValue(be->left, 1); - if (!right.mustEqual(1)) propogatePossibleValue(be->right, 1); + if (!left.mustEqual(1)) + propagatePossibleValue(be->left, 1); + if (!right.mustEqual(1)) + propagatePossibleValue(be->right, 1); } } } else { @@ -652,16 +653,18 @@ public: // XXX heuristic, which order? // force left to value we need - propogatePossibleValue(be->left, 1); + propagatePossibleValue(be->left, 1); left = evalRangeForExpr(be->left); // see if that worked if (!left.mustEqual(1)) - propogatePossibleValue(be->right, 1); + propagatePossibleValue(be->right, 1); } } else { - if (!left.mustEqual(0)) propogatePossibleValue(be->left, 0); - if (!right.mustEqual(0)) propogatePossibleValue(be->right, 0); + if (!left.mustEqual(0)) + propagatePossibleValue(be->left, 0); + if (!right.mustEqual(0)) + propagatePossibleValue(be->right, 0); } } } else { @@ -682,7 +685,7 @@ public: if (CE->getWidth() <= 64) { uint64_t value = CE->getZExtValue(); if (range.min()) { - propogatePossibleValue(be->right, value); + propagatePossibleValue(be->right, value); } else { CexValueData range; if (value==0) { @@ -693,7 +696,7 @@ public: // range? range = CexValueData(0, value - 1); } - propogatePossibleValues(be->right, range); + propagatePossibleValues(be->right, range); } } else { // XXX what now @@ -705,7 +708,7 @@ public: case Expr::Not: { if (e->getWidth() == Expr::Bool && range.isFixed()) { - propogatePossibleValue(e->getKid(0), !range.min()); + propagatePossibleValue(e->getKid(0), !range.min()); } break; } @@ -725,17 +728,17 @@ public: if (left.isFixed()) { if (range.min()) { - propogatePossibleValues(be->right, CexValueData(left.min()+1, - maxValue)); + propagatePossibleValues(be->right, + CexValueData(left.min() + 1, maxValue)); } else { - propogatePossibleValues(be->right, CexValueData(0, left.min())); + propagatePossibleValues(be->right, CexValueData(0, left.min())); } } else if (right.isFixed()) { if (range.min()) { - propogatePossibleValues(be->left, CexValueData(0, right.min()-1)); + propagatePossibleValues(be->left, CexValueData(0, right.min() - 1)); } else { - propogatePossibleValues(be->left, CexValueData(right.min(), - maxValue)); + propagatePossibleValues(be->left, + CexValueData(right.min(), maxValue)); } } else { // XXX ??? @@ -757,17 +760,17 @@ public: uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth()); if (left.isFixed()) { if (range.min()) { - propogatePossibleValues(be->right, CexValueData(left.min(), - maxValue)); + propagatePossibleValues(be->right, + CexValueData(left.min(), maxValue)); } else { - propogatePossibleValues(be->right, CexValueData(0, left.min()-1)); + propagatePossibleValues(be->right, CexValueData(0, left.min() - 1)); } } else if (right.isFixed()) { if (range.min()) { - propogatePossibleValues(be->left, CexValueData(0, right.min())); + propagatePossibleValues(be->left, CexValueData(0, right.min())); } else { - propogatePossibleValues(be->left, CexValueData(right.min()+1, - maxValue)); + propagatePossibleValues(be->left, + CexValueData(right.min() + 1, maxValue)); } } else { // XXX ??? @@ -788,7 +791,7 @@ public: } } - void propogateExactValues(ref<Expr> e, CexValueData range) { + void propagateExactValues(ref<Expr> e, CexValueData range) { switch (e->getKind()) { case Expr::Constant: { // FIXME: Assert that range contains this constant. @@ -808,13 +811,13 @@ public: for (const auto *un = re->updates.head.get(); un; un = un->next.get()) { CexValueData ui = evalRangeForExpr(un->index); - // If these indices can't alias, continue propogation + // If these indices can't alias, continue propagation if (!ui.mayEqual(index)) continue; - // Otherwise if we know they alias, propogate into the write value. + // Otherwise if we know they alias, propagate into the write value. if (ui.mustEqual(index) || re->index == un->index) - propogateExactValues(un->value, range); + propagateExactValues(un->value, range); return; } @@ -822,8 +825,7 @@ public: if (index.isFixed()) { if (array->isConstantArray()) { // Verify the range. - propogateExactValues(array->constantValues[index.min()], - range); + propagateExactValues(array->constantValues[index.min()], range); } else { CexValueData cvd = cod.getExactValues(index.min()); if (range.min() > cvd.min()) { @@ -886,13 +888,13 @@ public: if (CE->getWidth() <= 64) { uint64_t value = CE->getZExtValue(); if (range.min()) { - // If the equality is true, then propogate the value. - propogateExactValue(be->right, value); + // If the equality is true, then propagate the value. + propagateExactValue(be->right, value); } else { // If the equality is false and the comparison is of booleans, - // then we can infer the value to propogate. + // then we can infer the value to propagate. if (be->right->getWidth() == Expr::Bool) - propogateExactValue(be->right, !value); + propagateExactValue(be->right, !value); } } } @@ -903,7 +905,7 @@ public: // If a boolean not, and the result is known, propagate it case Expr::Not: { if (e->getWidth() == Expr::Bool && range.isFixed()) { - propogateExactValue(e->getKid(0), !range.min()); + propagateExactValue(e->getKid(0), !range.min()); } break; } @@ -944,7 +946,7 @@ public: } void dump() { - llvm::errs() << "-- propogated values --\n"; + llvm::errs() << "-- propagated values --\n"; for (std::map<const Array *, CexObjectData *>::iterator it = objects.begin(), ie = objects.end(); @@ -991,29 +993,29 @@ FastCexSolver::FastCexSolver() { } FastCexSolver::~FastCexSolver() { } -/// propogateValues - Propogate value ranges for the given query and return the -/// propogation results. +/// propagateValues - propagate value ranges for the given query and return the +/// propagation results. /// -/// \param query - The query to propogate values for. +/// \param query - The query to propagate values for. /// -/// \param cd - The initial object values resulting from the propogation. +/// \param cd - The initial object values resulting from the propagation. /// /// \param checkExpr - Include the query expression in the constraints to -/// propogate. +/// propagate. /// -/// \param isValid - If the propogation succeeds (returns true), whether the +/// \param isValid - If the propagation succeeds (returns true), whether the /// constraints were proven valid or invalid. /// -/// \return - True if the propogation was able to prove validity or invalidity. -static bool propogateValues(const Query& query, CexData &cd, - bool checkExpr, bool &isValid) { +/// \return - True if the propagation was able to prove validity or invalidity. +static bool propagateValues(const Query &query, CexData &cd, bool checkExpr, + bool &isValid) { for (const auto &constraint : query.constraints) { - cd.propogatePossibleValue(constraint, 1); - cd.propogateExactValue(constraint, 1); + cd.propagatePossibleValue(constraint, 1); + cd.propagateExactValue(constraint, 1); } if (checkExpr) { - cd.propogatePossibleValue(query.expr, 0); - cd.propogateExactValue(query.expr, 0); + cd.propagatePossibleValue(query.expr, 0); + cd.propagateExactValue(query.expr, 0); } KLEE_DEBUG(cd.dump()); @@ -1056,7 +1058,7 @@ FastCexSolver::computeTruth(const Query& query) { CexData cd; bool isValid; - bool success = propogateValues(query, cd, true, isValid); + bool success = propagateValues(query, cd, true, isValid); if (!success) return IncompleteSolver::None; @@ -1068,17 +1070,17 @@ bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) { CexData cd; bool isValid; - bool success = propogateValues(query, cd, false, isValid); + bool success = propagateValues(query, cd, false, isValid); - // Check if propogation wasn't able to determine anything. + // Check if propagation wasn't able to determine anything. if (!success) return false; // FIXME: We don't have a way to communicate valid constraints back. if (isValid) return false; - - // Propogation found a satisfying assignment, evaluate the expression. + + // propagation found a satisfying assignment, evaluate the expression. ref<Expr> value = cd.evaluatePossible(query.expr); if (isa<ConstantExpr>(value)) { @@ -1100,9 +1102,9 @@ FastCexSolver::computeInitialValues(const Query& query, CexData cd; bool isValid; - bool success = propogateValues(query, cd, true, isValid); + bool success = propagateValues(query, cd, true, isValid); - // Check if propogation wasn't able to determine anything. + // Check if propagation wasn't able to determine anything. if (!success) return false; @@ -1110,7 +1112,7 @@ FastCexSolver::computeInitialValues(const Query& query, if (!hasSolution) return true; - // Propogation found a satisfying assignment, compute the initial values. + // propagation found a satisfying assignment, compute the initial values. for (unsigned i = 0; i != objects.size(); ++i) { const Array *array = objects[i]; assert(array); diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index ed36816c..812aefb6 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -442,7 +442,7 @@ bool assertCreatedPointEvaluatesToTrue( std::vector<std::vector<unsigned char>> &values, std::map<const Array *, std::vector<unsigned char>> &retMap) { // _allowFreeValues is set to true so that if there are missing bytes in the - // assigment we will end up with a non ConstantExpr after evaluating the + // assignment we will end up with a non ConstantExpr after evaluating the // assignment and fail Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 12cfb180..5fe973fe 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -101,7 +101,7 @@ Solver::getInitialValues(const Query& query, bool hasSolution; bool success = impl->computeInitialValues(query, objects, values, hasSolution); - // FIXME: Propogate this out. + // FIXME: Propagate this out. if (!hasSolution) return false; |