diff options
| author | Lukas Zaoral <lzaoral@redhat.com> | 2021-07-07 10:33:46 +0200 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2021-09-10 15:14:56 +0100 |
| commit | 8775b9cf6c716f51fe90d668e734a1288c8b5404 (patch) | |
| tree | 5f586ff87b1fddfdebbcc670b658ea0e054c7d41 /test | |
| parent | 3d7c05a7e86a72a4fc8df115591bd1e7a50f9d84 (diff) | |
| download | klee-8775b9cf6c716f51fe90d668e734a1288c8b5404.tar.gz | |
llvm12: Implement llvm.abs intrinsic
The vector variants are not implemented at the moment. See: https://reviews.llvm.org/D84125 Co-authored-by: Lukas Zaoral <lzaoral@redhat.com> Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>
Diffstat (limited to 'test')
| -rw-r--r-- | test/Intrinsics/abs-no-overflow.ll | 57 | ||||
| -rw-r--r-- | test/Intrinsics/abs-overflow.ll | 12 |
2 files changed, 69 insertions, 0 deletions
diff --git a/test/Intrinsics/abs-no-overflow.ll b/test/Intrinsics/abs-no-overflow.ll new file mode 100644 index 00000000..7f476e2a --- /dev/null +++ b/test/Intrinsics/abs-no-overflow.ll @@ -0,0 +1,57 @@ +; LLVM has an intrinsic for abs. +; This file is based on the following code with poisoning of llvm.abs disabled. +; ``` +; #include "klee/klee.h" +; +; #include <assert.h> +; #include <limits.h> +; +; volatile int abs_a; +; +; int main(void) +; { +; int a; +; klee_make_symbolic(&a, sizeof(a), "a"); +; +; abs_a = a < 0 ? -a : a; +; if (abs_a == INT_MIN) +; assert(abs_a == a); +; else +; assert(abs_a >= 0); +; return abs_a; +; } +; ``` +; REQUIRES: geq-llvm-12.0 +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %s + +@0 = private unnamed_addr constant [2 x i8] c"a\00", align 1 +define dso_local i32 @main() local_unnamed_addr { + %1 = alloca i32, align 4 + %2 = bitcast i32* %1 to i8* + call void @klee_make_symbolic(i8* nonnull %2, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @0, i64 0, i64 0)) + %3 = load i32, i32* %1, align 4 + ; Call with is_int_min_poison == 0 (false), expects INT_MIN to be returned + %abs_a = call i32 @llvm.abs.i32(i32 %3, i1 false) + %4 = icmp eq i32 %abs_a, -2147483648 + br i1 %4, label %int_min, label %not_int_min + +int_min: + %5 = icmp eq i32 %abs_a, %3 + br i1 %5, label %exit.block, label %abort.block + +not_int_min: + %6 = icmp sgt i32 %abs_a, -1 + br i1 %6, label %exit.block, label %abort.block + +exit.block: + ret i32 0 + +abort.block: + call void @abort() + unreachable +} + +declare dso_local void @klee_make_symbolic(i8*, i64, i8*) +declare i32 @llvm.abs.i32(i32, i1 immarg) +declare void @abort() noreturn nounwind diff --git a/test/Intrinsics/abs-overflow.ll b/test/Intrinsics/abs-overflow.ll new file mode 100644 index 00000000..33b47ecf --- /dev/null +++ b/test/Intrinsics/abs-overflow.ll @@ -0,0 +1,12 @@ +; REQUIRES: geq-llvm-12.0 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out --optimize=false %s 2> %t.stderr.log +; RUN: FileCheck %s < %t.stderr.log + +define i32 @main() { + %1 = call i32 @llvm.abs.i32(i32 -2147483648, i1 true) + ; CHECK: llvm.abs called with poison and INT_MIN + ret i32 0 +} + +declare i32 @llvm.abs.i32(i32, i1 immarg) |