Eliminate .undefined_behavior.err category and simplify tests

15 files changed, 72 insertions, 52 deletions

diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h
index 435b6c05..4fe5583a 100644
--- a/include/klee/Core/TerminationTypes.h
+++ b/include/klee/Core/TerminationTypes.h
@@ -32,19 +32,23 @@
   TTYPE(Ptr, 16U, "ptr.err")                                                   \
   TTYPE(ReadOnly, 17U, "read_only.err")                                        \
   TTYPE(ReportError, 18U, "report_error.err")                                  \
-  TTYPE(ImplicitConversion, 19U, "implicit_conversion.err")                    \
-  TTYPE(NullableAttribute, 20U, "nullable_attribute.err")                      \
-  TTYPE(UndefinedBehavior, 21U, "undefined_behavior.err")                      \
-  MARK(PROGERR, 21U)                                                           \
-  TTYPE(User, 23U, "user.err")                                                 \
-  MARK(USERERR, 23U)                                                           \
-  TTYPE(Execution, 25U, "exec.err")                                            \
-  TTYPE(External, 26U, "external.err")                                         \
-  MARK(EXECERR, 26U)                                                           \
-  TTYPE(Replay, 27U, "")                                                       \
-  TTYPE(Merge, 28U, "")                                                        \
-  TTYPE(SilentExit, 29U, "")                                                   \
-  MARK(END, 29U)
+  TTYPE(InvalidBuiltin, 19U, "invalid_builtin_use.err")                        \
+  TTYPE(ImplicitTruncation, 20U, "implicit_truncation.err")                    \
+  TTYPE(ImplicitConversion, 21U, "implicit_conversion.err")                    \
+  TTYPE(UnreachableCall, 22U, "unreachable_call.err")                          \
+  TTYPE(MissingReturn, 23U, "missing_return.err")                              \
+  TTYPE(InvalidLoad, 24U, "invalid_load.err")                                  \
+  TTYPE(NullableAttribute, 25U, "nullable_attribute.err")                      \
+  MARK(PROGERR, 25U)                                                           \
+  TTYPE(User, 33U, "user.err")                                                 \
+  MARK(USERERR, 33U)                                                           \
+  TTYPE(Execution, 35U, "exec.err")                                            \
+  TTYPE(External, 36U, "external.err")                                         \
+  MARK(EXECERR, 36U)                                                           \
+  TTYPE(Replay, 37U, "")                                                       \
+  TTYPE(Merge, 38U, "")                                                        \
+  TTYPE(SilentExit, 39U, "")                                                   \
+  MARK(END, 39U)
 
 ///@brief Reason an ExecutionState got terminated.
 enum class StateTerminationType : std::uint8_t {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 157c1cc8..1187654d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -290,12 +290,24 @@ cl::list<StateTerminationType> ExitOnErrorType(
                    "Write to read-only memory"),
         clEnumValN(StateTerminationType::ReportError, "ReportError",
                    "klee_report_error called"),
+        clEnumValN(StateTerminationType::InvalidBuiltin, "InvalidBuiltin",
+                   "Passing invalid value to compiler builtin"),
+        clEnumValN(StateTerminationType::ImplicitTruncation, "ImplicitTruncation",
+                   "Implicit conversion from integer of larger bit width to "
+                   "smaller bit width that results in data loss"),
         clEnumValN(StateTerminationType::ImplicitConversion, "ImplicitConversion",
-                   "Undefined implicit conversion detected"),
+                   "Implicit conversion between integer types that changes the "
+                   "sign of the value"),
+        clEnumValN(StateTerminationType::UnreachableCall, "UnreachableCall",
+                   "Control flow reached an unreachable program point"),
+        clEnumValN(StateTerminationType::MissingReturn, "MissingReturn",
+                   "Reaching the end of a value-returning function without "
+                   "returning a value"),
+        clEnumValN(StateTerminationType::InvalidLoad, "InvalidLoad",
+                   "Load of a value which is not in the range of representable "
+                   "values for that type"),
         clEnumValN(StateTerminationType::NullableAttribute, "NullableAttribute",
                    "Violation of nullable attribute detected"),
-        clEnumValN(StateTerminationType::UndefinedBehavior, "UndefinedBehavior",
-                   "Undefined behavior detected"),
         clEnumValN(StateTerminationType::User, "User",
                    "Wrong klee_* functions invocation")),
     cl::ZeroOrMore,
diff --git a/runtime/Sanitizer/ubsan/ubsan_handlers.cpp b/runtime/Sanitizer/ubsan/ubsan_handlers.cpp
index cfb0287c..38f3425f 100644
--- a/runtime/Sanitizer/ubsan/ubsan_handlers.cpp
+++ b/runtime/Sanitizer/ubsan/ubsan_handlers.cpp
@@ -27,18 +27,20 @@ static const char *ConvertTypeToString(ErrorType Type) {
 #include "ubsan_checks.inc"
 #undef UBSAN_CHECK
   }
-  //  UNREACHABLE("unknown ErrorType!");
 }
 
 __attribute__((noreturn)) static void report_error(const char *msg,
                                                    const char *suffix) {
-    klee_report_error(__FILE__, __LINE__, msg, suffix);
+  klee_report_error(__FILE__, __LINE__, msg, suffix);
 }
 
 static const char *get_suffix(ErrorType ET) {
   switch (ET) {
   case ErrorType::GenericUB:
-    return "undefined_behavior.err";
+    // This ErrorType is only used in actual LLVM runtime
+    // when `report_error_type` environment option is set to false.
+    // It should never happen in KLEE runtime.
+    return "exec.err";
   case ErrorType::NullPointerUse:
 #if LLVM_VERSION_MAJOR >= 11
   case ErrorType::NullPointerUseWithNullability:
@@ -53,7 +55,9 @@ static const char *get_suffix(ErrorType ET) {
   case ErrorType::AlignmentAssumption:
     return "ptr.err";
   case ErrorType::InsufficientObjectSize:
-    return "undefined_behavior.err";
+    // Convenient test has not been found in LLVM sources and therefore not been
+    // added.
+    return "ptr.err";
   case ErrorType::SignedIntegerOverflow:
   case ErrorType::UnsignedIntegerOverflow:
     return "overflow.err";
@@ -61,14 +65,16 @@ static const char *get_suffix(ErrorType ET) {
   case ErrorType::FloatDivideByZero:
     return "div.err";
   case ErrorType::InvalidBuiltin:
-    return "undefined_behavior.err";
+    return "invalid_builtin_use.err";
 #if LLVM_VERSION_MAJOR >= 11
   case ErrorType::InvalidObjCCast:
-    return "undefined_behavior.err";
+    // Option `fsanitize=objc-cast` is not supported due to the requirement for
+    // Darwin system.
+    return "exec.err";
 #endif
   case ErrorType::ImplicitUnsignedIntegerTruncation:
   case ErrorType::ImplicitSignedIntegerTruncation:
-    return "implicit_conversion.err";
+    return "implicit_truncation.err";
   case ErrorType::ImplicitIntegerSignChange:
   case ErrorType::ImplicitSignedIntegerTruncationOrSignChange:
     return "implicit_conversion.err";
@@ -78,17 +84,16 @@ static const char *get_suffix(ErrorType ET) {
   case ErrorType::OutOfBoundsIndex:
     return "ptr.err";
   case ErrorType::UnreachableCall:
-    return "undefined_behavior.err";
+    return "unreachable_call.err";
   case ErrorType::MissingReturn:
-    return "undefined_behavior.err";
+    return "missing_return.err";
   case ErrorType::NonPositiveVLAIndex:
     return "ptr.err";
   case ErrorType::FloatCastOverflow:
     return "overflow.err";
   case ErrorType::InvalidBoolLoad:
-    return "undefined_behavior.err";
   case ErrorType::InvalidEnumLoad:
-    return "undefined_behavior.err";
+    return "invalid_load.err";
   case ErrorType::FunctionTypeMismatch:
     // This check is unsupported
     return "exec.err";
@@ -114,6 +119,7 @@ __attribute__((noreturn)) static void report_error_type(ErrorType ET) {
   report_error(ConvertTypeToString(ET), get_suffix(ET));
 }
 
+#if LLVM_VERSION_MAJOR >= 11
 /// 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.
@@ -152,6 +158,7 @@ enum TypeCheckKind {
   /// null or an object within its lifetime.
   TCK_DynamicOperation
 };
+#endif
 
 static void handleTypeMismatchImpl(TypeMismatchData *Data,
                                    ValueHandle Pointer) {
@@ -248,12 +255,12 @@ extern "C" void __ubsan_handle_negate_overflow_abort(OverflowData *Data,
 
 static void handleDivremOverflowImpl(OverflowData *Data, ValueHandle /*LHS*/,
                                      ValueHandle /*RHS*/) {
-  ErrorType ET;
   if (Data->Type.isIntegerTy())
     report_error("integer division overflow", "overflow.err");
-  else
-    ET = ErrorType::FloatDivideByZero;
-  report_error_type(ET);
+  else {
+    ErrorType ET = ErrorType::FloatDivideByZero;
+    report_error_type(ET);
+  }
 }
 
 extern "C" void __ubsan_handle_divrem_overflow(OverflowData *Data,
@@ -353,7 +360,7 @@ extern "C" void __ubsan_handle_float_cast_overflow_abort(void *Data,
 
 static void handleLoadInvalidValue(InvalidValueData * /*Data*/,
                                    ValueHandle /*Val*/) {
-  report_error("load invalid value", "undefined_behavior.err");
+  report_error("load invalid value", "invalid_load.err");
 }
 
 extern "C" void __ubsan_handle_load_invalid_value(InvalidValueData *Data,
diff --git a/test/Feature/ubsan/ubsan_bool.c b/test/Feature/ubsan/ubsan_bool.c
index 360af183..6873299d 100644
--- a/test/Feature/ubsan/ubsan_bool.c
+++ b/test/Feature/ubsan/ubsan_bool.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
-// RUN: ls %t.klee-out/ | grep undefined_behavior.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .invalid_load.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/Feature/ubsan/ubsan_builtin.c
index 72ff73da..cb04987e 100644
--- a/test/Feature/ubsan/ubsan_builtin.c
+++ b/test/Feature/ubsan/ubsan_builtin.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
-// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .invalid_builtin_use.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_enum.c b/test/Feature/ubsan/ubsan_enum.cpp
index 1c79629a..fe01f978 100644
--- a/test/Feature/ubsan/ubsan_enum.c
+++ b/test/Feature/ubsan/ubsan_enum.cpp
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
-// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .invalid_load.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
index 23213808..95002907 100644
--- a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
-// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .implicit_truncation.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
index f14b65ca..0db03cb0 100644
--- a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
-// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .implicit_truncation.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
index c33bab38..09591e29 100644
--- a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
+++ b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
@@ -6,15 +6,9 @@
 
 #include "klee/klee.h"
 
-#if defined(__SIZEOF_INT128__) && !defined(_WIN32)
-typedef __int128 intmax;
-#else
-typedef long long intmax;
-#endif
-
 int main() {
-  intmax x;
-  volatile intmax result;
+  int x;
+  volatile int result;
 
   klee_make_symbolic(&x, sizeof(x), "x");
 
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
index dcbba073..007a8ee2 100644
--- 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
@@ -17,6 +17,7 @@ int main() {
   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
index cb126742..20286bcc 100644
--- 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
@@ -17,6 +17,7 @@ int main() {
   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
index 20286bcc..f36dca61 100644
--- 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
@@ -3,7 +3,7 @@
 // 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
-// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
@@ -14,11 +14,11 @@ int main() {
   volatile char *result;
 
   klee_make_symbolic(&address, sizeof(address), "address");
-  klee_assume(address != 0);
+  klee_assume(address == 0);
 
   char *ptr = (char *)address;
 
-  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-after-nonzero-offset
+  // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-with-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
index 301952b9..b39b65e2 100644
--- 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
@@ -3,7 +3,7 @@
 // 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
-// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
@@ -14,8 +14,9 @@ int main() {
   volatile char *result;
 
   klee_make_symbolic(&address, sizeof(address), "address");
+  klee_assume(address == 0);
 
-  char *ptr = (char *)address;;
+  char *ptr = (char *)address;
 
   // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: nullptr-with-offset
   result = ptr + 0;
diff --git a/test/Feature/ubsan/ubsan_return.c b/test/Feature/ubsan/ubsan_return.cpp
index c2327db4..05f82098 100644
--- a/test/Feature/ubsan/ubsan_return.c
+++ b/test/Feature/ubsan/ubsan_return.cpp
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
-// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .missing_return.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unreachable.c b/test/Feature/ubsan/ubsan_unreachable.c
index 76e2e909..bfc7f6ad 100644
--- a/test/Feature/ubsan/ubsan_unreachable.c
+++ b/test/Feature/ubsan/ubsan_unreachable.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
-// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .unreachable_call.err | wc -l | grep 1
 
 #include "klee/klee.h"