about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorPeter Collingbourne <peter@pcc.me.uk>2012-04-10 01:05:46 +0000
committerPeter Collingbourne <peter@pcc.me.uk>2012-04-10 01:05:46 +0000
commit461594277fe53d64ab89b02856232276916379d6 (patch)
treee9c65659a692cb1db9baa1f7ab72cb36b831a048
parent7ee405c0c792aef83435a2a6fc0a10734f47ba97 (diff)
downloadklee-461594277fe53d64ab89b02856232276916379d6.tar.gz
Lowering support for the llvm.uadd.with.overflow intrinsic.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154367 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--lib/Module/IntrinsicCleaner.cpp26
-rw-r--r--test/Feature/Overflow.ll43
2 files changed, 69 insertions, 0 deletions
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 8e326af9..8b0be35a 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -23,6 +23,7 @@
 #include "llvm/Module.h"
 #include "llvm/Pass.h"
 #include "llvm/Type.h"
+#include "llvm/Support/IRBuilder.h"
 #include "llvm/Transforms/Scalar.h"
 #include "llvm/Transforms/Utils/BasicBlockUtils.h"
 #include "llvm/Target/TargetData.h"
@@ -94,6 +95,31 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         break;
       }
 
+      case Intrinsic::uadd_with_overflow: {
+        IRBuilder<> builder(ii->getParent(), ii);
+
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
+        Value *op1 = ii->getOperand(1);
+        Value *op2 = ii->getOperand(2);
+#else
+        Value *op1 = ii->getArgOperand(0);
+        Value *op2 = ii->getArgOperand(1);
+#endif
+        
+        Value *result = builder.CreateAdd(op1, op2);
+        Value *overflow = builder.CreateICmpULT(result, op1);
+        
+        Value *resultStruct =
+          builder.CreateInsertValue(UndefValue::get(ii->getType()), result, 0);
+        resultStruct = builder.CreateInsertValue(resultStruct, overflow, 1);
+        
+        ii->replaceAllUsesWith(resultStruct);
+        ii->removeFromParent();
+        delete ii;
+        dirty = true;
+        break;
+      }
+
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 7)
       case Intrinsic::dbg_stoppoint: {
         // We can remove this stoppoint if the next instruction is
diff --git a/test/Feature/Overflow.ll b/test/Feature/Overflow.ll
new file mode 100644
index 00000000..90ace60b
--- /dev/null
+++ b/test/Feature/Overflow.ll
@@ -0,0 +1,43 @@
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: %klee -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
+}