driver::totalTime statistic is now reported correctly on crashes, too

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b429ad0c24967e4bb88477c11193f097648dc773..c27179ee5cdbbbe334d3fbec0b120e6817b8d216 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -43,6 +43,7 @@
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 using namespace CVC4;
@@ -63,6 +64,9 @@ namespace CVC4 {
     /** A pointer to the CommandExecutor (the signal handlers need it) */
     CVC4::main::CommandExecutor* pExecutor = NULL;
 
+    /** A pointer to the totalTime driver stat (the signal handlers need it) */
+    CVC4::TimerStat* pTotalTime = NULL;
+
   }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
@@ -84,8 +88,8 @@ void printUsage(Options& opts, bool full) {
 int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Timer statistic
-  TimerStat s_totalTime("totalTime");
-  s_totalTime.start();
+  pTotalTime = new TimerStat("totalTime");
+  pTotalTime->start();
 
   // For the signal handlers' benefit
   pOptions = &opts;
@@ -216,7 +220,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   int returnValue = 0;
   {
     // Timer statistic
-    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), &s_totalTime);
+    RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), pTotalTime);
 
     // Filename statistics
     ReferenceStat< const char* > s_statFilename("filename", filename);
@@ -304,7 +308,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     ReferenceStat< Result > s_statSatResult("sat/unsat", result);
     RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), &s_statSatResult);
 
-    s_totalTime.stop();
+    pTotalTime->stop();
 
     // Set the global executor pointer to NULL first.  If we get a
     // signal while dumping statistics, we don't want to try again.
@@ -334,9 +338,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   // On exceptional exit, these are leaked, but that's okay... they
   // need to be around in that case for main() to print statistics.
+  delete pTotalTime;
   delete pExecutor;
   delete exprMgr;
 
+  pTotalTime = NULL;
   pExecutor = NULL;
 
   return returnValue;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 3e45b4f14bbfd2ad5cbbe8ccecb14b91e09e08f4..a83baf45ff67b15a960038a1c532694bfbbcbb1f 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -66,6 +66,7 @@ int main(int argc, char* argv[]) {
 #endif
     *opts[options::err] << "CVC4 Error:" << endl << e << endl;
     if(opts[options::statistics] && pExecutor != NULL) {
+      pTotalTime->stop();
       pExecutor->flushStatistics(*opts[options::err]);
     }
   }

diff --git a/src/main/main.h b/src/main/main.h
index 5b202c532774a3c25d04792ff39b1ca6d06e6793..56cd866da873eedc0765a5755fae8f11342ca7e3 100644 (file)
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -23,6 +23,7 @@
 #include "util/exception.h"
 #include "util/statistics.h"
 #include "util/tls.h"
+#include "util/statistics_registry.h"
 #include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
@@ -42,6 +43,9 @@ extern const char* progName;
 /** A reference for use by the signal handlers to print statistics */
 extern CVC4::main::CommandExecutor* pExecutor;
 
+/** A reference for use by the signal handlers to print statistics */
+extern CVC4::TimerStat* pTotalTime;
+
 /**
  * If true, will not spin on segfault even when CVC4_DEBUG is on.
  * Useful for nightly regressions, noninteractive performance runs

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 5e7436580225e44417ce322c0059ad5fc63ded26..d4d3e96d876c0d33ff9593f97784e174a380a201 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -58,6 +58,7 @@ bool segvNoSpin = false;
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   abort();
@@ -67,6 +68,7 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   abort();
@@ -92,6 +94,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
     abort();
@@ -112,6 +115,7 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   abort();
@@ -125,6 +129,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
     abort();
@@ -138,6 +143,7 @@ void ill_handler(int sig, siginfo_t* info, void*) {
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   abort();
@@ -162,6 +168,7 @@ void cvc4unexpected() {
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
     if((*pOptions)[options::statistics] && pExecutor != NULL) {
+      pTotalTime->stop();
       pExecutor->flushStatistics(cerr);
     }
     set_terminate(default_terminator);
@@ -175,6 +182,7 @@ void cvc4unexpected() {
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   set_terminate(default_terminator);
@@ -188,6 +196,7 @@ void cvc4terminate() {
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   default_terminator();
@@ -196,6 +205,7 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
   if((*pOptions)[options::statistics] && pExecutor != NULL) {
+    pTotalTime->stop();
     pExecutor->flushStatistics(cerr);
   }
   default_terminator();