Support UBSan-enabled binaries

34 files changed, 672 insertions, 50 deletions

diff --git a/test/Feature/ubsan/ubsan_alignment-assumption.c b/test/Feature/ubsan/ubsan_alignment-assumption.c
new file mode 100644
index 00000000..b48929ac
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_alignment-assumption.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-8.0
+
+// RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdlib.h>
+
+int main() {
+  size_t address;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+
+  char *ptr = (char *)address;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: alignment-assumption
+  __builtin_assume_aligned(ptr, 0x8000);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
new file mode 100644
index 00000000..587c5108
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-8.0
+
+// RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdlib.h>
+
+int main() {
+  size_t address;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+
+  char *ptr = (char *)address;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: alignment-assumption
+  __builtin_assume_aligned(ptr, 0x8000, 1);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
new file mode 100644
index 00000000..37eb0927
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
@@ -0,0 +1,18 @@
+// RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdlib.h>
+
+int main() {
+  int x = klee_range(0, 5, "x");
+  volatile int result;
+
+  char c[] __attribute__((aligned(8))) = {0, 0, 0, 0, 1, 2, 3, 4, 5};
+  int *p = (int *)&c[x];
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: misaligned-pointer-use
+  result = *p;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_array_bounds.c b/test/Feature/ubsan/ubsan_array_bounds.c
new file mode 100644
index 00000000..626d016b
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_array_bounds.c
@@ -0,0 +1,23 @@
+// RUN: %clang %s -fsanitize=array-bounds -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+unsigned int array_index(unsigned int n) {
+  unsigned int a[4] = {0};
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: out-of-bounds-index
+  return a[n];
+}
+
+int main() {
+  unsigned int x;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  result = array_index(x);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_bool.c b/test/Feature/ubsan/ubsan_bool.c
new file mode 100644
index 00000000..4c2a9dbb
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_bool.c
@@ -0,0 +1,17 @@
+// RUN: %clang %s -fsanitize=bool -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  unsigned char x;
+  volatile _Bool result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: load invalid value
+  result = *(_Bool *)&x;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/Feature/ubsan/ubsan_builtin.c
new file mode 100644
index 00000000..85cf02a8
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_builtin.c
@@ -0,0 +1,17 @@
+// REQUIRES: geq-llvm-6.0
+//
+// RUN: %clang %s -fsanitize=builtin -w -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  signed int x;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: invalid-builtin-use
+  __builtin_ctz(x);
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_enum.c b/test/Feature/ubsan/ubsan_enum.c
new file mode 100644
index 00000000..d6422fcb
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_enum.c
@@ -0,0 +1,22 @@
+// RUN: %clangxx %s -fsanitize=enum -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+enum E { a = 1 } e;
+
+int main() {
+  unsigned char x;
+  volatile bool result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  for (unsigned char *p = (unsigned char *)&e; p != (unsigned char *)(&e + 1); ++p)
+    *p = x;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: load invalid value
+  result = (int)e != -1;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_float_cast_overflow.c b/test/Feature/ubsan/ubsan_float_cast_overflow.c
new file mode 100644
index 00000000..749a340e
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_float_cast_overflow.c
@@ -0,0 +1,16 @@
+// RUN: %clang %s -fsanitize=float-cast-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  float f = 0x7fffff80;
+  volatile int result;
+
+  //  klee_make_symbolic(&f, sizeof(f), "f");
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: float-cast-overflow
+  result = f + 0x80;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_float_divide_by_zero.c b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
new file mode 100644
index 00000000..eec44393
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
@@ -0,0 +1,15 @@
+// RUN: %clang %s -fsanitize=float-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  float x = 1.0;
+
+  //  klee_make_symbolic(&x, sizeof(x), "x");
+  //  klee_assume(x != 0.0);
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: float-divide-by-zero
+  volatile float result = x / 0;
+}
diff --git a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
new file mode 100644
index 00000000..d8e99e54
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
@@ -0,0 +1,22 @@
+// REQUIRES: geq-llvm-8.0
+
+// RUN: %clang %s -fsanitize=implicit-integer-sign-change -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+signed int convert_unsigned_int_to_signed_int(unsigned int x) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: implicit-integer-sign-change
+  return x;
+}
+
+int main() {
+  unsigned int x;
+  volatile signed int result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  result = convert_unsigned_int_to_signed_int(x);
+  return 0;
+}
\ No newline at end of file
diff --git a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
new file mode 100644
index 00000000..3d6ffcd1
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
@@ -0,0 +1,22 @@
+// REQUIRES: geq-llvm-8.0
+
+// RUN: %clang %s -fsanitize=implicit-signed-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+unsigned char convert_signed_int_to_unsigned_char(signed int x) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: implicit-signed-integer-truncation
+  return x;
+}
+
+int main() {
+  signed int x;
+  volatile unsigned char result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  result = convert_signed_int_to_unsigned_char(x);
+  return 0;
+}
\ No newline at end of file
diff --git a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
new file mode 100644
index 00000000..5421d10f
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
@@ -0,0 +1,22 @@
+// REQUIRES: geq-llvm-8.0
+
+// RUN: %clang %s -fsanitize=implicit-unsigned-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+unsigned char convert_unsigned_int_to_unsigned_char(unsigned int x) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: implicit-unsigned-integer-truncation
+  return x;
+}
+
+int main() {
+  unsigned int x;
+  volatile unsigned char result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  result = convert_unsigned_int_to_unsigned_char(x);
+  return 0;
+}
\ No newline at end of file
diff --git a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
new file mode 100644
index 00000000..ff5458ab
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
@@ -0,0 +1,20 @@
+// RUN: %clang %s -fsanitize=integer-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#if defined(__SIZEOF_INT128__) && !defined(_WIN32)
+typedef __int128 intmax;
+#else
+typedef long long intmax;
+#endif
+
+int main() {
+  intmax x;
+  volatile intmax result;
+
+  klee_make_symbolic(&x, sizeof(x), "x");
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: integer division overflow
+  result = x / 0;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_nonnull_attribute.c b/test/Feature/ubsan/ubsan_nonnull_attribute.c
new file mode 100644
index 00000000..0e1c8411
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_nonnull_attribute.c
@@ -0,0 +1,21 @@
+// RUN: %clang %s -fsanitize=nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+__attribute__((nonnull)) int func(int *nonnull) { return *nonnull; }
+
+int main() {
+  _Bool null;
+  volatile int result;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  int local = 0;
+  int *arg = null ? 0x0 : &local;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: invalid-null-argument
+  result = func(arg);
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_null.c b/test/Feature/ubsan/ubsan_null.c
new file mode 100644
index 00000000..5f3a516f
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_null.c
@@ -0,0 +1,19 @@
+// RUN: %clang %s -fsanitize=null -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  _Bool null;
+  volatile int result;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  int local = 0;
+  int *arg = null ? 0x0 : &local;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: null-pointer-use
+  result = *arg;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_nullability_arg.c b/test/Feature/ubsan/ubsan_nullability_arg.c
new file mode 100644
index 00000000..38227a8b
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_nullability_arg.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-5.0
+
+// RUN: %clang %s -fsanitize=nullability-arg -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+void nonnull_arg(int *_Nonnull p) {}
+
+int main() {
+  _Bool null;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  int local = 0;
+  int *arg = null ? 0x0 : &local;
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: invalid-null-argument
+  nonnull_arg(arg);
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_nullability_assign.c b/test/Feature/ubsan/ubsan_nullability_assign.c
new file mode 100644
index 00000000..a2a9c5e4
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_nullability_assign.c
@@ -0,0 +1,25 @@
+// REQUIRES: geq-llvm-5.0
+
+// RUN: %clang %s -fsanitize=nullability-assign -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+void nonnull_assign(int *p) {
+  volatile int *_Nonnull local;
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: null-pointer-use
+  local = p;
+}
+
+int main() {
+  _Bool null;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  int local = 0;
+  int *arg = null ? 0x0 : &local;
+
+  nonnull_assign(arg);
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_nullability_return.c b/test/Feature/ubsan/ubsan_nullability_return.c
new file mode 100644
index 00000000..ffd7886c
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_nullability_return.c
@@ -0,0 +1,25 @@
+// REQUIRES: geq-llvm-5.0
+
+// RUN: %clang %s -fsanitize=nullability-return -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int *_Nonnull nonnull_retval(int *p) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: invalid-null-return
+  return p;
+}
+
+int main() {
+  _Bool null;
+  volatile int *result;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  int local = 0;
+  int *arg = null ? 0x0 : &local;
+
+  result = nonnull_retval(arg);
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
new file mode 100644
index 00000000..caee33af
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
@@ -0,0 +1,22 @@
+// REQUIRES: geq-llvm-5.0
+// REQUIRES: lt-llvm-10.0
+
+// RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  size_t address;
+  volatile char *result;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+  klee_assume(address != 0);
+
+  char *ptr = (char *)address;
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: pointer-overflow
+  result = ptr + 1;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
new file mode 100644
index 00000000..529c0d11
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-10.0
+
+// RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  size_t address;
+  volatile char *result;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+  klee_assume(address != 0);
+
+  char *ptr = (char *)address;
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-after-nonzero-offset
+  result = ptr + 1;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
new file mode 100644
index 00000000..dc9ff50f
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-10.0
+
+// RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  size_t address;
+  volatile char *result;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+
+  char *ptr = (char *)address;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-after-nonzero-offset
+  result = ptr + 1;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
new file mode 100644
index 00000000..29df3823
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
@@ -0,0 +1,21 @@
+// REQUIRES: geq-llvm-10.0
+
+// RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  size_t address;
+  volatile char *result;
+
+  klee_make_symbolic(&address, sizeof(address), "address");
+
+  char *ptr = (char *)address;;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-with-offset
+  result = ptr + 0;
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
new file mode 100644
index 00000000..8c445b0e
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
@@ -0,0 +1,24 @@
+// REQUIRES: geq-llvm-5.0
+
+// RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  char c;
+  char* ptr = &c;
+
+  size_t offset;
+  volatile char* result;
+
+  klee_make_symbolic(&offset, sizeof(offset), "offset");
+  klee_assume((size_t)(ptr) + offset != 0);
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: pointer-overflow
+  result = ptr + offset;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_return.c b/test/Feature/ubsan/ubsan_return.c
new file mode 100644
index 00000000..3e9c8ccb
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_return.c
@@ -0,0 +1,14 @@
+// RUN: %clangxx %s -fsanitize=return -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int no_return() {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: missing-return
+}
+
+int main() {
+  volatile int result = no_return();
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
new file mode 100644
index 00000000..d8fd661c
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
@@ -0,0 +1,22 @@
+// RUN: %clang %s -fsanitize=returns-nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+__attribute__((returns_nonnull)) char *foo(char *a) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: invalid-null-return
+  return a;
+}
+
+int main() {
+  _Bool null;
+  volatile char *result;
+
+  klee_make_symbolic(&null, sizeof(null), "null");
+
+  char local = 0;
+  char *arg = null ? 0x0 : &local;
+  result = foo(arg);
+  return 0;
+}
\ No newline at end of file
diff --git a/test/Feature/ubsan/ubsan_shift_base.c b/test/Feature/ubsan/ubsan_shift_base.c
new file mode 100644
index 00000000..31d87f43
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_shift_base.c
@@ -0,0 +1,23 @@
+// RUN: %clang %s -fsanitize=shift -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int lsh_overflow(signed int a, signed int b) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: shift out of bounds
+  return a << b;
+}
+
+int main() {
+  signed int a;
+  signed int b;
+  volatile signed int result;
+
+  klee_make_symbolic(&a, sizeof(a), "a");
+  klee_make_symbolic(&b, sizeof(b), "b");
+
+  result = lsh_overflow(a, b);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_shift_exponent.c b/test/Feature/ubsan/ubsan_shift_exponent.c
new file mode 100644
index 00000000..1716ecb9
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_shift_exponent.c
@@ -0,0 +1,23 @@
+// RUN: %clang %s -fsanitize=shift-exponent -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int rsh_inbounds(signed int a, signed int b) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: shift out of bounds
+  return a >> b;
+}
+
+int main() {
+  signed int a;
+  signed int b;
+  volatile signed int result;
+
+  klee_make_symbolic(&a, sizeof(a), "a");
+  klee_make_symbolic(&b, sizeof(b), "b");
+
+  result = rsh_inbounds(a, b);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_signed_integer_overflow.c b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
new file mode 100644
index 00000000..306d0935
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
@@ -0,0 +1,28 @@
+// RUN: %clang %s -fsanitize=signed-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#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: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: signed-integer-overflow
+  result = x + y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: signed-integer-overflow
+  result = x - y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: signed-integer-overflow
+  result = x * y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: signed-integer-overflow
+  result = -x;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_unreachable.c b/test/Feature/ubsan/ubsan_unreachable.c
new file mode 100644
index 00000000..56de8e61
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_unreachable.c
@@ -0,0 +1,16 @@
+// RUN: %clang %s -fsanitize=unreachable -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+void _Noreturn f() {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: unreachable-call
+  __builtin_unreachable();
+}
+
+int main() {
+  f();
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
new file mode 100644
index 00000000..fb90d97f
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
@@ -0,0 +1,28 @@
+// RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#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: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: unsigned-integer-overflow
+  result = x + y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: unsigned-integer-overflow
+  result = x - y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: unsigned-integer-overflow
+  result = x * y;
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: unsigned-integer-overflow
+  result = -x;
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_unsigned_shift_base.c b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
new file mode 100644
index 00000000..d08bfe16
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
@@ -0,0 +1,25 @@
+// REQUIRES: geq-llvm-12.0
+
+// RUN: %clang %s -fsanitize=unsigned-shift-base -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int lsh_overflow(unsigned int a, unsigned int b) {
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: shift out of bounds
+  return a << b;
+}
+
+int main() {
+  unsigned int a;
+  unsigned int b;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&a, sizeof(a), "a");
+  klee_make_symbolic(&b, sizeof(b), "b");
+
+  result = lsh_overflow(a, b);
+
+  return 0;
+}
diff --git a/test/Feature/ubsan/ubsan_vla_bound.c b/test/Feature/ubsan/ubsan_vla_bound.c
new file mode 100644
index 00000000..24a95d17
--- /dev/null
+++ b/test/Feature/ubsan/ubsan_vla_bound.c
@@ -0,0 +1,17 @@
+// RUN: %clang %s -fsanitize=vla-bound -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  int x;
+  volatile int result;
+
+  x = klee_range(-10, 10, "x");
+
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: non-positive-vla-index
+  int arr[x];
+  result = arr[0];
+  return 0;
+}
diff --git a/test/Feature/ubsan_signed_overflow.c b/test/Feature/ubsan_signed_overflow.c
deleted file mode 100644
index ced2ca06..00000000
--- a/test/Feature/ubsan_signed_overflow.c
+++ /dev/null
@@ -1,25 +0,0 @@
-// RUN: %clang %s -fsanitize=signed-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
-
-#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:[[@LINE+1]]: overflow on addition
-  result = x + y;
-
-  // CHECK: ubsan_signed_overflow.c:[[@LINE+1]]: overflow on subtraction
-  result = x - y;
-
-  // CHECK: ubsan_signed_overflow.c:[[@LINE+1]]: overflow on multiplication
-  result = x * y;
-
-  return 0;
-}
diff --git a/test/Feature/ubsan_unsigned_overflow.c b/test/Feature/ubsan_unsigned_overflow.c
deleted file mode 100644
index 2734f868..00000000
--- a/test/Feature/ubsan_unsigned_overflow.c
+++ /dev/null
@@ -1,25 +0,0 @@
-// RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s
-
-#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:[[@LINE+1]]: overflow on addition
-  result = x + y;
-
-  // CHECK: ubsan_unsigned_overflow.c:[[@LINE+1]]: overflow on subtraction
-  result = x - y;
-
-  // CHECK: ubsan_unsigned_overflow.c:[[@LINE+1]]: overflow on multiplication
-  result = x * y;
-
-  return 0;
-}