mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-07 02:45:19 +00:00
Code Activity

fix(anum): give anum move semantics to prevent sort-triggered double-free (#9320)

Browse source 
Fixes a double-free (SIGSEGV in mpz_manager::del) in
algebraic_numbers::manager:👿:del_poly, reached through the
destruction of nlsat::evaluator's scoped_anum_vector members on a
subsequent call to nra::solver:👿:reset.

Root cause: sort_roots runs std::sort over a numeral_vector with a
comparator (lt_proc -> manager::lt -> compare_core) that legitimately
throws when the reslimit fires mid-comparison. libc++'s insertion sort
shifts elements via move-assignment inside its inner loop, and because
anum previously had only compiler-generated shallow copy/move (both
just copied m_cell without nulling the source), a throw between two
consecutive shifts could leave two vector slots pointing at the same
algebraic_cell. When the owning scoped_anum_vector was later destroyed
it del'd the same cell twice, reading through a freed chunk whose
first bytes had been overwritten by small_object_allocator's free-list
next pointer.

Fix: give anum proper move constructor and move assignment that
transfer the tagged m_cell pointer and null the source. Copy stays
a shallow handle copy (ownership is still tracked externally by the
manager / owning vector, as before). With the new move, every
intermediate state of sort's move-via-tmp sequence has at most one
slot referencing any given cell, so a throwing comparator can leak
the in-flight tmp cell but cannot produce aliased slots and therefore
cannot cause the downstream double-free.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Arie 2026-04-19 09:55:52 -04:00 • committed by GitHub
parent daf2506b60
commit 38fbf486dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polynomial/algebraic_numbers.h
View file

@ -381,7 +381,7 @@ namespace algebraic_numbers {
class anum {
class anum {
enum anum_kind { BASIC = 0, ROOT };
void* m_cell;
public:
@ -389,6 +389,17 @@ namespace algebraic_numbers {
anum(basic_cell* cell) :m_cell(TAG(void*, cell, BASIC)) { }
anum(algebraic_cell * cell):m_cell(TAG(void*, cell, ROOT)) { }
// Move nulls the source so std::sort's inner shifts stay alias-free
// if the comparator throws between moves (avoids a later double-free).
anum(anum const &) = default;
anum & operator=(anum const &) = default;
anum(anum && other) noexcept : m_cell(other.m_cell) { other.m_cell = nullptr; }
anum & operator=(anum && other) noexcept {
m_cell = other.m_cell;
other.m_cell = nullptr;
return *this;
}
bool is_basic() const { return GET_TAG(m_cell) == BASIC; }
basic_cell * to_basic() const { SASSERT(is_basic()); return UNTAG(basic_cell*, m_cell); }
algebraic_cell * to_algebraic() const { SASSERT(!is_basic()); return UNTAG(algebraic_cell*, m_cell); }