From d8deadd787d0f857d701b73aeaa3e0753efd9405 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <tk1713@ic.ac.uk>
Date: Thu, 7 Nov 2019 14:27:07 +0000
Subject: [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.
---
 lib/Expr/ArrayExprOptimizer.cpp        | 22 +++++++++++++++++--
 test/ArrayOpt/test_update_list_order.c | 40 ++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 2 deletions(-)
 create mode 100644 test/ArrayOpt/test_update_list_order.c

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;
+}
-- 
cgit 1.4.1