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

9 files changed, 89 insertions, 80 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 73734da3..9afbabd7 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -476,6 +476,11 @@ public:
   // FIXME: Not 64-bit clean.
   unsigned size;
 
+  /// constantValues - The constant initial values for this array, or empty for
+  /// a symbolic array. If non-empty, this size of this array is equivalent to
+  /// the array size.
+  const std::vector< ref<ConstantExpr> > constantValues;
+
   // FIXME: This does not belong here.
   mutable void *stpInitialArray;
 
@@ -487,18 +492,34 @@ public:
   /// when printing expressions. When expressions are printed the output will
   /// not parse correctly since two arrays with the same name cannot be
   /// distinguished once printed.
-  Array(const std::string &_name, uint64_t _size) 
-    : name(_name), size(_size), stpInitialArray(0) {}
+  Array(const std::string &_name, uint64_t _size, 
+        const ref<ConstantExpr> *constantValuesBegin = 0,
+        const ref<ConstantExpr> *constantValuesEnd = 0)
+    : name(_name), size(_size), 
+      constantValues(constantValuesBegin, constantValuesEnd), 
+      stpInitialArray(0) {
+    assert((isSymbolicArray() || constantValues.size() == size) &&
+           "Invalid size for constant array!");
+#ifdef NDEBUG
+    for (const ref<ConstantExpr> *it = constantValuesBegin;
+         it != constantValuesEnd; ++it)
+      assert(it->getWidth() == getRange() &&
+             "Invalid initial constant value!");
+#endif
+  }
   ~Array() {
     // FIXME: This relies on caller to delete the STP array.
     assert(!stpInitialArray && "Array must be deleted by caller!");
   }
+
+  bool isSymbolicArray() const { return constantValues.empty(); }
+  bool isConstantArray() const { return !isSymbolicArray(); }
+
+  Expr::Width getDomain() const { return Expr::Int32; }
+  Expr::Width getRange() const { return Expr::Int8; }
 };
 
-/// Class representing a complete list of updates into an array. 
-/** The main trick is the isRooted bit, which enables important optimizations. 
-    ...
- */
+/// Class representing a complete list of updates into an array.
 class UpdateList { 
   friend class ReadExpr; // for default constructor
 
diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h
index 739e51e6..6b67a1cf 100644
--- a/include/klee/util/ExprEvaluator.h
+++ b/include/klee/util/ExprEvaluator.h
@@ -29,10 +29,11 @@ namespace klee {
   public:
     ExprEvaluator() {}
 
-    // override to implement evaluation, this function is called to
-    // get the initial value for a symbolic byte. if the value is
-    // unknown then the user can simply return a ReadExpr at version 0
-    // of this MemoryObject.
+    /// getInitialValue - Return the initial value for a symbolic byte.
+    ///
+    /// This will only be called for constant arrays if the index is
+    /// out-of-bounds. If the value is unknown then the user should return a
+    /// ReadExpr at the initial version of this array.
     virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0;
   };
 }
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h
index 2dafd6ff..61444c76 100644
--- a/include/klee/util/ExprRangeEvaluator.h
+++ b/include/klee/util/ExprRangeEvaluator.h
@@ -55,6 +55,8 @@ public:
 template<class T>
 class ExprRangeEvaluator {
 protected:
+  /// getInitialReadRange - Return a range for the initial value of the given
+  /// array (which may be constant), for the given range of indices.
   virtual T getInitialReadRange(const Array &os, T index) = 0;
 
   T evalRead(const UpdateList &ul, T index);
@@ -83,7 +85,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
       } 
     }
   }
-
+  
   return res.set_union(getInitialReadRange(*ul.root, index));
 }
 
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 {