Support UBSan-enabled binaries

47 files changed, 1624 insertions, 95 deletions

diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 2b788d60..f4b09f36 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -32,7 +32,7 @@
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
 
-#include <errno.h>
+#include <cerrno>
 #include <sstream>
 
 using namespace llvm;
@@ -139,13 +139,6 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   // operator new(unsigned long)
   add("_Znwm", handleNew, true),
 
-  // Run clang with -fsanitize=signed-integer-overflow and/or
-  // -fsanitize=unsigned-integer-overflow
-  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
 };
@@ -878,31 +871,3 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
     mo->isGlobal = true;
   }
 }
-
-void SpecialFunctionHandler::handleAddOverflow(
-    ExecutionState &state, KInstruction *target,
-    std::vector<ref<Expr>> &arguments) {
-  executor.terminateStateOnError(state, "overflow on addition",
-                                 StateTerminationType::Overflow);
-}
-
-void SpecialFunctionHandler::handleSubOverflow(
-    ExecutionState &state, KInstruction *target,
-    std::vector<ref<Expr>> &arguments) {
-  executor.terminateStateOnError(state, "overflow on subtraction",
-                                 StateTerminationType::Overflow);
-}
-
-void SpecialFunctionHandler::handleMulOverflow(
-    ExecutionState &state, KInstruction *target,
-    std::vector<ref<Expr>> &arguments) {
-  executor.terminateStateOnError(state, "overflow on multiplication",
-                                 StateTerminationType::Overflow);
-}
-
-void SpecialFunctionHandler::handleDivRemOverflow(
-    ExecutionState &state, KInstruction *target,
-    std::vector<ref<Expr>> &arguments) {
-  executor.terminateStateOnError(state, "overflow on division or remainder",
-                                 StateTerminationType::Overflow);
-}
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index a9f7100d..9487fdf5 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -34,7 +34,7 @@ namespace klee {
                                                     KInstruction *target, 
                                                     std::vector<ref<Expr> > 
                                                       &arguments);
-    typedef std::map<const llvm::Function*, 
+    typedef std::map<const llvm::Function*,
                      std::pair<Handler,bool> > handlers_ty;
 
     handlers_ty handlers;
@@ -144,10 +144,6 @@ namespace klee {
     HANDLER(handleUnderConstrained);
     HANDLER(handleWarning);
     HANDLER(handleWarningOnce);
-    HANDLER(handleAddOverflow);
-    HANDLER(handleMulOverflow);
-    HANDLER(handleSubOverflow);
-    HANDLER(handleDivRemOverflow);
 #undef HANDLER
   };
 } // End klee namespace
diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt
index 5747672c..c2f3e405 100644
--- a/runtime/CMakeLists.txt
+++ b/runtime/CMakeLists.txt
@@ -109,6 +109,9 @@ if (ENABLE_POSIX_RUNTIME)
     add_subdirectory(POSIX)
 endif ()
 
+list(APPEND RUNTIME_LIBRARIES UBSan)
+add_subdirectory(Sanitizer)
+
 add_custom_target(BuildKLEERuntimes
         DEPENDS "${RUNTIME_LIBRARIES}"
         )
diff --git a/runtime/Sanitizer/CMakeLists.txt b/runtime/Sanitizer/CMakeLists.txt
new file mode 100644
index 00000000..39031dfb
--- /dev/null
+++ b/runtime/Sanitizer/CMakeLists.txt
@@ -0,0 +1,18 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+# Set up
+set(LIB_PREFIX "UBSan")
+set(SRC_FILES
+        ubsan/ubsan_handlers.cpp
+        )
+
+# Build it
+include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake")
+prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files)
+add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "" "")
\ No newline at end of file
diff --git a/runtime/Sanitizer/sanitizer_common/sanitizer_common.h b/runtime/Sanitizer/sanitizer_common/sanitizer_common.h
new file mode 100644
index 00000000..ebb88600
--- /dev/null
+++ b/runtime/Sanitizer/sanitizer_common/sanitizer_common.h
@@ -0,0 +1,20 @@
+//===-- sanitizer_common.h --------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file is shared between run-time libraries of sanitizers.
+//
+// It declares common functions and classes that are used in both runtimes.
+// Implementation of some functions are provided in sanitizer_common, while
+// others must be defined by run-time library itself.
+//===----------------------------------------------------------------------===//
+#ifndef SANITIZER_COMMON_H
+#define SANITIZER_COMMON_H
+
+#include "sanitizer_internal_defs.h"
+
+#endif // SANITIZER_COMMON_H
diff --git a/runtime/Sanitizer/sanitizer_common/sanitizer_internal_defs.h b/runtime/Sanitizer/sanitizer_common/sanitizer_internal_defs.h
new file mode 100644
index 00000000..d0817abe
--- /dev/null
+++ b/runtime/Sanitizer/sanitizer_common/sanitizer_internal_defs.h
@@ -0,0 +1,51 @@
+//===-- sanitizer_internal_defs.h -------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file is shared between AddressSanitizer and ThreadSanitizer.
+// It contains macro used in run-time libraries code.
+//===----------------------------------------------------------------------===//
+#ifndef SANITIZER_DEFS_H
+#define SANITIZER_DEFS_H
+
+#include "sanitizer_platform.h"
+
+// For portability reasons we do not include stddef.h, stdint.h or any other
+// system header, but we do need some basic types that are not defined
+// in a portable way by the language itself.
+namespace __sanitizer {
+
+#if defined(_WIN64)
+// 64-bit Windows uses LLP64 data model.
+typedef unsigned long long uptr;
+typedef signed long long sptr;
+#else
+#if (SANITIZER_WORDSIZE == 64) || defined(__APPLE__) || defined(_WIN32)
+typedef unsigned long uptr;
+typedef signed long sptr;
+#else
+typedef unsigned int uptr;
+typedef signed int sptr;
+#endif
+#endif // defined(_WIN64)
+
+typedef unsigned char u8;
+typedef unsigned short u16;
+typedef unsigned int u32;
+typedef unsigned long long u64;
+typedef signed char s8;
+typedef signed short s16;
+typedef signed int s32;
+typedef signed long long s64;
+
+} // namespace __sanitizer
+
+namespace __ubsan {
+using namespace __sanitizer;
+}
+
+#endif // SANITIZER_DEFS_H
diff --git a/runtime/Sanitizer/sanitizer_common/sanitizer_platform.h b/runtime/Sanitizer/sanitizer_common/sanitizer_platform.h
new file mode 100644
index 00000000..074d2b74
--- /dev/null
+++ b/runtime/Sanitizer/sanitizer_common/sanitizer_platform.h
@@ -0,0 +1,21 @@
+//===-- sanitizer_platform.h ------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Common platform macros.
+//===----------------------------------------------------------------------===//
+
+#ifndef SANITIZER_PLATFORM_H
+#define SANITIZER_PLATFORM_H
+
+#if __LP64__ || defined(_WIN64)
+#define SANITIZER_WORDSIZE 64
+#else
+#define SANITIZER_WORDSIZE 32
+#endif
+
+#endif // SANITIZER_PLATFORM_H
diff --git a/runtime/Sanitizer/ubsan/ubsan_checks.inc b/runtime/Sanitizer/ubsan/ubsan_checks.inc
new file mode 100644
index 00000000..b426beea
--- /dev/null
+++ b/runtime/Sanitizer/ubsan/ubsan_checks.inc
@@ -0,0 +1,97 @@
+//===-- ubsan_checks.inc ----------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// List of checks handled by UBSan runtime.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Config/Version.h"
+
+#ifndef UBSAN_CHECK
+# error "Define UBSAN_CHECK prior to including this file!"
+#endif
+
+// UBSAN_CHECK(Name, SummaryKind, FSanitizeFlagName)
+// SummaryKind and FSanitizeFlagName should be string literals.
+
+UBSAN_CHECK(GenericUB, "undefined-behavior", "undefined")
+UBSAN_CHECK(NullPointerUse, "null-pointer-use", "null")
+#if LLVM_VERSION_MAJOR >= 11
+UBSAN_CHECK(NullPointerUseWithNullability, "null-pointer-use",
+            "nullability-assign")
+#endif
+#if LLVM_VERSION_MAJOR >= 10
+UBSAN_CHECK(NullptrWithOffset, "nullptr-with-offset", "pointer-overflow")
+UBSAN_CHECK(NullptrWithNonZeroOffset, "nullptr-with-nonzero-offset",
+            "pointer-overflow")
+UBSAN_CHECK(NullptrAfterNonZeroOffset, "nullptr-after-nonzero-offset",
+            "pointer-overflow")
+#endif
+#if LLVM_VERSION_MAJOR >= 5
+UBSAN_CHECK(PointerOverflow, "pointer-overflow", "pointer-overflow")
+#endif
+UBSAN_CHECK(MisalignedPointerUse, "misaligned-pointer-use", "alignment")
+#if LLVM_VERSION_MAJOR >= 8
+UBSAN_CHECK(AlignmentAssumption, "alignment-assumption", "alignment")
+#endif
+UBSAN_CHECK(InsufficientObjectSize, "insufficient-object-size", "object-size")
+UBSAN_CHECK(SignedIntegerOverflow, "signed-integer-overflow",
+            "signed-integer-overflow")
+UBSAN_CHECK(UnsignedIntegerOverflow, "unsigned-integer-overflow",
+            "unsigned-integer-overflow")
+UBSAN_CHECK(IntegerDivideByZero, "integer-divide-by-zero",
+            "integer-divide-by-zero")
+UBSAN_CHECK(FloatDivideByZero, "float-divide-by-zero", "float-divide-by-zero")
+#if LLVM_VERSION_MAJOR >= 6
+UBSAN_CHECK(InvalidBuiltin, "invalid-builtin-use", "invalid-builtin-use")
+#endif
+#if LLVM_VERSION_MAJOR >= 11
+UBSAN_CHECK(InvalidObjCCast, "invalid-objc-cast", "invalid-objc-cast")
+#endif
+#if LLVM_VERSION_MAJOR >= 8
+UBSAN_CHECK(ImplicitUnsignedIntegerTruncation,
+            "implicit-unsigned-integer-truncation",
+            "implicit-unsigned-integer-truncation")
+UBSAN_CHECK(ImplicitSignedIntegerTruncation,
+            "implicit-signed-integer-truncation",
+            "implicit-signed-integer-truncation")
+#elif LLVM_VERSION_MAJOR >= 7
+UBSAN_CHECK(ImplicitIntegerTruncation, "implicit-integer-truncation",
+            "implicit-integer-truncation")
+#endif
+#if LLVM_VERSION_MAJOR >= 8
+UBSAN_CHECK(ImplicitIntegerSignChange,
+            "implicit-integer-sign-change",
+            "implicit-integer-sign-change")
+UBSAN_CHECK(ImplicitSignedIntegerTruncationOrSignChange,
+            "implicit-signed-integer-truncation-or-sign-change",
+            "implicit-signed-integer-truncation,implicit-integer-sign-change")
+#endif
+UBSAN_CHECK(InvalidShiftBase, "invalid-shift-base", "shift-base")
+UBSAN_CHECK(InvalidShiftExponent, "invalid-shift-exponent", "shift-exponent")
+UBSAN_CHECK(OutOfBoundsIndex, "out-of-bounds-index", "bounds")
+UBSAN_CHECK(UnreachableCall, "unreachable-call", "unreachable")
+UBSAN_CHECK(MissingReturn, "missing-return", "return")
+UBSAN_CHECK(NonPositiveVLAIndex, "non-positive-vla-index", "vla-bound")
+UBSAN_CHECK(FloatCastOverflow, "float-cast-overflow", "float-cast-overflow")
+UBSAN_CHECK(InvalidBoolLoad, "invalid-bool-load", "bool")
+UBSAN_CHECK(InvalidEnumLoad, "invalid-enum-load", "enum")
+UBSAN_CHECK(FunctionTypeMismatch, "function-type-mismatch", "function")
+UBSAN_CHECK(InvalidNullReturn, "invalid-null-return",
+            "returns-nonnull-attribute")
+#if LLVM_VERSION_MAJOR >= 11
+UBSAN_CHECK(InvalidNullReturnWithNullability, "invalid-null-return",
+            "nullability-return")
+#endif
+UBSAN_CHECK(InvalidNullArgument, "invalid-null-argument", "nonnull-attribute")
+#if LLVM_VERSION_MAJOR >= 11
+UBSAN_CHECK(InvalidNullArgumentWithNullability, "invalid-null-argument",
+            "nullability-arg")
+#endif
+UBSAN_CHECK(DynamicTypeMismatch, "dynamic-type-mismatch", "vptr")
+UBSAN_CHECK(CFIBadType, "cfi-bad-type", "cfi")
diff --git a/runtime/Sanitizer/ubsan/ubsan_diag.h b/runtime/Sanitizer/ubsan/ubsan_diag.h
new file mode 100644
index 00000000..71219ab7
--- /dev/null
+++ b/runtime/Sanitizer/ubsan/ubsan_diag.h
@@ -0,0 +1,36 @@
+//===-- ubsan_diag.h --------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Diagnostics emission for Clang's undefined behavior sanitizer.
+//
+//===----------------------------------------------------------------------===//
+#ifndef UBSAN_DIAG_H
+#define UBSAN_DIAG_H
+
+#include "ubsan_value.h"
+
+namespace __ubsan {
+
+/// \brief A C++ type name. Really just a strong typedef for 'const char*'.
+class TypeName {
+  const char *Name;
+
+public:
+  TypeName(const char *Name) : Name(Name) {}
+  const char *getName() const { return Name; }
+};
+
+enum /*class*/ ErrorType {
+#define UBSAN_CHECK(Name, SummaryKind, FSanitizeFlagName) Name,
+#include "ubsan_checks.inc"
+#undef UBSAN_CHECK
+};
+
+} // namespace __ubsan
+
+#endif // UBSAN_DIAG_H
diff --git a/runtime/Sanitizer/ubsan/ubsan_handlers.cpp b/runtime/Sanitizer/ubsan/ubsan_handlers.cpp
new file mode 100644
index 00000000..3cc9af2a
--- /dev/null
+++ b/runtime/Sanitizer/ubsan/ubsan_handlers.cpp
@@ -0,0 +1,500 @@
+//===-- ubsan_handlers.cpp ------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Error logging entry points for the UBSan runtime.
+//
+//===----------------------------------------------------------------------===//
+
+#include "ubsan_handlers.h"
+#include "ubsan_diag.h"
+
+extern "C" __attribute__((noreturn)) void klee_report_error(const char *file,
+                                                            int line,
+                                                            const char *message,
+                                                            const char *suffix);
+
+namespace __ubsan {
+static const char *ConvertTypeToString(ErrorType Type) {
+  switch (Type) {
+#define UBSAN_CHECK(Name, SummaryKind, FSanitizeFlagName)                      \
+  case ErrorType::Name:                                                        \
+    return SummaryKind;
+#include "ubsan_checks.inc"
+#undef UBSAN_CHECK
+  }
+  //  UNREACHABLE("unknown ErrorType!");
+}
+
+__attribute__((noreturn)) static void
+report_error(const char *msg, const char *suffix = "undefined_behavior.err") {
+  klee_report_error(__FILE__, __LINE__, msg, suffix);
+}
+
+__attribute__((noreturn)) static void report_error_type(ErrorType ET) {
+  report_error(ConvertTypeToString(ET));
+}
+
+/// Situations in which we might emit a check for the suitability of a
+/// pointer or glvalue. Needs to be kept in sync with CodeGenFunction.h in
+/// clang.
+enum TypeCheckKind {
+  /// Checking the operand of a load. Must be suitably sized and aligned.
+  TCK_Load,
+  /// Checking the destination of a store. Must be suitably sized and aligned.
+  TCK_Store,
+  /// Checking the bound value in a reference binding. Must be suitably sized
+  /// and aligned, but is not required to refer to an object (until the
+  /// reference is used), per core issue 453.
+  TCK_ReferenceBinding,
+  /// Checking the object expression in a non-static data member access. Must
+  /// be an object within its lifetime.
+  TCK_MemberAccess,
+  /// Checking the 'this' pointer for a call to a non-static member function.
+  /// Must be an object within its lifetime.
+  TCK_MemberCall,
+  /// Checking the 'this' pointer for a constructor call.
+  TCK_ConstructorCall,
+  /// Checking the operand of a static_cast to a derived pointer type. Must be
+  /// null or an object within its lifetime.
+  TCK_DowncastPointer,
+  /// Checking the operand of a static_cast to a derived reference type. Must
+  /// be an object within its lifetime.
+  TCK_DowncastReference,
+  /// Checking the operand of a cast to a base object. Must be suitably sized
+  /// and aligned.
+  TCK_Upcast,
+  /// Checking the operand of a cast to a virtual base object. Must be an
+  /// object within its lifetime.
+  TCK_UpcastToVirtualBase,
+  /// Checking the value assigned to a _Nonnull pointer. Must not be null.
+  TCK_NonnullAssign,
+  /// Checking the operand of a dynamic_cast or a typeid expression.  Must be
+  /// null or an object within its lifetime.
+  TCK_DynamicOperation
+};
+
+static void handleTypeMismatchImpl(TypeMismatchData *Data,
+                                   ValueHandle Pointer) {
+#if LLVM_VERSION_MAJOR >= 4
+  uptr Alignment = (uptr)1 << Data->LogAlignment;
+#endif
+  ErrorType ET;
+  if (!Pointer)
+#if LLVM_VERSION_MAJOR >= 11
+    ET = (Data->TypeCheckKind == TCK_NonnullAssign)
+             ? ErrorType::NullPointerUseWithNullability
+             : ErrorType::NullPointerUse;
+#else
+    ET = ErrorType::NullPointerUse;
+#endif
+#if LLVM_VERSION_MAJOR >= 4
+  else if (Pointer & (Alignment - 1))
+#else
+  else if (Data->Alignment && (Pointer & (Data->Alignment - 1)))
+#endif
+    ET = ErrorType::MisalignedPointerUse;
+  else
+    ET = ErrorType::InsufficientObjectSize;
+
+  report_error_type(ET);
+}
+
+#if LLVM_VERSION_MAJOR >= 4
+extern "C" void __ubsan_handle_type_mismatch_v1(TypeMismatchData *Data,
+                                                ValueHandle Pointer) {
+
+  handleTypeMismatchImpl(Data, Pointer);
+}
+
+extern "C" void __ubsan_handle_type_mismatch_v1_abort(TypeMismatchData *Data,
+                                                      ValueHandle Pointer) {
+
+  handleTypeMismatchImpl(Data, Pointer);
+}
+#else
+extern "C" void __ubsan_handle_type_mismatch(TypeMismatchData *Data,
+                                             ValueHandle Pointer) {
+  handleTypeMismatchImpl(Data, Pointer);
+}
+
+extern "C" void __ubsan_handle_type_mismatch_abort(TypeMismatchData *Data,
+                                                   ValueHandle Pointer) {
+  handleTypeMismatchImpl(Data, Pointer);
+}
+#endif
+
+#if LLVM_VERSION_MAJOR >= 8
+static void handleAlignmentAssumptionImpl(AlignmentAssumptionData * /*Data*/,
+                                          ValueHandle /*Pointer*/,
+                                          ValueHandle /*Alignment*/,
+                                          ValueHandle /*Offset*/) {
+  ErrorType ET = ErrorType::AlignmentAssumption;
+  report_error_type(ET);
+}
+
+extern "C" void
+__ubsan_handle_alignment_assumption(AlignmentAssumptionData *Data,
+                                    ValueHandle Pointer, ValueHandle Alignment,
+                                    ValueHandle Offset) {
+  handleAlignmentAssumptionImpl(Data, Pointer, Alignment, Offset);
+}
+
+extern "C" void __ubsan_handle_alignment_assumption_abort(
+    AlignmentAssumptionData *Data, ValueHandle Pointer, ValueHandle Alignment,
+    ValueHandle Offset) {
+  handleAlignmentAssumptionImpl(Data, Pointer, Alignment, Offset);
+}
+#endif
+
+/// \brief Common diagnostic emission for various forms of integer overflow.
+static void handleIntegerOverflowImpl(OverflowData *Data, ValueHandle /*LHS*/,
+                                      const char * /*Operator*/) {
+  bool IsSigned = Data->Type.isSignedIntegerTy();
+  ErrorType ET = IsSigned ? ErrorType::SignedIntegerOverflow
+                          : ErrorType::UnsignedIntegerOverflow;
+  report_error_type(ET);
+}
+
+#define UBSAN_OVERFLOW_HANDLER(handler_name, op, unrecoverable)                \
+  extern "C" void handler_name(OverflowData *Data, ValueHandle LHS,            \
+                               ValueHandle RHS) {                              \
+    handleIntegerOverflowImpl(Data, LHS, op);                                  \
+  }
+
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_add_overflow, "+", false)
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_add_overflow_abort, "+", true)
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_sub_overflow, "-", false)
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_sub_overflow_abort, "-", true)
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_mul_overflow, "*", false)
+UBSAN_OVERFLOW_HANDLER(__ubsan_handle_mul_overflow_abort, "*", true)
+
+static void handleNegateOverflowImpl(OverflowData *Data,
+                                     ValueHandle /*OldVal*/) {
+  bool IsSigned = Data->Type.isSignedIntegerTy();
+  ErrorType ET = IsSigned ? ErrorType::SignedIntegerOverflow
+                          : ErrorType::UnsignedIntegerOverflow;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_negate_overflow(OverflowData *Data,
+                                               ValueHandle OldVal) {
+  handleNegateOverflowImpl(Data, OldVal);
+}
+
+extern "C" void __ubsan_handle_negate_overflow_abort(OverflowData *Data,
+                                                     ValueHandle OldVal) {
+  handleNegateOverflowImpl(Data, OldVal);
+}
+
+static void handleDivremOverflowImpl(OverflowData *Data, ValueHandle /*LHS*/,
+                                     ValueHandle /*RHS*/) {
+  ErrorType ET;
+  if (Data->Type.isIntegerTy())
+    report_error("integer division overflow");
+  else
+    ET = ErrorType::FloatDivideByZero;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_divrem_overflow(OverflowData *Data,
+                                               ValueHandle LHS,
+                                               ValueHandle RHS) {
+  handleDivremOverflowImpl(Data, LHS, RHS);
+}
+
+extern "C" void __ubsan_handle_divrem_overflow_abort(OverflowData *Data,
+                                                     ValueHandle LHS,
+                                                     ValueHandle RHS) {
+  handleDivremOverflowImpl(Data, LHS, RHS);
+}
+
+static void handleShiftOutOfBoundsImpl(ShiftOutOfBoundsData * /*Data*/,
+                                       ValueHandle /*LHS*/,
+                                       ValueHandle /*RHS*/) {
+  report_error("shift out of bounds");
+}
+
+extern "C" void __ubsan_handle_shift_out_of_bounds(ShiftOutOfBoundsData *Data,
+                                                   ValueHandle LHS,
+                                                   ValueHandle RHS) {
+  handleShiftOutOfBoundsImpl(Data, LHS, RHS);
+}
+
+extern "C" void
+__ubsan_handle_shift_out_of_bounds_abort(ShiftOutOfBoundsData *Data,
+                                         ValueHandle LHS, ValueHandle RHS) {
+  handleShiftOutOfBoundsImpl(Data, LHS, RHS);
+}
+
+static void handleOutOfBoundsImpl(OutOfBoundsData * /*Data*/,
+                                  ValueHandle /*Index*/) {
+  ErrorType ET = ErrorType::OutOfBoundsIndex;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_out_of_bounds(OutOfBoundsData *Data,
+                                             ValueHandle Index) {
+  handleOutOfBoundsImpl(Data, Index);
+}
+
+extern "C" void __ubsan_handle_out_of_bounds_abort(OutOfBoundsData *Data,
+                                                   ValueHandle Index) {
+  handleOutOfBoundsImpl(Data, Index);
+}
+
+static void handleBuiltinUnreachableImpl(UnreachableData * /*Data*/) {
+  ErrorType ET = ErrorType::UnreachableCall;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_builtin_unreachable(UnreachableData *Data) {
+  handleBuiltinUnreachableImpl(Data);
+}
+
+static void handleMissingReturnImpl(UnreachableData * /*Data*/) {
+  ErrorType ET = ErrorType::MissingReturn;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_missing_return(UnreachableData *Data) {
+  handleMissingReturnImpl(Data);
+}
+
+static void handleVLABoundNotPositive(VLABoundData * /*Data*/,
+                                      ValueHandle /*Bound*/) {
+  ErrorType ET = ErrorType::NonPositiveVLAIndex;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_vla_bound_not_positive(VLABoundData *Data,
+                                                      ValueHandle Bound) {
+  handleVLABoundNotPositive(Data, Bound);
+}
+
+extern "C" void __ubsan_handle_vla_bound_not_positive_abort(VLABoundData *Data,
+                                                            ValueHandle Bound) {
+  handleVLABoundNotPositive(Data, Bound);
+}
+
+static void handleFloatCastOverflow(void * /*DataPtr*/, ValueHandle /*From*/) {
+  ErrorType ET = ErrorType::FloatCastOverflow;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_float_cast_overflow(void *Data,
+                                                   ValueHandle From) {
+  handleFloatCastOverflow(Data, From);
+}
+
+extern "C" void __ubsan_handle_float_cast_overflow_abort(void *Data,
+                                                         ValueHandle From) {
+  handleFloatCastOverflow(Data, From);
+}
+
+static void handleLoadInvalidValue(InvalidValueData * /*Data*/,
+                                   ValueHandle /*Val*/) {
+  report_error("load invalid value");
+}
+
+extern "C" void __ubsan_handle_load_invalid_value(InvalidValueData *Data,
+                                                  ValueHandle Val) {
+  handleLoadInvalidValue(Data, Val);
+}
+extern "C" void __ubsan_handle_load_invalid_value_abort(InvalidValueData *Data,
+                                                        ValueHandle Val) {
+  handleLoadInvalidValue(Data, Val);
+}
+
+#if LLVM_VERSION_MAJOR >= 7
+static void handleImplicitConversion(ImplicitConversionData *Data,
+                                     ValueHandle /*Src*/, ValueHandle /*Dst*/) {
+  ErrorType ET = ErrorType::GenericUB;
+
+#if LLVM_VERSION_MAJOR >= 8
+  const TypeDescriptor &SrcTy = Data->FromType;
+  const TypeDescriptor &DstTy = Data->ToType;
+
+  bool SrcSigned = SrcTy.isSignedIntegerTy();
+  bool DstSigned = DstTy.isSignedIntegerTy();
+
+  switch (Data->Kind) {
+  case ICCK_IntegerTruncation: { // Legacy, no longer used.
+    // Let's figure out what it should be as per the new types, and upgrade.
+    // If both types are unsigned, then it's an unsigned truncation.
+    // Else, it is a signed truncation.
+    if (!SrcSigned && !DstSigned) {
+      ET = ErrorType::ImplicitUnsignedIntegerTruncation;
+    } else {
+      ET = ErrorType::ImplicitSignedIntegerTruncation;
+    }
+    break;
+  }
+  case ICCK_UnsignedIntegerTruncation:
+    ET = ErrorType::ImplicitUnsignedIntegerTruncation;
+    break;
+  case ICCK_SignedIntegerTruncation:
+    ET = ErrorType::ImplicitSignedIntegerTruncation;
+    break;
+  case ICCK_IntegerSignChange:
+    ET = ErrorType::ImplicitIntegerSignChange;
+    break;
+  case ICCK_SignedIntegerTruncationOrSignChange:
+    ET = ErrorType::ImplicitSignedIntegerTruncationOrSignChange;
+    break;
+  }
+#else
+  switch (Data->Kind) {
+  case ICCK_IntegerTruncation:
+    ET = ErrorType::ImplicitIntegerTruncation;
+    break;
+  }
+#endif
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_implicit_conversion(ImplicitConversionData *Data,
+                                                   ValueHandle Src,
+                                                   ValueHandle Dst) {
+  handleImplicitConversion(Data, Src, Dst);
+}
+
+extern "C" void
+__ubsan_handle_implicit_conversion_abort(ImplicitConversionData *Data,
+                                         ValueHandle Src, ValueHandle Dst) {
+  handleImplicitConversion(Data, Src, Dst);
+}
+#endif
+
+#if LLVM_VERSION_MAJOR >= 6
+static void handleInvalidBuiltin(InvalidBuiltinData * /*Data*/) {
+  ErrorType ET = ErrorType::InvalidBuiltin;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_invalid_builtin(InvalidBuiltinData *Data) {
+  handleInvalidBuiltin(Data);
+}
+
+extern "C" void __ubsan_handle_invalid_builtin_abort(InvalidBuiltinData *Data) {
+  handleInvalidBuiltin(Data);
+}
+#endif
+
+#if LLVM_VERSION_MAJOR >= 5
+static void handleNonNullReturn(NonNullReturnData * /*Data*/,
+                                SourceLocation * /*LocPtr*/, bool IsAttr) {
+#if LLVM_VERSION_MAJOR >= 11
+  ErrorType ET = IsAttr ? ErrorType::InvalidNullReturn
+                        : ErrorType::InvalidNullReturnWithNullability;
+#else
+  ErrorType ET = ErrorType::InvalidNullReturn;
+#endif
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_nonnull_return_v1(NonNullReturnData *Data,
+                                                 SourceLocation *LocPtr) {
+  handleNonNullReturn(Data, LocPtr, true);
+}
+
+extern "C" void __ubsan_handle_nonnull_return_v1_abort(NonNullReturnData *Data,
+                                                       SourceLocation *LocPtr) {
+  handleNonNullReturn(Data, LocPtr, true);
+}
+#else
+static void handleNonNullReturn(NonNullReturnData * /*Data*/) {
+  ErrorType ET = ErrorType::InvalidNullReturn;
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_nonnull_return(NonNullReturnData *Data) {
+  handleNonNullReturn(Data);
+}
+
+extern "C" void __ubsan_handle_nonnull_return_abort(NonNullReturnData *Data) {
+  handleNonNullReturn(Data);
+}
+#endif
+
+#if LLVM_VERSION_MAJOR >= 5
+extern "C" void __ubsan_handle_nullability_return_v1(NonNullReturnData *Data,
+                                                     SourceLocation *LocPtr) {
+  handleNonNullReturn(Data, LocPtr, false);
+}
+
+extern "C" void
+__ubsan_handle_nullability_return_v1_abort(NonNullReturnData *Data,
+                                           SourceLocation *LocPtr) {
+  handleNonNullReturn(Data, LocPtr, false);
+}
+#endif
+
+static void handleNonNullArg(NonNullArgData * /*Data*/, bool IsAttr) {
+#if LLVM_VERSION_MAJOR >= 11
+  ErrorType ET = IsAttr ? ErrorType::InvalidNullArgument
+                        : ErrorType::InvalidNullArgumentWithNullability;
+#else
+  ErrorType ET = ErrorType::InvalidNullArgument;
+#endif
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_nonnull_arg(NonNullArgData *Data) {
+  handleNonNullArg(Data, true);
+}
+
+extern "C" void __ubsan_handle_nonnull_arg_abort(NonNullArgData *Data) {
+  handleNonNullArg(Data, true);
+}
+
+#if LLVM_VERSION_MAJOR >= 5
+extern "C" void __ubsan_handle_nullability_arg(NonNullArgData *Data) {
+  handleNonNullArg(Data, false);
+}
+
+extern "C" void __ubsan_handle_nullability_arg_abort(NonNullArgData *Data) {
+
+  handleNonNullArg(Data, false);
+}
+#endif
+
+#if LLVM_VERSION_MAJOR >= 5
+static void handlePointerOverflowImpl(PointerOverflowData * /*Data*/,
+                                      ValueHandle Base, ValueHandle Result) {
+#if LLVM_VERSION_MAJOR >= 10
+  ErrorType ET;
+  if (Base == 0 && Result == 0)
+    ET = ErrorType::NullptrWithOffset;
+  else if (Base == 0 && Result != 0)
+    ET = ErrorType::NullptrWithNonZeroOffset;
+  else if (Base != 0 && Result == 0)
+    ET = ErrorType::NullptrAfterNonZeroOffset;
+  else
+    ET = ErrorType::PointerOverflow;
+#else
+  ErrorType ET = ErrorType::PointerOverflow;
+#endif
+  report_error_type(ET);
+}
+
+extern "C" void __ubsan_handle_pointer_overflow(PointerOverflowData *Data,
+                                                ValueHandle Base,
+                                                ValueHandle Result) {
+
+  handlePointerOverflowImpl(Data, Base, Result);
+}
+
+extern "C" void __ubsan_handle_pointer_overflow_abort(PointerOverflowData *Data,
+                                                      ValueHandle Base,
+                                                      ValueHandle Result) {
+
+  handlePointerOverflowImpl(Data, Base, Result);
+}
+#endif
+
+} // namespace __ubsan
\ No newline at end of file
diff --git a/runtime/Sanitizer/ubsan/ubsan_handlers.h b/runtime/Sanitizer/ubsan/ubsan_handlers.h
new file mode 100644
index 00000000..be2b8225
--- /dev/null
+++ b/runtime/Sanitizer/ubsan/ubsan_handlers.h
@@ -0,0 +1,115 @@
+//===-- ubsan_handlers.h ----------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Entry points to the runtime library for Clang's undefined behavior sanitizer.
+//
+//===----------------------------------------------------------------------===//
+#ifndef UBSAN_HANDLERS_H
+#define UBSAN_HANDLERS_H
+
+#include "ubsan_value.h"
+
+#include "klee/Config/Version.h"
+
+using namespace __ubsan;
+
+struct TypeMismatchData {
+  SourceLocation Loc;
+  const TypeDescriptor &Type;
+#if LLVM_VERSION_MAJOR >= 4
+  unsigned char LogAlignment;
+#else
+  uptr Alignment;
+#endif
+  unsigned char TypeCheckKind;
+};
+
+#if LLVM_VERSION_MAJOR >= 8
+struct AlignmentAssumptionData {
+  SourceLocation Loc;
+  SourceLocation AssumptionLoc;
+  const TypeDescriptor &Type;
+};
+#endif
+
+struct OverflowData {
+  SourceLocation Loc;
+  const TypeDescriptor &Type;
+};
+
+struct ShiftOutOfBoundsData {
+  SourceLocation Loc;
+  const TypeDescriptor &LHSType;
+  const TypeDescriptor &RHSType;
+};
+
+struct OutOfBoundsData {
+  SourceLocation Loc;
+  const TypeDescriptor &ArrayType;
+  const TypeDescriptor &IndexType;
+};
+
+struct UnreachableData {
+  SourceLocation Loc;
+};
+
+struct VLABoundData {
+  SourceLocation Loc;
+  const TypeDescriptor &Type;
+};
+
+struct InvalidValueData {
+  SourceLocation Loc;
+  const TypeDescriptor &Type;
+};
+
+#if LLVM_VERSION_MAJOR >= 7
+/// Known implicit conversion check kinds.
+/// Keep in sync with the enum of the same name in CGExprScalar.cpp
+enum ImplicitConversionCheckKind : unsigned char {
+  ICCK_IntegerTruncation = 0, // Legacy, was only used by clang 7.
+  ICCK_UnsignedIntegerTruncation = 1,
+  ICCK_SignedIntegerTruncation = 2,
+  ICCK_IntegerSignChange = 3,
+  ICCK_SignedIntegerTruncationOrSignChange = 4,
+};
+#endif
+
+#if LLVM_VERSION_MAJOR >= 7
+struct ImplicitConversionData {
+  SourceLocation Loc;
+  const TypeDescriptor &FromType;
+  const TypeDescriptor &ToType;
+  /* ImplicitConversionCheckKind */ unsigned char Kind;
+};
+#endif
+
+#if LLVM_VERSION_MAJOR >= 6
+struct InvalidBuiltinData {
+  SourceLocation Loc;
+  unsigned char Kind;
+};
+#endif
+
+struct NonNullReturnData {
+  SourceLocation AttrLoc;
+};
+
+struct NonNullArgData {
+  SourceLocation Loc;
+  SourceLocation AttrLoc;
+  int ArgIndex;
+};
+
+#if LLVM_VERSION_MAJOR >= 5
+struct PointerOverflowData {
+  SourceLocation Loc;
+};
+#endif
+
+#endif // UBSAN_HANDLERS_H
\ No newline at end of file
diff --git a/runtime/Sanitizer/ubsan/ubsan_value.h b/runtime/Sanitizer/ubsan/ubsan_value.h
new file mode 100644
index 00000000..5474961e
--- /dev/null
+++ b/runtime/Sanitizer/ubsan/ubsan_value.h
@@ -0,0 +1,76 @@
+//===-- ubsan_value.h -------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// Representation of data which is passed from the compiler-generated calls into
+// the ubsan runtime.
+//
+//===----------------------------------------------------------------------===//
+#ifndef UBSAN_VALUE_H
+#define UBSAN_VALUE_H
+
+#include "../sanitizer_common/sanitizer_common.h"
+
+namespace __ubsan {
+
+/// \brief A description of a source location. This corresponds to Clang's
+/// \c PresumedLoc type.
+class SourceLocation {
+  __attribute__((unused)) const char *Filename;
+  __attribute__((unused)) u32 Line;
+  __attribute__((unused)) u32 Column;
+
+public:
+  SourceLocation() : Filename(), Line(), Column() {}
+  SourceLocation(const char *Filename, unsigned Line, unsigned Column)
+      : Filename(Filename), Line(Line), Column(Column) {}
+};
+
+/// \brief A description of a type.
+class TypeDescriptor {
+  /// A value from the \c Kind enumeration, specifying what flavor of type we
+  /// have.
+  u16 TypeKind;
+
+  /// A \c Type-specific value providing information which allows us to
+  /// interpret the meaning of a ValueHandle of this type.
+  u16 TypeInfo;
+
+  /// The name of the type follows, in a format suitable for including in
+  /// diagnostics.
+  char TypeName[1];
+
+public:
+  enum Kind {
+    /// An integer type. Lowest bit is 1 for a signed value, 0 for an unsigned
+    /// value. Remaining bits are log_2(bit width). The value representation is
+    /// the integer itself if it fits into a ValueHandle, and a pointer to the
+    /// integer otherwise.
+    TK_Integer = 0x0000,
+    /// A floating-point type. Low 16 bits are bit width. The value
+    /// representation is that of bitcasting the floating-point value to an
+    /// integer type.
+    TK_Float = 0x0001,
+    /// Any other type. The value representation is unspecified.
+    TK_Unknown = 0xffff
+  };
+
+  const char *getTypeName() const { return TypeName; }
+
+  Kind getKind() const { return static_cast<Kind>(TypeKind); }
+
+  bool isIntegerTy() const { return getKind() == TK_Integer; }
+  bool isSignedIntegerTy() const { return isIntegerTy() && (TypeInfo & 1); }
+  bool isUnsignedIntegerTy() const { return isIntegerTy() && !(TypeInfo & 1); }
+};
+
+/// \brief An opaque handle to a value.
+typedef uptr ValueHandle;
+
+} // namespace __ubsan
+
+#endif // UBSAN_VALUE_H
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;
-}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index d94cdc76..7d938ab2 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -187,6 +187,10 @@ namespace {
                    cl::init(false),
                    cl::cat(LinkCat));
 
+  cl::opt<bool> WithUBSanRuntime("ubsan-runtime",
+                                 cl::desc("Link with UBSan runtime."),
+                                 cl::init(false), cl::cat(LinkCat));
+
   cl::opt<std::string> RuntimeBuild(
       "runtime-build",
       cl::desc("Link with versions of the runtime library that were built with "
@@ -794,10 +798,6 @@ static const char *modelledExternals[] = {
   "_Znwj",
   "_Znam",
   "_Znwm",
-  "__ubsan_handle_add_overflow",
-  "__ubsan_handle_sub_overflow",
-  "__ubsan_handle_mul_overflow",
-  "__ubsan_handle_divrem_overflow",
 };
 
 // Symbols we aren't going to warn about
@@ -1265,6 +1265,15 @@ int main(int argc, char **argv, char **envp) {
     preparePOSIX(loadedModules, libcPrefix);
   }
 
+  if (WithUBSanRuntime) {
+    SmallString<128> Path(Opts.LibraryDir);
+    llvm::sys::path::append(Path, "libkleeUBSan" + opt_suffix + ".bca");
+    if (!klee::loadFile(Path.c_str(), mainModule->getContext(), loadedModules,
+                        errorMsg))
+      klee_error("error loading UBSan support '%s': %s", Path.c_str(),
+                 errorMsg.c_str());
+  }
+
   if (Libcxx) {
 #ifndef SUPPORT_KLEE_LIBCXX
     klee_error("KLEE was not compiled with libc++ support");