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

3 files changed, 24 insertions, 59 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();
   }