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, 30 insertions, 10 deletions

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 {