mirror of
https://github.com/Z3Prover/z3
synced 2026-08-03 04:33:28 +00:00
Address high-confidence clang analyzer findings from warning report (#10355)
The clang-tidy warning report surfaced a small set of high-confidence
analyzer findings with straightforward fixes: intentional null
dereference in debug-only crash paths, undefined oversized shifts in
`mpff`, uninitialized state in sorting-network setup, and `% 0` in a
unit test edge case.
- **Debug crash path**
- Replaced intentional null writes in `src/util/debug.cpp` with an
explicit crash helper based on `SIGSEGV`/`abort`.
- Keeps the failure mode intentional without relying on undefined
pointer dereference.
```c++
[[noreturn]] static void force_segfault() {
std::raise(SIGSEGV);
std::abort();
}
```
- **`mpff` integer extraction**
- Hardened `get_uint64` / `get_int64` against analyzer-reported
oversized right shifts.
- Computes the shift count in `int64_t`, asserts the valid range, and
guards the shift site.
- **Sorting-network initialization**
- Initialized `psort_nw::m_t` in the constructor to avoid
uninitialized-object diagnostics on construction paths that inspect
state before later assignment.
- **Test-only edge cases**
- Added an early return in `src/test/total_order.cpp` for `sz == 0` to
avoid `% 0` in randomized loops.
- Removed the extra trailing semicolon pattern around the `find_q`
namespace in `src/test/var_subst.cpp`.
- **Scope**
- Focused only on localized, semantics-preserving fixes from the warning
artifact.
- Left broader architectural warnings (for example,
constructor/destructor virtual-call diagnostics) out of this change.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
parent
a8542f5612
commit
07ccba46a1
5 changed files with 22 additions and 14 deletions
|
|
@ -50,6 +50,8 @@ static void tst2() {
|
|||
}
|
||||
|
||||
static void tst3(unsigned sz, unsigned num_rounds) {
|
||||
if (sz == 0)
|
||||
return;
|
||||
uint_total_order to;
|
||||
to.insert(0);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
|
|
@ -100,6 +102,8 @@ void move_after(unsigned_vector & v, unsigned_vector & inv_v, unsigned a, unsign
|
|||
}
|
||||
|
||||
static void tst4(unsigned sz, unsigned num_rounds) {
|
||||
if (sz == 0)
|
||||
return;
|
||||
uint_total_order to;
|
||||
unsigned_vector v;
|
||||
unsigned_vector inv_v;
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ namespace find_q {
|
|||
void operator()(app * n) {}
|
||||
void operator()(quantifier * n) { m_q = n; }
|
||||
};
|
||||
};
|
||||
}
|
||||
|
||||
quantifier * find_quantifier(expr * n) {
|
||||
find_q::proc p;
|
||||
|
|
|
|||
|
|
@ -17,6 +17,8 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#include<cstdio>
|
||||
#include<cstdlib>
|
||||
#include<csignal>
|
||||
#ifndef _WINDOWS
|
||||
#include<unistd.h>
|
||||
#endif
|
||||
|
|
@ -185,9 +187,13 @@ debug_action ask_debug_action(std::istream& in) {
|
|||
}
|
||||
|
||||
#if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
|
||||
[[noreturn]] static void force_segfault() {
|
||||
std::raise(SIGSEGV);
|
||||
std::abort();
|
||||
}
|
||||
|
||||
void invoke_debugger() {
|
||||
std::string buffer;
|
||||
int *x = nullptr;
|
||||
debug_action a = get_default_debug_action();
|
||||
for (;;) {
|
||||
switch (a) {
|
||||
|
|
@ -197,8 +203,7 @@ void invoke_debugger() {
|
|||
exit(1);
|
||||
case debug_action::stop:
|
||||
// force seg fault...
|
||||
*x = 0;
|
||||
return;
|
||||
force_segfault();
|
||||
case debug_action::throw_exception:
|
||||
throw default_exception("assertion violation");
|
||||
case debug_action::invoke_gdb:
|
||||
|
|
@ -210,8 +215,7 @@ void invoke_debugger() {
|
|||
else {
|
||||
std::cerr << "error starting GDB...\n";
|
||||
// forcing seg fault.
|
||||
int *x = nullptr;
|
||||
*x = 0;
|
||||
force_segfault();
|
||||
}
|
||||
return;
|
||||
case debug_action::invoke_lldb:
|
||||
|
|
@ -223,8 +227,7 @@ void invoke_debugger() {
|
|||
else {
|
||||
std::cerr << "error starting LLDB...\n";
|
||||
// forcing seg fault.
|
||||
int *x = nullptr;
|
||||
*x = 0;
|
||||
force_segfault();
|
||||
}
|
||||
return;
|
||||
case debug_action::ask:
|
||||
|
|
|
|||
|
|
@ -158,24 +158,26 @@ bool mpff_manager::is_uint64(mpff const & n) const {
|
|||
uint64_t mpff_manager::get_uint64(mpff const & a) const {
|
||||
SASSERT(is_uint64(a));
|
||||
if (is_zero(a)) return 0;
|
||||
int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
|
||||
int64_t exp = -static_cast<int64_t>(a.m_exponent) - sizeof(unsigned) * 8 * (m_precision - 2);
|
||||
SASSERT(exp >= 0);
|
||||
SASSERT(exp < 64);
|
||||
uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
|
||||
return *s >> static_cast<unsigned>(exp);
|
||||
return exp < 64 ? *s >> static_cast<unsigned>(exp) : 0;
|
||||
}
|
||||
|
||||
int64_t mpff_manager::get_int64(mpff const & a) const {
|
||||
SASSERT(is_int64(a));
|
||||
if (is_zero(a)) return 0;
|
||||
int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
|
||||
int64_t exp = -static_cast<int64_t>(a.m_exponent) - sizeof(unsigned) * 8 * (m_precision - 2);
|
||||
SASSERT(exp >= 0);
|
||||
SASSERT(exp < 64);
|
||||
uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
|
||||
// INT64_MIN case
|
||||
if (exp == 0 && *s == 0x8000000000000000ull && is_neg(a)) {
|
||||
return INT64_MIN;
|
||||
}
|
||||
else {
|
||||
int64_t r = *s >> static_cast<unsigned>(exp);
|
||||
int64_t r = exp < 64 ? *s >> static_cast<unsigned>(exp) : 0;
|
||||
if (is_neg(a))
|
||||
r = -r;
|
||||
return r;
|
||||
|
|
|
|||
|
|
@ -224,7 +224,7 @@ Notes:
|
|||
}
|
||||
};
|
||||
|
||||
psort_nw(psort_expr& c): ctx(c) {}
|
||||
psort_nw(psort_expr& c): ctx(c), m_t(GE) {}
|
||||
|
||||
sorting_network_config& cfg() { return m_cfg; }
|
||||
|
||||
|
|
@ -1497,4 +1497,3 @@ Notes:
|
|||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue