mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

fix exception unsafety leading to double free, issues #184 and issue #175. Location and fix strategy suggested by Nuno

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-09 00:34:59 +02:00
parent ff24375550
commit 7c9dd6b8a8
2 changed files with 19 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/math/grobner/grobner.cpp
View file

@ -59,15 +59,19 @@ void grobner::del_equation(equation * eq) {
m_to_process.erase(eq); m_to_process.erase(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
m_equations_to_delete[eq->m_bidx] = 0; m_equations_to_delete[eq->m_bidx] = 0;
ptr_vector<monomial>::iterator it1 = eq->m_monomials.begin(); del_monomials(eq->m_monomials);
ptr_vector<monomial>::iterator end1 = eq->m_monomials.end();
for (; it1 != end1; ++it1) {
monomial * m = *it1;
del_monomial(m);
}
dealloc(eq); dealloc(eq);
} }
void grobner::del_monomials(ptr_vector<monomial>& ms) {
ptr_vector<monomial>::iterator it = ms.begin();
ptr_vector<monomial>::iterator end = ms.end();
for (; it != end; ++it) {
del_monomial(*it);
}
ms.reset();
}
void grobner::del_monomial(monomial * m) { void grobner::del_monomial(monomial * m) {
ptr_vector<expr>::iterator it2 = m->m_vars.begin(); ptr_vector<expr>::iterator it2 = m->m_vars.begin();
ptr_vector<expr>::iterator end2 = m->m_vars.end(); ptr_vector<expr>::iterator end2 = m->m_vars.end();
@ -436,16 +440,18 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
unsigned sz = monomials.size(); unsigned sz = monomials.size();
if (sz == 0) if (sz == 0)
return; return;
ptr_vector<monomial>& to_delete = m_tmp_monomials;
to_delete.reset();
for (unsigned i = 1; i < sz; ++i) { for (unsigned i = 1; i < sz; ++i) {
monomial * m1 = monomials[j]; monomial * m1 = monomials[j];
monomial * m2 = monomials[i]; monomial * m2 = monomials[i];
if (is_eq_monomial_body(m1, m2)) { if (is_eq_monomial_body(m1, m2)) {
m1->m_coeff += m2->m_coeff; m1->m_coeff += m2->m_coeff;
del_monomial(m2); to_delete.push_back(m2);
} }
else { else {
if (m1->m_coeff.is_zero()) if (m1->m_coeff.is_zero())
del_monomial(m1); // cancelled to_delete.push_back(m1);
else else
j++; j++;
monomials[j] = m2; monomials[j] = m2;
@ -454,10 +460,11 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
SASSERT(j < sz); SASSERT(j < sz);
monomial * m1 = monomials[j]; monomial * m1 = monomials[j];
if (m1->m_coeff.is_zero()) if (m1->m_coeff.is_zero())
del_monomial(m1); // cancelled to_delete.push_back(m1);
else else
j++; j++;
monomials.shrink(j); monomials.shrink(j);
del_monomials(to_delete);
TRACE("grobner", tout << "after merging monomials:\n"; display_monomials(tout, monomials.size(), monomials.c_ptr()); tout << "\n";); TRACE("grobner", tout << "after merging monomials:\n"; display_monomials(tout, monomials.size(), monomials.c_ptr()); tout << "\n";);
} }
@ -649,6 +656,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
target->m_lc = false; target->m_lc = false;
mul_append(1, source, coeff, rest, new_monomials); mul_append(1, source, coeff, rest, new_monomials);
del_monomial(curr); del_monomial(curr);
target->m_monomials[i] = 0;
} }
else { else {
target->m_monomials[j] = curr; target->m_monomials[j] = curr;

2
src/math/grobner/grobner.h
View file

@ -126,6 +126,8 @@ protected:
void del_equations(unsigned old_size); void del_equations(unsigned old_size);
void del_monomials(ptr_vector<monomial>& monomials);
void unfreeze_equations(unsigned old_size); void unfreeze_equations(unsigned old_size);
void del_equation(equation * eq); void del_equation(equation * eq);