refactor integer overflow detection, add signed int

Instead of checking for every possible casse which result in overflow,
it is much simpler to perform the operation using integers with bigger
dimension and check if the result overflow

10 files changed, 141 insertions, 49 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 04a82cf7..f06ae4f5 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("__ubsan_handle_add_overflow", handleAddOverflow, false),
   add("__ubsan_handle_sub_overflow", handleSubOverflow, false),
   add("__ubsan_handle_mul_overflow", handleMulOverflow, false),
+  add("__ubsan_handle_divrem_overflow", handleDivRemOverflow, false),
 
 #undef addDNR
 #undef add  
@@ -736,3 +737,11 @@ void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state,
                                  "overflow on unsigned multiplication",
                                  "overflow.err");
 }
+
+void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state,
+                                               KInstruction *target,
+                                               std::vector<ref<Expr> > &arguments) {
+  executor.terminateStateOnError(state,
+                                 "overflow on division or remainder",
+                                 "overflow.err");
+}
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 601b149b..d52b8fc5 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -135,6 +135,7 @@ namespace klee {
     HANDLER(handleAddOverflow);
     HANDLER(handleMulOverflow);
     HANDLER(handleSubOverflow);
+    HANDLER(handleDivRemOverflow);
 #undef HANDLER
   };
 } // End klee namespace
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 9d4f0fec..da97621a 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -118,59 +118,83 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
         break;
       }
 
+      case Intrinsic::sadd_with_overflow:
+      case Intrinsic::ssub_with_overflow:
+      case Intrinsic::smul_with_overflow:
       case Intrinsic::uadd_with_overflow:
       case Intrinsic::usub_with_overflow:
       case Intrinsic::umul_with_overflow: {
         IRBuilder<> builder(ii->getParent(), ii);
-        Function *F = builder.GetInsertBlock()->getParent();
 
         Value *op1 = ii->getArgOperand(0);
         Value *op2 = ii->getArgOperand(1);
         
         Value *result = 0;
+        Value *result_ext = 0;
         Value *overflow = 0;
-        if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow){
-          result = builder.CreateAdd(op1, op2);
-          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){
-          BasicBlock *entry = builder.GetInsertBlock();
-          entry->setName(Twine(entry->getName(), "_umul_start"));
-          BasicBlock *cont_of = entry->splitBasicBlock(builder.GetInsertPoint(),
-                                                       "umul_end");
-          BasicBlock *on_of = BasicBlock::Create(builder.getContext(),
-                                                 "umul_overflow", F, cont_of);
-
-          // remove the branch inserted by splitBasicBlock, we'll add our own
-          entry->getTerminator()->eraseFromParent();
-          builder.SetInsertPoint(entry);
-          Value *no_overflow = builder.getFalse();
-          Value *one = ConstantInt::getSigned(op1->getType(), 1);
-          Value *op1_g1 = builder.CreateICmpUGT(op1, one);
-          Value *op2_g1 = builder.CreateICmpUGT(op2, one);
-          Value *may_of = builder.CreateAnd(op1_g1, op2_g1);
-          builder.CreateCondBr(may_of, on_of, cont_of);
-
-          builder.SetInsertPoint(on_of);
-          uint64_t bit_size = op1->getType()->getPrimitiveSizeInBits();
-          Value *uint_max = ConstantInt::get(op1->getType(),
-                                             APInt::getMaxValue(bit_size));
-          Value *div1 = builder.CreateUDiv(uint_max, op1);
-          Value *overflow1 = builder.CreateICmpUGT(op2, div1);
-          builder.CreateBr(cont_of);
-
-          builder.SetInsertPoint(cont_of, cont_of->begin());
-          PHINode *phi_of = builder.CreatePHI(no_overflow->getType(), 2);
-          phi_of->addIncoming(overflow1, on_of);
-          phi_of->addIncoming(no_overflow, entry);
-
-          result = builder.CreateMul(op1, op2);
-          overflow = phi_of;
-          block_split = true;
+
+        unsigned int bw = op1->getType()->getPrimitiveSizeInBits();
+        unsigned int bw2 = op1->getType()->getPrimitiveSizeInBits()*2;
+
+        if ((ii->getIntrinsicID() == Intrinsic::uadd_with_overflow) ||
+            (ii->getIntrinsicID() == Intrinsic::usub_with_overflow) ||
+            (ii->getIntrinsicID() == Intrinsic::umul_with_overflow)) {
+
+          Value *op1ext =
+            builder.CreateZExt(op1, IntegerType::get(M.getContext(), bw2));
+          Value *op2ext =
+            builder.CreateZExt(op2, IntegerType::get(M.getContext(), bw2));
+          Value *int_max_s =
+            ConstantInt::get(op1->getType(), APInt::getMaxValue(bw));
+          Value *int_max =
+            builder.CreateZExt(int_max_s, IntegerType::get(M.getContext(), bw2));
+
+          if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow){
+            result_ext = builder.CreateAdd(op1ext, op2ext);
+          } else if (ii->getIntrinsicID() == Intrinsic::usub_with_overflow){
+            result_ext = builder.CreateSub(op1ext, op2ext);
+          } else if (ii->getIntrinsicID() == Intrinsic::umul_with_overflow){
+            result_ext = builder.CreateMul(op1ext, op2ext);
+          }
+          overflow = builder.CreateICmpUGT(result_ext, int_max);
+
+        } else if ((ii->getIntrinsicID() == Intrinsic::sadd_with_overflow) ||
+                   (ii->getIntrinsicID() == Intrinsic::ssub_with_overflow) ||
+                   (ii->getIntrinsicID() == Intrinsic::smul_with_overflow)) {
+
+          Value *op1ext =
+            builder.CreateSExt(op1, IntegerType::get(M.getContext(), bw2));
+          Value *op2ext =
+            builder.CreateSExt(op2, IntegerType::get(M.getContext(), bw2));
+          Value *int_max_s =
+            ConstantInt::get(op1->getType(), APInt::getSignedMaxValue(bw));
+          Value *int_min_s =
+            ConstantInt::get(op1->getType(), APInt::getSignedMinValue(bw));
+          Value *int_max =
+            builder.CreateSExt(int_max_s, IntegerType::get(M.getContext(), bw2));
+          Value *int_min =
+            builder.CreateSExt(int_min_s, IntegerType::get(M.getContext(), bw2));
+
+          if (ii->getIntrinsicID() == Intrinsic::sadd_with_overflow){
+            result_ext = builder.CreateAdd(op1ext, op2ext);
+          } else if (ii->getIntrinsicID() == Intrinsic::ssub_with_overflow){
+            result_ext = builder.CreateSub(op1ext, op2ext);
+          } else if (ii->getIntrinsicID() == Intrinsic::smul_with_overflow){
+            result_ext = builder.CreateMul(op1ext, op2ext);
+          }
+          overflow = builder.CreateOr(builder.CreateICmpSGT(result_ext, int_max),
+                                      builder.CreateICmpSLT(result_ext, int_min));
         }
 
+        // This trunc cound be replaced by a more general trunc replacement
+        // that allows to detect also undefined behavior in assignments or
+        // overflow in operation with integers whose dimension is smaller than
+        // int's dimension, e.g.
+        //     uint8_t = uint8_t + uint8_t;
+        // if one desires the wrapping should write
+        //     uint8_t = (uint8_t + uint8_t) & 0xFF;
+        // before this, must check if it has side effects on other operations
+        result = builder.CreateTrunc(result_ext, op1->getType());
         Value *resultStruct =
           builder.CreateInsertValue(UndefValue::get(ii->getType()), result, 0);
         resultStruct = builder.CreateInsertValue(resultStruct, overflow, 1);
diff --git a/test/Feature/ubsan_sadd_overflow.c b/test/Feature/ubsan_sadd_overflow.c
new file mode 100644
index 00000000..6ab3c3ab
--- /dev/null
+++ b/test/Feature/ubsan_sadd_overflow.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee %t.bc 2> %t.log
+// RUN: grep -c "overflow on unsigned addition" %t.log
+// RUN: grep -c "ubsan_sadd_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  signed int x;
+  signed int y;
+  volatile signed int result;
+
+  klee_make_symbolic(&x, sizeof(x), "signed add 1");
+  klee_make_symbolic(&y, sizeof(y), "signed add 2");
+  result = x + y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_smul_overflow.c b/test/Feature/ubsan_smul_overflow.c
new file mode 100644
index 00000000..21a796cb
--- /dev/null
+++ b/test/Feature/ubsan_smul_overflow.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee %t.bc 2> %t.log
+// RUN: grep -c "overflow on unsigned multiplication" %t.log
+// RUN: grep -c "ubsan_smul_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  int x;
+  int y;
+  volatile int result;
+
+  klee_make_symbolic(&x, sizeof(x), "signed mul 1");
+  klee_make_symbolic(&y, sizeof(y), "signed mul 2");
+  result = x * y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_ssub_overflow.c b/test/Feature/ubsan_ssub_overflow.c
new file mode 100644
index 00000000..5ba62567
--- /dev/null
+++ b/test/Feature/ubsan_ssub_overflow.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee %t.bc 2> %t.log
+// RUN: grep -c "overflow on unsigned subtraction" %t.log
+// RUN: grep -c "ubsan_ssub_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  signed int x;
+  signed int y;
+  volatile signed int result;
+
+  klee_make_symbolic(&x, sizeof(x), "signed sub 1");
+  klee_make_symbolic(&y, sizeof(y), "signed sub 2");
+  result = x - y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_add_overflow.c b/test/Feature/ubsan_uadd_overflow.c
index 87701029..9dc6832d 100644
--- a/test/Feature/ubsan_add_overflow.c
+++ b/test/Feature/ubsan_uadd_overflow.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
 // RUN: %klee %t.bc 2> %t.log
 // RUN: grep -c "overflow on unsigned addition" %t.log
-// RUN: grep -c "ubsan_add_overflow.c:16: overflow" %t.log
+// RUN: grep -c "ubsan_uadd_overflow.c:16: overflow" %t.log
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan_mul_overflow.c b/test/Feature/ubsan_umul_overflow.c
index 12300b05..2525a5e0 100644
--- a/test/Feature/ubsan_mul_overflow.c
+++ b/test/Feature/ubsan_umul_overflow.c
@@ -1,8 +1,8 @@
 // RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
 // RUN: %klee %t.bc 2> %t.log
 // RUN: grep -c "overflow on unsigned multiplication" %t.log
-// RUN: grep -c "ubsan_mul_overflow.c:18: overflow" %t.log
-// RUN: grep -c "ubsan_mul_overflow.c:19: overflow" %t.log
+// RUN: grep -c "ubsan_umul_overflow.c:18: overflow" %t.log
+// RUN: grep -c "ubsan_umul_overflow.c:19: overflow" %t.log
 
 #include "klee/klee.h"
 
@@ -13,8 +13,8 @@ int main()
   uint32_t x2=3147483648, y2=3727483648;
   volatile unsigned int result;
 
-  klee_make_symbolic(&x, sizeof(x), "unsigned add 1");
-  klee_make_symbolic(&y, sizeof(y), "unsigned add 2");
+  klee_make_symbolic(&x, sizeof(x), "unsigned mul 1");
+  klee_make_symbolic(&y, sizeof(y), "unsigned mul 2");
   result = x * y;
   result = x2 * y2;
 
diff --git a/test/Feature/ubsan_sub_overflow.c b/test/Feature/ubsan_usub_overflow.c
index 37a251bc..bfd94e3c 100644
--- a/test/Feature/ubsan_sub_overflow.c
+++ b/test/Feature/ubsan_usub_overflow.c
@@ -1,7 +1,7 @@
 // RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
 // RUN: %klee %t.bc 2> %t.log
 // RUN: grep -c "overflow on unsigned subtraction" %t.log
-// RUN: grep -c "ubsan_sub_overflow.c:16: overflow" %t.log
+// RUN: grep -c "ubsan_usub_overflow.c:16: overflow" %t.log
 
 #include "klee/klee.h"
 
@@ -11,8 +11,8 @@ int main()
   unsigned int y;
   volatile unsigned int result;
 
-  klee_make_symbolic(&x, sizeof(x), "unsigned add 1");
-  klee_make_symbolic(&y, sizeof(y), "unsigned add 2");
+  klee_make_symbolic(&x, sizeof(x), "unsigned sub 1");
+  klee_make_symbolic(&y, sizeof(y), "unsigned sub 2");
   result = x - y;
 
   return 0;
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index decf586d..8a246685 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -768,6 +768,7 @@ static const char *modelledExternals[] = {
   "__ubsan_handle_add_overflow",
   "__ubsan_handle_sub_overflow",
   "__ubsan_handle_mul_overflow",
+  "__ubsan_handle_divrem_overflow",
 };
 // Symbols we aren't going to warn about
 static const char *dontCareExternals[] = {