From b994f336a7db6180427014721d673519ee6febf3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 31 Jan 2022 10:19:35 -0800 Subject: [PATCH] Fix memory leak in quantifier info (#8005) Fixes #8001. One of the maps in `QuantInfo` was containing heap-allocated objects that were not being destroyed. This commit changes the raw pointers to `std::unique_ptr` to avoid the memory leak. --- src/theory/quantifiers/quant_conflict_find.cpp | 6 +++--- src/theory/quantifiers/quant_conflict_find.h | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 | 4 ++++ 4 files changed, 9 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index dbe141c66..e1bebee74 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -70,14 +70,14 @@ QuantInfo::QuantInfo(Env& env, QuantConflictFind* p, Node q) j++) { if( d_vars[j].getKind()!=BOUND_VARIABLE ){ - d_var_mg[j] = NULL; + d_var_mg[j] = nullptr; bool is_tsym = false; if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){ is_tsym = true; d_tsym_vars.push_back( j ); } if( !is_tsym || options::qcfTConstraint() ){ - d_var_mg[j] = new MatchGen(p, this, d_vars[j], true); + d_var_mg[j] = std::make_unique(p, this, d_vars[j], true); } if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){ Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl; @@ -280,7 +280,7 @@ bool QuantInfo::reset_round() d_tconstraints.clear(); d_mg->reset_round(); - for (const std::pair& vg : d_var_mg) + for (const std::pair>& vg : d_var_mg) { if (!vg.second->reset_round()) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index c9cce84b9..b546aacd5 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -124,7 +124,7 @@ class MatchGen { class QuantInfo : protected EnvObj { public: - typedef std::map VarMgMap; + using VarMgMap = std::map>; QuantInfo(Env& env, QuantConflictFind* p, Node q); ~QuantInfo(); /** get quantified formula */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b746102b5..c86be3e76 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -982,6 +982,7 @@ set(regress_0_tests regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 regress0/quantifiers/issue7353-var-elim-par-dt.smt2 + regress0/quantifiers/issue8001-mem-leak.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 b/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 new file mode 100644 index 000000000..33695a7af --- /dev/null +++ b/test/regress/regress0/quantifiers/issue8001-mem-leak.smt2 @@ -0,0 +1,4 @@ +; COMMAND-LINE: -q +; EXPECT: unknown +(assert (forall ((V (Array Int Int))) (= 0 (select V 0)))) +(check-sat) -- 2.30.2