diff options
author | Alastair Reid <adreid@google.com> | 2020-06-16 16:57:46 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-06-29 22:22:48 +0100 |
commit | 67ea19efc36bbf8885f32e85d11f920342a7949c (patch) | |
tree | 17d329f3901bc349d92a4e8ab570b10d6f066ad8 /test/Intrinsics/fshlr.ll | |
parent | 51e28268a927e1e40899ff2df11faa553d3c2e79 (diff) | |
download | klee-67ea19efc36bbf8885f32e85d11f920342a7949c.tar.gz |
Implement fshr/fshl intrinsics
Changes: - IntrinsicCleaner accepts fshr/fshl as accepted intrinsics - Executor::executeCall converts fshr/fshl to urem/zext/concat/shift/extract - Klee/main suppresses warnings about externals that are LLVM reserved (i.e., begin with "llvm.") - New test exercises 32 and 7 bit versions including oversize shift values Test values are based on LLVM's test for fshl/fshr - Changes that depend on existence of fshr/fshl are guarded by #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0) or ; REQUIRES: geq-llvm-7.0
Diffstat (limited to 'test/Intrinsics/fshlr.ll')
-rw-r--r-- | test/Intrinsics/fshlr.ll | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/test/Intrinsics/fshlr.ll b/test/Intrinsics/fshlr.ll new file mode 100644 index 00000000..fcdf32ff --- /dev/null +++ b/test/Intrinsics/fshlr.ll @@ -0,0 +1,76 @@ +; Tests for the Funnel Shift intrinsics fshl/fshr(a, b, c) which +; - concatenate 'a' and 'b' +; - shift the result by an amount 'c' (left or right) +; - return the top or bottom half of result (depending on direction) +; +; This file consists of a sequence of tests of the form +; ``` +; T = llvm_fshl(a, b, c); +; C = T != r; +; if C { +; klee_abort(); +; } +; ``` +; where the constants a, b, c and r are copied from the constants +; used in the LLVM testfile llvm/test/Analysis/ConstantFolding/funnel-shift.ll + +; REQUIRES: geq-llvm-7.0 +; RUN: %llvmas %s -o=%t.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %t.bc + +target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-pc-linux-gnu" + +declare i32 @llvm.fshl.i32(i32, i32, i32) +declare i32 @llvm.fshr.i32(i32, i32, i32) +declare i7 @llvm.fshl.i7(i7, i7, i7) +declare i7 @llvm.fshr.i7(i7, i7, i7) + +declare void @klee_abort() + +; Function Attrs: noinline nounwind optnone uwtable +define dso_local i32 @main() #0 { + + ; T1: extract(concat(0x12345678, 0xABCDEF01) << 5) = 0x468ACF15 + %T1 = call i32 @llvm.fshl.i32(i32 305419896, i32 2882400001, i32 5) + %C1 = icmp ne i32 %T1, 1183502101 + br i1 %C1, label %FAIL1, label %OK1 +FAIL1: + call void @klee_abort() + unreachable +OK1: + + ; T2: extract(concat(0x12345678, 0xABCDEF01) >> 5) = 0xC55E6F78 + ; Try an oversized shift (37) to test modulo functionality. + %T2 = call i32 @llvm.fshr.i32(i32 305419896, i32 2882400001, i32 37) + %C2 = icmp ne i32 %T2, 3311300472 + br i1 %C2, label %FAIL2, label %OK2 +FAIL2: + call void @klee_abort() + unreachable +OK2: + + ; T3: extract(concat(0b1110000, 0b1111111) << 2) = 0b1000011 + ; Use a weird type. + ; Try an oversized shift (9) to test modulo functionality. + %T3 = call i7 @llvm.fshl.i7(i7 112, i7 127, i7 9) + %C3 = icmp ne i7 %T3, 67 + br i1 %C3, label %FAIL3, label %OK3 +FAIL3: + call void @klee_abort() + unreachable +OK3: + + ; T4: extract(concat(0b1110000, 0b1111111) >> 2) = 0b0011111 + ; Try an oversized shift (16) to test modulo functionality. + %T4 = call i7 @llvm.fshr.i7(i7 112, i7 127, i7 16) + %C4 = icmp ne i7 %T4, 31 + br i1 %C4, label %FAIL4, label %OK4 +FAIL4: + call void @klee_abort() + unreachable +OK4: + + ret i32 0 +} |