Merge pull request #359 from delcypher/fix_indep_solver_bug

Bug fix in IndependentSolver

1 files changed, 20 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;
 }