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

6 files changed, 65 insertions, 8 deletions

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;