From 38fbf486dcb92ec1c8b6fedceb81026ea184f783 Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Sun, 19 Apr 2026 09:55:52 -0400 Subject: [PATCH] fix(anum): give anum move semantics to prevent sort-triggered double-free (#9320) Fixes a double-free (SIGSEGV in mpz_manager::del) in algebraic_numbers::manager::imp::del_poly, reached through the destruction of nlsat::evaluator's scoped_anum_vector members on a subsequent call to nra::solver::imp::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) --- src/math/polynomial/algebraic_numbers.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 46cb3c6da..e60f8ea1a 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -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); }