3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-01 19:54:04 +00:00

Fix releaseClang segfault: declare invoke_exit_action [[noreturn]], remove __builtin_unreachable() from UNREACHABLE() (#10295)

Commit d46fbad3 added `__builtin_unreachable()` to the `UNREACHABLE()`
macro in Clang builds to suppress `-Wimplicit-fallthrough` warnings. In
Release+Clang mode, this causes UB: Clang can legally eliminate the
`invoke_exit_action` call (since reaching `__builtin_unreachable()` is
UB, the compiler assumes the entire branch is dead), so when
`UNREACHABLE()` is actually hit, the function continues with
uninitialized state — producing the segfault observed in the FPA C
example.

## Changes

- **`src/util/debug.h`** — Declare `invoke_exit_action` as
`[[noreturn]]`. This is semantically accurate: the function always
terminates via `exit()` or `throw`, never returning normally. The
`[[noreturn]]` annotation naturally suppresses `-Wimplicit-fallthrough`
after `UNREACHABLE()` without any UB.
- **`src/util/debug.h`** — Remove `__compiler_unreachable` macro and its
use in `UNREACHABLE()`. With `[[noreturn]]` on `invoke_exit_action`, it
is redundant.
- **`src/util/debug.cpp`** — Add `[[noreturn]]` to the
`invoke_exit_action` definition to match.

```cpp
// Before (broken in Release+Clang: UB allows optimizer to eliminate invoke_exit_action)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); }; __builtin_unreachable()

// After (invoke_exit_action is [[noreturn]], no UB)
# define UNREACHABLE() { notify_assertion_violation(...); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-29 13:23:43 -07:00 committed by GitHub
parent 0692c3e01d
commit a3be01b9ca
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 21032 additions and 10 deletions

View file

@ -122,7 +122,7 @@ void set_default_exit_action(exit_action a) {
g_default_exit_action = a;
}
void invoke_exit_action(unsigned int code) {
[[noreturn]] void invoke_exit_action(unsigned int code) {
exit_action a = get_default_exit_action();
switch (a) {
case exit_action::exit:

View file

@ -42,7 +42,7 @@ enum class exit_action {
};
exit_action get_default_exit_action();
void set_default_exit_action(exit_action a);
void invoke_exit_action(unsigned int code);
[[noreturn]] void invoke_exit_action(unsigned int code);
#include "util/error_codes.h"
#include "util/warning.h"
@ -92,16 +92,10 @@ bool is_debug_enabled(const char * tag);
INVOKE_DEBUGGER(); \
})
#ifdef __clang__
#define __compiler_unreachable __builtin_unreachable()
#else
#define __compiler_unreachable
#endif
#ifdef Z3DEBUG
# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER(); __compiler_unreachable;)
# 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."); invoke_exit_action(ERR_UNREACHABLE); }; __compiler_unreachable
# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
#endif
#ifdef Z3DEBUG

21028
z3.log Normal file

File diff suppressed because it is too large Load diff