mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-31 08:39:01 +00:00
Code Activity

fix heap corruption from root_function move/sort operations

Browse source 
root_function's move constructor and move assignment were doing deep
copies of algebraic numbers via anum_manager::set() instead of proper
moves. During std::vector reallocation (emplace) and std::sort, this
caused massive allocation churn that corrupted the heap.

Fixes:
1. Move constructor: use std::move(other.val) for proper swap semantics.
2. Move assignment: use val.swap(other.val) instead of deep copy.
3. Add friend swap() for ADL so std::sort uses efficient swaps.
4. Sort root_function partitions via index permutation + swap cycles
   instead of std::sort directly on root_function objects.
5. Reserve rfunc vector before emplace in add_linear_approximations().
6. Reserve lhalf/uhalf vectors before collecting root functions.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-28 04:57:44 -10:00 • committed by Lev Nachmanson
parent e760eabd2b
commit 20548c08ec
1 changed files with 53 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/nlsat/levelwise.cpp
View file

@ -9,6 +9,7 @@
#include <algorithm>
#include <cstdint>
#include <numeric>
#include <set>
#include <unordered_map>
#include <utility>
@ -85,15 +86,20 @@ namespace nlsat {
unsigned ps_idx; // index in m_level_ps
root_function(anum_manager& am, poly* p, unsigned idx, anum const& v, unsigned ps_idx)
: val(am), ire{ p, idx }, ps_idx(ps_idx) { am.set(val, v); }
root_function(root_function&& other) noexcept : val(other.val.m()), ire(other.ire), ps_idx(other.ps_idx) { val = other.val; }
root_function(root_function&& other) noexcept : val(std::move(other.val)), ire(other.ire), ps_idx(other.ps_idx) { }
root_function(root_function const&) = delete;
root_function& operator=(root_function const&) = delete;
root_function& operator=(root_function&& other) noexcept {
val = other.val;
val.swap(other.val);
ire = other.ire;
ps_idx = other.ps_idx;
return *this;
}
friend void swap(root_function& a, root_function& b) noexcept {
a.val.swap(b.val);
std::swap(a.ire, b.ire);
std::swap(a.ps_idx, b.ps_idx);
}
};
// Root functions (Theta) and the chosen relation (≼) on a given level.
@ -950,12 +956,48 @@ namespace nlsat {
return m_pm.id(a.ire.p) < m_pm.id(b.ire.p);
}
// Apply a permutation to a range of root_functions using swap cycles,
// avoiding the bulk anum allocations that std::sort's move operations cause.
void apply_permutation(std_vector<root_function>& rfs, unsigned offset, std_vector<unsigned>& perm) {
std_vector<bool> done(perm.size(), false);
for (unsigned i = 0; i < perm.size(); ++i) {
if (done[i] || perm[i] == i)
continue;
unsigned j = i;
while (!done[j]) {
done[j] = true;
unsigned k = perm[j];
if (!done[k])
swap(rfs[offset + j], rfs[offset + k]);
j = k;
}
}
}
void sort_root_function_partitions(std_vector<root_function>::iterator mid) {
auto& rfs = m_rel.m_rfunc;
std::sort(rfs.begin(), mid,
[&](root_function const& a, root_function const& b) { return root_function_lt(a, b, true); });
std::sort(mid, rfs.end(),
[&](root_function const& a, root_function const& b) { return root_function_lt(a, b, false); });
unsigned mid_pos = static_cast<unsigned>(mid - rfs.begin());
// Sort lower partition [0, mid_pos) by index permutation
if (mid_pos > 1) {
std_vector<unsigned> perm(mid_pos);
std::iota(perm.begin(), perm.end(), 0u);
std::sort(perm.begin(), perm.end(), [&](unsigned a, unsigned b) {
return root_function_lt(rfs[a], rfs[b], true);
});
apply_permutation(rfs, 0, perm);
}
// Sort upper partition [mid_pos, size) by index permutation
unsigned upper_sz = static_cast<unsigned>(rfs.size()) - mid_pos;
if (upper_sz > 1) {
std_vector<unsigned> perm(upper_sz);
std::iota(perm.begin(), perm.end(), 0u);
std::sort(perm.begin(), perm.end(), [&](unsigned a, unsigned b) {
return root_function_lt(rfs[mid_pos + a], rfs[mid_pos + b], false);
});
apply_permutation(rfs, mid_pos, perm);
}
}
// Populate Θ (root functions) around the sample, partitioned at `mid`, and sort each partition.
@ -964,6 +1006,9 @@ namespace nlsat {
init_poly_has_roots();
std_vector<root_function> lhalf, uhalf;
// Pre-reserve to reduce reallocation during emplace_back
lhalf.reserve(m_level_ps.size());
uhalf.reserve(m_level_ps.size());
if (!collect_partitioned_root_functions_around_sample(v, lhalf, uhalf))
return false;
@ -1039,6 +1084,8 @@ namespace nlsat {
void add_linear_approximations(anum const& v) {
polynomial_ref p_lower(m_pm), p_upper(m_pm);
auto& r = m_rel.m_rfunc;
// Reserve space to avoid reallocation during emplace
r.reserve(r.size() + 2);
if (m_I[m_level].is_section()) {
if (!m_am.is_rational(v)) {
NOT_IMPLEMENTED_YET();