Fix representation of ReadExpr of equivalent arrays

ObjectStates can be shared between multiple states.
A read expression of a symbolic object can be represented differently
depending on previous read expression on the same object.

If the read expression uses a symbolic index, all pending updates
will become entries in the update list of the object state.
If the same object state is read again, with a concrete index,
the latest update list item will be referenced, even though it might
contain more recent but non-essential updates.

If, instead, a concrete read will be executed first, it does not contain
the non-essential updates.

For both executions, the ReadExpr with a constant index will have two
different representations, which is not intented.

This patch makes sure, we do not include more recent, non-essential
updates for concrete reads.

Fixes #921

1 files changed, 22 insertions, 8 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 93b6c213..54f68f21 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -531,29 +531,30 @@ unsigned Array::computeHash() {
 /***/
 
 ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
-  // rollback index when possible... 
-
-  // XXX this doesn't really belong here... there are basically two
-  // cases, one is rebuild, where we want to optimistically try various
-  // optimizations when the index has changed, and the other is 
-  // initial creation, where we expect the ObjectState to have constructed
-  // a smart UpdateList so it is not worth rescanning.
+  // rollback update nodes if possible
 
+  // Iterate throught the update list from the most recent to the
+  // least reasent to find a potential written value for a concrete index;
+  // stop, if an update with symbolic has been found as we don't know which
+  // array element has been updated
   const UpdateNode *un = ul.head;
   bool updateListHasSymbolicWrites = false;
   for (; un; un=un->next) {
+    // Check if we have an equivalent concrete index
     ref<Expr> cond = EqExpr::create(index, un->index);
-    
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
       if (CE->isTrue())
+        // Return the found value
         return un->value;
     } else {
+      // Found write with symbolic index
       updateListHasSymbolicWrites = true;
       break;
     }
   }
 
   if (ul.root->isConstantArray() && !updateListHasSymbolicWrites) {
+    // No updates with symbolic index to a constant array have been found
     if (ConstantExpr *CE = dyn_cast<ConstantExpr>(index)) {
       assert(CE->getWidth() <= 64 && "Index too large");
       uint64_t concreteIndex = CE->getZExtValue();
@@ -564,6 +565,19 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
     }
   }
 
+  // Now, no update with this concrete index exists
+  // Try to remove any most recent but unimportant updates
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(index)) {
+    assert(CE->getWidth() <= 64 && "Index too large");
+    uint64_t concreteIndex = CE->getZExtValue();
+    uint64_t size = ul.root->size;
+    if (concreteIndex < size) {
+      // Create shortened update list
+      UpdateList newUpdateList(ul.root, un);
+      return ReadExpr::alloc(newUpdateList, index);
+    }
+  }
+
   return ReadExpr::alloc(ul, index);
 }