From 92c21e2d581bd7405032eaf67544611ccd30ab4e Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Fri, 13 Feb 2015 18:45:07 +0000
Subject: Fixed and refactored overflow test cases.

---
 test/Feature/ubsan_sadd_overflow.c     | 19 -------------------
 test/Feature/ubsan_signed_overflow.c   | 29 +++++++++++++++++++++++++++++
 test/Feature/ubsan_smul_overflow.c     | 19 -------------------
 test/Feature/ubsan_ssub_overflow.c     | 19 -------------------
 test/Feature/ubsan_uadd_overflow.c     | 19 -------------------
 test/Feature/ubsan_umul_overflow.c     | 22 ----------------------
 test/Feature/ubsan_unsigned_overflow.c | 29 +++++++++++++++++++++++++++++
 test/Feature/ubsan_usub_overflow.c     | 19 -------------------
 8 files changed, 58 insertions(+), 117 deletions(-)
 delete mode 100644 test/Feature/ubsan_sadd_overflow.c
 create mode 100644 test/Feature/ubsan_signed_overflow.c
 delete mode 100644 test/Feature/ubsan_smul_overflow.c
 delete mode 100644 test/Feature/ubsan_ssub_overflow.c
 delete mode 100644 test/Feature/ubsan_uadd_overflow.c
 delete mode 100644 test/Feature/ubsan_umul_overflow.c
 create mode 100644 test/Feature/ubsan_unsigned_overflow.c
 delete mode 100644 test/Feature/ubsan_usub_overflow.c

(limited to 'test')

diff --git a/test/Feature/ubsan_sadd_overflow.c b/test/Feature/ubsan_sadd_overflow.c
deleted file mode 100644
index 6ab3c3ab..00000000
--- a/test/Feature/ubsan_sadd_overflow.c
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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_signed_overflow.c b/test/Feature/ubsan_signed_overflow.c
new file mode 100644
index 00000000..9816d496
--- /dev/null
+++ b/test/Feature/ubsan_signed_overflow.c
@@ -0,0 +1,29 @@
+// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+
+// llvm-gcc 2.9 does not support -fsanitize=signed-integer-overflow
+// REQUIRES: not-llvm-2.9
+
+#include "klee/klee.h"
+
+int main()
+{
+  signed int x;
+  signed int y;
+  volatile signed int result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&y, sizeof(y), "y");
+
+  // CHECK: ubsan_signed_overflow.c:20: overflow on unsigned addition
+  result = x + y;
+
+  // CHECK: ubsan_signed_overflow.c:23: overflow on unsigned subtraction
+  result = x - y;
+
+  // CHECK: ubsan_signed_overflow.c:26: overflow on unsigned multiplication
+  result = x * y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_smul_overflow.c b/test/Feature/ubsan_smul_overflow.c
deleted file mode 100644
index 21a796cb..00000000
--- a/test/Feature/ubsan_smul_overflow.c
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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
deleted file mode 100644
index 5ba62567..00000000
--- a/test/Feature/ubsan_ssub_overflow.c
+++ /dev/null
@@ -1,19 +0,0 @@
-// 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_uadd_overflow.c b/test/Feature/ubsan_uadd_overflow.c
deleted file mode 100644
index 9dc6832d..00000000
--- a/test/Feature/ubsan_uadd_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_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
deleted file mode 100644
index 2525a5e0..00000000
--- a/test/Feature/ubsan_umul_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_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_unsigned_overflow.c b/test/Feature/ubsan_unsigned_overflow.c
new file mode 100644
index 00000000..82eacdd7
--- /dev/null
+++ b/test/Feature/ubsan_unsigned_overflow.c
@@ -0,0 +1,29 @@
+// RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
+
+// llvm-gcc 2.9 does not support -fsanitize=unsigned-integer-overflow
+// REQUIRES: not-llvm-2.9
+
+#include "klee/klee.h"
+
+int main()
+{
+  unsigned int x;
+  unsigned int y;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+  klee_make_symbolic(&y, sizeof(y), "y");
+
+  // CHECK: ubsan_unsigned_overflow.c:20: overflow on unsigned addition
+  result = x + y;
+
+  // CHECK: ubsan_unsigned_overflow.c:23: overflow on unsigned subtraction
+  result = x - y;
+
+  // CHECK: ubsan_unsigned_overflow.c:26: overflow on unsigned multiplication
+  result = x * y;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan_usub_overflow.c b/test/Feature/ubsan_usub_overflow.c
deleted file mode 100644
index bfd94e3c..00000000
--- a/test/Feature/ubsan_usub_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_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