Use unique_ptr for domains and strategy solvers

Instead of using raw pointers and managing memory manually, start using
unique_ptr. If an object contains a unique_ptr to another object as a
member, it is the owner.
In particular:
- template generator owns the abstract domain
- ssa analyzer owns the abstract value
- ssa analyzer owns the strategy solver (as a local variable in
  operator())
- product domain owns the inner domains, likewise for the product value
  and for the product strategy solver
- sympath domain owns the inner domain, likewise for the sympath solver
- sympath value owns all the inner values for individual symbolic paths,
  it also owns the inner value template

Generic abstract value has an abstract method "clone" that returns a
covariant type. Since this cannot be implemented using unique_ptr, it
returns a raw pointer. The caller is therefore responsible for taking
ownership of the cloned object.

Author: viktormalik

src/domains/domain.h

@@ -97,6 +97,8 @@ class domaint
     /// Each abstract value needs to implement clone with covariant return type.
     /// This is needed to properly clone abstract value when only a pointer to
     /// valuet is available.
+    /// Since the method returns a raw pointer, the caller is responsible for
+    /// taking ownership of the created object.
     virtual valuet *clone()=0;
 
     basic_valuet basic_value;

src/domains/product_domain.h

@@ -17,6 +17,10 @@ Author: Viktor Malik
 
 #include "domain.h"
 #include "strategy_solver_base.h"
+#include <memory>
+
+typedef std::vector<std::unique_ptr<domaint>> domain_vect;
+typedef std::vector<std::unique_ptr<domaint::valuet>> value_vect;
 
 class product_domaint:public domaint
 {
@@ -25,38 +29,23 @@ class product_domaint:public domaint
     unsigned int domainNumber,
     replace_mapt &renamingMap,
     const namespacet &ns,
-    const std::vector<domaint *> &domains):
-    domaint(domainNumber, renamingMap, ns), domains(domains) {}
-
-  // The domain owns the inner domains, therefore it must delete them properly
-  ~product_domaint() override
-  {
-    for(auto &domain : domains)
-      delete domain;
-  }
+    domain_vect domains):
+    domaint(domainNumber, renamingMap, ns), domains(std::move(domains)) {}
 
   /// Abstract value is a vector of abstract values of inner domains.
   /// The order has to match the order of domains.
-  struct valuet:domaint::valuet, std::vector<domaint::valuet *>
+  struct valuet:domaint::valuet, value_vect
   {
     valuet()=default;
-    explicit valuet(const std::vector<domaint::valuet *> &values):
-      vector(values) {}
+    explicit valuet(value_vect values):vector(std::move(values)) {}
 
     valuet *clone() override
     {
       auto new_value=new valuet();
       for(const auto &val : *this)
-        new_value->push_back(val->clone());
+        new_value->emplace_back(val->clone());
       return new_value;
     }
-
-    // The value owns the inner values and therefore has to delete them
-    ~valuet() override
-    {
-      for(auto &val : *this)
-        delete val;
-    };
   };
 
   // Most of the domain methods are implemented in such way that the
@@ -80,8 +69,17 @@ class product_domaint:public domaint
   void undo_sympath_restriction() override;
   void remove_all_sympath_restrictions() override;
 
+  /// Get a vector of raw pointers to the inner domains
+  std::vector<domaint *> get_domains()
+  {
+    std::vector<domaint *> result;
+    for(auto &d : domains)
+      result.push_back(d.get());
+    return result;
+  }
+
   // Product domain contains a vector of domains
-  std::vector<domaint *> domains;
+  domain_vect domains;
 
   // Value is a vector of values in corresponding domains
   valuet value;

src/domains/ssa_analyzer.cpp

@@ -78,19 +78,23 @@ void ssa_analyzert::operator()(
   domain=template_generator.domain();
 
   // get strategy solver from options
-  strategy_solver_baset *s_solver;
+  std::unique_ptr<strategy_solver_baset> s_solver;
   if(template_generator.options.get_bool_option("compute-ranking-functions"))
   {
     if(template_generator.options.get_bool_option(
       "monolithic-ranking-function"))
     {
-      s_solver=new SIMPLE_SOLVER(domain, linrank_domaint);
-      result=new linrank_domaint::templ_valuet();
+      s_solver=std::unique_ptr<strategy_solver_baset>(
+        new SIMPLE_SOLVER(domain, linrank_domaint));
+      result=std::unique_ptr<domaint::valuet>(
+        new linrank_domaint::templ_valuet());
     }
     else
     {
-      s_solver=new SIMPLE_SOLVER(domain, lexlinrank_domaint);
-      result=new lexlinrank_domaint::templ_valuet();
+      s_solver=std::unique_ptr<strategy_solver_baset>(
+        new SIMPLE_SOLVER(domain, lexlinrank_domaint));
+      result=std::unique_ptr<domaint::valuet>(
+        new lexlinrank_domaint::templ_valuet());
     }
   }
   else
@@ -99,37 +103,38 @@ void ssa_analyzert::operator()(
     // Check if symbolic paths domain is used. If so, invariant_domain points to
     // the inner domain of the symbolic paths domain.
     if(template_generator.options.get_bool_option("sympath"))
-      invariant_domain=dynamic_cast<sympath_domaint *>(domain)->inner_domain;
+      invariant_domain=
+        dynamic_cast<sympath_domaint *>(domain)->inner_domain.get();
     else
       invariant_domain=domain;
 
-    // simple_domains contains a vector of simple domains used.
+    // simple_domains contains a vector of pointers to simple domains used.
     // This is either invariant_domain (if a single simple domain is used) or
     // the vector of domains retrieved from the product domain.
     std::vector<domaint *> simple_domains;
     unsigned next_domain=0;
     auto *product_domain=dynamic_cast<product_domaint *>(invariant_domain);
     if(product_domain)
-      simple_domains=product_domain->domains;
+      simple_domains=product_domain->get_domains();
     else
       simple_domains.push_back(invariant_domain);
 
     // Create list of solvers and values.
     // Important: these must follow the order of domains created in the
     // template generator.
-    std::vector<strategy_solver_baset *> solvers;
-    std::vector<domaint::valuet *> values;
+    solver_vect solvers;
+    value_vect values;
     if(template_generator.options.get_bool_option("equalities"))
     {
-      solvers.push_back(
+      solvers.emplace_back(
         new SIMPLE_SOLVER(simple_domains[next_domain++], equality_domaint));
-      values.push_back(new equality_domaint::equ_valuet());
+      values.emplace_back(new equality_domaint::equ_valuet());
     }
     if(template_generator.options.get_bool_option("heap"))
     {
-      solvers.push_back(
+      solvers.emplace_back(
         new SIMPLE_SOLVER(simple_domains[next_domain++], heap_domaint));
-      values.push_back(new heap_domaint::heap_valuet());
+      values.emplace_back(new heap_domaint::heap_valuet());
     }
     if(template_generator.options.get_bool_option("intervals") ||
        template_generator.options.get_bool_option("zones") ||
@@ -138,42 +143,49 @@ void ssa_analyzert::operator()(
     {
       if(template_generator.options.get_bool_option("enum-solver"))
       {
-        solvers.push_back(
+        solvers.emplace_back(
           new SIMPLE_SOLVER(simple_domains[next_domain++], tpolyhedra_domaint));
-        values.push_back(new tpolyhedra_domaint::templ_valuet());
+        values.emplace_back(new tpolyhedra_domaint::templ_valuet());
       }
       else if(template_generator.options.get_bool_option("predabs-solver"))
       {
-        solvers.push_back(
+        solvers.emplace_back(
           new SIMPLE_SOLVER(simple_domains[next_domain++], predabs_domaint));
-        values.push_back(new predabs_domaint::templ_valuet());
+        values.emplace_back(new predabs_domaint::templ_valuet());
       }
       else if(template_generator.options.get_bool_option("binsearch-solver"))
       {
-        solvers.push_back(new BINSEARCH_SOLVER);
-        values.push_back(new tpolyhedra_domaint::templ_valuet());
+        solvers.emplace_back(new BINSEARCH_SOLVER);
+        values.emplace_back(new tpolyhedra_domaint::templ_valuet());
       }
       else
         assert(false);
     }
 
     if(solvers.size()==1)
     {
-      s_solver=solvers[0];
-      result=values[0];
+      s_solver=std::move(solvers[0]);
+      result=std::move(values[0]);
     }
     else
     {
-      s_solver=new strategy_solver_productt(
-        *product_domain, solver, SSA.ns, solvers);
-      result=new product_domaint::valuet(values);
+      s_solver=std::unique_ptr<strategy_solver_baset>(
+        new strategy_solver_productt(
+          *product_domain, solver, SSA.ns, std::move(solvers)));
+      result=std::unique_ptr<domaint::valuet>(
+        new product_domaint::valuet(std::move(values)));
     }
 
     if(template_generator.options.get_bool_option("sympath"))
     {
-      s_solver=new strategy_solver_sympatht(
-        *dynamic_cast<sympath_domaint *>(domain), solver, SSA, s_solver);
-      result=new sympath_domaint::sympath_valuet(result);
+      s_solver=std::unique_ptr<strategy_solver_baset>(
+        new strategy_solver_sympatht(
+          *dynamic_cast<sympath_domaint *>(domain),
+          solver,
+          SSA,
+          std::move(s_solver)));
+      result=std::unique_ptr<domaint::valuet>(
+        new sympath_domaint::sympath_valuet(std::move(result)));
     }
   }
 
@@ -191,8 +203,6 @@ void ssa_analyzert::operator()(
   solver_instances+=s_solver->get_number_of_solver_instances();
   solver_calls+=s_solver->get_number_of_solver_calls();
   solver_instances+=s_solver->get_number_of_solver_instances();
-
-  delete s_solver;
 }
 
 void ssa_analyzert::get_result(exprt &_result, const var_sett &vars)

src/domains/ssa_analyzer.h

@@ -26,19 +26,6 @@ class ssa_analyzert:public messaget
   typedef strategy_solver_baset::constraintst constraintst;
   typedef strategy_solver_baset::var_listt var_listt;
 
-  ssa_analyzert():
-    result(NULL),
-    solver_instances(0),
-    solver_calls(0)
-  {
-  }
-
-  ~ssa_analyzert()
-  {
-    if(result!=NULL)
-      delete result;
-  }
-
   void operator()(
     incremental_solvert &solver,
     local_SSAt &SSA,
@@ -51,8 +38,8 @@ class ssa_analyzert:public messaget
   inline unsigned get_number_of_solver_calls() { return solver_calls; }
 
 protected:
-  domaint *domain; // template generator is responsable for the domain object
-  domaint::valuet *result;
+  domaint *domain; // template generator is responsible for the domain object
+  std::unique_ptr<domaint::valuet> result;
 
   // statistics
   unsigned solver_instances;

src/domains/strategy_solver_product.h

@@ -17,6 +17,9 @@ Author: Viktor Malik
 
 #include "strategy_solver_base.h"
 #include "product_domain.h"
+#include <memory>
+
+typedef std::vector<std::unique_ptr<strategy_solver_baset>> solver_vect;
 
 class strategy_solver_productt:public strategy_solver_baset
 {
@@ -25,8 +28,9 @@ class strategy_solver_productt:public strategy_solver_baset
     product_domaint &domain,
     incremental_solvert &solver,
     const namespacet &ns,
-    const std::vector<strategy_solver_baset *> &solvers):
-    strategy_solver_baset(solver, ns), domain(domain), solvers(solvers) {}
+    solver_vect solvers):
+    strategy_solver_baset(solver, ns), domain(domain),
+    solvers(std::move(solvers)) {}
 
   bool iterate(invariantt &inv) override;
 
@@ -37,7 +41,7 @@ class strategy_solver_productt:public strategy_solver_baset
 protected:
   product_domaint &domain;
   // The solver contains a list of inner solvers
-  std::vector<strategy_solver_baset *> solvers;
+  solver_vect solvers;
 };
 
 #endif // CPROVER_2LS_DOMAINS_STRATEGY_SOLVER_PRODUCT_H

src/domains/strategy_solver_sympath.cpp

@@ -57,7 +57,7 @@ bool strategy_solver_sympatht::iterate(
       // The path has been altered during computation (solver has found another
       // loop-select guard that can be true
       auto new_sympath=inner_solver->symbolic_path.get_expr();
-      inv.emplace(new_sympath, inv.at(sympath));
+      inv.emplace(new_sympath, std::move(inv.at(sympath)));
       inv.erase(sympath);
       symbolic_path=inner_solver->symbolic_path;
 #ifdef DEBUG
@@ -70,7 +70,8 @@ bool strategy_solver_sympatht::iterate(
   else
   {
     // Computing invariant for a new path
-    auto new_value=inv.inner_value_template->clone();
+    auto new_value=std::unique_ptr<domaint::valuet>(
+      inv.inner_value_template->clone());
     domain.inner_domain->initialize_value(*new_value);
     improved=inner_solver->iterate(*new_value);
 
@@ -82,7 +83,7 @@ bool strategy_solver_sympatht::iterate(
       std::cerr << from_expr(ns, "", symbolic_path.get_expr()) << "\n";
 #endif
       const exprt sympath=inner_solver->symbolic_path.get_expr();
-      inv.emplace(sympath, new_value);
+      inv.emplace(sympath, std::move(new_value));
       new_path=false;
     }
   }

src/domains/strategy_solver_sympath.h

@@ -23,10 +23,10 @@ class strategy_solver_sympatht:public strategy_solver_baset
     sympath_domaint &_domain,
     incremental_solvert &_solver,
     const local_SSAt &SSA,
-    strategy_solver_baset *inner_solver):
+    std::unique_ptr<strategy_solver_baset> _inner_solver):
     strategy_solver_baset(_solver, SSA.ns),
     domain(_domain),
-    inner_solver(inner_solver)
+    inner_solver(std::move(_inner_solver))
   {
     build_loop_conds_map(SSA);
     inner_solver->use_sympaths();
@@ -40,7 +40,7 @@ class strategy_solver_sympatht:public strategy_solver_baset
   sympath_domaint &domain;
 
   // Strategy solver for the inner domain
-  strategy_solver_baset *inner_solver;
+  std::unique_ptr<strategy_solver_baset> inner_solver;
 
   std::vector<symbolic_patht> visited_paths;
   bool new_path=true;