From 57bf4f3e6760fd98fbff4e552ef1700c84759243 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2013 18:41:08 -0800 Subject: [PATCH] feat(kernel/expr): avoid recursion when deleting expressions Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 74 ++++++++++++++++++++++++++++++++++++--------- src/kernel/expr.h | 12 ++++++++ 2 files changed, 72 insertions(+), 14 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 55d3840904..cb1ab138d8 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/hash.h" +#include "util/buffer.h" #include "kernel/expr.h" #include "kernel/free_vars.h" #include "kernel/expr_eq.h" @@ -53,6 +54,15 @@ expr_cell::expr_cell(expr_kind k, unsigned h, bool has_mv): g_hash_alloc_counter++; } +void expr_cell::dec_ref(expr & e, buffer & todelete) { + if (e) { + expr_cell * c = e.steal_ptr(); + lean_assert(!e); + if (c->dec_ref_core()) + todelete.push_back(c); + } +} + expr_var::expr_var(unsigned idx): expr_cell(expr_kind::Var, idx, false), m_vidx(idx) {} @@ -65,9 +75,15 @@ expr_app::expr_app(unsigned num_args, bool has_mv): expr_cell(expr_kind::App, 0, has_mv), m_num_args(num_args) { } -expr_app::~expr_app() { - for (unsigned i = 0; i < m_num_args; i++) - (m_args+i)->~expr(); +expr_app::~expr_app() {} +void expr_app::dealloc(buffer & todelete) { + unsigned i = m_num_args; + while (i > 0) { + --i; + dec_ref(m_args[i], todelete); + lean_assert(!m_args[i]); + } + delete[] reinterpret_cast(this); } expr mk_app(unsigned n, expr const * as) { lean_assert(n > 1); @@ -105,12 +121,24 @@ expr_eq::expr_eq(expr const & lhs, expr const & rhs): m_rhs(rhs) { } expr_eq::~expr_eq() {} +void expr_eq::dealloc(buffer & todelete) { + dec_ref(m_rhs, todelete); + dec_ref(m_lhs, todelete); + delete(this); +} expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & b): expr_cell(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar()), m_name(n), m_domain(t), m_body(b) { } +void expr_abstraction::dealloc(buffer & todelete) { + dec_ref(m_body, todelete); + dec_ref(m_domain, todelete); + lean_assert(!m_body); + lean_assert(!m_domain); + delete(this); +} expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Lambda, n, t, e) {} expr_pi::expr_pi(name const & n, expr const & t, expr const & e):expr_abstraction(expr_kind::Pi, n, t, e) {} expr_type::expr_type(level const & l): @@ -125,6 +153,12 @@ expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & m_value(v), m_body(b) { } +void expr_let::dealloc(buffer & todelete) { + dec_ref(m_body, todelete); + dec_ref(m_value, todelete); + dec_ref(m_type, todelete); + delete(this); +} expr_let::~expr_let() {} name value::get_unicode_name() const { return get_name(); } bool value::normalize(unsigned, expr const *, expr &) const { return false; } @@ -153,17 +187,29 @@ expr_metavar::expr_metavar(name const & n, local_context const & lctx): expr_metavar::~expr_metavar() {} void expr_cell::dealloc() { - switch (kind()) { - case expr_kind::Var: delete static_cast(this); break; - case expr_kind::Constant: delete static_cast(this); break; - case expr_kind::App: static_cast(this)->~expr_app(); delete[] reinterpret_cast(this); break; - case expr_kind::Eq: delete static_cast(this); break; - case expr_kind::Lambda: delete static_cast(this); break; - case expr_kind::Pi: delete static_cast(this); break; - case expr_kind::Type: delete static_cast(this); break; - case expr_kind::Value: delete static_cast(this); break; - case expr_kind::Let: delete static_cast(this); break; - case expr_kind::MetaVar: delete static_cast(this); break; + try { + buffer todo; + todo.push_back(this); + while (!todo.empty()) { + expr_cell * it = todo.back(); + todo.pop_back(); + lean_assert(it->get_rc() == 0); + switch (it->kind()) { + case expr_kind::Var: delete static_cast(it); break; + case expr_kind::Constant: delete static_cast(it); break; + case expr_kind::Value: delete static_cast(it); break; + case expr_kind::MetaVar: delete static_cast(it); break; + case expr_kind::Type: delete static_cast(it); break; + case expr_kind::Eq: static_cast(it)->dealloc(todo); break; + case expr_kind::App: static_cast(it)->dealloc(todo); break; + case expr_kind::Lambda: static_cast(it)->dealloc(todo); break; + case expr_kind::Pi: static_cast(it)->dealloc(todo); break; + case expr_kind::Let: static_cast(it)->dealloc(todo); break; + } + } + } catch (std::bad_alloc&) { + // We need this catch, because push_back may fail when expanding the buffer. + // In this case, we avoid the crash, and "accept" the memory leak. } } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index ec75f6a3b3..084835a8f1 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -47,6 +47,7 @@ The main API is divided in the following sections - Accessors - Miscellaneous ======================================= */ +class expr; enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type, Eq, Let, MetaVar }; class local_entry; /** @@ -82,6 +83,7 @@ protected: bool is_closed() const { return (m_flags & 2) != 0; } void set_closed() { m_flags |= 2; } friend class has_free_var_fn; + static void dec_ref(expr & c, buffer & todelete); public: expr_cell(expr_kind k, unsigned h, bool has_mv); expr_kind kind() const { return static_cast(m_kind); } @@ -96,6 +98,8 @@ class expr { private: expr_cell * m_ptr; explicit expr(expr_cell * ptr):m_ptr(ptr) {} + friend class expr_cell; + expr_cell * steal_ptr() { expr_cell * r = m_ptr; m_ptr = nullptr; return r; } public: expr():m_ptr(nullptr) {} expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } @@ -165,6 +169,8 @@ class expr_app : public expr_cell { unsigned m_num_args; expr m_args[0]; friend expr mk_app(unsigned num_args, expr const * args); + friend expr_cell; + void dealloc(buffer & todelete); public: expr_app(unsigned size, bool has_mv); ~expr_app(); @@ -177,6 +183,8 @@ public: class expr_eq : public expr_cell { expr m_lhs; expr m_rhs; + friend class expr_cell; + void dealloc(buffer & todelete); public: expr_eq(expr const & lhs, expr const & rhs); ~expr_eq(); @@ -188,6 +196,8 @@ class expr_abstraction : public expr_cell { name m_name; expr m_domain; expr m_body; + friend class expr_cell; + void dealloc(buffer & todelete); public: expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e); name const & get_name() const { return m_name; } @@ -210,6 +220,8 @@ class expr_let : public expr_cell { expr m_type; expr m_value; expr m_body; + friend class expr_cell; + void dealloc(buffer & todelete); public: expr_let(name const & n, expr const & t, expr const & v, expr const & b); ~expr_let();