From 1398e960ec9aca3f0ceac5e37062631986b9c2a8 Mon Sep 17 00:00:00 2001 From: Lukáš Zaoral Date: Sun, 17 Apr 2022 13:32:15 +0200 Subject: 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 --- test/ArrayOpt/test_multindex_multarray.c | 46 ++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 test/ArrayOpt/test_multindex_multarray.c (limited to 'test') 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 + +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; +} -- cgit 1.4.1