From c4c9de08383bbe55d0f1d43e6f6c511fb43adc8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Jan 2017 20:09:27 -0800 Subject: [PATCH] fix memory leaks from cancellations Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 47 ++++++++++++++++++++++---------- src/muz/pdr/pdr_context.h | 6 ++-- src/muz/pdr/pdr_dl_interface.cpp | 6 +--- src/smt/asserted_formulas.cpp | 4 +-- 4 files changed, 39 insertions(+), 24 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 32f8e1ef1..587488fc9 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -575,7 +575,7 @@ namespace pdr { // Predicates that are variable representatives. Other predicates at // positions the variables occur are made equivalent with these. expr_ref_vector conj(m); - app_ref_vector& var_reprs = *(alloc(app_ref_vector, m)); + app_ref_vector var_reprs(m); ptr_vector aux_vars; unsigned ut_size = rule.get_uninterpreted_tail_size(); @@ -584,8 +584,9 @@ namespace pdr { init_atom(pts, rule.get_head(), var_reprs, conj, UINT_MAX); for (unsigned i = 0; i < ut_size; ++i) { if (rule.is_neg_tail(i)) { - dealloc(&var_reprs); - throw default_exception("PDR does not support negated predicates in rule tails"); + char const* msg = "PDR does not supported negated predicates in rule tails"; + IF_VERBOSE(0, verbose_stream() << msg << "\n";); + throw default_exception(msg); } init_atom(pts, rule.get_tail(i), var_reprs, conj, i); } @@ -600,14 +601,14 @@ namespace pdr { flatten_and(tail); for (unsigned i = 0; i < tail.size(); ++i) { expr_ref tmp(m); - var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); + var_subst vs(m, false); + vs(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); conj.push_back(tmp); TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";); if (!is_ground(tmp)) { std::stringstream msg; msg << "PDR cannot solve non-ground tails: " << tmp; IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); - dealloc(&var_reprs); throw default_exception(msg.str()); } } @@ -631,7 +632,7 @@ namespace pdr { m_rule2transition.insert(&rule, fml.get()); rules.push_back(&rule); } - m_rule2inst.insert(&rule, &var_reprs); + m_rule2inst.insert(&rule, alloc(app_ref_vector, var_reprs)); m_rule2vars.insert(&rule, aux_vars); TRACE("pdr", tout << rule.get_decl()->get_name() << "\n"; @@ -1468,13 +1469,20 @@ namespace pdr { reset(); } - void context::reset() { - TRACE("pdr", tout << "\n";); - decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); + void context::reset(decl2rel& rels) { + decl2rel::iterator it = rels.begin(), end = rels.end(); for (; it != end; ++it) { dealloc(it->m_value); } - m_rels.reset(); + rels.reset(); + } + + void context::reset(bool full) { + TRACE("pdr", tout << "reset\n";); + reset(m_rels); + if (full) { + reset(m_rels_tmp); + } m_search.reset(); m_query = 0; m_last_result = l_undef; @@ -1496,6 +1504,7 @@ namespace pdr { e->get_data().m_value->add_rule(pred_rules[i]); } } + TRACE("pdr", tout << "adding rules\n";); datalog::rule_set::iterator rit = rules.begin(), rend = rules.end(); for (; rit != rend; ++rit) { datalog::rule* r = *rit; @@ -1510,6 +1519,7 @@ namespace pdr { } } // Initialize use list dependencies + TRACE("pdr", tout << "initialize use list dependencies\n";); decl2rel::iterator it = rels.begin(), end = rels.end(); for (; it != end; ++it) { func_decl* pred = it->m_key; @@ -1523,9 +1533,11 @@ namespace pdr { } } + TRACE("pdr", tout << "initialize predicate transformers\n";); // Initialize the predicate transformers. it = rels.begin(), end = rels.end(); for (; it != end; ++it) { + SASSERT(it->m_value); pred_transformer& rel = *it->m_value; rel.initialize(rels); TRACE("pdr", rel.display(tout); ); @@ -1533,21 +1545,24 @@ namespace pdr { } void context::update_rules(datalog::rule_set& rules) { - decl2rel rels; + TRACE("pdr", tout << "update rules\n";); + reset(m_rels_tmp); init_core_generalizers(rules); - init_rules(rules, rels); - decl2rel::iterator it = rels.begin(), end = rels.end(); + init_rules(rules, m_rels_tmp); + decl2rel::iterator it = m_rels_tmp.begin(), end = m_rels_tmp.end(); for (; it != end; ++it) { pred_transformer* pt = 0; if (m_rels.find(it->m_key, pt)) { it->m_value->inherit_properties(*pt); } } - reset(); - it = rels.begin(), end = rels.end(); + reset(false); + it = m_rels_tmp.begin(), end = m_rels_tmp.end(); for (; it != end; ++it) { m_rels.insert(it->m_key, it->m_value); } + m_rels_tmp.reset(); + TRACE("pdr", tout << "done update rules\n";); } unsigned context::get_num_levels(func_decl* p) { @@ -1875,6 +1890,7 @@ namespace pdr { } lbool context::solve() { + TRACE("pdr", tout << "solve\n";); m_last_result = l_undef; try { solve_impl(); @@ -2090,6 +2106,7 @@ namespace pdr { } case l_undef: { TRACE("pdr", tout << "unknown state: " << mk_pp(m_pm.mk_and(cube), m) << "\n";); + IF_VERBOSE(1, verbose_stream() << "unknown state\n";); throw unknown_exception(); } } diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index c3567bdd8..a32a65c48 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -328,6 +328,7 @@ namespace pdr { datalog::context* m_context; manager m_pm; decl2rel m_rels; // Map from relation predicate to fp-operator. + decl2rel m_rels_tmp; func_decl_ref m_query_pred; pred_transformer* m_query; mutable model_search m_search; @@ -370,6 +371,8 @@ namespace pdr { void reset_core_generalizers(); + void reset(decl2rel& rels); + void validate(); void validate_proof(); void validate_search(); @@ -410,8 +413,7 @@ namespace pdr { lbool solve(); - - void reset(); + void reset(bool full = true); void set_query(func_decl* q) { m_query_pred = q; } diff --git a/src/muz/pdr/pdr_dl_interface.cpp b/src/muz/pdr/pdr_dl_interface.cpp index 761b730ce..5f4a200fc 100644 --- a/src/muz/pdr/pdr_dl_interface.cpp +++ b/src/muz/pdr/pdr_dl_interface.cpp @@ -19,12 +19,8 @@ Revision History: #include "dl_context.h" #include "dl_mk_coi_filter.h" -#include "dl_mk_interp_tail_simplifier.h" -#include "dl_mk_subsumption_checker.h" -#include "dl_mk_rule_inliner.h" #include "dl_rule.h" #include "dl_rule_transformer.h" -#include "smt2parser.h" #include "pdr_context.h" #include "pdr_dl_interface.h" #include "dl_rule_set.h" @@ -164,7 +160,7 @@ lbool dl_interface::query(expr * query) { m_context->set_proof_converter(m_ctx.get_proof_converter()); m_context->set_model_converter(m_ctx.get_model_converter()); m_context->set_query(query_pred); - m_context->set_axioms(bg_assertion); + m_context->set_axioms(bg_assertion); m_context->update_rules(m_pdr_rules); if (m_pdr_rules.get_rules().empty()) { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3c67cadcf..26395f9ab 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector & result) { } void asserted_formulas::push_scope() { - SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size()); + SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled()); TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); m_scopes.push_back(scope()); m_macro_manager.push_scope(); scope & s = m_scopes.back(); s.m_asserted_formulas_lim = m_asserted_formulas.size(); - SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead); + SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled()); s.m_inconsistent_old = m_inconsistent; m_defined_names.push(); m_bv_sharing.push_scope();