about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorLukáš Zaoral <lzaoral@redhat.com>2022-04-17 13:32:15 +0200
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2023-03-20 16:05:38 +0000
commit1398e960ec9aca3f0ceac5e37062631986b9c2a8 (patch)
treeff7ed01317fa2ef90b9678c8ea1bc86fb94ba531 /test
parentd9da9eadbc0aacf61b336231560abb67bcba91ad (diff)
downloadklee-1398e960ec9aca3f0ceac5e37062631986b9c2a8.tar.gz
ConstantArrayExprVisitor: Fix detection of multiple array indices
Previously, the code did two consecutive checks.  First one succeeded
only if the given index was not already seen and the second one did
an analogous check but for arrays.  However, if the given index usage
was already detected for some array, its usage for another array that
already had some other index detected would be silently skipped and the
`incompatible` flag would not be set.

Therefore, if the code contained e.g. the following conditional jump on two
arrays with two symbolic indices, the multi-index access would remain
undetected:

if ((array1[k] + array2[x] + array2[k]) == 0)

Resulting in the following output:

KLEE: WARNING: OPT_I: infeasible branch!
KLEE: WARNING: OPT_I: successful
Diffstat (limited to 'test')
-rw-r--r--test/ArrayOpt/test_multindex_multarray.c46
1 files changed, 46 insertions, 0 deletions
diff --git a/test/ArrayOpt/test_multindex_multarray.c b/test/ArrayOpt/test_multindex_multarray.c
new file mode 100644
index 00000000..54e91f48
--- /dev/null
+++ b/test/ArrayOpt/test_multindex_multarray.c
@@ -0,0 +1,46 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1
+// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1
+// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V
+// RUN: test -f %t.klee-out/test000001.kquery
+// RUN: test -f %t.klee-out/test000002.kquery
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR
+// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR
+
+// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful
+// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
+// CHECK-CONST_ARR: const_arr
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+char array1[5] = {0, 1, 2, 3, 4};
+char array2[5] = {0, 1, 2, 3, 4};
+
+int main() {
+  unsigned k;
+  unsigned x;
+
+  klee_make_symbolic(&k, sizeof(k), "k");
+  klee_assume(k < 5);
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_assume(x < 5);
+
+  // CHECK: Yes
+  if ((array1[k] + array2[x] + array2[k]) - 7 == 0)
+    printf("Yes\n");
+
+  // CHECK: KLEE: done: completed paths = 2
+
+  return 0;
+}