Detect overflow of unsigned add, sub and mul operations

This requires clang with -fsanitize=unsigned-integer-overflow
tested with clang and llvm 3.4.2

4 files changed, 45 insertions, 4 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 59e269cb..04a82cf7 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -108,6 +108,11 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   // operator new(unsigned long)
   add("_Znwm", handleNew, true),
 
+  // clang -fsanitize=unsigned-integer-overflow
+  add("__ubsan_handle_add_overflow", handleAddOverflow, false),
+  add("__ubsan_handle_sub_overflow", handleSubOverflow, false),
+  add("__ubsan_handle_mul_overflow", handleMulOverflow, false),
+
 #undef addDNR
 #undef add  
 };
@@ -707,3 +712,27 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
+
+void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state,
+                                               KInstruction *target,
+                                               std::vector<ref<Expr> > &arguments) {
+  executor.terminateStateOnError(state,
+                                 "overflow on unsigned addition",
+                                 "overflow.err");
+}
+
+void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state,
+                                               KInstruction *target,
+                                               std::vector<ref<Expr> > &arguments) {
+  executor.terminateStateOnError(state,
+                                 "overflow on unsigned subtraction",
+                                 "overflow.err");
+}
+
+void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state,
+                                               KInstruction *target,
+                                               std::vector<ref<Expr> > &arguments) {
+  executor.terminateStateOnError(state,
+                                 "overflow on unsigned multiplication",
+                                 "overflow.err");
+}
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index f68c6edb..601b149b 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -132,6 +132,9 @@ namespace klee {
     HANDLER(handleUnderConstrained);
     HANDLER(handleWarning);
     HANDLER(handleWarningOnce);
+    HANDLER(handleAddOverflow);
+    HANDLER(handleMulOverflow);
+    HANDLER(handleSubOverflow);
 #undef HANDLER
   };
 } // End klee namespace
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 0f095269..ebdbd3a6 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -117,6 +117,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
       }
 
       case Intrinsic::uadd_with_overflow:
+      case Intrinsic::usub_with_overflow:
       case Intrinsic::umul_with_overflow: {
         IRBuilder<> builder(ii->getParent(), ii);
 
@@ -124,13 +125,18 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
         Value *op2 = ii->getArgOperand(1);
         
         Value *result = 0;
-        if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow)
+        Value *overflow = 0;
+        if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow){
           result = builder.CreateAdd(op1, op2);
-        else
+          overflow = builder.CreateICmpULT(result, op1);
+        } else if (ii->getIntrinsicID() == Intrinsic::usub_with_overflow){
+          result = builder.CreateSub(op1, op2);
+          overflow = builder.CreateICmpUGT(result, op1);
+        } else if (ii->getIntrinsicID() == Intrinsic::umul_with_overflow){
           result = builder.CreateMul(op1, op2);
+          overflow = builder.CreateICmpULT(result, op1);
+        }
 
-        Value *overflow = builder.CreateICmpULT(result, op1);
-        
         Value *resultStruct =
           builder.CreateInsertValue(UndefValue::get(ii->getType()), result, 0);
         resultStruct = builder.CreateInsertValue(resultStruct, overflow, 1);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 23c07f03..decf586d 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -765,6 +765,9 @@ static const char *modelledExternals[] = {
   "_Znwj", 
   "_Znam", 
   "_Znwm", 
+  "__ubsan_handle_add_overflow",
+  "__ubsan_handle_sub_overflow",
+  "__ubsan_handle_mul_overflow",
 };
 // Symbols we aren't going to warn about
 static const char *dontCareExternals[] = {