diff options
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 54 | ||||
| -rw-r--r-- | test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery | 15 | ||||
| -rw-r--r-- | test/regression/lit.local.cfg | 2 |
3 files changed, 64 insertions, 7 deletions
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<Expr> &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } +bool canPerformConcreteAssignment(const std::vector<const Array*> &objects, const ref<Expr> 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 Array *>::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<const Array*> &objects, std::vector< std::vector<unsigned char> > &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<Expr> constraint = *it; + + if (!canPerformConcreteAssignment(objects, constraint)) { + // We have to skip checking assigning to this constraint + continue; + } + ref<Expr> ret = assign.evaluate(*it); - if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){ + + assert(isa<ConstantExpr>(ret) && "Could not use assignment to evaluate constraint"); + ref<ConstantExpr> evaluatedConstraint = dyn_cast<ConstantExpr>(ret); + if(evaluatedConstraint->isFalse()){ return false; } } ref<Expr> neg = Expr::createIsZero(query.expr); - ref<Expr> q = assign.evaluate(neg); - - assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); - return cast<ConstantExpr>(q)->isTrue(); + if (canPerformConcreteAssignment(objects, neg)) { + ref<Expr> q = assign.evaluate(neg); + assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); + return cast<ConstantExpr>(q)->isTrue(); + } + // Can't assign to query expression + return true; } bool IndependentSolver::computeInitialValues(const Query& query, diff --git a/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery new file mode 100644 index 00000000..9116ea47 --- /dev/null +++ b/test/regression/2016-03-22-independence-solver-missing-objects-for-assignment.kquery @@ -0,0 +1,15 @@ +# RUN: %kleaver %s 2>&1 | FileCheck %s +array n_args[4] : w32 -> w8 = symbolic +array n_args_1[4] : w32 -> w8 = symbolic +array A-data-stat[144] : w32 -> w8 = symbolic +array stdin-stat[144] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 n_args) 2) +(Slt 0 N0) +(Ult N1:(ReadLSB w32 0 n_args_1) 3) +(Slt 0 N1) +(Slt 1 N1) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 A-data-stat) 2147483647))) +(Ult (ReadLSB w64 56 A-data-stat) 65536) +(Eq false (Eq 0 (And w64 (ReadLSB w64 8 stdin-stat) 2147483647)))] +(Eq false (Ult (ReadLSB w64 56 stdin-stat) 65536)) [] [n_args]) +# CHECK: INVALID diff --git a/test/regression/lit.local.cfg b/test/regression/lit.local.cfg new file mode 100644 index 00000000..d64daf29 --- /dev/null +++ b/test/regression/lit.local.cfg @@ -0,0 +1,2 @@ +# Look for .kquery files too +config.suffixes.add('.kquery') |