From 85c22c2486c79b463451aeeba56a33313d4e460d Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Wed, 30 Oct 2019 10:48:05 +0000 Subject: [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. --- test/ArrayOpt/test_expr_arbitrary.c | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test/ArrayOpt/test_expr_arbitrary.c (limited to 'test/ArrayOpt/test_expr_arbitrary.c') 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 + +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; +} -- cgit 1.4.1