From 8dd640c8a0fd19047f7a30d3952e12dbac0311f7 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
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')

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<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. 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<const Array*> &objects,
-                                       std::vector< std::vector<unsigned char> > &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);
-  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;
-    }
+  // 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);
 
-    assert(isa<ConstantExpr>(ret) && "Could not use assignment to evaluate constraint");
+    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);
-  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;
+  ref<Expr> q = assign.evaluate(neg);
+  assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant");
+  return cast<ConstantExpr>(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