diff options
author | Richard Trembecký <richardt@centrum.sk> | 2016-04-29 22:33:41 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-05-24 14:08:27 +0100 |
commit | a0cd85b41f02ce5c476612eec182aa1ff3e6fe2b (patch) | |
tree | b7d938116cae4f4a18225e9aef2f8934b761e063 /test/Feature | |
parent | 870f2d6aac35457e7524078a4b4a8b011f84c45c (diff) | |
download | klee-a0cd85b41f02ce5c476612eec182aa1ff3e6fe2b.tar.gz |
test: add versions of some tests for LLVM 3.7
Clone some tests to have their 3.7 version. 'call's, 'load's and 'getelementptr's match the new specification in them. @andreamattavelli: Fixed test cases: BitCastAlias test cases included modification to alias specifications that require LLVM 3.8 [v2] added comments what was changed and why [v3] the new tests are without suffix, the old ones have ".leq36". Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
Diffstat (limited to 'test/Feature')
-rw-r--r-- | test/Feature/BitcastAlias.leq36.ll | 35 | ||||
-rw-r--r-- | test/Feature/BitcastAlias.ll | 9 | ||||
-rw-r--r-- | test/Feature/BitcastAliasMD2U.leq36.ll | 35 | ||||
-rw-r--r-- | test/Feature/BitcastAliasMD2U.ll | 9 | ||||
-rw-r--r-- | test/Feature/ConstantArray.leq36.ll | 52 | ||||
-rw-r--r-- | test/Feature/ConstantArray.ll | 32 | ||||
-rw-r--r-- | test/Feature/ConstantStruct.leq36.ll | 34 | ||||
-rw-r--r-- | test/Feature/ConstantStruct.ll | 6 | ||||
-rw-r--r-- | test/Feature/GetElementPtr.leq36.ll | 30 | ||||
-rw-r--r-- | test/Feature/GetElementPtr.ll | 10 | ||||
-rw-r--r-- | test/Feature/InsertExtractValue.leq36.ll | 34 | ||||
-rw-r--r-- | test/Feature/InsertExtractValue.ll | 6 | ||||
-rw-r--r-- | test/Feature/Overflow.leq36.ll | 45 | ||||
-rw-r--r-- | test/Feature/Overflow.ll | 6 | ||||
-rw-r--r-- | test/Feature/OverflowMul.leq36.ll | 45 | ||||
-rw-r--r-- | test/Feature/OverflowMul.ll | 6 | ||||
-rw-r--r-- | test/Feature/_utils._ll | 39 | ||||
-rw-r--r-- | test/Feature/_utils.leq36._ll | 71 |
18 files changed, 454 insertions, 50 deletions
diff --git a/test/Feature/BitcastAlias.leq36.ll b/test/Feature/BitcastAlias.leq36.ll new file mode 100644 index 00000000..d203e52c --- /dev/null +++ b/test/Feature/BitcastAlias.leq36.ll @@ -0,0 +1,35 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +@foo = alias i32 (i32)* @__foo + +define i32 @__foo(i32 %i) nounwind { +entry: + ret i32 %i +} + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %r = icmp eq i32 %call, 52 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/BitcastAlias.ll b/test/Feature/BitcastAlias.ll index e0e3653f..5bd30193 100644 --- a/test/Feature/BitcastAlias.ll +++ b/test/Feature/BitcastAlias.ll @@ -1,3 +1,6 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; LLVM 3.7 no longer accepts '*' with a 'call' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -20,15 +23,15 @@ declare i32 @puts(i8*) define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { entry: - %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) %r = icmp eq i32 %call, 52 br i1 %r, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/BitcastAliasMD2U.leq36.ll b/test/Feature/BitcastAliasMD2U.leq36.ll new file mode 100644 index 00000000..cef8ac54 --- /dev/null +++ b/test/Feature/BitcastAliasMD2U.leq36.ll @@ -0,0 +1,35 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +@foo = alias i32 (i32)* @__foo + +define i32 @__foo(i32 %i) nounwind { +entry: + ret i32 %i +} + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %r = icmp eq i32 %call, 52 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/BitcastAliasMD2U.ll b/test/Feature/BitcastAliasMD2U.ll index 24eabaa5..7eddd3d6 100644 --- a/test/Feature/BitcastAliasMD2U.ll +++ b/test/Feature/BitcastAliasMD2U.ll @@ -1,3 +1,6 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; LLVM 3.7 no longer accepts '*' with a 'call' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt -search=nurs:md2u %t1.bc > %t2 @@ -20,15 +23,15 @@ declare i32 @puts(i8*) define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { entry: - %call = call i32 (i64)* bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) + %call = call i32 (i64) bitcast (i32 (i32)* @foo to i32 (i64)*)(i64 52) %r = icmp eq i32 %call, 52 br i1 %r, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/ConstantArray.leq36.ll b/test/Feature/ConstantArray.leq36.ll new file mode 100644 index 00000000..a4986ff4 --- /dev/null +++ b/test/Feature/ConstantArray.leq36.ll @@ -0,0 +1,52 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc 2>&1 | FileCheck %s +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@.str = private unnamed_addr constant [2 x i8] c"0\00", align 1 +@.str2 = private unnamed_addr constant [2 x i8] c"1\00", align 1 + +%struct.dirent = type { i32, i32, i16, i8 } +declare void @klee_print_expr(i8*, ...) + +define i32 @main() { +entry: + %a = alloca %struct.dirent + %tmp1 = getelementptr %struct.dirent* %a, i32 0 + %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>* + ; Initialize with constant vector + store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2 + br label %exit +exit: + ; Print first initialized element + %idx = getelementptr %struct.dirent* %a, i32 0, i32 0 + %val = load i32* %idx + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val) + ; CHECK: 0:42 + + ; Print second initialized element + %idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1 + %val2 = load i32* %idx2 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val2) + ; CHECK: 1:4096 + + ; Initialize with constant array + %array = alloca [2 x i32]; + store [2 x i32][i32 7, i32 9], [2 x i32]* %array + + ; Print first initialized element + %idx3 = getelementptr [2 x i32]* %array, i32 0, i32 0 + %val3 = load i32* %idx3 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val3) + ; CHECK: 0:7 + + ; Print second initialized element + %idx4 = getelementptr [2 x i32]* %array, i32 0, i32 1 + %val4 = load i32* %idx4 + call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val4) + ; CHECK: 1:9 + + ret i32 0 +} diff --git a/test/Feature/ConstantArray.ll b/test/Feature/ConstantArray.ll index 161b2a16..195b4cb0 100644 --- a/test/Feature/ConstantArray.ll +++ b/test/Feature/ConstantArray.ll @@ -1,3 +1,7 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; LLVM 3.7 requires a type as the first argument to 'load' +; LLVM 3.7 no longer accepts '*' with a 'call' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc 2>&1 | FileCheck %s @@ -13,22 +17,22 @@ declare void @klee_print_expr(i8*, ...) define i32 @main() { entry: %a = alloca %struct.dirent - %tmp1 = getelementptr %struct.dirent* %a, i32 0 + %tmp1 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0 %tmp2 = bitcast %struct.dirent* %tmp1 to <2 x i32>* ; Initialize with constant vector store <2 x i32> <i32 42, i32 4096>, <2 x i32>* %tmp2 br label %exit exit: ; Print first initialized element - %idx = getelementptr %struct.dirent* %a, i32 0, i32 0 - %val = load i32* %idx - call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val) + %idx = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 0 + %val = load i32, i32* %idx + call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val) ; CHECK: 0:42 ; Print second initialized element - %idx2 = getelementptr %struct.dirent* %a, i32 0, i32 1 - %val2 = load i32* %idx2 - call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val2) + %idx2 = getelementptr %struct.dirent, %struct.dirent* %a, i32 0, i32 1 + %val2 = load i32, i32* %idx2 + call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val2) ; CHECK: 1:4096 ; Initialize with constant array @@ -36,16 +40,16 @@ exit: store [2 x i32][i32 7, i32 9], [2 x i32]* %array ; Print first initialized element - %idx3 = getelementptr [2 x i32]* %array, i32 0, i32 0 - %val3 = load i32* %idx3 - call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0), i32 %val3) + %idx3 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 0 + %val3 = load i32, i32* %idx3 + call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i32 0, i32 0), i32 %val3) ; CHECK: 0:7 ; Print second initialized element - %idx4 = getelementptr [2 x i32]* %array, i32 0, i32 1 - %val4 = load i32* %idx4 - call void(i8*, ...)* @klee_print_expr(i8* getelementptr inbounds ([2 x i8]* @.str2, i32 0, i32 0), i32 %val4) + %idx4 = getelementptr [2 x i32], [2 x i32]* %array, i32 0, i32 1 + %val4 = load i32, i32* %idx4 + call void(i8*, ...) @klee_print_expr(i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str2, i32 0, i32 0), i32 %val4) ; CHECK: 1:9 ret i32 0 -} \ No newline at end of file +} diff --git a/test/Feature/ConstantStruct.leq36.ll b/test/Feature/ConstantStruct.leq36.ll new file mode 100644 index 00000000..073544d3 --- /dev/null +++ b/test/Feature/ConstantStruct.leq36.ll @@ -0,0 +1,34 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +%struct.sfoo = type { i32, i64 } + +declare i32 @puts(i8*) +declare i32 @printf(i8*, ...) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %f0 = extractvalue %struct.sfoo { i32 3, i64 1 }, 0 + %f1 = extractvalue %struct.sfoo { i32 3, i64 1 }, 1 + %xf0 = zext i32 %f0 to i64 + %f0mf1 = sub i64 %xf0, %f1 + %r = icmp eq i64 %f0mf1, 2 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/ConstantStruct.ll b/test/Feature/ConstantStruct.ll index 4fe6b5d0..e4b3d07b 100644 --- a/test/Feature/ConstantStruct.ll +++ b/test/Feature/ConstantStruct.ll @@ -1,3 +1,5 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -24,10 +26,10 @@ entry: br i1 %r, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/GetElementPtr.leq36.ll b/test/Feature/GetElementPtr.leq36.ll new file mode 100644 index 00000000..43f33e27 --- /dev/null +++ b/test/Feature/GetElementPtr.leq36.ll @@ -0,0 +1,30 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main() { +entry: + %addr = alloca i8, align 4 + %addrp1 = getelementptr i8* %addr, i32 1 + %addrp1m1 = getelementptr i8* %addrp1, i32 -1 + %test = icmp eq i8* %addr, %addrp1m1 + br i1 %test, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/GetElementPtr.ll b/test/Feature/GetElementPtr.ll index da94441c..f7f8aada 100644 --- a/test/Feature/GetElementPtr.ll +++ b/test/Feature/GetElementPtr.ll @@ -1,3 +1,5 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -14,16 +16,16 @@ declare i32 @puts(i8*) define i32 @main() { entry: %addr = alloca i8, align 4 - %addrp1 = getelementptr i8* %addr, i32 1 - %addrp1m1 = getelementptr i8* %addrp1, i32 -1 + %addrp1 = getelementptr i8, i8* %addr, i32 1 + %addrp1m1 = getelementptr i8, i8* %addrp1, i32 -1 %test = icmp eq i8* %addr, %addrp1m1 br i1 %test, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/InsertExtractValue.leq36.ll b/test/Feature/InsertExtractValue.leq36.ll new file mode 100644 index 00000000..431e14c4 --- /dev/null +++ b/test/Feature/InsertExtractValue.leq36.ll @@ -0,0 +1,34 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +%struct.sfoo = type { i32, i32 } + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main(i32 %argc, i8** nocapture %argv) nounwind readnone { +entry: + %s0 = insertvalue %struct.sfoo undef, i32 3, 0 + %s1 = insertvalue %struct.sfoo %s0, i32 1, 1 + %f0 = extractvalue %struct.sfoo %s1, 0 + %f1 = extractvalue %struct.sfoo %s1, 1 + %f0mf1 = sub i32 %f0, %f1 + %r = icmp eq i32 %f0mf1, 2 + br i1 %r, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/InsertExtractValue.ll b/test/Feature/InsertExtractValue.ll index 83e8f851..fff6da7c 100644 --- a/test/Feature/InsertExtractValue.ll +++ b/test/Feature/InsertExtractValue.ll @@ -1,3 +1,5 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -24,10 +26,10 @@ entry: br i1 %r, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/Overflow.leq36.ll b/test/Feature/Overflow.leq36.ll new file mode 100644 index 00000000..2ab04772 --- /dev/null +++ b/test/Feature/Overflow.leq36.ll @@ -0,0 +1,45 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +declare {i8, i1} @llvm.uadd.with.overflow.i8(i8 %a, i8 %b) + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main() { +bb0: + %s0 = call {i8, i1} @llvm.uadd.with.overflow.i8(i8 0, i8 -1) + %v0 = extractvalue {i8, i1} %s0, 0 + %c0 = icmp eq i8 %v0, -1 + br i1 %c0, label %bb0_1, label %bbfalse + +bb0_1: + %o0 = extractvalue {i8, i1} %s0, 1 + br i1 %o0, label %bbfalse, label %bb1 + +bb1: + %s1 = call {i8, i1} @llvm.uadd.with.overflow.i8(i8 1, i8 -1) + %v1 = extractvalue {i8, i1} %s1, 0 + %c1 = icmp eq i8 %v1, 0 + br i1 %c1, label %bb1_1, label %bbfalse + +bb1_1: + %o1 = extractvalue {i8, i1} %s1, 1 + br i1 %o1, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/Overflow.ll b/test/Feature/Overflow.ll index 35dfbd10..1dbe1216 100644 --- a/test/Feature/Overflow.ll +++ b/test/Feature/Overflow.ll @@ -1,3 +1,5 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -35,10 +37,10 @@ bb1_1: br i1 %o1, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/OverflowMul.leq36.ll b/test/Feature/OverflowMul.leq36.ll new file mode 100644 index 00000000..1b14d380 --- /dev/null +++ b/test/Feature/OverflowMul.leq36.ll @@ -0,0 +1,45 @@ +; REQUIRES: lt-llvm-3.7 +; RUN: llvm-as %s -f -o %t1.bc +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 +; RUN: grep PASS %t2 + +target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64" +target triple = "x86_64-unknown-linux-gnu" + +declare {i8, i1} @llvm.umul.with.overflow.i8(i8 %a, i8 %b) + +declare i32 @puts(i8*) + +@.passstr = private constant [5 x i8] c"PASS\00", align 1 +@.failstr = private constant [5 x i8] c"FAIL\00", align 1 + +define i32 @main() { +bb0: + %s0 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 1, i8 128) + %v0 = extractvalue {i8, i1} %s0, 0 + %c0 = icmp eq i8 %v0, 128 + br i1 %c0, label %bb0_1, label %bbfalse + +bb0_1: + %o0 = extractvalue {i8, i1} %s0, 1 + br i1 %o0, label %bbfalse, label %bb1 + +bb1: + %s1 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 2, i8 128) + %v1 = extractvalue {i8, i1} %s1, 0 + %c1 = icmp eq i8 %v1, 0 + br i1 %c1, label %bb1_1, label %bbfalse + +bb1_1: + %o1 = extractvalue {i8, i1} %s1, 1 + br i1 %o1, label %bbtrue, label %bbfalse + +bbtrue: + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + ret i32 0 + +bbfalse: + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + ret i32 0 +} diff --git a/test/Feature/OverflowMul.ll b/test/Feature/OverflowMul.ll index 7026aa74..3173e43c 100644 --- a/test/Feature/OverflowMul.ll +++ b/test/Feature/OverflowMul.ll @@ -1,3 +1,5 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; REQUIRES: geq-llvm-3.7 ; RUN: llvm-as %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out -disable-opt %t1.bc > %t2 @@ -35,10 +37,10 @@ bb1_1: br i1 %o1, label %bbtrue, label %bbfalse bbtrue: - %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind + %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.passstr, i64 0, i64 0)) nounwind ret i32 0 bbfalse: - %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind + %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8], [5 x i8]* @.failstr, i64 0, i64 0)) nounwind ret i32 0 } diff --git a/test/Feature/_utils._ll b/test/Feature/_utils._ll index 32a73bb1..d825df3a 100644 --- a/test/Feature/_utils._ll +++ b/test/Feature/_utils._ll @@ -1,3 +1,6 @@ +; LLVM 3.7 requires a type as the first argument to 'getelementptr' +; LLVM 3.7 requires a type as the first argument to 'load' + define i32 @util_make_and_i1(i32 %a, i32 %b) { %a_i1 = icmp ne i32 %a, 0 %b_i1 = icmp ne i32 %b, 0 @@ -17,26 +20,26 @@ define i32 @util_make_or_i1(i32 %a, i32 %b) { define i16 @util_make_concat2(i8 %a, i8 %b) { %tmp = alloca i16 %tmp8 = bitcast i16* %tmp to i8* - %p0 = getelementptr i8* %tmp8, i32 0 - %p1 = getelementptr i8* %tmp8, i32 1 + %p0 = getelementptr i8, i8* %tmp8, i32 0 + %p1 = getelementptr i8, i8* %tmp8, i32 1 store i8 %b, i8* %p0 store i8 %a, i8* %p1 - %concat = load i16* %tmp + %concat = load i16, i16* %tmp ret i16 %concat } define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) { %tmp = alloca i32 %tmp8 = bitcast i32* %tmp to i8* - %p0 = getelementptr i8* %tmp8, i32 0 - %p1 = getelementptr i8* %tmp8, i32 1 - %p2 = getelementptr i8* %tmp8, i32 2 - %p3 = getelementptr i8* %tmp8, i32 3 + %p0 = getelementptr i8, i8* %tmp8, i32 0 + %p1 = getelementptr i8, i8* %tmp8, i32 1 + %p2 = getelementptr i8, i8* %tmp8, i32 2 + %p3 = getelementptr i8, i8* %tmp8, i32 3 store i8 %d, i8* %p0 store i8 %c, i8* %p1 store i8 %b, i8* %p2 store i8 %a, i8* %p3 - %concat = load i32* %tmp + %concat = load i32, i32* %tmp ret i32 %concat } @@ -44,14 +47,14 @@ define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d, i8 %e, i8 %f, i8 %g, i8 %h) { %tmp = alloca i64 %tmp8 = bitcast i64* %tmp to i8* - %p0 = getelementptr i8* %tmp8, i32 0 - %p1 = getelementptr i8* %tmp8, i32 1 - %p2 = getelementptr i8* %tmp8, i32 2 - %p3 = getelementptr i8* %tmp8, i32 3 - %p4 = getelementptr i8* %tmp8, i32 4 - %p5 = getelementptr i8* %tmp8, i32 5 - %p6 = getelementptr i8* %tmp8, i32 6 - %p7 = getelementptr i8* %tmp8, i32 7 + %p0 = getelementptr i8, i8* %tmp8, i32 0 + %p1 = getelementptr i8, i8* %tmp8, i32 1 + %p2 = getelementptr i8, i8* %tmp8, i32 2 + %p3 = getelementptr i8, i8* %tmp8, i32 3 + %p4 = getelementptr i8, i8* %tmp8, i32 4 + %p5 = getelementptr i8, i8* %tmp8, i32 5 + %p6 = getelementptr i8, i8* %tmp8, i32 6 + %p7 = getelementptr i8, i8* %tmp8, i32 7 store i8 %h, i8* %p0 store i8 %g, i8* %p1 store i8 %f, i8* %p2 @@ -60,7 +63,7 @@ define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d, store i8 %c, i8* %p5 store i8 %b, i8* %p6 store i8 %a, i8* %p7 - %concat = load i64* %tmp + %concat = load i64, i64* %tmp ret i64 %concat } @@ -68,4 +71,4 @@ define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) { %cond_i1 = icmp ne i32 %cond, 0 %res = select i1 %cond_i1, i32 %t, i32 %f ret i32 %res -} \ No newline at end of file +} diff --git a/test/Feature/_utils.leq36._ll b/test/Feature/_utils.leq36._ll new file mode 100644 index 00000000..32a73bb1 --- /dev/null +++ b/test/Feature/_utils.leq36._ll @@ -0,0 +1,71 @@ +define i32 @util_make_and_i1(i32 %a, i32 %b) { + %a_i1 = icmp ne i32 %a, 0 + %b_i1 = icmp ne i32 %b, 0 + %res_i1 = and i1 %a_i1, %b_i1 + %res = zext i1 %res_i1 to i32 + ret i32 %res +} + +define i32 @util_make_or_i1(i32 %a, i32 %b) { + %a_i1 = icmp ne i32 %a, 0 + %b_i1 = icmp ne i32 %b, 0 + %res_i1 = or i1 %a_i1, %b_i1 + %res = zext i1 %res_i1 to i32 + ret i32 %res +} + +define i16 @util_make_concat2(i8 %a, i8 %b) { + %tmp = alloca i16 + %tmp8 = bitcast i16* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + store i8 %b, i8* %p0 + store i8 %a, i8* %p1 + %concat = load i16* %tmp + ret i16 %concat +} + +define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) { + %tmp = alloca i32 + %tmp8 = bitcast i32* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + %p2 = getelementptr i8* %tmp8, i32 2 + %p3 = getelementptr i8* %tmp8, i32 3 + store i8 %d, i8* %p0 + store i8 %c, i8* %p1 + store i8 %b, i8* %p2 + store i8 %a, i8* %p3 + %concat = load i32* %tmp + ret i32 %concat +} + +define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d, + i8 %e, i8 %f, i8 %g, i8 %h) { + %tmp = alloca i64 + %tmp8 = bitcast i64* %tmp to i8* + %p0 = getelementptr i8* %tmp8, i32 0 + %p1 = getelementptr i8* %tmp8, i32 1 + %p2 = getelementptr i8* %tmp8, i32 2 + %p3 = getelementptr i8* %tmp8, i32 3 + %p4 = getelementptr i8* %tmp8, i32 4 + %p5 = getelementptr i8* %tmp8, i32 5 + %p6 = getelementptr i8* %tmp8, i32 6 + %p7 = getelementptr i8* %tmp8, i32 7 + store i8 %h, i8* %p0 + store i8 %g, i8* %p1 + store i8 %f, i8* %p2 + store i8 %e, i8* %p3 + store i8 %d, i8* %p4 + store i8 %c, i8* %p5 + store i8 %b, i8* %p6 + store i8 %a, i8* %p7 + %concat = load i64* %tmp + ret i64 %concat +} + +define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) { + %cond_i1 = icmp ne i32 %cond, 0 + %res = select i1 %cond_i1, i32 %t, i32 %f + ret i32 %res +} \ No newline at end of file |