More constant Array support.

 - The are parsed, printed, and solved now.

 - Remove some members of ArrayDecl which are only duplicates of Array members.

 - KLEE still doesn't create these, but you can write them by hand.

The EXE style constant array optimization for STP (turning the initial writes
into asserts) is now only a stones throw away, but I need to leave something fun
to do tomorrow. :)


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

6 files changed, 59 insertions, 33 deletions

diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index 65105f12..f67e27ab 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -71,16 +71,12 @@ namespace expr {
   ///
   /// For example:
   ///   array obj[] : w32 -> w8 = symbolic
-  ///   array obj[32] : w32 -> w8 = { ... }
+  ///   array obj[32] : w32 -> w8 = [ ... ]
   class ArrayDecl : public Decl {
   public:
     /// Name - The name of this array.
     const Identifier *Name;
 
-    /// Size - The maximum array size (or 0 if unspecified). Concrete
-    /// arrays always are specified with a size.
-    const uint64_t Size;
-
     /// Domain - The width of indices.
     const unsigned Domain;
 
@@ -90,17 +86,12 @@ namespace expr {
     /// Root - The root array object defined by this decl.
     const Array *Root;
 
-    /// Contents - The initial contents of the array. The array is
-    /// symbolic if no contents are specified. The contained
-    /// expressions are guaranteed to be constants.
-    const std::vector<ExprHandle> Contents;
-
   public:
     ArrayDecl(const Identifier *_Name, uint64_t _Size, 
               unsigned _Domain, unsigned _Range,
               const Array *_Root)
       : Decl(ArrayDeclKind), Name(_Name), 
-        Size(_Size), Domain(_Domain), Range(_Range), 
+        Domain(_Domain), Range(_Range), 
         Root(_Root) {
     }
 
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index e3a83f9a..6ad5fffd 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -532,8 +532,18 @@ void ExprPPrinter::printQuery(std::ostream &os,
       // FIXME: Print correct name, domain, and range.
       PC << "array " << A->name
          << "[" << A->size << "]"
-         << " : " << "w32" << " -> " << "w8"
-         << " = symbolic";
+         << " : " << "w32" << " -> " << "w8" << " = ";
+      if (A->isSymbolicArray()) {
+        PC << "symbolic";
+      } else {
+        PC << "[";
+        for (unsigned i = 0, e = A->size; i != e; ++i) {
+          if (i)
+            PC << " ";
+          PC << A->constantValues[i];
+        }
+        PC << "]";
+      }
       PC.breakLine();
     }
   }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 8e5349c5..1f2f8412 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -407,7 +407,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
   IntegerResult Size;
   TypeResult DomainType;
   TypeResult RangeType;
-  std::vector<ExprHandle> Values;
+  std::vector< ref<ConstantExpr> > Values;
 
   ConsumeToken();
   
@@ -458,7 +458,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
 
       ExprResult Res = ParseNumber(RangeType.get());
       if (Res.isValid())
-        Values.push_back(Res.get());
+        Values.push_back(cast<ConstantExpr>(Res.get()));
     }
     ConsumeRSquare();
   } else {
@@ -502,11 +502,6 @@ DeclResult ParserImpl::ParseArrayDecl() {
     Values.clear();
   }
 
-  if (!Values.empty()) {
-    Error("constant arrays are not yet supported.");
-    Values.clear();
-  }
-
   // FIXME: Validate that this array is undeclared.
 
  exit:
@@ -519,7 +514,12 @@ DeclResult ParserImpl::ParseArrayDecl() {
 
   // FIXME: Array should take domain and range.
   const Identifier *Label = GetOrCreateIdentifier(Name);
-  Array *Root = new Array(Label->Name, Size.get());
+  Array *Root;
+  if (!Values.empty())
+    Root = new Array(Label->Name, Size.get(),
+                     &Values[0], &Values[0] + Values.size());
+  else
+    Root = new Array(Label->Name, Size.get());
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
                                 DomainType.get(), RangeType.get(), Root);
 
@@ -1554,22 +1554,20 @@ void ParserImpl::Error(const char *Message, const Token &At) {
 Decl::Decl(DeclKind _Kind) : Kind(_Kind) {}
 
 void ArrayDecl::dump() {
-  // FIXME: For now, print using the Array* "name".
   std::cout << "array " << Root->name
-            << "[" << Size << "]"
+            << "[" << Root->size << "]"
             << " : " << 'w' << Domain << " -> " << 'w' << Range << " = ";
 
-  if (Contents.empty()) {
+  if (Root->isSymbolicArray()) {
     std::cout << "symbolic\n";
   } else {
-    std::cout << '{';
-    for (std::vector<ExprHandle>::const_iterator it = Contents.begin(),
-           ie = Contents.end(); it != ie;) {
-      std::cout << *it;
-      if (++it != ie)
+    std::cout << '[';
+    for (unsigned i = 0, e = Root->size; i != e; ++i) {
+      if (i)
         std::cout << " ";
+      std::cout << Root->constantValues[i];
     }
-    std::cout << "}\n";
+    std::cout << "]\n";
   }
 }
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 6d0a1b62..ab65f254 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -385,8 +385,6 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
 }
 
 ::VCExpr STPBuilder::getInitialArray(const Array *root) {
-  assert(root->isSymbolicArray() && "FIXME: Support constant arrays!");
-
   if (root->stpInitialArray) {
     return root->stpInitialArray;
   } else {
@@ -395,6 +393,21 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width
     char buf[32];
     sprintf(buf, "%s_%p", root->name.c_str(), (void*) root);
     root->stpInitialArray = buildArray(buf, 32, 8);
+
+    if (root->isConstantArray()) {
+      // FIXME: Flush the concrete values into STP. Ideally we would do this
+      // using assertions, which is much faster, but we need to fix the caching
+      // to work correctly in that case.
+      for (unsigned i = 0, e = root->size; i != e; ++i) {
+        ::VCExpr prev = root->stpInitialArray;
+        root->stpInitialArray = 
+          vc_writeExpr(vc, prev,
+                       construct(ConstantExpr::alloc(i, root->getDomain()), 0),
+                       construct(root->constantValues[i], 0));
+        vc_DeleteExpr(prev);
+      }
+    }
+
     return root->stpInitialArray;
   }
 }
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 71516c24..7a1b356c 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -675,6 +675,13 @@ STPSolverImpl::computeInitialValues(const Query &query,
 
   ExprHandle stp_e = builder->construct(query.expr);
      
+  if (0) {
+    char *buf;
+    unsigned long len;
+    vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
+    fprintf(stderr, "note: STP query: %.*s\n", (unsigned) len, buf);
+  }
+
   bool success;
   if (useForkedSTP) {
     success = runAndGetCexForked(vc, builder, stp_e, objects, values, 
diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc
index 0dac0cc8..418a712d 100644
--- a/test/Expr/Evaluate.pc
+++ b/test/Expr/Evaluate.pc
@@ -13,4 +13,11 @@ array arr1[8] : w32 -> w8 = symbolic
 (query [(Eq N0:(ReadLSB w32 0 arr1) 10)
         (Eq N1:(ReadLSB w32 4 arr1) 20)]
        (Eq (Add w32 N0 N1)
-           30))
\ No newline at end of file
+           30))
+
+# RUN: grep "Query 2:	VALID" %t.log
+# Query 2
+array hello[4] : w32 -> w8 = [ 1 2 3 5 ]
+(query [] (Eq (Add w8 (Read w8 0 hello)
+                      (Read w8 3 hello))
+              6))