From 714dc22ccb12efdc203e8ce92d6e546ca9ffb157 Mon Sep 17 00:00:00 2001
From: Luca Dariz <l.dariz@imamoter.cnr.t>
Date: Thu, 20 Nov 2014 12:41:12 +0100
Subject: 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
---
 test/Feature/ubsan_add_overflow.c  | 19 -------------------
 test/Feature/ubsan_mul_overflow.c  | 22 ----------------------
 test/Feature/ubsan_sadd_overflow.c | 19 +++++++++++++++++++
 test/Feature/ubsan_smul_overflow.c | 19 +++++++++++++++++++
 test/Feature/ubsan_ssub_overflow.c | 19 +++++++++++++++++++
 test/Feature/ubsan_sub_overflow.c  | 19 -------------------
 test/Feature/ubsan_uadd_overflow.c | 19 +++++++++++++++++++
 test/Feature/ubsan_umul_overflow.c | 22 ++++++++++++++++++++++
 test/Feature/ubsan_usub_overflow.c | 19 +++++++++++++++++++
 9 files changed, 117 insertions(+), 60 deletions(-)
 delete mode 100644 test/Feature/ubsan_add_overflow.c
 delete mode 100644 test/Feature/ubsan_mul_overflow.c
 create mode 100644 test/Feature/ubsan_sadd_overflow.c
 create mode 100644 test/Feature/ubsan_smul_overflow.c
 create mode 100644 test/Feature/ubsan_ssub_overflow.c
 delete mode 100644 test/Feature/ubsan_sub_overflow.c
 create mode 100644 test/Feature/ubsan_uadd_overflow.c
 create mode 100644 test/Feature/ubsan_umul_overflow.c
 create mode 100644 test/Feature/ubsan_usub_overflow.c

(limited to 'test/Feature')

diff --git a/test/Feature/ubsan_add_overflow.c b/test/Feature/ubsan_add_overflow.c
deleted file mode 100644
index 87701029..00000000
--- a/test/Feature/ubsan_add_overflow.c
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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
-
-#include "klee/klee.h"
-
-int main()
-{
-  unsigned int x;
-  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");
-  result = x + y;
-
-  return 0;
-}
diff --git a/test/Feature/ubsan_mul_overflow.c b/test/Feature/ubsan_mul_overflow.c
deleted file mode 100644
index 12300b05..00000000
--- a/test/Feature/ubsan_mul_overflow.c
+++ /dev/null
@@ -1,22 +0,0 @@
-// 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
-
-#include "klee/klee.h"
-
-int main()
-{
-  unsigned int x;
-  unsigned int y;
-  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");
-  result = x * y;
-  result = x2 * y2;
-
-  return 0;
-}
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_sub_overflow.c b/test/Feature/ubsan_sub_overflow.c
deleted file mode 100644
index 37a251bc..00000000
--- a/test/Feature/ubsan_sub_overflow.c
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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
-
-#include "klee/klee.h"
-
-int main()
-{
-  unsigned int x;
-  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");
-  result = x - y;
-
-  return 0;
-}
diff --git a/test/Feature/ubsan_uadd_overflow.c b/test/Feature/ubsan_uadd_overflow.c
new file mode 100644
index 00000000..9dc6832d
--- /dev/null
+++ b/test/Feature/ubsan_uadd_overflow.c
@@ -0,0 +1,19 @@
+// 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_uadd_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  unsigned int x;
+  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");
+  result = x + y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_umul_overflow.c b/test/Feature/ubsan_umul_overflow.c
new file mode 100644
index 00000000..2525a5e0
--- /dev/null
+++ b/test/Feature/ubsan_umul_overflow.c
@@ -0,0 +1,22 @@
+// 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_umul_overflow.c:18: overflow" %t.log
+// RUN: grep -c "ubsan_umul_overflow.c:19: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  unsigned int x;
+  unsigned int y;
+  uint32_t x2=3147483648, y2=3727483648;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&x, sizeof(x), "unsigned mul 1");
+  klee_make_symbolic(&y, sizeof(y), "unsigned mul 2");
+  result = x * y;
+  result = x2 * y2;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_usub_overflow.c b/test/Feature/ubsan_usub_overflow.c
new file mode 100644
index 00000000..bfd94e3c
--- /dev/null
+++ b/test/Feature/ubsan_usub_overflow.c
@@ -0,0 +1,19 @@
+// 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_usub_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  unsigned int x;
+  unsigned int y;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&x, sizeof(x), "unsigned sub 1");
+  klee_make_symbolic(&y, sizeof(y), "unsigned sub 2");
+  result = x - y;
+
+  return 0;
+}
-- 
cgit 1.4.1