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

1 files changed, 38 insertions, 0 deletions

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