diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-07-29 16:56:56 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-24 14:15:25 +0300 |
commit | 54851ed24b9d8a8937d7bf7d02ee6020ef770204 (patch) | |
tree | 04d1b3ffcf243d05e852e605f26e05bb6946f1a6 /test | |
parent | ecc7fae9cbac9aa970aac072276e5bca1c583c02 (diff) | |
download | klee-54851ed24b9d8a8937d7bf7d02ee6020ef770204.tar.gz |
Add testcase for shift check
Validate non-optimised and optimised variant of added checks.
Diffstat (limited to 'test')
-rw-r--r-- | test/Feature/ShiftCheck.c | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/test/Feature/ShiftCheck.c b/test/Feature/ShiftCheck.c new file mode 100644 index 00000000..326eadb2 --- /dev/null +++ b/test/Feature/ShiftCheck.c @@ -0,0 +1,50 @@ +// Check if shift-instructions are correctly instrumented: +// * unoptimized code will contain a call to klee_overshift_check +// * optimized code will have this check inlined +// In both cases, the `ashr` instruction should have been marked with meta-data: klee.check.shift +// +// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --check-overshift=true %t.bc >%t.shift_enabled.log +// RUN: FileCheck %s -input-file=%t.klee-out/assembly.ll -check-prefix=SHIFT-ENABLED +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --check-overshift=true --optimize %t.bc >%t.shift_enabled.log +// RUN: FileCheck %s -input-file=%t.klee-out/assembly.ll -check-prefix=SHIFT-ENABLED-OPT +// Same test without debug information +// RUN: %llvmgcc %s -emit-llvm -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --check-overshift=true %t.bc >%t.shift_enabled.log +// RUN: FileCheck %s -input-file=%t.klee-out/assembly.ll -check-prefix=SHIFT-ENABLED +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --check-overshift=true --optimize %t.bc >%t.shift_enabled.log +// RUN: FileCheck %s -input-file=%t.klee-out/assembly.ll -check-prefix=SHIFT-ENABLED-OPT + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char **argv) { + char c; + + klee_make_symbolic(&c, sizeof(c), "index"); + + // Validate + if (argc >> c == 5) + return 1; + // Check for klee_overshift_check call + // SHIFT-ENABLED: call {{.*}}void @klee_overshift_check + // Check that double-instrumentation does not happen + // SHIFT-ENABLED-NOT: call {{.*}}void @klee_overshift_check + // SHIFT-ENABLED: ashr {{.*}} !klee.check.shift + // SHIFT-ENABLED-OPT: ashr {{.*}} !klee.check.shift + + // Validate + uint32_t value = (uint32_t)argc; + if (value >> 3 == 5) + return 1; + // Check that the second shift was not instrumented + // SHIFT-ENABLED-NOT: call {{.*}}void @klee_overshift_check(i32 i{{.+.+}} 3) + // SHIFT-ENABLED-NOT: ashr {{.*}} !klee.check.shift + // SHIFT-ENABLED-OPT-NOT: ashr {{.*}} !klee.check.shift + + return 0; +} |