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

2 files changed, 22 insertions, 2 deletions

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,