Implement array declarations.

 - Printing current prints all declarations, and we allow redefinition, since
   the printer doesn't know what has already been printed.

 - Names don't print right yet, since the Array* object doesn't have the name.

 - Various things are unsupported.
   o Array domain/range must be w32/w8.
   o Concrete initializers for arrays are unsupported.


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

14 files changed, 368 insertions, 87 deletions

diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h
index 4ae760a0..a8719b4d 100644
--- a/include/expr/Lexer.h
+++ b/include/expr/Lexer.h
@@ -28,9 +28,11 @@ namespace expr {
       EndOfFile,                /// <end of file>
       Equals,                   /// ' = '
       Identifier,               /// [a-zA-Z_][a-zA-Z0-9._]*
+      KWArray,                  /// 'array'
       KWFalse,                  /// 'false'
       KWQuery,                  /// 'query'
       KWReserved,               /// fp[0-9]+([.].*)?, i[0-9]+
+      KWSymbolic,               /// 'symbolic'
       KWTrue,                   /// 'true'
       KWWidth,                  /// w[0-9]+
       LBrace,                   /// '{'
@@ -41,7 +43,10 @@ namespace expr {
       RParen,                   /// ')'
       RSquare,                  /// ']'
       Semicolon,                /// ';'
-      Unknown                   /// <other>
+      Unknown,                   /// <other>
+      
+      KWKindFirst=KWArray,
+      KWKindLast=KWWidth
     };
 
     Kind        kind;           /// The token kind.
@@ -60,7 +65,7 @@ namespace expr {
 
     /// isKeyword - True if this token is a keyword.
     bool isKeyword() const { 
-      return kind >= KWFalse && kind <= KWTrue; 
+      return kind >= KWKindFirst && kind <= KWKindLast; 
     }
 
     // dump - Dump the token to stderr.
diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index 5caf0027..65105f12 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -79,7 +79,7 @@ namespace expr {
 
     /// Size - The maximum array size (or 0 if unspecified). Concrete
     /// arrays always are specified with a size.
-    const unsigned Size;
+    const uint64_t Size;
 
     /// Domain - The width of indices.
     const unsigned Domain;
@@ -96,7 +96,7 @@ namespace expr {
     const std::vector<ExprHandle> Contents;
 
   public:
-    ArrayDecl(const Identifier *_Name, unsigned _Size, 
+    ArrayDecl(const Identifier *_Name, uint64_t _Size, 
               unsigned _Domain, unsigned _Range,
               const Array *_Root)
       : Decl(ArrayDeclKind), Name(_Name), 
diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h
index 50ccd203..4d1930d8 100644
--- a/include/klee/util/ExprPPrinter.h
+++ b/include/klee/util/ExprPPrinter.h
@@ -65,7 +65,8 @@ namespace klee {
                            const ref<Expr> *evalExprsBegin = 0,
                            const ref<Expr> *evalExprsEnd = 0,
                            const Array * const* evalArraysBegin = 0,
-                           const Array * const* evalArraysEnd = 0);
+                           const Array * const* evalArraysEnd = 0,
+                           bool printArrayDecls = true);
   };
 
 }
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 1e346e89..a1e030a5 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -46,7 +46,10 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
   
   switch (ce->getOpcode()) {
     default :
-      assert(0 && "unknown ConstantExpr type");
+      ce->dump();
+      llvm::cerr << "error: unknown ConstantExpr type\n"
+                 << "opcode: " << ce->getOpcode() << "\n";
+      abort();
 
     case Instruction::Trunc: return ExtractExpr::createByteOff(op1, 
 							       0,
@@ -128,6 +131,9 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) {
       return SelectExpr::create(op1, op2, op3);
     }
 
+    case Instruction::FAdd:
+    case Instruction::FSub:
+    case Instruction::FMul:
     case Instruction::FDiv:
     case Instruction::FRem:
     case Instruction::FPTrunc:
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index affde4ad..7bfb6567 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -81,6 +81,9 @@ public:
 };
 
 class PPrinter : public ExprPPrinter {
+public:
+  std::set<const Array*> usedArrays;
+private:
   std::map<ref<Expr>, unsigned> bindings;
   std::map<const UpdateNode*, unsigned> updateBindings;
   std::set< ref<Expr> > couldPrint, shouldPrint;
@@ -131,6 +134,7 @@ class PPrinter : public ExprPPrinter {
   }
   
   void scanUpdate(const UpdateNode *un) {
+    // FIXME: This needs to be non-recursive.
     if (un) {
       if (couldPrintUpdates.insert(un).second) {
         scanUpdate(un->next);
@@ -148,8 +152,10 @@ class PPrinter : public ExprPPrinter {
         Expr *ep = e.get();
         for (unsigned i=0; i<ep->getNumKids(); i++)
           scan1(ep->getKid(i));
-        if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) 
+        if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+          usedArrays.insert(re->updates.root);
           scanUpdate(re->updates.head);
+        }
       } else {
         shouldPrint.insert(e);
       }
@@ -507,7 +513,8 @@ void ExprPPrinter::printQuery(std::ostream &os,
                               const ref<Expr> *evalExprsBegin,
                               const ref<Expr> *evalExprsEnd,
                               const Array * const *evalArraysBegin,
-                              const Array * const *evalArraysEnd) {
+                              const Array * const *evalArraysEnd,
+                              bool printArrayDecls) {
   PPrinter p(os);
   
   for (ConstraintManager::const_iterator it = constraints.begin(),
@@ -519,6 +526,21 @@ void ExprPPrinter::printQuery(std::ostream &os,
     p.scan(*it);
 
   PrintContext PC(os);
+  
+  // Print array declarations.
+  if (printArrayDecls) {
+    for (std::set<const Array*>::iterator it = p.usedArrays.begin(), 
+           ie = p.usedArrays.end(); it != ie; ++it) {
+      const Array *A = *it;
+      // FIXME: Print correct name, domain, and range.
+      PC << "array " << "arr" << A->id 
+         << "[" << A->size << "]"
+         << " : " << "w32" << " -> " << "w8"
+         << " = symbolic";
+      PC.breakLine();
+    }
+  }
+
   PC << "(query [";
   
   // Ident at constraint list;
diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp
index 77e25f62..d8809a53 100644
--- a/lib/Expr/Lexer.cpp
+++ b/lib/Expr/Lexer.cpp
@@ -34,9 +34,11 @@ const char *Token::getKindName() const {
   case EndOfFile:  return "EndOfFile";
   case Equals:     return "Equals";
   case Identifier: return "Identifier";
+  case KWArray:    return "KWArray";
   case KWFalse:    return "KWFalse";
   case KWQuery:    return "KWQuery";
   case KWReserved: return "KWReserved";
+  case KWSymbolic: return "KWSymbolic";
   case KWTrue:     return "KWTrue";
   case KWWidth:    return "KWWidth";
   case LBrace:     return "LBrace";
@@ -153,7 +155,7 @@ Token &Lexer::SetIdentifierTokenKind(Token &Result) {
 
   case 5:
     if (memcmp("array", Result.start, 5) == 0)
-      return SetTokenKind(Result, Token::KWReserved);
+      return SetTokenKind(Result, Token::KWArray);
     if (memcmp("false", Result.start, 5) == 0)
       return SetTokenKind(Result, Token::KWFalse);
     if (memcmp("query", Result.start, 5) == 0)
@@ -169,6 +171,11 @@ Token &Lexer::SetIdentifierTokenKind(Token &Result) {
     if (memcmp("declare", Result.start, 7) == 0)
       return SetTokenKind(Result, Token::KWReserved);
     break;
+
+  case 8:
+    if (memcmp("symbolic", Result.start, 8) == 0)
+      return SetTokenKind(Result, Token::KWSymbolic);
+    break;
   }
 
   if (isReservedKW(Result.start, Length))
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index dedbaa3a..f6487674 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -36,7 +36,7 @@ namespace {
     T Value;
 
   public:
-    ParseResult() : IsValid(false) {}
+    ParseResult() : IsValid(false), Value() {}
     ParseResult(T _Value) : IsValid(true), Value(_Value) {}
     ParseResult(bool _IsValid, T _Value) : IsValid(_IsValid), Value(_Value) {}
 
@@ -71,6 +71,7 @@ namespace {
   typedef ParseResult<Decl*> DeclResult;
   typedef ParseResult<Expr::Width> TypeResult;
   typedef ParseResult<VersionHandle> VersionResult;
+  typedef ParseResult<uint64_t> IntegerResult;
 
   /// NumberOrExprResult - Represent a number or expression. This is used to
   /// wrap an expression production which may be a number, but for
@@ -137,37 +138,43 @@ namespace {
 
     /// ConsumeToken - Consume the current 'peek token' and lex the next one.
     void ConsumeToken() {
-      assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen);
+      assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen &&
+             Tok.kind != Token::LSquare && Tok.kind != Token::RSquare);
       GetNextNonCommentToken();
     }
 
     /// ConsumeExpectedToken - Check that the current token is of the
     /// expected kind and consume it.
     void ConsumeExpectedToken(Token::Kind k) {
+      assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen &&
+             Tok.kind != Token::LSquare && Tok.kind != Token::RSquare);
+      _ConsumeExpectedToken(k);
+    }
+    void _ConsumeExpectedToken(Token::Kind k) {
       assert(Tok.kind == k && "Unexpected token!");
       GetNextNonCommentToken();
     }
 
     void ConsumeLParen() {
       ++ParenLevel;
-      ConsumeExpectedToken(Token::LParen);
+      _ConsumeExpectedToken(Token::LParen);
     }
 
     void ConsumeRParen() {
       if (ParenLevel) // Cannot go below zero.
         --ParenLevel;
-      ConsumeExpectedToken(Token::RParen);
+      _ConsumeExpectedToken(Token::RParen);
     }
 
     void ConsumeLSquare() {
       ++SquareLevel;
-      ConsumeExpectedToken(Token::LSquare);
+      _ConsumeExpectedToken(Token::LSquare);
     }
 
     void ConsumeRSquare() {
       if (SquareLevel) // Cannot go below zero.
         --SquareLevel;
-      ConsumeExpectedToken(Token::RSquare);
+      _ConsumeExpectedToken(Token::RSquare);
     }
 
     void ConsumeAnyToken() {
@@ -277,6 +284,7 @@ namespace {
     /* Etc. */
 
     NumberOrExprResult ParseNumberOrExpr();
+    IntegerResult ParseIntegerConstant(Expr::Width Type);
 
     ExprResult ParseExpr(TypeResult ExpectedType);
     ExprResult ParseParenExpr(TypeResult ExpectedType);
@@ -355,13 +363,23 @@ const Identifier *ParserImpl::GetOrCreateIdentifier(const Token &Tok) {
 Decl *ParserImpl::ParseTopLevelDecl() {
   // Repeat until success or EOF.
   while (Tok.kind != Token::EndOfFile) {
-    // Only handle commands for now.
-    if (Tok.kind == Token::LParen) {
+    switch (Tok.kind) {
+    case Token::KWArray: {
+      DeclResult Res = ParseArrayDecl();
+      if (Res.isValid())
+        return Res.get();
+      break;
+    }
+
+    case Token::LParen: {
       DeclResult Res = ParseCommandDecl();
       if (Res.isValid())
         return Res.get();
-    } else {
-      Error("expected '(' token.");
+      break;
+    }
+
+    default:
+      Error("expected 'array' or '(' token.");
       ConsumeAnyToken();
     }
   }
@@ -369,6 +387,153 @@ Decl *ParserImpl::ParseTopLevelDecl() {
   return 0;
 }
 
+/// ParseArrayDecl - Parse an array declaration. The lexer should be positioned
+/// at the opening 'array'.
+///
+/// array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range 
+///                       "=" array-initializer
+/// array-initializer = "symbolic" | "{" { numeric-literal } "}"
+DeclResult ParserImpl::ParseArrayDecl() {
+  // FIXME: Recovery here is horrible, we need to scan to next decl start or
+  // something.
+  ConsumeExpectedToken(Token::KWArray);
+  
+  if (Tok.kind != Token::Identifier) {
+    Error("expected identifier token.");
+    return DeclResult();
+  }
+
+  Token Name = Tok;
+  IntegerResult Size;
+  TypeResult DomainType;
+  TypeResult RangeType;
+  std::vector<ExprHandle> Values;
+
+  ConsumeToken();
+  
+  if (Tok.kind != Token::LSquare) {
+    Error("expected '['.");
+    goto exit;
+  }
+  ConsumeLSquare();
+
+  if (Tok.kind != Token::RSquare) {
+    Size = ParseIntegerConstant(64);
+  }
+  if (Tok.kind != Token::RSquare) {
+    Error("expected ']'.");
+    goto exit;
+  }
+  ConsumeRSquare();
+  
+  if (Tok.kind != Token::Colon) {
+    Error("expected ':'.");
+    goto exit;
+  }
+  ConsumeExpectedToken(Token::Colon);
+
+  DomainType = ParseTypeSpecifier();
+  if (Tok.kind != Token::Arrow) {
+    Error("expected '->'.");
+    goto exit;
+  }
+  ConsumeExpectedToken(Token::Arrow);
+
+  RangeType = ParseTypeSpecifier();
+  if (Tok.kind != Token::Equals) {
+    Error("expected '='.");
+    goto exit;
+  }
+  ConsumeExpectedToken(Token::Equals);
+
+  if (Tok.kind == Token::KWSymbolic) {
+    ConsumeExpectedToken(Token::KWSymbolic);    
+  } else if (Tok.kind == Token::LSquare) {
+    ConsumeLSquare();
+    while (Tok.kind != Token::RSquare) {
+      if (Tok.kind == Token::EndOfFile) {
+        Error("unexpected end of file.");
+        goto exit;
+      }
+
+      ExprResult Res = ParseNumber(RangeType.get());
+      if (Res.isValid())
+        Values.push_back(Res.get());
+    }
+    ConsumeRSquare();
+  } else {
+    Error("expected 'symbolic' or '['.");
+    goto exit;
+  }
+
+  // Type check size.
+  if (!Size.isValid()) {
+    if (Values.empty()) {
+      Error("unsized arrays are not yet supported.");
+      Size = 1;
+    } else {
+      Size = Values.size();
+    }
+  }
+
+  if (!Values.empty()) {
+    if (Size.get() != Values.size()) {
+      // FIXME: Lame message.
+      Error("constant arrays must be completely specified.");
+      Values.clear();
+    }
+
+    for (unsigned i = 0; i != Size.get(); ++i) {
+      // FIXME: Must be constant expression.
+    }
+  }
+
+  // FIXME: Validate that size makes sense for domain type.
+
+  if (DomainType.get() != Expr::Int32) {
+    Error("array domain must currently be w32.");
+    DomainType = Expr::Int32;
+    Values.clear();
+  }
+
+  if (RangeType.get() != Expr::Int8) {
+    Error("array domain must currently be w8.");
+    RangeType = Expr::Int8;
+    Values.clear();
+  }
+
+  if (!Values.empty()) {
+    Error("constant arrays are not yet supported.");
+    Values.clear();
+  }
+
+  // FIXME: Validate that this array is undeclared.
+
+ exit:
+  if (!Size.isValid())
+    Size = 1;
+  if (!DomainType.isValid())
+    DomainType = 32;
+  if (!RangeType.isValid())
+    RangeType = 8;
+
+  // FIXME: Array should take name, not id.
+  // FIXME: Array should take domain and range.
+  const Identifier *Label = GetOrCreateIdentifier(Name);
+  static int counter = 0;
+  Array *Root = new Array(0, ++counter, Size.get());
+  ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
+                                DomainType.get(), RangeType.get(), Root);
+
+  ArraySymTab.insert(std::make_pair(Label, AD));
+
+  // Create the initial version reference.
+  VersionSymTab.insert(std::make_pair(Label,
+                                      UpdateList(Root, true, NULL)));
+
+  return AD;
+}
+
 /// ParseCommandDecl - Parse a command declaration. The lexer should
 /// be positioned at the opening '('.
 ///
@@ -407,6 +572,16 @@ DeclResult ParserImpl::ParseQueryCommand() {
   ExprSymTab.clear();
   VersionSymTab.clear();
 
+  // Reinsert initial array versions.
+  // FIXME: Remove this!
+  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)));
+  }
+
+
   ConsumeExpectedToken(Token::KWQuery);
   if (Tok.kind != Token::LSquare) {
     Error("malformed query, expected constraint list.");
@@ -414,7 +589,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
     return DeclResult();
   }
 
-  ConsumeExpectedToken(Token::LSquare);
+  ConsumeLSquare();
   // FIXME: Should avoid reading past unbalanced parens here.
   while (Tok.kind != Token::RSquare) {
     if (Tok.kind == Token::EndOfFile) {
@@ -437,7 +612,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
   if (Tok.kind == Token::RParen)
     goto exit;
   
-  ConsumeExpectedToken(Token::LSquare);
+  ConsumeLSquare();
   // FIXME: Should avoid reading past unbalanced parens here.
   while (Tok.kind != Token::RSquare) {
     if (Tok.kind == Token::EndOfFile) {
@@ -455,7 +630,7 @@ DeclResult ParserImpl::ParseQueryCommand() {
   if (Tok.kind == Token::RParen)
     goto exit;
 
-  ConsumeExpectedToken(Token::LSquare);
+  ConsumeLSquare();
   // FIXME: Should avoid reading past unbalanced parens here.
   while (Tok.kind != Token::RSquare) {
     if (Tok.kind == Token::EndOfFile) {
@@ -474,15 +649,15 @@ DeclResult ParserImpl::ParseQueryCommand() {
     const Identifier *Label = GetOrCreateIdentifier(Tok);
     ConsumeToken();
 
-    // Declare or create array.
-    const ArrayDecl *AD = ArraySymTab[Label];
-    if (!AD) {
-      // FIXME: Don't make up arrays.
-      unsigned Id = atoi(&Label->Name.c_str()[3]);
-      AD = new ArrayDecl(Label, 0, 32, 8, new Array(0, Id, 0));
+    // Lookup array.
+    std::map<const Identifier*, const ArrayDecl*>::iterator
+      it = ArraySymTab.find(Label);
+
+    if (it == ArraySymTab.end()) {
+      Error("unknown array", LTok);
+    } else {
+      Objects.push_back(it->second->Root);
     }
-    
-    Objects.push_back(AD->Root);
   }
   ConsumeRSquare();
 
@@ -995,10 +1170,18 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name,
   return ConcatExpr::createN(Kids.size(), &Kids[0]);
 }
 
+IntegerResult ParserImpl::ParseIntegerConstant(Expr::Width Type) {
+  ExprResult Res = ParseNumber(Type);
+
+  if (!Res.isValid())
+    return IntegerResult();
+
+  return cast<ConstantExpr>(Res.get())->getConstantValue();
+}
+
 ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
                                              Expr::Width ResTy) {
-  // FIXME: Pull out parse constant integer expression.
-  ExprResult OffsetExpr = ParseNumber(Expr::Int32);
+  IntegerResult OffsetExpr = ParseIntegerConstant(Expr::Int32);
   ExprResult Child = ParseExpr(TypeResult());
 
   ExpectRParen("unexpected argument to expression.");
@@ -1006,9 +1189,7 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name,
   if (!OffsetExpr.isValid() || !Child.isValid())
     return ConstantExpr::alloc(0, ResTy);
 
-  unsigned Offset = 
-    (unsigned) cast<ConstantExpr>(OffsetExpr.get())->getConstantValue();
-
+  unsigned Offset = (unsigned) OffsetExpr.get();
   if (Offset + ResTy > Child.get()->getWidth()) {
     Error("extract out-of-range of child expression.", Name);
     return ConstantExpr::alloc(0, ResTy);
@@ -1086,26 +1267,11 @@ VersionResult ParserImpl::ParseVersionSpecifier() {
     Label = GetOrCreateIdentifier(Tok);
     ConsumeToken();
 
-    // FIXME: hack: add array declarations and ditch this.
-    if (memcmp(Label->Name.c_str(), "arr", 3) == 0) {
-      // Declare or create array.
-      const ArrayDecl *&A = ArraySymTab[Label];
-      if (!A) {
-        unsigned id = atoi(&Label->Name.c_str()[3]);
-        Array *root = new Array(0, id, 0);
-        ArrayDecl *AD = new ArrayDecl(Label, 0, 32, 8, root);
-        // Create update list mapping of name -> array.
-        VersionSymTab.insert(std::make_pair(Label,
-                                            UpdateList(root, true, NULL)));
-        ArraySymTab.insert(std::make_pair(Label, AD));
-      }
-    }
-
     if (Tok.kind != Token::Colon) {
       VersionSymTabTy::iterator it = VersionSymTab.find(Label);
       
       if (it == VersionSymTab.end()) {
-        Error("invalid update list label reference.", LTok);
+        Error("invalid version reference.", LTok);
         return VersionResult(false,
                              UpdateList(0, true, NULL));
       }
@@ -1381,9 +1547,10 @@ void ParserImpl::Error(const char *Message, const Token &At) {
 Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
-  std::cout << "array " << Name->Name << " : "
-            << 'w' << Domain << " -> "
-            << 'w' << Range << " = ";
+  // FIXME: For now, print using the Array* "name".
+  std::cout << "array " << "arr" << Root->id
+            << "[" << Size << "]"
+            << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
   if (Contents.empty()) {
     std::cout << "symbolic\n";
@@ -1412,7 +1579,8 @@ void QueryCommand::dump() {
   }
   ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), 
                            Query, ValuesBegin, ValuesEnd,
-                           ObjectsBegin, ObjectsEnd);
+                           ObjectsBegin, ObjectsEnd,
+                           false);
 }
 
 // Public parser API
diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc
index 354b0489..0dac0cc8 100644
--- a/test/Expr/Evaluate.pc
+++ b/test/Expr/Evaluate.pc
@@ -1,8 +1,11 @@
 # RUN: %kleaver -evaluate %s > %t.log
 
+array arr0[4] : w32 -> w8 = symbolic
+array arr1[8] : w32 -> w8 = symbolic
+
 # RUN: grep "Query 0:	INVALID" %t.log
 # Query 0
-(query [] (Not (Ult (ReadLSB w32 0 arr65)
+(query [] (Not (Ult (ReadLSB w32 0 arr0)
                     16)))
 
 # RUN: grep "Query 1:	VALID" %t.log
diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.pc
index 6af40133..6b8e2e37 100644
--- a/test/Expr/Lexer/Numbers.pc
+++ b/test/Expr/Lexer/Numbers.pc
@@ -17,7 +17,7 @@
 # RUN: grep "(Token .LBrace. .{. 1 56 0)" %t1
 # RUN: grep "(Token .RBrace. .}. 1 56 2)" %t1
 # RUN: grep "(Token .Identifier. ._hello_world. 12 58 0)" %t1
-# RUN: grep "(Token .KWReserved. .array. 5 62 0)" %t1
+# RUN: grep "(Token .KWArray. .array. 5 62 0)" %t1
 # RUN: grep "(Token .KWReserved. .declare. 7 63 0)" %t1
 # RUN: grep "(Token .KWReserved. .def. 3 64 0)" %t1
 # RUN: grep "(Token .KWReserved. .define. 6 65 0)" %t1
diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.pc
index e57e9760..0b1479d4 100644
--- a/test/Expr/Parser/Concat64.pc
+++ b/test/Expr/Parser/Concat64.pc
@@ -1,5 +1,6 @@
 # RUN: kleaver --print-ast %s
 
+array arr1[8] : w32 -> w8 = symbolic
 (query [(Eq 0
             (Concat w64 (Read w8 7 arr1)
             (Concat w56 (Read w8 6 arr1)
diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc
index 742a0185..4a6adf7e 100644
--- a/test/Expr/Parser/Exprs.pc
+++ b/test/Expr/Parser/Exprs.pc
@@ -6,64 +6,79 @@
 # RUN: %kleaver -print-ast %s
 
 # Query 0 -- Type: Truth, Instructions: 31
+array arr53[4] : w32 -> w8 = symbolic
 (query [] (Not (Ult (ReadLSB w32 0 arr53)
                     16)))
-#   OK -- Elapsed: 0.00128889
+#   OK -- Elapsed: 0.00137401
 #   Is Valid: false
 
 # Query 1 -- Type: Value, Instructions: 39
+array arr53[4] : w32 -> w8 = symbolic
 (query [(Ult N0:(ReadLSB w32 0 arr53)
              16)]
        false
-       [(Add w32 31543472 (Mul w32 4 N0))])
-#   OK -- Elapsed: 0.000106812
-#   Result: 31543472
+       [(Add w32 31543488 (Mul w32 4 N0))])
+#   OK -- Elapsed: 0.000108004
+#   Result: 31543488
 
 # Query 2 -- Type: Truth, Instructions: 39
+array arr53[4] : w32 -> w8 = symbolic
 (query [(Ult N0:(ReadLSB w32 0 arr53)
              16)]
        (Ult (Mul w32 4 N0) 61))
-#   OK -- Elapsed: 0.0014112
+#   OK -- Elapsed: 0.00140095
 #   Is Valid: true
 
 # Query 3 -- Type: Truth, Instructions: 55
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)]
        (Not (Ult (ReadLSB w32 0 arr60)
                  16)))
-#   OK -- Elapsed: 0.00128603
+#   OK -- Elapsed: 0.00106597
 #   Is Valid: false
 
 # Query 4 -- Type: Value, Instructions: 60
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult N0:(ReadLSB w32 0 arr60)
              16)]
        false
-       [(Add w32 31543472 (Mul w32 4 N0))])
-#   OK -- Elapsed: 0.000141144
-#   Result: 31543472
+       [(Add w32 31543488 (Mul w32 4 N0))])
+#   OK -- Elapsed: 0.000138998
+#   Result: 31543488
 
 # Query 5 -- Type: Truth, Instructions: 60
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult N0:(ReadLSB w32 0 arr60)
              16)]
        (Ult (Mul w32 4 N0) 61))
-#   OK -- Elapsed: 0.00145102
+#   OK -- Elapsed: 0.00137782
 #   Is Valid: true
 
 # Query 6 -- Type: Truth, Instructions: 77
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
              16)]
        (Not (Ult (ReadLSB w32 0 arr67)
                  16)))
-#   OK -- Elapsed: 0.00127888
+#   OK -- Elapsed: 0.001127
 #   Is Valid: false
 
 # Query 7 -- Type: Value, Instructions: 85
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -71,11 +86,14 @@
         (Ult N0:(ReadLSB w32 0 arr67)
              16)]
        false
-       [(Add w32 31543472 (Mul w32 4 N0))])
-#   OK -- Elapsed: 0.000179052
-#   Result: 31543472
+       [(Add w32 31543488 (Mul w32 4 N0))])
+#   OK -- Elapsed: 0.000175953
+#   Result: 31543488
 
 # Query 8 -- Type: Truth, Instructions: 85
+array arr53[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -87,6 +105,10 @@
 #   Is Valid: true
 
 # Query 9 -- Type: Truth, Instructions: 101
+array arr53[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -98,10 +120,14 @@
             (And (Not (Eq 2 N0))
                  (And (Not (Eq 1 N0))
                       (Not (Eq 0 N0))))))
-#   OK -- Elapsed: 0.00163794
+#   OK -- Elapsed: 0.00157499
 #   Is Valid: false
 
 # Query 10 -- Type: Value, Instructions: 106
+array arr53[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -114,11 +140,15 @@
                        (And (Not (Eq 1 N0))
                             (Not (Eq 0 N0))))))]
        false
-       [(Add w32 31583216 N0)])
-#   OK -- Elapsed: 0.000283003
-#   Result: 31583219
+       [(Add w32 31583232 N0)])
+#   OK -- Elapsed: 0.000259876
+#   Result: 31583235
 
 # Query 11 -- Type: Truth, Instructions: 106
+array arr53[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -132,10 +162,15 @@
                             (Not N4:(Eq 0 N1))))))]
        (Or N0
            (Or N2 (Or N3 N4))))
-#   OK -- Elapsed: 0.00217485
+#   OK -- Elapsed: 0.00194788
 #   Is Valid: true
 
 # Query 12 -- Type: Truth, Instructions: 112
+array arr53[4] : w32 -> w8 = symbolic
+array arr49[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -150,10 +185,15 @@
        (Not (Eq 104
                 (Read w8 0 [N0=0,
                             1=97] @ arr49))))
-#   OK -- Elapsed: 0.00330305
+#   OK -- Elapsed: 0.0030148
 #   Is Valid: false
 
 # Query 13 -- Type: Truth, Instructions: 122
+array arr53[4] : w32 -> w8 = symbolic
+array arr49[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult (ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -172,10 +212,16 @@
                  (Concat w32 (Read w8 3 U0)
                              (Concat w24 (Read w8 2 U0)
                                          (Concat w16 (Read w8 1 U0) (w8 104)))))))
-#   OK -- Elapsed: 0.00039506
+#   OK -- Elapsed: 0.000394106
 #   Is Valid: false
 
 # Query 14 -- Type: Truth, Instructions: 128
+array arr5[64] : w32 -> w8 = symbolic
+array arr53[4] : w32 -> w8 = symbolic
+array arr49[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult N0:(ReadLSB w32 0 arr53)
              16)
         (Ult (ReadLSB w32 0 arr60)
@@ -204,10 +250,16 @@
                                     (Add w32 3 N6)=(Extract w8 24 N7),
                                     63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5)
                 N3)))
-#   OK -- Elapsed: 0.018568
+#   OK -- Elapsed: 0.0180621
 #   Is Valid: false
 
 # Query 15 -- Type: Truth, Instructions: 133
+array arr5[64] : w32 -> w8 = symbolic
+array arr53[4] : w32 -> w8 = symbolic
+array arr49[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult N0:(ReadLSB w32 0 arr53)
              16)
         (Ult N1:(ReadLSB w32 0 arr60)
@@ -238,10 +290,16 @@
             N4)]
        (Eq 32
            (ReadLSB w32 N9:(Mul w32 4 N1) U2)))
-#   OK -- Elapsed: 0.00105405
+#   OK -- Elapsed: 0.00104594
 #   Is Valid: false
 
 # Query 16 -- Type: InitialValues, Instructions: 135
+array arr5[64] : w32 -> w8 = symbolic
+array arr53[4] : w32 -> w8 = symbolic
+array arr49[4] : w32 -> w8 = symbolic
+array arr74[4] : w32 -> w8 = symbolic
+array arr60[4] : w32 -> w8 = symbolic
+array arr67[4] : w32 -> w8 = symbolic
 (query [(Ult N0:(ReadLSB w32 0 arr53)
              16)
         (Ult N1:(ReadLSB w32 0 arr60)
@@ -278,7 +336,7 @@
         arr60
         arr67
         arr74])
-#   OK -- Elapsed: 0.00058198
+#   OK -- Elapsed: 0.000574112
 #   Solvable: true
 #     arr49 = [104,0,0,0]
 #     arr53 = [12,0,0,0]
diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.pc
index af94b516..ea2e7a5d 100644
--- a/test/Expr/Parser/MultiByteReads.pc
+++ b/test/Expr/Parser/MultiByteReads.pc
@@ -2,6 +2,9 @@
 # RUN: grep -q "(ReadLSB w32 4 arr1)" log
 # RUN: grep -q "(ReadMSB w32 2 arr2)" log
 
+array arr1[8] : w32 -> w8 = symbolic
+array arr2[8] : w32 -> w8 = symbolic
+
 (query [(Not (Slt 100
                   (Concat w32 (Read w8 7 arr1)
                               (Concat w24 (Read w8 6 arr1)
diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc
index 9e29d0db..66991c20 100644
--- a/test/Expr/Parser/TypeChecking.pc
+++ b/test/Expr/Parser/TypeChecking.pc
@@ -2,13 +2,15 @@
 
 
 
-# RUN: grep "TypeChecking.pc:6:9: error: type widths do not match in binary expression" %t.log
+# RUN: grep "TypeChecking.pc:7:9: error: type widths do not match in binary expression" %t.log
+array arr1[8] : w32 -> w8 = symbolic
 (query [(Eq (ReadLSB w32 0 arr1) true)] 
        false)
 
-# 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
+# RUN: grep "TypeChecking.pc:14:25: error: invalid write index (doesn't match array domain)" %t.log
+# RUN: grep "TypeChecking.pc:14: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)
+array arr2[8] : w32 -> w8 = symbolic
+(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)
 
 # RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log
diff --git a/www/KQuery.html b/www/KQuery.html
index db0d2b59..f0aaffae 100644
--- a/www/KQuery.html
+++ b/www/KQuery.html
@@ -265,13 +265,18 @@
   <p><b>Syntax:</b></p>
   <div class="syntax">
     array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range "=" array-initializer<br>
-    array-initializer = "symbolic" | "{" { numeric-literal } "}"<br>
+    array-initializer = "symbolic" | "[" { numeric-literal } "]"<br>
   </div>
 
+  <p>Arrays can be initialized to be either symbolic, or to have a given list of
+  constant values. For constant arrays, the initializer list must exactly match
+  the size of the array (if the size was unspecified, it will be the number of
+  constant values).</p>
+
   <p><b>Examples:</b></p>
   <div class="example">
     array foo[10] : w32 -> w8 = symbolic <font color="Red"># A ten element symbolic array</font><br>
-    array foo[4] : w8 -> w1 = { true, false, false, true } <font color="Red"># A constant array of four booleans</font><br>
+    array foo[] : w8 -> w1 = [ true, false, false, true ] <font color="Red"># A constant array of four booleans</font><br>
   </div>
   
   <h3><a name="query_commands">Query Commands</a></h3>