diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2018-10-27 22:14:50 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-05-30 09:45:21 +0100 |
commit | 3629e3ef0fc999ba9c1e0f43db061bdcc875d735 (patch) | |
tree | 3f35cecfc8f1139f113b7f2fc76b6a2ba9be9b81 /test/Feature | |
parent | 4b93a3ecf7514d181730f5a8f8bfe7e086160b4c (diff) | |
download | klee-3629e3ef0fc999ba9c1e0f43db061bdcc875d735.tar.gz |
implement FunctionAliasPass
Diffstat (limited to 'test/Feature')
-rw-r--r-- | test/Feature/FunctionAlias.c | 89 | ||||
-rw-r--r-- | test/Feature/FunctionAliasExit.c | 31 | ||||
-rw-r--r-- | test/Feature/FunctionAliasVarArg.c | 58 |
3 files changed, 178 insertions, 0 deletions
diff --git a/test/Feature/FunctionAlias.c b/test/Feature/FunctionAlias.c new file mode 100644 index 00000000..2fcb5beb --- /dev/null +++ b/test/Feature/FunctionAlias.c @@ -0,0 +1,89 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=:oneint %t.bc 2>&1 | FileCheck --check-prefix=CHECK-EMPTY --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=oneint: %t.bc 2>&1 | FileCheck --check-prefix=CHECK-EMPTY --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=oneint:oneint %t.bc 2>&1 | FileCheck --check-prefix=CHECK-SAME --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=oneint:oneshort %t.bc 2>&1 | FileCheck --check-prefix=CHECK-TYPE-MISMATCH --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=oneint:twoints %t.bc 2>&1 | FileCheck --check-prefix=CHECK-TYPE-MISMATCH --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=twoints:twoshorts2int %t.bc 2>&1 | FileCheck --check-prefix=CHECK-TYPE-MISMATCH --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=oneint:unknownfunction %t.bc 2>&1 | FileCheck --check-prefix=CHECK-UNKNOWN --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=twoints:twointsmul %t.bc 2>&1 | FileCheck --check-prefix=CHECK-SUCCESS %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=xxx.*:somethingwithtwoints %t.bc 2>&1 | FileCheck --check-prefix=CHECK-REGEX-NO-MATCH --check-prefix=CHECK-ERROR %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=twoints.*:somethingwithtwoints %t.bc 2>&1 | FileCheck --check-prefix=CHECK-REGEX-PREFIX %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=.*twoints.*:twoints %t.bc 2>&1 | FileCheck --check-prefix=CHECK-REGEX-INFIX %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=two.*:twoints %t.bc 2>&1 | FileCheck --check-prefix=CHECK-REGEX-TYPE-MISMATCH %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=somethingwith.*:twoints -function-alias=twoints:twointsmul %t.bc 2>&1 | FileCheck --check-prefix=CHECK-MULTIPLE %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -output-module -function-alias=oneshort:shortminusone %t.bc 2>&1 | FileCheck --check-prefix=CHECK-BITCAST-ALIAS %s + +#include <stdio.h> +#include <stdlib.h> +#include <unistd.h> + +// CHECK-EMPTY: KLEE: ERROR: function-alias: {{name or pattern|replacement}} cannot be empty + +// CHECK-SAME: KLEE: ERROR: function-alias: @oneint cannot replace itself + +// CHECK-TYPE-MISMATCH: KLEE: WARNING: function-alias: @{{[a-z0-9]+}} could not be replaced with @{{[a-z0-9]+}} + +// CHECK-SUCCESS: KLEE: function-alias: replaced @twoints with @twointsmul + +// CHECK-REGEX-NO-MATCH: KLEE: ERROR: function-alias: no (replacable) match for 'xxx.*' found + +// CHECK-REGEX-PREFIX: KLEE: function-alias: replaced @twoints (matching 'twoints.*') with @somethingwithtwoints +// CHECK-REGEX-PREFIX: KLEE: function-alias: replaced @twointsmul (matching 'twoints.*') with @somethingwithtwoints + +// CHECK-REGEX-INFIX: KLEE: WARNING: function-alias: do not replace @twoints (matching '.*twoints.*') with @twoints: cannot replace itself +// CHECK-REGEX-INFIX: KLEE: function-alias: replaced @twointsmul (matching '.*twoints.*') with @twoints +// CHECK-REGEX-INFIX: KLEE: function-alias: replaced @somethingwithtwoints (matching '.*twoints.*') with @twoints + +// CHECK-REGEX-TYPE-MISMATCH: KLEE: WARNING: function-alias: @twoshorts2int could not be replaced with @twoints: parameter types differ +// CHECK-REGEX-TYPE-MISMATCH: KLEE: function-alias: replaced @twointsmul (matching 'two.*') with @twoints + +// CHECK-MULTIPLE: KLEE: function-alias: replaced @somethingwithtwoints (matching 'somethingwith.*') with @twoints +// CHECK-MULTIPLE: KLEE: function-alias: replaced @twoints with @twointsmul + +// CHECK-BITCAST-ALIAS: function-alias: replaced @oneshort with @shortminusone + +int __attribute__ ((noinline)) oneint(int a) { return a; } +short __attribute__ ((noinline)) oneshort(short a) { return a + 1; } +int __attribute__ ((noinline)) minusone(int a) { return a - 1; } +int __attribute__ ((noinline)) twoints(int a, int b) { return a + b; } +int __attribute__ ((noinline)) twoshorts2int(short a, short b) { return a + b + 2; } +int __attribute__ ((noinline)) twointsmul(int a, int b) { return a * b + 5; } +int __attribute__ ((noinline)) somethingwithtwoints(int a, int b) { return 2 * a + 3 * b; } + +extern short shortminusone(short) __attribute__((alias("minusone"))); + +int main() { + short a = 2; + short b = 3; + int result = 0; + result += shortminusone(a); + result += oneint(a); + result += oneshort(a); + result += twoints(a, b); + result += twoshorts2int(a, b); + result += twointsmul(a, b); + result += somethingwithtwoints(a, b); + // CHECK-ERROR-NOT: result = + // CHECK-SUCCESS: result = 48 + // CHECK-REGEX-PREFIX: result = 52 + // CHECK-REGEX-INFIX: result = 28 + // CHECK-REGEX-TYPE-MISMATCH: result = 36 + // CHECK-MULTIPLE: result = 46 + // CHECK-BITCAST-ALIAS: 40 + printf("result = %d\n", result); +} diff --git a/test/Feature/FunctionAliasExit.c b/test/Feature/FunctionAliasExit.c new file mode 100644 index 00000000..b30838d0 --- /dev/null +++ b/test/Feature/FunctionAliasExit.c @@ -0,0 +1,31 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=exit:end %t.bc 2>&1 | FileCheck %s + +#include <stdio.h> +#include <stdlib.h> +#include <unistd.h> + +// CHECK: KLEE: function-alias: replaced @exit with @end + +void start(int x) { + // CHECK: START + printf("START\n"); + if (x == 53) + // CHECK: END: status = 1 + exit(1); +} + +void __attribute__ ((noinline)) end(int status) { + printf("END: status = %d\n", status); + klee_silent_exit(status); +} + +int main() { + int x; + klee_make_symbolic(&x, sizeof(x), "x"); + + start(x); + // CHECK: END: status = 0 + end(0); +} diff --git a/test/Feature/FunctionAliasVarArg.c b/test/Feature/FunctionAliasVarArg.c new file mode 100644 index 00000000..17893772 --- /dev/null +++ b/test/Feature/FunctionAliasVarArg.c @@ -0,0 +1,58 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=printf:highlight_prefix_printf %t.bc 2>&1 | FileCheck --check-prefix=CHECK-HIGHLIGHT %s +// RUN: rm -rf %t.klee-out +// RUN: not %klee --output-dir=%t.klee-out -function-alias=printf:printf_format_only %t.bc 2>&1 | FileCheck --check-prefix=CHECK-VA-FAIL %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -function-alias=printf:printf_format_only_with_varargs %t.bc 2>&1 | FileCheck --check-prefix=CHECK-VA-SUCCESS %s + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> + +// CHECK-HIGHLIGHT: KLEE: function-alias: replaced @printf with @highlight_prefix_printf +int highlight_prefix_printf(const char *format, ...) { + va_list args; + int result; + const char *bold_start = "*+*"; + const char *bold_end = "*+*"; + + va_start(args, format); + const char *prefix = va_arg(args, const char *); + + const char *prefixless_format = strstr(format, "%s") + 2; + size_t new_length = strlen(bold_start) + strlen(prefix) + strlen(bold_end) + strlen(prefixless_format) + 1; + char *new_format = (char *)malloc(new_length); + memset(new_format, 0, new_length); + strcat(new_format, bold_start); + strcat(new_format, prefix); + strcat(new_format, bold_end); + strcat(new_format, prefixless_format); + result = vfprintf(stdout, new_format, args); + va_end(args); + + free(new_format); + return result; +} + +// CHECK-VA-FAIL: KLEE: WARNING: function-alias: @printf could not be replaced with @printf_format_only: one has varargs while the other does not +int printf_format_only(const char *format) { + int result; + result = puts(format); + return result; +} + +// CHECK-VA-SUCCESS: KLEE: function-alias: replaced @printf with @printf_format_only_with_varargs +int printf_format_only_with_varargs(const char *format, ...) { + int result; + result = puts(format); + return result; +} + +int main() { + int i = 42; + // CHECK: KLEE: some warning about 42 + // CHECK-HIGHLIGHT: *+*KLEE*+* + // CHECK-VA-SUCCESS: %s: some warning about %d + printf("%s: some warning about %d\n", "KLEE", i); +} |