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

13 files changed, 36 insertions, 60 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index d1fdfa73..e774eaff 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -507,11 +507,8 @@ public:
   /// pointer to the most recent update node
   const UpdateNode *head;
   
-  // shouldn't this be part of the ReadExpr? 
-  bool isRooted;
-
 public:
-  UpdateList(const Array *_root, bool isRooted, const UpdateNode *_head);
+  UpdateList(const Array *_root, const UpdateNode *_head);
   UpdateList(const UpdateList &b);
   ~UpdateList();
   
diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h
index 051a84f9..458b8d8d 100644
--- a/include/klee/util/Assignment.h
+++ b/include/klee/util/Assignment.h
@@ -72,7 +72,7 @@ namespace klee {
       return ConstantExpr::alloc(it->second[index], Expr::Int8);
     } else {
       if (allowFreeValues) {
-        return ReadExpr::create(UpdateList(array, true, 0), 
+        return ReadExpr::create(UpdateList(array, 0), 
                                 ConstantExpr::alloc(index, Expr::Int32));
       } else {
         return ConstantExpr::alloc(0, Expr::Int8);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 8f144456..ba1b8e1f 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -102,7 +102,7 @@ ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
     flushMask(0),
     knownSymbolics(0),
     size(_size),
-    updates(mo->array, false, 0),
+    updates(mo->array, 0),
     readOnly(false) {
 }
 
@@ -149,7 +149,6 @@ void ObjectState::makeConcrete() {
 void ObjectState::makeSymbolic() {
   assert(!updates.head &&
          "XXX makeSymbolic of objects with symbolic values is unsupported");
-  updates.isRooted = true;
 
   // XXX simplify this, can just delete various arrays I guess
   for (unsigned i=0; i<size; i++) {
@@ -792,7 +791,6 @@ void ObjectState::print() {
   llvm::cerr << "-- ObjectState --\n";
   llvm::cerr << "\tMemoryObject ID: " << object->id << "\n";
   llvm::cerr << "\tRoot Object: " << updates.root << "\n";
-  llvm::cerr << "\tIs Rooted? " << updates.isRooted << "\n";
   llvm::cerr << "\tSize: " << size << "\n";
 
   llvm::cerr << "\tBytes:\n";
diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp
index 6fcfe596..dc3ff931 100644
--- a/lib/Core/SeedInfo.cpp
+++ b/lib/Core/SeedInfo.cpp
@@ -87,7 +87,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
          it = directReads.begin(), ie = directReads.end(); it != ie; ++it) {
     const Array *array = it->first;
     unsigned i = it->second;
-    ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
+    ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                       ConstantExpr::alloc(i, Expr::Int32));
     
     // If not in bindings then this can't be a violation?
@@ -124,7 +124,7 @@ void SeedInfo::patchSeed(const ExecutionState &state,
          ie = assignment.bindings.end(); it != ie; ++it) {
     const Array *array = it->first;
     for (unsigned i=0; i<array->size; ++i) {
-      ref<Expr> read = ReadExpr::create(UpdateList(array, true, 0),
+      ref<Expr> read = ReadExpr::create(UpdateList(array, 0),
                                         ConstantExpr::alloc(i, Expr::Int32));
       ref<Expr> isSeed = EqExpr::create(read, ConstantExpr::alloc(it->second[i], Expr::Int8));
       bool res;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 57898969..3f5ef95f 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -38,7 +38,7 @@ namespace {
 unsigned Expr::count = 0;
 
 ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
-  UpdateList ul(array, true, 0);
+  UpdateList ul(array, 0);
 
   switch (w) {
   default: assert(0 && "invalid width");
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index eced0e87..bf229731 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -24,8 +24,7 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
       // cannot guarantee value. we can rewrite to read at this
       // version though (mostly for debugging).
       
-      UpdateList fwd(ul.root, un, 0);
-      return Action::changeTo(ReadExpr::create(fwd, 
+      return Action::changeTo(ReadExpr::create(UpdateList(ul.root, un), 
                                                ConstantExpr::alloc(index, Expr::Int32)));
     }
   }
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 3fa7155b..831a4d91 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -167,11 +167,7 @@ private:
 
     // Special case empty list.
     if (!head) {
-      if (updates.isRooted) {
-        PC << "arr" << updates.root->id;
-      } else {
-        PC << "[]";
-      }
+      PC << "arr" << updates.root->id;
       return;
     }
 
@@ -221,9 +217,6 @@ private:
     if (openedList)
       PC << ']';
 
-    // FIXME: Figure out how isRooted should be dealt with in the language. The
-    // old solution of using "anonymous" arrays is not a good idea.
-
     PC << " @ arr" << updates.root->id;
   }
 
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 0c150a51..1213edeb 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -89,9 +89,8 @@ protected:
       visit(un->value);
     }
 
-    if (ul.isRooted)
-      if (results.insert(ul.root).second)
-        objects.push_back(ul.root);
+    if (results.insert(ul.root).second)
+      objects.push_back(ul.root);
 
     return Action::doChildren();
   }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index a2a5d2e2..496472bf 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -529,7 +529,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
 
   // Create the initial version reference.
   VersionSymTab.insert(std::make_pair(Label,
-                                      UpdateList(Root, true, NULL)));
+                                      UpdateList(Root, NULL)));
 
   return AD;
 }
@@ -577,8 +577,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
   for (std::map<const Identifier*, const ArrayDecl*>::iterator
          it = ArraySymTab.begin(), ie = ArraySymTab.end(); it != ie; ++it) {
     VersionSymTab.insert(std::make_pair(it->second->Name,
-                                        UpdateList(it->second->Root, 
-                                                   true, NULL)));
+                                        UpdateList(it->second->Root, NULL)));
   }
 
 
@@ -1284,8 +1283,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
       
       if (it == VersionSymTab.end()) {
         Error("invalid version reference.", LTok);
-        return VersionResult(false,
-                             UpdateList(0, true, NULL));
+        return VersionResult(false, UpdateList(0, NULL));
       }
 
       return it->second;
@@ -1302,8 +1300,7 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
   VersionResult Res = ParseVersion();
   // Define update list to avoid use-of-undef errors.
   if (!Res.isValid()) {
-    Res = VersionResult(true,
-                        UpdateList(new Array(0, -1, 0), true, NULL));
+    Res = VersionResult(true, UpdateList(new Array(0, -1, 0), NULL));
   }
   
   if (Label)
@@ -1332,7 +1329,7 @@ namespace {
 /// update-list - lhs '=' rhs [',' update-list]
 VersionResult ParserImpl::ParseVersion() {
   if (Tok.kind != Token::LSquare)
-    return VersionResult(false, UpdateList(0, false, NULL));
+    return VersionResult(false, UpdateList(0, NULL));
   
   std::vector<WriteInfo> Writes;
   ConsumeLSquare();
@@ -1358,11 +1355,11 @@ VersionResult ParserImpl::ParseVersion() {
   }
   ExpectRSquare("expected close of update list");
 
-  VersionHandle Base(0, false, NULL);
+  VersionHandle Base(0, NULL);
 
   if (Tok.kind != Token::At) {
     Error("expected '@'.", Tok);
-    return VersionResult(false, UpdateList(0, true, NULL));
+    return VersionResult(false, UpdateList(0, NULL));
   } 
 
   ConsumeExpectedToken(Token::At);
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp
index 7c3f41d4..22544820 100644
--- a/lib/Expr/Updates.cpp
+++ b/lib/Expr/Updates.cpp
@@ -56,18 +56,15 @@ unsigned UpdateNode::computeHash() {
 
 ///
 
-UpdateList::UpdateList(const Array *_root, bool _isRooted,
-                       const UpdateNode *_head)
+UpdateList::UpdateList(const Array *_root, const UpdateNode *_head)
   : root(_root),
-    head(_head),
-    isRooted(_isRooted) {
+    head(_head) {
   if (head) ++head->refCount;
 }
 
 UpdateList::UpdateList(const UpdateList &b)
   : root(b.root),
-    head(b.head),
-    isRooted(b.isRooted) {
+    head(b.head) {
   if (head) ++head->refCount;
 }
 
@@ -87,7 +84,6 @@ UpdateList &UpdateList::operator=(const UpdateList &b) {
   if (head && --head->refCount==0) delete head;
   root = b.root;
   head = b.head;
-  isRooted = b.isRooted;
   return *this;
 }
 
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)));
       }