[optimize-array] Fix value transformation

Value transformation operates on word instead of byte arrays.
That means the Read indicies need to be adjusted to reflect that.
Previously IndexCleanerVisitor tried to remove the multiplications in the index
to covert byte indicies to word indicies. However as the two added test cases show
this is not sufficent. Therefore we remove the IndexCleanerVisistor and just divide
the index with word size which should always be correct.

2 files changed, 74 insertions, 0 deletions

diff --git a/test/ArrayOpt/test_expr_arbitrary.c b/test/ArrayOpt/test_expr_arbitrary.c
new file mode 100644
index 00000000..145efea9
--- /dev/null
+++ b/test/ArrayOpt/test_expr_arbitrary.c
@@ -0,0 +1,35 @@
+// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --use-query-log=all:kquery --output-dir=%t.klee-out %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --optimize-array=value --write-kqueries --use-query-log=all:kquery --output-dir=%t.klee-out %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-V
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+short array[10] = {42, 1, 42, 42, 2, 5, 6, 42, 8, 9};
+
+int main() {
+  char k;
+  // CHECK-V: KLEE: WARNING: OPT_V: successful
+
+  klee_make_symbolic(&k, sizeof(k), "k");
+  klee_assume(k < 4);
+  klee_assume(k >= 0);
+
+  short *ptrs[4] = {array + 3, array + 0, array + 7, array + 2};
+
+  // CHECK-DAG: Yes
+  if ((*(ptrs[k])) == 42)
+    printf("Yes\n");
+  else
+    printf("No\n");
+
+  // CHECK-DAG: KLEE: done: completed paths = 1
+  // CHECK-NOT: No
+
+  return 0;
+}
diff --git a/test/ArrayOpt/test_expr_mul.c b/test/ArrayOpt/test_expr_mul.c
new file mode 100644
index 00000000..c2b0b22e
--- /dev/null
+++ b/test/ArrayOpt/test_expr_mul.c
@@ -0,0 +1,39 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --use-query-log=all:kquery --output-dir=%t.klee-out %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --optimize-array=value --write-kqueries --use-query-log=all:kquery --output-dir=%t.klee-out %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-V
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+char array[10] = {1, 2, 3, 2, 5, 6, 5, 8, 9, 10};
+char array2[10] = {0, 1, 7, 19, 20, 21, 22, 23, 24, 25};
+
+int main() {
+  char k;
+  // CHECK-V: KLEE: WARNING: OPT_V: successful
+
+  klee_make_symbolic(&k, sizeof(k), "k");
+  klee_assume(k < 4);
+  klee_assume(k >= 1);
+
+  // CHECK-DAG: Yes
+  // CHECK-DAG: Yes
+  char r = (array[k] * 3) & 1;
+  char v = array2[r];
+  if (v == 0)
+    printf("Yes\n");
+  else if (v == 1)
+    printf("Yes\n");
+  else
+    printf("No\n");
+
+  // CHECK-DAG: KLEE: done: completed paths = 2
+  // CHECK-NOT: No
+
+  return 0;
+}