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

6 files changed, 15 insertions, 31 deletions

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;
 }