[optimize-array] Fix update list read order

ArrayExprOptimizer read the UpdateList in the wrong order, which
meant that it used least recent update instead of the most recent one.
This patch fixes this as well as adds a test to illustrate the issue.

2 files changed, 60 insertions, 2 deletions

diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 1a48adfe..e43530ec 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -280,8 +280,17 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
       // assume that the UpdateNodes contain ConstantExpr indexes and values
       assert(read->updates.root->isConstantArray() &&
              "Expected concrete array, found symbolic array");
+
+      // We need to read updates from lest recent to most recent, therefore
+      // reverse the list
+      std::vector<const UpdateNode *> us;
+      us.reserve(read->updates.getSize());
+      for (const UpdateNode *un = read->updates.head; un; un = un->next)
+        us.push_back(un);
+
       auto arrayConstValues = read->updates.root->constantValues;
-      for (const UpdateNode *un = read->updates.head; un; un = un->next) {
+      for (auto it = us.rbegin(); it != us.rend(); it++) {
+        const UpdateNode *un = *it;
         auto ce = dyn_cast<ConstantExpr>(un->index);
         assert(ce && "Not a constant expression");
         uint64_t index = ce->getAPValue().getZExtValue();
@@ -356,7 +365,16 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
           arrayConstValues.push_back(ConstantExpr::create(0, Expr::Int8));
         }
       }
-      for (const UpdateNode *un = read->updates.head; un; un = un->next) {
+
+      // We need to read updates from lest recent to most recent, therefore
+      // reverse the list
+      std::vector<const UpdateNode *> us;
+      us.reserve(read->updates.getSize());
+      for (const UpdateNode *un = read->updates.head; un; un = un->next)
+        us.push_back(un);
+
+      for (auto it = us.rbegin(); it != us.rend(); it++) {
+        const UpdateNode *un = *it;
         auto ce = dyn_cast<ConstantExpr>(un->index);
         assert(ce && "Not a constant expression");
         uint64_t index = ce->getAPValue().getLimitedValue();
diff --git a/test/ArrayOpt/test_update_list_order.c b/test/ArrayOpt/test_update_list_order.c
new file mode 100644
index 00000000..1c6ed951
--- /dev/null
+++ b/test/ArrayOpt/test_update_list_order.c
@@ -0,0 +1,40 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --optimize-array=value --use-query-log=all:kquery --write-kqueries --output-dir=%t.klee-out %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: FileCheck %s -input-file=%t.log
+// RUN: rm -rf %t.klee-out
+
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
+// CHECK-CONST_ARR: const_arr
+
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdio.h>
+
+char array[5] = {1, 2, 3, 4, 5};
+
+int main() {
+  char idx;
+  char updateListBreaker;
+  klee_make_symbolic(&updateListBreaker, sizeof(updateListBreaker), "ulBreak");
+  klee_make_symbolic(&idx, sizeof(idx), "idx");
+  klee_assume(idx < 5);
+  klee_assume(idx > 0);
+  klee_assume(updateListBreaker != 3);
+  array[0] = updateListBreaker;
+  array[2] = 6;
+  updateListBreaker = array[idx];
+  array[2] = 3;
+  assert(updateListBreaker != 3 && "keep updateListBreak alive");
+
+  // CHECK: KLEE: done: completed paths = 2
+  // CHECK: No
+  // CHECK-NEXT: Yes
+  if (array[idx] == 3)
+    printf("Yes\n");
+  else
+    printf("No\n");
+
+  return 0;
+}