mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

Implement API to set exit action to exception

Browse source
This commit is contained in:
Steven Moy 2024-03-26 14:28:44 -07:00
parent c18a42cf5b
commit 1c43da6663
6 changed files with 66 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/CMakeLists.txt
View file

@ -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

8
src/api/api_debug.cpp Normal file
View file

@ -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);
}
}

5
src/api/python/z3/z3.py
View file

@ -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

7
src/api/z3_api.h
View file

@ -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

31
src/util/debug.cpp
View file

@ -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() {

19
src/util/debug.h
View file

@ -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_)