From 461594277fe53d64ab89b02856232276916379d6 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Tue, 10 Apr 2012 01:05:46 +0000
Subject: 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
---
 lib/Module/IntrinsicCleaner.cpp | 26 +++++++++++++++++++++++++
 test/Feature/Overflow.ll        | 43 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+)
 create mode 100644 test/Feature/Overflow.ll

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
+}
-- 
cgit 1.4.1