mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-28 19:01:29 +00:00
Code Activity

Fix memory leaks in model_based_opt def ref-counting

Browse source 
Three bugs in the def ref-counting infrastructure:

1. dec_ref() incremented (++) instead of decrementing (--) the ref count,
   so objects were never freed.

2. def_ref lacked copy and move constructors, so the compiler-generated
   default copy just copied the raw pointer without inc_ref. This caused
   use-after-free when def_ref values were copied into vectors.

3. Compound def types (add_def, mul_def, div_def) lacked destructors to
   dec_ref their children. Added virtual destructor to base def class
   and child-releasing destructors to compound types.

Fixes the memory leak from #7027 (model_based_opt.cpp:81).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-02-27 17:15:20 -10:00
parent 6ec40153cc
commit fc6696c5e4
2 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/model_based_opt.cpp
View file

@ -89,7 +89,7 @@ namespace opt {
}
void model_based_opt::def::dec_ref() {
SASSERT(m_ref_count > 0);
++m_ref_count;
--m_ref_count;
if (m_ref_count == 0)
dealloc(this);
}

19
src/math/simplex/model_based_opt.h
View file

@ -85,6 +85,7 @@ namespace opt {
enum def_t { add_t, mul_t, div_t, const_t, var_t};
struct def {
def() = default;
virtual ~def() = default;
static def* from_row(row const& r, unsigned x);
def_t m_type;
unsigned m_ref_count = 0;
@ -120,6 +121,12 @@ namespace opt {
if (d) d->inc_ref();
m_def = d;
}
def_ref(def_ref const& other) : m_def(other.m_def) {
if (m_def) m_def->inc_ref();
}
def_ref(def_ref&& other) noexcept : m_def(other.m_def) {
other.m_def = nullptr;
}
def_ref& operator=(def* d) {
if (d) d->inc_ref();
if (m_def) m_def->dec_ref();
@ -136,6 +143,15 @@ namespace opt {
return *this;
}
def_ref& operator=(def_ref&& d) noexcept {
if (&d == this)
return *this;
if (m_def) m_def->dec_ref();
m_def = d.m_def;
d.m_def = nullptr;
return *this;
}
def& operator*() { return *m_def; }
def* operator->() { return m_def; }
def const& operator*() const { return *m_def; }
@ -146,15 +162,18 @@ namespace opt {
struct add_def : public def {
def* x, *y;
add_def(def* x, def* y) : x(x), y(y) { m_type = add_t; x->inc_ref(); y->inc_ref(); }
~add_def() { x->dec_ref(); y->dec_ref(); }
};
struct mul_def : public def {
def* x, *y;
mul_def(def* x, def* y) : x(x), y(y) { m_type = mul_t; x->inc_ref(); y->inc_ref(); }
~mul_def() { x->dec_ref(); y->dec_ref(); }
};
struct div_def : public def {
def* x;
rational m_div{ 1 };
div_def(def* x, rational const& d) : x(x), m_div(d) { m_type = div_t; x->inc_ref(); }
~div_def() { x->dec_ref(); }
};
struct var_def : public def {
var v;