Fixes two memory leaks coming from Transf. (#1564)

First, it adds a virtual destructor so the subclasses will get cleaned up. Second, it wraps the returned
pointer in a unique_ptr. Should fix ASAN failures in the nightly run.

diff --git a/src/theory/quantifiers/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus_grammar_norm.cpp
index 1b5cd345233e4a21587d1f64f20f8b644ce70c5d..6776aca154d69e236a8d959132a50ac49b195326 100644 (file)
--- a/src/theory/quantifiers/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus_grammar_norm.cpp
@@ -35,7 +35,7 @@ namespace quantifiers {
 
 bool OpPosTrie::getOrMakeType(TypeNode tn,
                               TypeNode& unres_tn,
-                              std::vector<unsigned> op_pos,
+                              const std::vector<unsigned>& op_pos,
                               unsigned ind)
 {
   if (ind == op_pos.size())
@@ -274,7 +274,7 @@ std::map<TypeNode, Node> SygusGrammarNorm::d_tn_to_id = {};
  *
  * returns true if collected anything
  */
-SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
+std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
     TypeNode tn, const Datatype& dt, const std::vector<unsigned>& op_pos)
 {
   NodeManager* nm = NodeManager::currentNM();
@@ -295,7 +295,7 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
       Trace("sygus-gnorm") << "...drop transf, " << rindices.size() << "/"
                            << op_pos.size() << " constructors." << std::endl;
       Assert(rindices.size() < op_pos.size());
-      return new TransfDrop(rindices);
+      return std::unique_ptr<Transf>(new TransfDrop(rindices));
     }
   }
 
@@ -363,7 +363,7 @@ SygusGrammarNorm::Transf* SygusGrammarNorm::inferTransf(
     Trace("sygus-gnorm") << "...chain transf." << std::endl;
     Trace("sygus-grammar-normalize-infer")
         << "\tInfering chain transformation\n";
-    return new TransfChain(chain_op_pos, elem_pos);
+    return std::unique_ptr<Transf>(new TransfChain(chain_op_pos, elem_pos));
   }
   return nullptr;
 }
@@ -417,7 +417,7 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
 
   /* Determine normalization transformation based on sygus type and given
     * operators */
-  Transf* transformation = inferTransf(tn, dt, op_pos);
+  std::unique_ptr<Transf> transformation = inferTransf(tn, dt, op_pos);
   /* If a transformation was selected, apply it */
   if (transformation != nullptr)
   {

diff --git a/src/theory/quantifiers/sygus_grammar_norm.h b/src/theory/quantifiers/sygus_grammar_norm.h
index d1894ac2e409ac752211ae4e0983d9fc2be55fae..f72a83e5aa5332883e96b303278fcfe4efd18e3f 100644 (file)
--- a/src/theory/quantifiers/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus_grammar_norm.h
@@ -17,7 +17,16 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
 
+#include <map>
+#include <memory>
+#include <string>
+#include <vector>
+
+#include "expr/datatype.h"
+#include "expr/node.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "expr/type.h"
+#include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
@@ -78,7 +87,7 @@ class OpPosTrie
    */
   bool getOrMakeType(TypeNode tn,
                      TypeNode& unres_tn,
-                     std::vector<unsigned> op_pos,
+                     const std::vector<unsigned>& op_pos,
                      unsigned ind = 0);
   /** clear all data from this trie */
   void clear() { d_children.clear(); }
@@ -241,6 +250,8 @@ class SygusGrammarNorm
   class Transf
   {
    public:
+    virtual ~Transf() {}
+
     /** abstract function for building normalized types
      *
      * Builds normalized types for the operators specifed by the positions in
@@ -262,12 +273,14 @@ class SygusGrammarNorm
   class TransfDrop : public Transf
   {
    public:
-    TransfDrop(std::vector<unsigned>& indices) : d_drop_indices(indices) {}
+    TransfDrop(const std::vector<unsigned>& indices) : d_drop_indices(indices)
+    {
+    }
     /** build type */
-    virtual void buildType(SygusGrammarNorm* sygus_norm,
-                           TypeObject& to,
-                           const Datatype& dt,
-                           std::vector<unsigned>& op_pos);
+    void buildType(SygusGrammarNorm* sygus_norm,
+                   TypeObject& to,
+                   const Datatype& dt,
+                   std::vector<unsigned>& op_pos) override;
 
    private:
     std::vector<unsigned> d_drop_indices;
@@ -294,7 +307,7 @@ class SygusGrammarNorm
   class TransfChain : public Transf
   {
    public:
-    TransfChain(unsigned chain_op_pos, std::vector<unsigned>& elem_pos)
+    TransfChain(unsigned chain_op_pos, const std::vector<unsigned>& elem_pos)
         : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){};
 
     /** builds types encoding a chain in which each link contains a repetition
@@ -322,10 +335,10 @@ class SygusGrammarNorm
      * transformation and so on until all operators originally given are
      * considered.
      */
-    virtual void buildType(SygusGrammarNorm* sygus_norm,
-                           TypeObject& to,
-                           const Datatype& dt,
-                           std::vector<unsigned>& op_pos) override;
+    void buildType(SygusGrammarNorm* sygus_norm,
+                   TypeObject& to,
+                   const Datatype& dt,
+                   std::vector<unsigned>& op_pos) override;
 
     /** Whether operator is chainable for the type (e.g. PLUS for Int)
      *
@@ -430,9 +443,9 @@ class SygusGrammarNorm
    *
    * TODO: #1304: Infer more complex transformations
    */
-  Transf* inferTransf(TypeNode tn,
-                      const Datatype& dt,
-                      const std::vector<unsigned>& op_pos);
+  std::unique_ptr<Transf> inferTransf(TypeNode tn,
+                                      const Datatype& dt,
+                                      const std::vector<unsigned>& op_pos);
 }; /* class SygusGrammarNorm */
 
 }  // namespace quantifiers