From a6e21a84f3ffa0bfb2031db2abf7e584bc07649f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 22 Mar 2016 09:55:53 +0000 Subject: Try to fix #348 The problem was that ``assertCreatedPointEvaluatesToTrue()`` used in the IndependentSolver assumed that it would be given an assignment for every array. If this wasn't the case the ``Assignment`` object by default would just replace every read of an unknown array with a byte filled with zeros. This problem would appear if ``IndependentSolver::getInitialValues(...)`` was called without asking for assignment for used arrays. I saw two ways of fixing this * Get an assignment for all arrays even if the client didn't ask for them. This guarantees that is the query is satisfiable then we can compute a concrete assignment. * Just do a "best effort" check and only check expressions that can be fully assigned to. I chose the latter because the first option seems pretty wasteful, especially for an assert. The second option isn't ideal though as it would be possible to compute an assignment that for the whole query leads to "unsat" but we wouldn't notice. --- lib/Solver/IndependentSolver.cpp | 54 ++++++++++++++++++++++++++++++++++------ 1 file changed, 47 insertions(+), 7 deletions(-) (limited to 'lib/Solver/IndependentSolver.cpp') diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 78126ede..84e7adb6 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -438,25 +438,65 @@ bool IndependentSolver::computeValue(const Query& query, ref &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } +bool canPerformConcreteAssignment(const std::vector &objects, const ref e) { + // Get the arrays used in the constraint. If an array isn't in objects we + // don't have an assignment for it so skip it because can't evaluate to a + // constant. This means we might not be checking every constraint which is + // not ideal but the alternative would require getting an assignment for + // all arrays which is wasteful given that the client didn't ask for them + IndependentElementSet ieSet(e); + for (std::vector::const_iterator ai = objects.begin(), + ae = objects.end(); + ai != ae; ++ai) { + ieSet.wholeObjects.erase(*ai); + ieSet.elements.erase(*ai); + } + + if (ieSet.wholeObjects.size() > 0 || ieSet.elements.size() > 0) { + // There are arrays used in ``e`` that aren't in objects, + // therefore we can't perform a complete assignment + return false; + } + return true; +} // Helper function used only for assertions to make sure point created -// during computeInitialValues is in fact correct. +// during computeInitialValues is in fact correct. This function is +// a "best effort" check because if the query uses an Array that an +// assignment is not given for then that Query cannot be fully evaluated so +// this function only checks that all expressions that can be fully +// assigned to evaluate to true. bool assertCreatedPointEvaluatesToTrue(const Query &query, const std::vector &objects, std::vector< std::vector > &values){ - Assignment assign = Assignment(objects, values); + // _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 and fail + Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); for(ConstraintManager::constraint_iterator it = query.constraints.begin(); it != query.constraints.end(); ++it){ + ref constraint = *it; + + if (!canPerformConcreteAssignment(objects, constraint)) { + // We have to skip checking assigning to this constraint + continue; + } + ref ret = assign.evaluate(*it); - if(! isa(ret) || ! cast(ret)->isTrue()){ + + assert(isa(ret) && "Could not use assignment to evaluate constraint"); + ref evaluatedConstraint = dyn_cast(ret); + if(evaluatedConstraint->isFalse()){ return false; } } ref neg = Expr::createIsZero(query.expr); - ref q = assign.evaluate(neg); - - assert(isa(q) && "assignment evaluation did not result in constant"); - return cast(q)->isTrue(); + if (canPerformConcreteAssignment(objects, neg)) { + ref q = assign.evaluate(neg); + assert(isa(q) && "assignment evaluation did not result in constant"); + return cast(q)->isTrue(); + } + // Can't assign to query expression + return true; } bool IndependentSolver::computeInitialValues(const Query& query, -- cgit 1.4.1 From 8dd640c8a0fd19047f7a30d3952e12dbac0311f7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 22 Mar 2016 18:27:14 +0000 Subject: Properly assert that an assignment computed in ``IndependentSolver::computeInitialValues(...)`` satisfies the whole query. The previous commit only checked expressions evaluated to true where there was an assignment for ``Array`` objects that the caller asked for. This is incomplete and may miss problems with the assignment. Instead in ``assertCreatedPointEvaluatesToTrue()`` augment the ``Assignment`` object with additional arrays in the ``retMap`` map. --- lib/Solver/IndependentSolver.cpp | 61 +++++++++++----------------------------- 1 file changed, 17 insertions(+), 44 deletions(-) (limited to 'lib/Solver/IndependentSolver.cpp') diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 84e7adb6..3594fecf 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -438,65 +438,38 @@ bool IndependentSolver::computeValue(const Query& query, ref &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } -bool canPerformConcreteAssignment(const std::vector &objects, const ref e) { - // Get the arrays used in the constraint. If an array isn't in objects we - // don't have an assignment for it so skip it because can't evaluate to a - // constant. This means we might not be checking every constraint which is - // not ideal but the alternative would require getting an assignment for - // all arrays which is wasteful given that the client didn't ask for them - IndependentElementSet ieSet(e); - for (std::vector::const_iterator ai = objects.begin(), - ae = objects.end(); - ai != ae; ++ai) { - ieSet.wholeObjects.erase(*ai); - ieSet.elements.erase(*ai); - } - - if (ieSet.wholeObjects.size() > 0 || ieSet.elements.size() > 0) { - // There are arrays used in ``e`` that aren't in objects, - // therefore we can't perform a complete assignment - return false; - } - return true; -} - // Helper function used only for assertions to make sure point created -// during computeInitialValues is in fact correct. This function is -// a "best effort" check because if the query uses an Array that an -// assignment is not given for then that Query cannot be fully evaluated so -// this function only checks that all expressions that can be fully -// assigned to evaluate to true. +// during computeInitialValues is in fact correct. The ``retMap`` is used +// in the case ``objects`` doesn't contain all the assignments needed. bool assertCreatedPointEvaluatesToTrue(const Query &query, const std::vector &objects, - std::vector< std::vector > &values){ + std::vector< std::vector > &values, + std::map > &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 and fail Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); - for(ConstraintManager::constraint_iterator it = query.constraints.begin(); - it != query.constraints.end(); ++it){ - ref constraint = *it; - if (!canPerformConcreteAssignment(objects, constraint)) { - // We have to skip checking assigning to this constraint - continue; - } + // Add any additional bindings. + // The semantics of std::map should be to not insert a (key, value) + // pair if it already exists so we should continue to use the assignment + // from ``objects`` and ``values``. + if (retMap.size() > 0) + assign.bindings.insert(retMap.begin(), retMap.end()); + for(ConstraintManager::constraint_iterator it = query.constraints.begin(); + it != query.constraints.end(); ++it){ ref ret = assign.evaluate(*it); - assert(isa(ret) && "Could not use assignment to evaluate constraint"); + assert(isa(ret) && "assignment evaluation did not result in constant"); ref evaluatedConstraint = dyn_cast(ret); if(evaluatedConstraint->isFalse()){ return false; } } ref neg = Expr::createIsZero(query.expr); - if (canPerformConcreteAssignment(objects, neg)) { - ref q = assign.evaluate(neg); - assert(isa(q) && "assignment evaluation did not result in constant"); - return cast(q)->isTrue(); - } - // Can't assign to query expression - return true; + ref q = assign.evaluate(neg); + assert(isa(q) && "assignment evaluation did not result in constant"); + return cast(q)->isTrue(); } bool IndependentSolver::computeInitialValues(const Query& query, @@ -569,7 +542,7 @@ bool IndependentSolver::computeInitialValues(const Query& query, values.push_back(retMap[arr]); } } - assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"); + assert(assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && "should satisfy the equation"); delete factors; return true; } -- cgit 1.4.1