From b715ffa0c805f4d4813f0cda8b17eeb618e1ebf0 Mon Sep 17 00:00:00 2001
From: Timotej Kapus <tk1713@ic.ac.uk>
Date: Fri, 8 Nov 2019 12:25:59 +0000
Subject: [optimize-array] Fix hole index in buildMixedSelectExpr

buildMixedSelectExpr was using the byte index for holes in the
select condition instead of the word based one. This only occured
if there was more than 1 hole.
---
 lib/Expr/ArrayExprOptimizer.cpp |  3 +--
 test/ArrayOpt/test_mixed_hole.c | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100644 test/ArrayOpt/test_mixed_hole.c

diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 8ba0b40d..b55974d0 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -643,8 +643,7 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr(
         ref<Expr> temp_idx = MulExpr::create(
             ConstantExpr::create(holes[i], re->index->getWidth()),
             ConstantExpr::create(width / 8, re->index->getWidth()));
-        ref<Expr> cond = EqExpr::create(
-            re->index, ConstantExpr::create(holes[i], re->index->getWidth()));
+        ref<Expr> cond = EqExpr::create(re->index, temp_idx);
         ref<Expr> temp = SelectExpr::create(
             cond, extendRead(re->updates, temp_idx, width), result);
         result = temp;
diff --git a/test/ArrayOpt/test_mixed_hole.c b/test/ArrayOpt/test_mixed_hole.c
new file mode 100644
index 00000000..1a95a5ef
--- /dev/null
+++ b/test/ArrayOpt/test_mixed_hole.c
@@ -0,0 +1,38 @@
+// 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
+
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
+// CHECK-CONST_ARR: const_arr
+
+#include "klee/klee.h"
+#include <assert.h>
+#include <stdio.h>
+
+short array[6] = {1, 2, 3, 4, 5, 0};
+
+int main() {
+  char idx;
+  short symHole, symHole2;
+  klee_make_symbolic(&symHole, sizeof(symHole), "hole");
+  klee_make_symbolic(&symHole2, sizeof(symHole2), "hole2");
+  klee_make_symbolic(&idx, sizeof(idx), "idx");
+  klee_assume(idx < 5);
+  klee_assume(idx > 0);
+  klee_assume((symHole < 401) & (symHole > 399));
+  klee_assume(symHole2 != 400);
+  array[2] = symHole;
+  array[0] = symHole2;
+
+  // CHECK: KLEE: done: completed paths = 2
+  // CHECK: Yes
+  // CHECK-NEXT: No
+  if (array[idx + 1] == 400)
+    printf("Yes\n");
+  else
+    printf("No\n");
+
+  return 0;
+}
-- 
cgit 1.4.1