From 60b5c574ea565b3132cc60d946d87a4d1243801b Mon Sep 17 00:00:00 2001 From: Lukas Wölfer Date: Sat, 24 Jun 2017 19:59:48 +0200 Subject: Implemented bounded merging functionality --- test/Merging/batching_break.c | 42 ++++++++++++++++++++++++++++++++++++ test/Merging/easy_merge.c | 44 +++++++++++++++++++++++++++++++++++++ test/Merging/indirect_value.c | 32 +++++++++++++++++++++++++++ test/Merging/loop_merge.c | 38 ++++++++++++++++++++++++++++++++ test/Merging/merge_fail.c | 36 +++++++++++++++++++++++++++++++ test/Merging/nested_merge.c | 48 +++++++++++++++++++++++++++++++++++++++++ test/Merging/split_merge.c | 41 +++++++++++++++++++++++++++++++++++ test/Merging/unexpected_close.c | 35 ++++++++++++++++++++++++++++++ 8 files changed, 316 insertions(+) create mode 100644 test/Merging/batching_break.c create mode 100644 test/Merging/easy_merge.c create mode 100644 test/Merging/indirect_value.c create mode 100644 test/Merging/loop_merge.c create mode 100644 test/Merging/merge_fail.c create mode 100644 test/Merging/nested_merge.c create mode 100644 test/Merging/split_merge.c create mode 100644 test/Merging/unexpected_close.c (limited to 'test') diff --git a/test/Merging/batching_break.c b/test/Merging/batching_break.c new file mode 100644 index 00000000..67570734 --- /dev/null +++ b/test/Merging/batching_break.c @@ -0,0 +1,42 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: KLEE: done: generated tests = 3{{$}} + +#include + +int main(int argc, char** args){ + + int x; + int p; + int i; + + klee_make_symbolic(&x, sizeof(x), "x"); + x = x % 20; + + klee_open_merge(); + for (i = 0; i < x; ++i){ + if (x % 3 == 0){ + klee_close_merge(); + if (x > 10){ + return 1; + } else { + return 2; + } + } + } + klee_close_merge(); + + klee_open_merge(); + if (x > 10){ + p = 1; + } else { + p = 2; + } + klee_close_merge(); + return p; + +} diff --git a/test/Merging/easy_merge.c b/test/Merging/easy_merge.c new file mode 100644 index 00000000..b9c634dc --- /dev/null +++ b/test/Merging/easy_merge.c @@ -0,0 +1,44 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} +#include + +int main(int argc, char** args){ + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + if (a == 0){ + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + + return foo; +} diff --git a/test/Merging/indirect_value.c b/test/Merging/indirect_value.c new file mode 100644 index 00000000..ffea14ec --- /dev/null +++ b/test/Merging/indirect_value.c @@ -0,0 +1,32 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s + +// CHECK: generated tests = 2{{$}} +#include +#include + +#include + +int main(int argc, char** argv) { + + int sym = klee_int("sym"); + int* heap_int = calloc(1, sizeof(*heap_int)); + + klee_open_merge(); + + if(sym != 0) { + *heap_int = 1; + } + + klee_close_merge(); + + klee_print_expr("*heap_int: ", *heap_int); + if(*heap_int != 0) { + printf("true\n"); + } else { + printf("false\n"); + } + + return 0; +} diff --git a/test/Merging/loop_merge.c b/test/Merging/loop_merge.c new file mode 100644 index 00000000..4a38d98f --- /dev/null +++ b/test/Merging/loop_merge.c @@ -0,0 +1,38 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// There will be 20 'close merge' statements. Only checking a few, the generated +// test count will confirm that the merge was closed correctly +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} + +#include + +int main(int argc, char** args){ + + int x; + int i; + + klee_make_symbolic(&x, sizeof(x), "x"); + x = x % 20; + + klee_open_merge(); + for (i = 0; i < x; ++i){ + if (x % 3 == 0){ + klee_close_merge(); + return 1; + } + } + klee_close_merge(); + + return 0; +} diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c new file mode 100644 index 00000000..5cd9f782 --- /dev/null +++ b/test/Merging/merge_fail.c @@ -0,0 +1,36 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// CHECK: generated tests = 2{{$}} + +// This test will not merge because we cannot merge states when they allocated memory. + +#include + +int main(int argc, char **args) { + + int* arr = 0; + int a = 0; + + klee_make_symbolic(&a, sizeof(a), "a"); + + klee_open_merge(); + if (a == 0) { + arr = (int*) malloc(7 * sizeof(int)); + arr[0] = 7; + } else { + arr = (int*) malloc(8 * sizeof(int)); + arr[0] = 8; + } + klee_close_merge(); + a = arr[0]; + free(arr); + + return a; +} diff --git a/test/Merging/nested_merge.c b/test/Merging/nested_merge.c new file mode 100644 index 00000000..027c72d3 --- /dev/null +++ b/test/Merging/nested_merge.c @@ -0,0 +1,48 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + +// CHECK: open merge: +// 5 close merges +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 1{{$}} + +#include + +int main(int argc, char **args) { + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + klee_open_merge(); + if (a == 0) { + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + klee_close_merge(); + + return foo; +} diff --git a/test/Merging/split_merge.c b/test/Merging/split_merge.c new file mode 100644 index 00000000..bca8a5a2 --- /dev/null +++ b/test/Merging/split_merge.c @@ -0,0 +1,41 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=bfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs --use-batching-search %t.bc 2>&1 | FileCheck %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew %t.bc 2>&1 | FileCheck %s + + +// CHECK: open merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: close merge: +// CHECK: generated tests = 2{{$}} + +#include + +int main(int argc, char** args){ + + int x; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + + klee_open_merge(); + + if (x == 1){ + foo = 5; + } else if (x == 2){ + klee_close_merge(); + return 6; + } else { + foo = 7; + } + + klee_close_merge(); + + return foo; +} diff --git a/test/Merging/unexpected_close.c b/test/Merging/unexpected_close.c new file mode 100644 index 00000000..b4994de1 --- /dev/null +++ b/test/Merging/unexpected_close.c @@ -0,0 +1,35 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: klee --output-dir=%t.klee-out --use-merge --search=nurs:covnew --max-time=2 %t.bc + +// CHECK: ran into a close at +// CHECK: generated tests = 2{{$}} + +#include + +int main(int argc, char **args) { + + int x; + int a; + int foo = 0; + + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&a, sizeof(a), "a"); + + if (a == 0) { + klee_open_merge(); + + if (x == 1) { + foo = 5; + } else if (x == 2) { + foo = 6; + } else { + foo = 7; + } + + klee_close_merge(); + } + klee_close_merge(); + + return foo; +} -- cgit 1.4.1