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, 35 insertions, 11 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));
 }