From 8775b9cf6c716f51fe90d668e734a1288c8b5404 Mon Sep 17 00:00:00 2001 From: Lukas Zaoral Date: Wed, 7 Jul 2021 10:33:46 +0200 Subject: 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 Co-authored-by: Martin Nowack --- test/Intrinsics/abs-no-overflow.ll | 57 ++++++++++++++++++++++++++++++++++++++ test/Intrinsics/abs-overflow.ll | 12 ++++++++ 2 files changed, 69 insertions(+) create mode 100644 test/Intrinsics/abs-no-overflow.ll create mode 100644 test/Intrinsics/abs-overflow.ll (limited to 'test/Intrinsics') 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 +; #include +; +; 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) -- cgit 1.4.1