From 1c43da66634a18383c85cb9f79377958668fee18 Mon Sep 17 00:00:00 2001 From: Steven Moy Date: Tue, 26 Mar 2024 14:28:44 -0700 Subject: [PATCH 1/2] Implement API to set exit action to exception --- src/api/CMakeLists.txt | 1 + src/api/api_debug.cpp | 8 ++++++++ src/api/python/z3/z3.py | 5 +++++ src/api/z3_api.h | 7 +++++++ src/util/debug.cpp | 31 +++++++++++++++++++++++++++++++ src/util/debug.h | 19 ++++++++++++++----- 6 files changed, 66 insertions(+), 5 deletions(-) create mode 100644 src/api/api_debug.cpp diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 38a09b63187..086ed1822ac 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -44,6 +44,7 @@ z3_add_component(api api_context.cpp api_datalog.cpp api_datatype.cpp + api_debug.cpp api_fpa.cpp api_goal.cpp api_log.cpp diff --git a/src/api/api_debug.cpp b/src/api/api_debug.cpp new file mode 100644 index 00000000000..a5cfed9ac55 --- /dev/null +++ b/src/api/api_debug.cpp @@ -0,0 +1,8 @@ +#include "api/z3.h" +#include "util/util.h" + +extern "C" { + void Z3_API Z3_set_exit_action_to_throw_exception() { + set_default_exit_action(exit_action::throw_exception); + } +} \ No newline at end of file diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9a3dadda23e..76777223b68 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -316,6 +316,11 @@ def get_param(name): return r raise Z3Exception("failed to retrieve value for '%s'" % name) + +def set_exit_action_to_throw_exception(): + """Set the debug exit action to throw exception""" + Z3_set_exit_action_to_throw_exception() + ######################################### # # ASTs base class diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cbf9803dbbf..6bb97a6769b 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7455,6 +7455,13 @@ extern "C" { /**@}*/ + /** + \brief Set exit action to throw exception. + + def_API('Z3_set_exit_action_to_throw_exception', VOID, ()) + */ + void Z3_API Z3_set_exit_action_to_throw_exception(); + #ifdef __cplusplus } #endif // __cplusplus diff --git a/src/util/debug.cpp b/src/util/debug.cpp index c9ca9fc312a..ee57ac4b330 100644 --- 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 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 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 index 5f092b181ed..5e9ea9b2cb3 100644 --- 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_) From eae6814fce3c783b1a8adfcc3a5c5f9c05d93a43 Mon Sep 17 00:00:00 2001 From: Steven Moy Date: Wed, 27 Mar 2024 10:10:15 -0700 Subject: [PATCH 2/2] Turn on exit_action_to_throw_exception upon API context creation --- src/api/CMakeLists.txt | 1 - src/api/api_context.cpp | 2 ++ src/api/api_debug.cpp | 8 -------- src/api/python/z3/z3.py | 5 ----- src/api/z3_api.h | 7 ------- 5 files changed, 2 insertions(+), 21 deletions(-) delete mode 100644 src/api/api_debug.cpp diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 086ed1822ac..38a09b63187 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -44,7 +44,6 @@ z3_add_component(api api_context.cpp api_datalog.cpp api_datatype.cpp - api_debug.cpp api_fpa.cpp api_goal.cpp api_log.cpp diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 344224dd386..2f1f5071221 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include +#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(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); Z3_CATCH_RETURN_NO_HANDLE(nullptr); diff --git a/src/api/api_debug.cpp b/src/api/api_debug.cpp deleted file mode 100644 index a5cfed9ac55..00000000000 --- a/src/api/api_debug.cpp +++ /dev/null @@ -1,8 +0,0 @@ -#include "api/z3.h" -#include "util/util.h" - -extern "C" { - void Z3_API Z3_set_exit_action_to_throw_exception() { - set_default_exit_action(exit_action::throw_exception); - } -} \ No newline at end of file diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 76777223b68..9a3dadda23e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -316,11 +316,6 @@ def get_param(name): return r raise Z3Exception("failed to retrieve value for '%s'" % name) - -def set_exit_action_to_throw_exception(): - """Set the debug exit action to throw exception""" - Z3_set_exit_action_to_throw_exception() - ######################################### # # ASTs base class diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 6bb97a6769b..cbf9803dbbf 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -7455,13 +7455,6 @@ extern "C" { /**@}*/ - /** - \brief Set exit action to throw exception. - - def_API('Z3_set_exit_action_to_throw_exception', VOID, ()) - */ - void Z3_API Z3_set_exit_action_to_throw_exception(); - #ifdef __cplusplus } #endif // __cplusplus