Improve UX for unreachable/unimplemented errors (#4094)

This should replace several "segfaults" and "illegal instruction" errors
with messages that contain a bit more context. I also put in a link to
the bug tracker to make users' lives a bit easier.

For context, `__builtin_unreachable`'s behavior is undefined and is
intended only as a mechanism to help the compiler see that code will not
return. I do still include it in the new code because if I don't,
compilation produces a lot more warnings as it can't see that
`NOT_IMPLEMENTED_YET` and `UNREACHABLE` cannot return.

src/util/debug.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include<iostream>
 #include "util/str_hashtable.h"
 #include "util/z3_exception.h"
+#include "util/z3_version.h"
 
 static volatile bool g_enable_assertions = true;
 
@@ -39,6 +40,10 @@ void notify_assertion_violation(const char * fileName, int line, const char * co
     std::cerr << "File: " << fileName << "\n";
     std::cerr << "Line: " << line << "\n";
     std::cerr << condition << "\n";
+#ifndef Z3DEBUG
+    std::cerr << Z3_FULL_VERSION << "\n";
+    std::cerr << "Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new\n";
+#endif
 }
 
 static str_hashtable* g_enabled_debug_tags = nullptr;

src/util/debug.h

@@ -75,20 +75,27 @@ bool is_debug_enabled(const char * tag);
 #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
 
+/**
+  We use __builtin_unreachable where possible to suppress control flow compilation warnings, but it should
+  not be called because its behavior is undefined, so we do need to exit before "calling" it.
+*/
+#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
+# define EXIT_WITH(ERR_CODE) { exit(ERR_CODE); __builtin_unreachable(); } ((void) 0)
+#else
+# define EXIT_WITH(ERR_CODE) { exit(ERR_CODE); } ((void) 0)
+#endif
+
 #ifdef Z3DEBUG
 # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
 #else
-#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); EXIT_WITH(ERR_UNREACHABLE); } ((void) 0)
-// only available in gcc >= 4.5 and in newer versions of clang
-# define UNREACHABLE() __builtin_unreachable()
-#elif defined(_MSC_VER)
-# define UNREACHABLE() __assume(0)
-#else
-#define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
-#endif
 #endif
 
-#define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
+#ifdef Z3DEBUG
+# define NOT_IMPLEMENTED_YET() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); INVOKE_DEBUGGER();)
+#else
+# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); EXIT_WITH(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
+#endif
 
 #define VERIFY(_x_) if (!(_x_)) {                               \
         std::cerr << "Failed to verify: " << #_x_ << "\n";      \

src/util/error_codes.h

@@ -33,6 +33,7 @@ Revision History:
 #define ERR_TYPE_CHECK          111
 #define ERR_UNKNOWN_RESULT      112
 #define ERR_ALLOC_EXCEEDED      113
+#define ERR_UNREACHABLE         114
 
 #endif /* ERROR_CODES_H_ */
 

src/util/z3_exception.cpp

@@ -49,6 +49,7 @@ char const * z3_error::msg() const {
     case ERR_INTERNAL_FATAL: return "internal error";
     case ERR_TYPE_CHECK: return "type error";
     case ERR_ALLOC_EXCEEDED: return "number of configured allocations exceeded";
+    case ERR_UNREACHABLE: return "unreachable code was reached";
     default: return "unknown error";
     }
 }