Implement API to set exit action to exception (#7192)

* Implement API to set exit action to exception * Turn on exit_action_to_throw_exception upon API context creation
Z3Prover · Mar 28, 2024 · 111fcb9 · 111fcb9
1 parent c18a42c
commit 111fcb9
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 5 deletions.
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
@@ -18,6 +18,7 @@ Revision History:
 
 --*/
 #include<typeinfo>
+#include "util/debug.h"
 #include "util/z3_version.h"
 #include "api/api_context.h"
 #include "ast/ast_pp.h"
@@ -393,6 +394,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_context_rc(c);
         memory::initialize(UINT_MAX);
+        set_default_exit_action(exit_action::throw_exception);
         Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<ast_context_params*>(c), true));
         RETURN_Z3(r);
         Z3_CATCH_RETURN_NO_HANDLE(nullptr);

diff --git a/src/util/debug.cpp b/src/util/debug.cpp
@@ -75,6 +75,37 @@ bool is_debug_enabled(const char * tag) {
     return g_enabled_debug_tags->contains(tag);
 }
 
+atomic<exit_action> g_default_exit_action(exit_action::exit);
+
+exit_action get_default_exit_action() {
+    return g_default_exit_action;
+}
+
+void set_default_exit_action(exit_action a) {
+    g_default_exit_action = a;
+}
+
+void invoke_exit_action(unsigned int code) {
+    exit_action a = get_default_exit_action();
+    switch (a) {
+    case exit_action::exit:
+        exit(code);
+    case exit_action::throw_exception:
+        switch (code) {
+            case ERR_INTERNAL_FATAL:
+                throw default_exception("internal fatal");
+            case ERR_UNREACHABLE:
+                throw default_exception("unreachable");
+            case ERR_NOT_IMPLEMENTED_YET:
+                throw default_exception("not implemented yet");
+            default:
+                throw default_exception("unknown");
+        }
+    default:
+        exit(code);
+    }
+}
+
 atomic<debug_action> g_default_debug_action(debug_action::ask);
 
 debug_action get_default_debug_action() {

diff --git a/src/util/debug.h b/src/util/debug.h
@@ -35,6 +35,14 @@ enum class debug_action {
 debug_action get_default_debug_action();
 void set_default_debug_action(debug_action a);
 
+enum class exit_action {
+    exit,
+    throw_exception,
+};
+exit_action get_default_exit_action();
+void set_default_exit_action(exit_action a);
+void invoke_exit_action(unsigned int code);
+
 #include "util/error_codes.h"
 #include "util/warning.h"
 
@@ -56,7 +64,7 @@ void set_default_debug_action(debug_action a);
 #endif
 
 #ifdef NO_Z3_DEBUGGER
-#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
+#define INVOKE_DEBUGGER() invoke_exit_action(ERR_INTERNAL_FATAL)
 #else
 #ifdef _WINDOWS
 #define INVOKE_DEBUGGER() __debugbreak()
@@ -71,6 +79,7 @@ void enable_debug(const char * tag);
 void disable_debug(const char * tag);
 bool is_debug_enabled(const char * tag);
 
+
 #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #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(); })
@@ -85,25 +94,25 @@ bool is_debug_enabled(const char * tag);
 #ifdef Z3DEBUG
 # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
 #else
-# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); exit(ERR_UNREACHABLE); } ((void) 0)
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
 #endif
 
 #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(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
+# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); invoke_exit_action(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
 #endif
 
 #define VERIFY(_x_) if (!(_x_)) {                                                       \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \
-        exit(ERR_UNREACHABLE);                                                          \
+        invoke_exit_action(ERR_UNREACHABLE);                                                          \
     }
 
 #define VERIFY_EQ(LHS, RHS)                                                                         \
     if (!((LHS) == (RHS))) {                                                                        \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \
         std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n";                    \
-        exit(ERR_UNREACHABLE);                                                                      \
+        invoke_exit_action(ERR_UNREACHABLE);                                                                      \
     }
 
 #define ENSURE(_x_) VERIFY(_x_)