From 24e065075e7ec973db84639725696b9f84975b2f Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Sun, 7 Jun 2009 07:36:26 +0000
Subject: Eliminate anonymous versions.   - For now, this means the isRooted
 flag for arrays isn't propogated to the     kquery language. We should figure
 out how to do this, but allow anonymous     versions isn't the right way.

Also, improved the error on invalid writes a bit.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Expr/ExprPPrinter.cpp |  6 ++--
 lib/Expr/Parser.cpp       | 74 +++++++++++++++++++++++++++--------------------
 2 files changed, 46 insertions(+), 34 deletions(-)

(limited to 'lib')

diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index f8c6cabc..affde4ad 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -215,8 +215,10 @@ class PPrinter : public ExprPPrinter {
     if (openedList)
       PC << ']';
 
-    if (updates.isRooted)
-      PC << " @ arr" << updates.root->id;
+    // 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;
   }
 
   void printWidth(PrintContext &PC, ref<Expr> e) {
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index e664c9dd..b73c72d6 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1132,20 +1132,33 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
   return Res;
 }
 
-/// version - '[' update-list? ']' ['@' version-specifier]
+namespace {
+  /// WriteInfo - Helper class used for storing information about a parsed
+  /// write, prior to type checking.
+  struct WriteInfo {
+    NumberOrExprResult LHS;
+    NumberOrExprResult RHS;
+    Token LHSTok;
+    Token RHSTok;
+    
+    WriteInfo(NumberOrExprResult _LHS, NumberOrExprResult _RHS,
+              Token _LHSTok, Token _RHSTok) : LHS(_LHS), RHS(_RHS),
+                                              LHSTok(_LHSTok), RHSTok(_RHSTok) {
+    }
+  };
+}
+
+/// version - '[' update-list? ']' '@' version-specifier
 /// update-list - empty
 /// update-list - lhs '=' rhs [',' update-list]
 VersionResult ParserImpl::ParseVersion() {
   if (Tok.kind != Token::LSquare)
     return VersionResult(false, UpdateList(0, false, NULL));
   
-  std::vector< std::pair<NumberOrExprResult, NumberOrExprResult> > Writes;
+  std::vector<WriteInfo> Writes;
   ConsumeLSquare();
   for (;;) {
-    // FIXME: Type check exprs.
-
-    // FIXME: We need to do this (the above) anyway just to handle
-    // implicit constants correctly.
+    Token LHSTok = Tok;
     NumberOrExprResult LHS = ParseNumberOrExpr();
     
     if (Tok.kind != Token::Equals) {
@@ -1154,9 +1167,10 @@ VersionResult ParserImpl::ParseVersion() {
     }
     
     ConsumeToken();
+    Token RHSTok = Tok;
     NumberOrExprResult RHS = ParseNumberOrExpr();
 
-    Writes.push_back(std::make_pair(LHS, RHS));
+    Writes.push_back(WriteInfo(LHS, RHS, LHSTok, RHSTok));
     
     if (Tok.kind == Token::Comma)
       ConsumeToken();
@@ -1167,48 +1181,44 @@ VersionResult ParserImpl::ParseVersion() {
 
   VersionHandle Base(0, false, NULL);
 
-  // Anonymous array case.
-  if (Tok.kind != Token::At) { 
-    Array *root = new Array(0, 0, 0);
-    Base = UpdateList(root, false, NULL);
-  } else {
-    ConsumeToken();
+  if (Tok.kind != Token::At) {
+    Error("expected '@'.", Tok);
+    return VersionResult(false, UpdateList(0, true, NULL));
+  } 
 
-    VersionResult BaseRes = ParseVersionSpecifier();
-    if (!BaseRes.isValid())
-      return BaseRes;
+  ConsumeExpectedToken(Token::At);
 
-    Base = BaseRes.get();
-  }
+  VersionResult BaseRes = ParseVersionSpecifier();
+  if (!BaseRes.isValid())
+    return BaseRes;
+
+  Base = BaseRes.get();
 
   Expr::Width ArrayDomainType = Expr::Int32;
   Expr::Width ArrayRangeType = Expr::Int8;
 
-  for (std::vector< std::pair<NumberOrExprResult, NumberOrExprResult> >::reverse_iterator
-         it = Writes.rbegin(), ie = Writes.rend(); it != ie; ++it) {
+  for (std::vector<WriteInfo>::reverse_iterator it = Writes.rbegin(), 
+         ie = Writes.rend(); it != ie; ++it) {
+    const WriteInfo &WI = *it;
     ExprResult LHS, RHS;
     // FIXME: This can be factored into common helper for coercing a
     // NumberOrExpr into an Expr.
-    if (it->first.isNumber()) {
-      LHS = ParseNumberToken(ArrayDomainType, it->first.getNumber());
+    if (WI.LHS.isNumber()) {
+      LHS = ParseNumberToken(ArrayDomainType, WI.LHS.getNumber());
     } else {
-      LHS = it->first.getExpr(); 
+      LHS = WI.LHS.getExpr();
       if (LHS.isValid() && LHS.get()->getWidth() != ArrayDomainType) {
-        // FIXME: bad token location. We should maybe try and know the
-        // array up-front?
-        Error("invalid value in write index (doesn't match domain).", Tok);
+        Error("invalid write index (doesn't match array domain).", WI.LHSTok);
         LHS = ExprResult();
       }
     }
 
-    if (it->second.isNumber()) {
-      RHS = ParseNumberToken(ArrayRangeType, it->second.getNumber());
+    if (WI.RHS.isNumber()) {
+      RHS = ParseNumberToken(ArrayRangeType, WI.RHS.getNumber());
     } else {
-      RHS = it->second.getExpr();
+      RHS = WI.RHS.getExpr();
       if (RHS.isValid() && RHS.get()->getWidth() != ArrayRangeType) {
-        // FIXME: bad token location. We should maybe try and know the
-        // array up-front?
-        Error("invalid value in write assignment (doesn't match range).", Tok);
+        Error("invalid write value (doesn't match array range).", WI.RHSTok);
         RHS = ExprResult();
       }
     }
-- 
cgit 1.4.1