Add initial support for constant Arrays.

 - This doesn't actually start using them, it just attempts to update all
   clients to do the right thing in the presence of them.


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

6 files changed, 54 insertions, 69 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 3f5ef95f..2b6f3d96 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -888,73 +888,33 @@ static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 /// returns the initial equality expression. 
 static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl, 
 				  ReadExpr *rd) {
-  assert(rd->getKind() == Expr::Read && "read expression required");
-  
   uint64_t ct = cl->getConstantValue();
-  ref<Expr> first_idx_match;
 
-  // number of positions in the array that contain value ct
-  unsigned matches = 0;
+  if (rd->updates.root->isSymbolicArray() || rd->updates.getSize())
+    return EqExpr_create(cl, rd);
 
-  //llvm::cerr << "Size updates/root: " << rd->updates.getSize() << " / " << (rd->updates.root)->size << "\n";
+  // Number of positions in the array that contain value ct.
+  unsigned numMatches = 0;
 
   // for now, just assume standard "flushing" of a concrete array,
   // where the concrete array has one update for each index, in order
-  bool all_const = true;
-  if (rd->updates.getSize() == rd->updates.root->size) {
-    unsigned k = rd->updates.getSize();
-    for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
-      assert(k > 0);
-      k--;
-
-      ref<Expr> idx = un->index;
-      ref<Expr> val = un->value;
-      ConstantExpr *idxCE = dyn_cast<ConstantExpr>(idx);
-      ConstantExpr *valCE = dyn_cast<ConstantExpr>(val);
-      if (!idxCE || !valCE) {
-        all_const = false;
-        break;
-      }
-
-      if (idxCE->getConstantValue() != k) {
-        all_const = false;
-        break;
-      }
-      if (valCE->getConstantValue() == ct) {
-        matches++;
-        if (matches == 1)
-          first_idx_match = un->index;
-      }
-    }
-  }
-  else all_const = false;
-  
-  if (all_const && matches <= 100) {
-    // apply optimization
-    //llvm::cerr << "\n\n=== Applying const array optimization ===\n\n";
-
-    if (matches == 0)
-      return ConstantExpr::alloc(0, Expr::Bool);
-
-    ref<Expr> res = EqExpr::create(first_idx_match, rd->index);
-    if (matches == 1)
-      return res;
-    
-    for (const UpdateNode *un = rd->updates.head; un; un = un->next) {
-      if (un->index != first_idx_match && 
-          cast<ConstantExpr>(un->value)->getConstantValue() == ct) {
-	ref<Expr> curr_eq = EqExpr::create(un->index, rd->index);
-	res = OrExpr::create(curr_eq, res);
-      }
+  ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
+  for (unsigned i = 0, e = rd->updates.root->size; i != e; ++i) {
+    if (ct == rd->updates.root->constantValues[i]->getConstantValue()) {
+      // Arbitrary maximum on the size of disjunction.
+      if (++numMatches > 100)
+        return EqExpr_create(cl, rd);
+      
+      ref<Expr> mayBe = 
+        EqExpr::create(rd->index, ConstantExpr::alloc(i, 
+                                                      rd->index->getWidth()));
+      res = OrExpr::create(res, mayBe);
     }
-    
-    return res;
   }
 
-  return EqExpr_create(cl, ref<Expr>(rd));
+  return res;
 }
 
-
 static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {  
   uint64_t value = cl->getConstantValue();
   Expr::Width width = cl->getWidth();
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index bf229731..41cb7c48 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -25,10 +25,14 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
       // version though (mostly for debugging).
       
       return Action::changeTo(ReadExpr::create(UpdateList(ul.root, un), 
-                                               ConstantExpr::alloc(index, Expr::Int32)));
+                                               ConstantExpr::alloc(index, 
+                                                                   ul.root->getDomain())));
     }
   }
   
+  if (ul.root->isConstantArray() && index < ul.root->size)
+    return Action::changeTo(ul.root->constantValues[index]);
+
   return Action::changeTo(getInitialValue(*ul.root, index));
 }
 
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 1213edeb..ed60a4a9 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -89,8 +89,9 @@ protected:
       visit(un->value);
     }
 
-    if (results.insert(ul.root).second)
-      objects.push_back(ul.root);
+    if (ul.root->isSymbolicArray())
+      if (results.insert(ul.root).second)
+        objects.push_back(ul.root);
 
     return Action::doChildren();
   }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 608388bb..af2666ab 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -341,7 +341,13 @@ public:
   CexRangeEvaluator(std::map<const Array*, CexObjectData*> &_objects) 
     : objects(_objects) {}
 
-  ValueRange getInitialReadRange(const Array &os, ValueRange index) {
+  ValueRange getInitialReadRange(const Array &array, ValueRange index) {
+    // Check for a concrete read of a constant array.
+    if (array.isConstantArray() && 
+        index.isFixed() && 
+        index.min() < array.size)
+      return ValueRange(array.constantValues[index.min()]->getConstantValue());
+
     return ValueRange(0, 255);
   }
 };
@@ -765,16 +771,22 @@ public:
 
       // We reached the initial array write, update the exact range if possible.
       if (index.isFixed()) {
-        CexValueData cvd = cod.getExactValues(index.min());
-        if (range.min() > cvd.min()) {
-          assert(range.min() <= cvd.max());
-          cvd = CexValueData(range.min(), cvd.max());
-        }
-        if (range.max() < cvd.max()) {
-          assert(range.max() >= cvd.min());
-          cvd = CexValueData(cvd.min(), range.max());
+        if (array->isConstantArray()) {
+          // Verify the range.
+          propogateExactValues(array->constantValues[index.min()],
+                               range);
+        } else {
+          CexValueData cvd = cod.getExactValues(index.min());
+          if (range.min() > cvd.min()) {
+            assert(range.min() <= cvd.max());
+            cvd = CexValueData(range.min(), cvd.max());
+          }
+          if (range.max() < cvd.max()) {
+            assert(range.max() >= cvd.min());
+            cvd = CexValueData(cvd.min(), range.max());
+          }
+          cod.setExactValues(index.min(), cvd);
         }
-        cod.setExactValues(index.min(), cvd);
       }
       break;
     }
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 69f9567c..1f3ea798 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -95,6 +95,12 @@ public:
     for (unsigned i = 0; i != reads.size(); ++i) {
       ReadExpr *re = reads[i].get();
       const Array *array = re->updates.root;
+      
+      // Reads of a constant array don't alias.
+      if (re->updates.root->isConstantArray() &&
+          !re->updates.head)
+        continue;
+
       if (!wholeObjects.count(array)) {
         if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
           DenseSet<unsigned> &dis = elements[array];
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 856540fe..6d0a1b62 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -385,6 +385,8 @@ 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 {