From d8deadd787d0f857d701b73aeaa3e0753efd9405 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Thu, 7 Nov 2019 14:27:07 +0000 Subject: [optimize-array] Fix update list read order ArrayExprOptimizer read the UpdateList in the wrong order, which meant that it used least recent update instead of the most recent one. This patch fixes this as well as adds a test to illustrate the issue. --- test/ArrayOpt/test_update_list_order.c | 40 ++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 test/ArrayOpt/test_update_list_order.c (limited to 'test/ArrayOpt') diff --git a/test/ArrayOpt/test_update_list_order.c b/test/ArrayOpt/test_update_list_order.c new file mode 100644 index 00000000..1c6ed951 --- /dev/null +++ b/test/ArrayOpt/test_update_list_order.c @@ -0,0 +1,40 @@ +// 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 +// RUN: rm -rf %t.klee-out + +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful +// CHECK-CONST_ARR: const_arr + +#include "klee/klee.h" +#include +#include + +char array[5] = {1, 2, 3, 4, 5}; + +int main() { + char idx; + char updateListBreaker; + klee_make_symbolic(&updateListBreaker, sizeof(updateListBreaker), "ulBreak"); + klee_make_symbolic(&idx, sizeof(idx), "idx"); + klee_assume(idx < 5); + klee_assume(idx > 0); + klee_assume(updateListBreaker != 3); + array[0] = updateListBreaker; + array[2] = 6; + updateListBreaker = array[idx]; + array[2] = 3; + assert(updateListBreaker != 3 && "keep updateListBreak alive"); + + // CHECK: KLEE: done: completed paths = 2 + // CHECK: No + // CHECK-NEXT: Yes + if (array[idx] == 3) + printf("Yes\n"); + else + printf("No\n"); + + return 0; +} -- cgit 1.4.1