about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2020-04-29 19:44:29 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-06-06 19:03:03 +0100
commit6ca440f14381c8f0461ede18eccc16bba1135e88 (patch)
treeadeb3a84fe2c10bd937293068c6b2860f89f6479
parentdaa2d4d202929f9f7ba38dd76feabf2fa34816ab (diff)
downloadklee-6ca440f14381c8f0461ede18eccc16bba1135e88.tar.gz
[Module] Add testcase for inline asm lifting
-rw-r--r--test/Feature/asm_lifting.ll27
1 files changed, 27 insertions, 0 deletions
diff --git a/test/Feature/asm_lifting.ll b/test/Feature/asm_lifting.ll
new file mode 100644
index 00000000..4f414eeb
--- /dev/null
+++ b/test/Feature/asm_lifting.ll
@@ -0,0 +1,27 @@
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: rm -rf %t.klee-out
+; RUN: %klee --output-dir=%t.klee-out --optimize=false %t1.bc
+; RUN: FileCheck %s --input-file=%t.klee-out/assembly.ll
+
+define i32 @asm_free() nounwind {
+entry:
+  call void asm sideeffect "", "~{memory},~{dirflag},~{fpsr},~{flags}"()
+  ; Make sure simple memory barrier is lifted
+  ; CHECK-NOT: call void asm sideeffect "", "~{memory},~{dirflag},~{fpsr},~{flags}"()
+  ret i32 0
+}
+
+define i32 @unlifted_asm() nounwind {
+entry:
+  %0 = alloca [47 x i8], align 16
+  %1 = getelementptr inbounds [47 x i8], [47 x i8]* %0, i64 0, i64 0
+  ; Make sure memory barrier with function arguments is kept
+  %2 = call i8* asm sideeffect "", "=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1)
+  ; CHECK: %2 = call i8* asm sideeffect "", "=r,0,~{memory},~{dirflag},~{fpsr},~{flags}"(i8* nonnull %1)
+  ret i32 0
+}
+
+define i32 @main() nounwind {
+entry:
+  ret i32 0
+}