Kill off UpdateList::isRooted flag.

 - The right way to handle this is by using constant arrays, where the semantics
   are easier to define and implement.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 16 insertions, 19 deletions

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index ea5427e3..1d06ca33 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -352,7 +352,7 @@ protected:
     // If the index is out of range, we cannot assign it a value, since that
     // value cannot be part of the assignment.
     if (index >= array.size)
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
       
     std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id);
@@ -373,17 +373,17 @@ protected:
     // If the index is out of range, we cannot assign it a value, since that
     // value cannot be part of the assignment.
     if (index >= array.size)
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
       
     std::map<unsigned, CexObjectData*>::iterator it = objects.find(array.id);
     if (it == objects.end())
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
 
     CexValueData cvd = it->second->getExactValues(index);
     if (!cvd.isFixed())
-      return ReadExpr::create(UpdateList(&array, true, 0), 
+      return ReadExpr::create(UpdateList(&array, 0), 
                               ConstantExpr::alloc(index, Expr::Int32));
 
     return ConstantExpr::alloc(cvd.min(), Expr::Int8);
@@ -1020,7 +1020,7 @@ FastCexSolver::computeInitialValues(const Query& query,
 
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
-        ReadExpr::create(UpdateList(array, true, 0),
+        ReadExpr::create(UpdateList(array, 0),
                          ConstantExpr::create(i, kMachinePointerType));
       ref<Expr> value = cd.evaluatePossible(read);
       
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 455e9240..7ebee1c7 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -94,18 +94,16 @@ public:
     findReads(e, /* visitUpdates= */ true, reads);
     for (unsigned i = 0; i != reads.size(); ++i) {
       ReadExpr *re = reads[i].get();
-      if (re->updates.isRooted) {
-        const Array *array = re->updates.root;
-        if (!wholeObjects.count(array)) {
-          if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
-            DenseSet<unsigned> &dis = elements[array];
-            dis.add((unsigned) CE->getConstantValue());
-          } else {
-            elements_ty::iterator it2 = elements.find(array);
-            if (it2!=elements.end())
-              elements.erase(it2);
-            wholeObjects.insert(array);
-          }
+      const Array *array = re->updates.root;
+      if (!wholeObjects.count(array)) {
+        if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+          DenseSet<unsigned> &dis = elements[array];
+          dis.add((unsigned) CE->getConstantValue());
+        } else {
+          elements_ty::iterator it2 = elements.find(array);
+          if (it2!=elements.end())
+            elements.erase(it2);
+          wholeObjects.insert(array);
         }
       }
     }
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 98dcad0b..71516c24 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -343,8 +343,7 @@ ValidatingSolver::computeInitialValues(const Query& query,
       const Array *array = objects[i];
       for (unsigned j=0; j<array->size; j++) {
         unsigned char value = values[i][j];
-        bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array,
-                                                                      true, 0),
+        bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
                                                            ConstantExpr::alloc(j, Expr::Int32)),
                                           ConstantExpr::alloc(value, Expr::Int8)));
       }