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

4 files changed, 53 insertions, 39 deletions

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();
       }
     }
diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc
index 4633313d..9e29d0db 100644
--- a/test/Expr/Parser/TypeChecking.pc
+++ b/test/Expr/Parser/TypeChecking.pc
@@ -6,4 +6,9 @@
 (query [(Eq (ReadLSB w32 0 arr1) true)] 
        false)
 
-# RUN: grep "TypeChecking.pc: parse failure: 1 errors." %t.log
+# RUN: grep "TypeChecking.pc:12:25: error: invalid write index (doesn't match array domain)" %t.log
+# RUN: grep "TypeChecking.pc:12:35: error: invalid write value (doesn't match array range)" %t.log
+# FIXME: Add array declarations
+(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr0) 0)] false)
+
+# RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log
diff --git a/www/KQuery.html b/www/KQuery.html
index 4f613c4e..db0d2b59 100644
--- a/www/KQuery.html
+++ b/www/KQuery.html
@@ -317,8 +317,7 @@
 
   <p><b>Syntax:</b></p>
   <div class="syntax">
-    version = identifier<br>
-    version = "[" [ update-list ] "]" [ "@" version "]"<br>
+    version = identifier | "[" [ update-list ] "]" "@" version<br>
     update-list = lhs-expression "=" rhs-expression [ "," update-list ]<br>
   </div>
 
@@ -327,8 +326,6 @@
   of writes which are to be concatenated to another version (the most recent
   writes are first).</p>
 
-  <p>FIXME: Get rid of anonymous arrays.</p>
-
   <h2><a name="exprs">Expressions</a></h2>
 
   <p>Expressions are strongly typed, and have the following general