[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.

2 files changed, 39 insertions, 2 deletions

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