diff options
| author | Lukáš Zaoral <lzaoral@redhat.com> | 2022-06-15 21:17:46 +0200 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2022-06-26 18:52:31 +0100 |
| commit | 42bca7ee2db48b0fc080cdb4af6a05cb666efb8c (patch) | |
| tree | 123c54c6a312e53fc01bf21d598136a5ab528c56 /test/Intrinsics | |
| parent | 19f40fefaba602d1db2e26ad77df1a85a1a69c21 (diff) | |
| download | klee-42bca7ee2db48b0fc080cdb4af6a05cb666efb8c.tar.gz | |
Intrinsics: Add support for @llvm.f{ma,muladd}.f*
Diffstat (limited to 'test/Intrinsics')
| -rw-r--r-- | test/Intrinsics/FMulAdd.ll | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/test/Intrinsics/FMulAdd.ll b/test/Intrinsics/FMulAdd.ll new file mode 100644 index 00000000..989b88a8 --- /dev/null +++ b/test/Intrinsics/FMulAdd.ll @@ -0,0 +1,55 @@ +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %s + +define dso_local i32 @main() local_unnamed_addr { +fma.float: + %0 = call float @llvm.fma.f32(float 2.0, float 2.0, float 1.0) + %cmp0 = fcmp one float %0, 5.0 + br i1 %cmp0, label %abort.block, label %fma.double + +fma.double: + %1 = call double @llvm.fma.f64(double 2.0, double 2.0, double 1.0) + %cmp1 = fcmp one double %1, 5.0 + br i1 %cmp1, label %abort.block, label %fma.fp80 + +fma.fp80: + %2 = call x86_fp80 @llvm.fma.f80(x86_fp80 0xK40008000000000000000, + x86_fp80 0xK40008000000000000000, + x86_fp80 0xK3FFF8000000000000000) + %cmp2 = fcmp one x86_fp80 %2, 0xK4001A000000000000000 + br i1 %cmp2, label %abort.block, label %fmuladd.float + +fmuladd.float: + %3 = call float @llvm.fmuladd.f32(float 2.0, float 2.0, float 1.0) + %cmp3 = fcmp one float %3, 5.0 + br i1 %cmp3, label %abort.block, label %fmuladd.double + +fmuladd.double: + %4 = call double @llvm.fmuladd.f64(double 2.0, double 2.0, double 1.0) + %cmp4 = fcmp one double %4, 5.0 + br i1 %cmp4, label %abort.block, label %fmuladd.fp80 + +fmuladd.fp80: + %5 = call x86_fp80 @llvm.fmuladd.f80(x86_fp80 0xK40008000000000000000, + x86_fp80 0xK40008000000000000000, + x86_fp80 0xK3FFF8000000000000000) + %cmp5 = fcmp one x86_fp80 %5, 0xK4001A000000000000000 + br i1 %cmp4, label %abort.block, label %exit.block + +exit.block: + ret i32 0 + +abort.block: + call void @abort() + unreachable +} + +declare void @abort() noreturn nounwind + +declare float @llvm.fma.f32(float %a, float %b, float %c) +declare double @llvm.fma.f64(double %a, double %b, double %c) +declare x86_fp80 @llvm.fma.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c) + +declare float @llvm.fmuladd.f32(float %a, float %b, float %c) +declare double @llvm.fmuladd.f64(double %a, double %b, double %c) +declare x86_fp80 @llvm.fmuladd.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c) |