only selectively kill child, not entire process group

Author: Daniel Kroening

src/util/run.cpp

@@ -181,6 +181,9 @@ int run(
     }
     else /* fork() returns new pid to the parent process */
     {
+      // must do before resuming signals to avoid race
+      register_child(childpid);
+
       // resume signals
       sigprocmask(SIG_SETMASK, &old_mask, nullptr);
 
@@ -192,6 +195,8 @@ int run(
           continue; // try again
         else
         {
+          unregister_child();
+
           perror("Waiting for child process failed");
           if(stdin_fd!=STDIN_FILENO)
             close(stdin_fd);
@@ -202,6 +207,8 @@ int run(
           return 1;
         }
 
+      unregister_child();
+
       if(stdin_fd!=STDIN_FILENO)
         close(stdin_fd);
       if(stdout_fd!=STDOUT_FILENO)

src/util/signal_catcher.cpp

@@ -21,13 +21,23 @@ Author: Daniel Kroening, [email protected]
 
 // Here we have an instance of an ugly global object.
 // It keeps track of any child processes that we'll kill
-// when we are told to terminate.
+// when we are told to terminate. "No child" is indicated by '0'.
 
 #ifdef _WIN32
 #else
-std::vector<pid_t> pids_of_children;
+pid_t child_pid = 0;
 #endif
 
+void register_child(pid_t pid)
+{
+  child_pid = pid;
+}
+
+void unregister_child()
+{
+  child_pid = 0;
+}
+
 void install_signal_catcher()
 {
   #if defined(_WIN32)
@@ -66,13 +76,13 @@ void signal_catcher(int sig)
   #if defined(_WIN32)
   #else
 
-  #if 1
+  #if 0
   // kill any children by killing group
   killpg(0, sig);
   #else
-  // pass on to any children
-  for(const auto &pid : pids_of_children)
-    kill(pid, sig);
+  // pass on to our child, if any
+  if(child_pid != 0)
+    kill(child_pid, sig);
   #endif
 
   exit(sig); // should contemplate something from sysexits.h

src/util/signal_catcher.h

@@ -14,4 +14,10 @@ void install_signal_catcher();
 void remove_signal_catcher();
 void signal_catcher(int sig);
 
+#ifndef _WIN32
+#include <csignal>
+void register_child(pid_t);
+void unregister_child();
+#endif
+
 #endif // CPROVER_UTIL_SIGNAL_CATCHER_H