From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 20 Sep 2017 18:24:13 +0000 (-0700)
Subject: Fix issue #1081, memory leak in cmd executor (#1109)
X-Git-Tag: cvc5-1.0.0~5625
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=54ed57102bbd35241c68d128f88bf2b93dd236cf;p=cvc5.git

Fix issue #1081, memory leak in cmd executor (#1109)

The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a18bb1fe4..7c8ee7827 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -20,7 +20,9 @@
 
 #include <cassert>
 #include <iostream>
+#include <memory>
 #include <string>
+#include <vector>
 
 #include "main/main.h"
 #include "smt/command.h"
@@ -130,15 +132,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 
   // dump the model/proof/unsat core if option is set
   if (status) {
-    Command* g = NULL;
+    std::vector<std::unique_ptr<Command> > getterCommands;
     if (d_options.getProduceModels() && d_options.getDumpModels() &&
         (res.asSatisfiabilityResult() == Result::SAT ||
          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) {
-      g = new GetModelCommand();
+      getterCommands.emplace_back(new GetModelCommand());
     }
     if (d_options.getProof() && d_options.getDumpProofs() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetProofCommand();
+      getterCommands.emplace_back(new GetProofCommand());
     }
 
     if (d_options.getDumpInstantiations() &&
@@ -146,26 +148,30 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
           (res.asSatisfiabilityResult() == Result::SAT ||
            (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) ||
          res.asSatisfiabilityResult() == Result::UNSAT)) {
-      g = new GetInstantiationsCommand();
+      getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
     if (d_options.getDumpSynth() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetSynthSolutionCommand();
+      getterCommands.emplace_back(new GetSynthSolutionCommand());
     }
 
     if (d_options.getDumpUnsatCores() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetUnsatCoreCommand();
+      getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
-    if (g != NULL) {
+    if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
       if (d_options.getForceNoLimitCpuWhileDump()) {
         setNoLimitCPU();
       }
-      status = doCommandSingleton(g);
-      delete g;
+      for (const auto& getterCommand : getterCommands) {
+        status = doCommandSingleton(getterCommand.get());
+        if (!status && !d_options.getContinuedExecution()) {
+          break;
+        }
+      }
     }
   }
   return status;