Support UBSan-enabled binaries

10 files changed, 937 insertions, 0 deletions

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