Improve why3-cpulimit so that it forcibly kills processes after a while.

A child process (e.g. CVC4) might catch SIGXCPU. If it gets stuck then, it
won't consume any additional cpu time, so the system won't forcibly kill
it. So why3-cpulimit has to kill it.

Note that, if the system is overloaded, why3-cpulimit might kill the child
process before it has even reached its cpu time limit. Hopefully, the 60'
additional time will suffice in practice.

src/tools/cpulimit.c

@@ -22,50 +22,84 @@
 #include <string.h>
 #include <sys/wait.h>
 
+void do_nothing() {}
+
+void usage(char *argv0) {
+  fprintf(stderr,
+          "usage: %s <time limit in seconds> <virtual memory limit in MiB>\n"
+          "          <show/hide cpu time: -s|-h> <command> <args>...\n\n"
+          "Zero sets no limit (keeps the actual limit)\n", argv0);
+  exit(EXIT_FAILURE);
+}
+
 int main(int argc, char *argv[]) {
   long timelimit, memlimit;
   int showtime, hidetime;
   struct rlimit res;
 
-  showtime = argc >= 4 && !strncmp("-s",argv[3],3);
-  hidetime = argc >= 4 && !strncmp("-h",argv[3],3);
+  if (argc < 5) usage(argv[0]);
 
-  if (argc < 5 || !(showtime || hidetime)) {
-    fprintf(stderr, "usage: %s <time limit in seconds> <virtual memory limit in MiB>\n"
-                    "          <show/hide cpu time: -s|-h> <command> <args>...\n\n"
-                    "Zero sets no limit (keeps the actual limit)\n", argv[0]);
-    return EXIT_FAILURE;
-  }
-
-  /* Fork if requested */
-  if (showtime) {
-      int pid = fork ();
+  showtime = !strcmp("-s", argv[3]);
+  hidetime = !strcmp("-h", argv[3]);
 
-      if (pid == -1) {
-          perror("fork");
-          exit(EXIT_FAILURE);
-      }
+  if (!(showtime || hidetime)) usage(argv[0]);
 
-      if (pid > 0) {
-          int status;
-          struct tms tms;
-          double time;
+  /* get time limit in seconds from command line */
+  timelimit = atol(argv[1]);
+  if (timelimit < 0) usage(argv[0]);
 
-          waitpid(pid, &status, 0);
+  /* get virtual memory limit in MiB from command line */
+  memlimit = atol(argv[2]);
+  if (memlimit < 0) usage(argv[0]);
 
-          times(&tms);
-          time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
-                                 / sysconf(_SC_CLK_TCK));
-          fprintf(stdout, "why3cpulimit time : %f s\n", time);
-          fflush(stdout);
+  /* Fork if requested */
+  if (showtime || timelimit) {
+    pid_t pid = fork ();
+
+    if (pid == -1) {
+      perror("fork");
+      exit(EXIT_FAILURE);
+    }
+
+    if (pid > 0) {
+      int status;
+      struct tms tms;
+      double time;
+      pid_t p;
+      struct sigaction sa;
+
+      sa.sa_handler = &do_nothing;
+      sigemptyset(&sa.sa_mask);
+      sa.sa_flags = 0;
+      sigaction(SIGALRM, &sa, NULL);
+
+      alarm(timelimit + 60);
+
+      p = waitpid(pid, &status, 0);
+
+      if (p <= 0) {
+        kill(pid, SIGKILL);
+        p = waitpid(pid, &status, 0);
+        if (p <= 0) {
+          perror("why3cpulimit waitpid");
+          kill(getpid(), SIGTERM);
+        }
+      }
 
-          if (WIFEXITED(status)) return WEXITSTATUS(status);
-          kill(getpid(),SIGTERM);
+      if (showtime) {
+        times(&tms);
+        time = (double)((tms.tms_cutime + tms.tms_cstime + 0.0)
+                        / sysconf(_SC_CLK_TCK));
+        fprintf(stderr, "why3cpulimit time : %f s\n", time);
       }
-  }
 
-  /* get time limit in seconds from command line */
-  timelimit = atol(argv[1]);
+      if (WIFEXITED(status)) return WEXITSTATUS(status);
+      if (WIFSIGNALED(status)) kill(getpid(), WTERMSIG(status));
+
+      fprintf(stderr, "why3cpulimit: child exited neither normally nor because of a signal\n");
+      kill(getpid(), SIGTERM);
+    }
+  }
 
   if (timelimit > 0) {
     /* set the CPU time limit */
@@ -74,9 +108,6 @@ int main(int argc, char *argv[]) {
     setrlimit(RLIMIT_CPU,&res);
   }
 
-  /* get virtual memory limit in MiB from command line */
-  memlimit = atol(argv[2]);
-
   if (memlimit > 0) {
     /* set the CPU memory limit */
     getrlimit(RLIMIT_AS,&res);