From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 31 Jan 2022 18:19:35 +0000 (-0800)
Subject: Fix memory leak in quantifier info (#8005)
X-Git-Tag: cvc5-1.0.0~491
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b994f336a7db6180427014721d673519ee6febf3;p=cvc5.git

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<MatchGen>` to avoid the
memory leak.
---

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<MatchGen>(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<const size_t, MatchGen*>& vg : d_var_mg)
+  for (const std::pair<const size_t, std::unique_ptr<MatchGen>>& 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<size_t, MatchGen*> VarMgMap;
+  using VarMgMap = std::map<size_t, std::unique_ptr<MatchGen>>;
   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)