diff options
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 27 | ||||
| -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, 37 insertions, 7 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 78126ede..3594fecf 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -438,23 +438,36 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } - // Helper function used only for assertions to make sure point created -// during computeInitialValues is in fact correct. +// 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<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values){ - Assignment assign = Assignment(objects, values); + 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 and fail + Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); + + // 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<Expr> ret = assign.evaluate(*it); - if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){ + + assert(isa<ConstantExpr>(ret) && "assignment evaluation did not result in constant"); + 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(); } @@ -529,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; } 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') |