Fixes memory leak when an exception goes through runCvc4(). (Fixes #4590) (#4750)

As noted in #4590, CVC4 may leak memory if an exception is thrown that interrupts the command execution loop in runCvc4().
While not a major issue (the binary is terminated anyway in this case, this is also why we label it as feature), we should fix it nevertheless.

This commit makes sure that the current command is properly managed by using `std::unique_ptr` to handle its deletion.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7081e0f56892031b8f8133ac7d43a217ad91597a..d63861b0c68ed4058c5c134801ff688d5d5da5ca 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -78,7 +78,7 @@ bool CommandExecutor::doCommand(Command* cmd)
   }
 
   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
-  if(seq != NULL) {
+  if(seq != nullptr) {
     // assume no error
     bool status = true;
 
@@ -120,24 +120,24 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(d_options.getVerbosity() >= -1) {
     status = smtEngineInvoke(d_smtEngine, cmd, d_options.getOut());
   } else {
-    status = smtEngineInvoke(d_smtEngine, cmd, NULL);
+    status = smtEngineInvoke(d_smtEngine, cmd, nullptr);
   }
 
   Result res;
-  CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
-  if(cs != NULL) {
+  const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
+  if(cs != nullptr) {
     d_result = res = cs->getResult();
   }
-  QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
-  if(q != NULL) {
+  const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
+  if(q != nullptr) {
     d_result = res = q->getResult();
   }
-  CheckSynthCommand* csy = dynamic_cast<CheckSynthCommand*>(cmd);
-  if(csy != NULL) {
+ const  CheckSynthCommand* csy = dynamic_cast<const CheckSynthCommand*>(cmd);
+  if(csy != nullptr) {
     d_result = res = csy->getResult();
   }
 
-  if((cs != NULL || q != NULL) && d_options.getStatsEveryQuery()) {
+  if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
     flushStatistics(ossCurStats);
     std::ostream& err = *d_options.getErr();

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index ca49d9964e1a1979fdfe764d531959240accc287..de21db74df6aa2c15f6416c3d7e18e255c20a73d 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -59,6 +59,10 @@ class CommandExecutor
    */
   bool doCommand(CVC4::Command* cmd);
 
+  bool doCommand(std::unique_ptr<CVC4::Command>& cmd) {
+    return doCommand(cmd.get());
+  }
+
   /** Get a pointer to the solver object owned by this CommandExecutor. */
   api::Solver* getSolver() { return d_solver.get(); }
 

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b8d845f9e10f9d23513de9d605f1fd7a9c581c28..1c32f069b60e1be0c07415aaae304b5e03eb87bb 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -60,10 +60,10 @@ namespace CVC4 {
     const std::string *progName;
 
     /** A pointer to the CommandExecutor (the signal handlers need it) */
-    CVC4::main::CommandExecutor* pExecutor = NULL;
+    CVC4::main::CommandExecutor* pExecutor = nullptr;
 
     /** A pointer to the totalTime driver stat (the signal handlers need it) */
-    CVC4::TimerStat* pTotalTime = NULL;
+    CVC4::TimerStat* pTotalTime = nullptr;
 
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
@@ -201,7 +201,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
 
     // Parse and execute commands until we are done
-    Command* cmd;
+    std::unique_ptr<Command> cmd;
     bool status = true;
     if(opts.getInteractive() && inputFromStdin) {
       if(opts.getTearDownIncremental() > 0) {
@@ -209,10 +209,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             "--tear-down-incremental doesn't work in interactive mode");
       }
       if(!opts.wasSetByUserIncrementalSolving()) {
-        cmd = new SetOptionCommand("incremental", SExpr(true));
+        cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        delete cmd;
       }
       InteractiveShell shell(pExecutor->getSolver());
       if(opts.getInteractivePrompt()) {
@@ -230,37 +229,33 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
       while(true) {
         try {
-          cmd = shell.readCommand();
+          cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
           (*opts.getOut()) << CommandInterrupted();
           break;
         }
-        if (cmd == NULL)
+        if (cmd == nullptr)
           break;
         status = pExecutor->doCommand(cmd) && status;
         if (cmd->interrupted()) {
-          delete cmd;
           break;
         }
-        delete cmd;
       }
     } else if( opts.getTearDownIncremental() > 0) {
       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
         // For tear-down-incremental values greater than 1, need incremental
         // on too.
-        cmd = new SetOptionCommand("incremental", SExpr(true));
+        cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        delete cmd;
         // if(opts.wasSetByUserIncrementalSolving()) {
         //   throw OptionException(
         //     "--tear-down-incremental incompatible with --incremental");
         // }
 
-        // cmd = new SetOptionCommand("incremental", SExpr(false));
+        // cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
         // cmd->setMuted(true);
         // pExecutor->doCommand(cmd);
-        // delete cmd;
       }
 
       ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
@@ -287,14 +282,14 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         }
 
         try {
-          cmd = parser->nextCommand();
-          if (cmd == NULL) break;
+          cmd.reset(parser->nextCommand());
+          if (cmd == nullptr) break;
         } catch (UnsafeInterruptException& e) {
           interrupted = true;
           continue;
         }
 
-        if(dynamic_cast<PushCommand*>(cmd) != NULL) {
+        if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
           if(needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
@@ -321,21 +316,20 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             interrupted = true;
             continue;
           }
-        } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
+        } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
           allCommands.pop_back(); // fixme leaks cmds here
           if (needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
               {
-                Command* ccmd = allCommands[i][j]->clone();
+                std::unique_ptr<Command> ccmd(allCommands[i][j]->clone());
                 ccmd->setMuted(true);
                 pExecutor->doCommand(ccmd);
                 if (ccmd->interrupted())
                 {
                   interrupted = true;
                 }
-                delete ccmd;
               }
             }
             if (interrupted) continue;
@@ -348,8 +342,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
               continue;
             }
           }
-        } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-                  dynamic_cast<QueryCommand*>(cmd) != NULL) {
+        } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
+                  dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
           if(needReset >= opts.getTearDownIncremental()) {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
@@ -378,7 +372,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             interrupted = true;
             continue;
           }
-        } else if(dynamic_cast<ResetCommand*>(cmd) != NULL) {
+        } else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) {
           pExecutor->doCommand(cmd);
           allCommands.clear();
           allCommands.push_back(vector<Command*>());
@@ -386,16 +380,16 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           // We shouldn't copy certain commands, because they can cause
           // an error on replay since there's no associated sat/unsat check
           // preceding them.
-          if(dynamic_cast<GetUnsatCoreCommand*>(cmd) == NULL &&
-             dynamic_cast<GetProofCommand*>(cmd) == NULL &&
-             dynamic_cast<GetValueCommand*>(cmd) == NULL &&
-             dynamic_cast<GetModelCommand*>(cmd) == NULL &&
-             dynamic_cast<GetAssignmentCommand*>(cmd) == NULL &&
-             dynamic_cast<GetInstantiationsCommand*>(cmd) == NULL &&
-             dynamic_cast<GetAssertionsCommand*>(cmd) == NULL &&
-             dynamic_cast<GetInfoCommand*>(cmd) == NULL &&
-             dynamic_cast<GetOptionCommand*>(cmd) == NULL &&
-             dynamic_cast<EchoCommand*>(cmd) == NULL) {
+          if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr &&
+             dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) {
             Command* copy = cmd->clone();
             allCommands.back().push_back(copy);
           }
@@ -405,19 +399,16 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             continue;
           }
 
-          if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
-            delete cmd;
+          if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
             break;
           }
         }
-        delete cmd;
       }
     } else {
       if(!opts.wasSetByUserIncrementalSolving()) {
-        cmd = new SetOptionCommand("incremental", SExpr(false));
+        cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        delete cmd;
       }
 
       ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
@@ -440,8 +431,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           break;
         }
         try {
-          cmd = parser->nextCommand();
-          if (cmd == NULL) break;
+          cmd.reset(parser->nextCommand());
+          if (cmd == nullptr) break;
         } catch (UnsafeInterruptException& e) {
           interrupted = true;
           continue;
@@ -453,11 +444,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
           break;
         }
 
-        if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
-          delete cmd;
+        if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) {
           break;
         }
-        delete cmd;
       }
     }
 
@@ -485,7 +474,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     pTotalTime->stop();
 
     // Tim: I think that following comment is out of date?
-    // Set the global executor pointer to NULL first.  If we get a
+    // Set the global executor pointer to nullptr first.  If we get a
     // signal while dumping statistics, we don't want to try again.
     pExecutor->flushOutputStreams();
 
@@ -505,8 +494,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   delete pTotalTime;
   delete pExecutor;
 
-  pTotalTime = NULL;
-  pExecutor = NULL;
+  pTotalTime = nullptr;
+  pExecutor = nullptr;
 
   signal_handlers::cleanup();