Merge pull request #1713 from karkhaz/kk-debug-timestamps

Emit timestamps on each line of output

Author: tautschnig

src/cbmc/all_properties.cpp

@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "all_properties_class.h"
 
-#include <util/time_stopping.h>
+#include <chrono>
+
 #include <util/xml.h>
 #include <util/json.h>
 
@@ -56,8 +57,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   solver.set_message_handler(get_message_handler());
 
-  // stop the time
-  absolute_timet sat_start=current_time();
+  auto now = std::chrono::steady_clock::now();
+  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
 
   bmc.do_conversion();
 
@@ -131,12 +132,12 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
         g.second.status=goalt::statust::SUCCESS;
   }
 
-  // output runtime
-
   {
-    absolute_timet sat_stop=current_time();
-    status() << "Runtime decision procedure: "
-             << (sat_stop-sat_start) << "s" << eom;
+    now = std::chrono::steady_clock::now();
+    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
+
+    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+             << "s" << eom;
   }
 
   // report

src/cbmc/bmc.cpp

@@ -11,14 +11,14 @@ Author: Daniel Kroening, [email protected]
 
 #include "bmc.h"
 
+#include <chrono>
 #include <fstream>
 #include <iostream>
 #include <memory>
 
 #include <util/string2int.h>
 #include <util/source_location.h>
 #include <util/string_utils.h>
-#include <util/time_stopping.h>
 #include <util/message.h>
 #include <util/json.h>
 #include <util/cprover_prefix.h>
@@ -154,20 +154,20 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
   prop_conv.set_message_handler(get_message_handler());
 
-  // stop the time
-  absolute_timet sat_start=current_time();
+  auto now = std::chrono::steady_clock::now();
+  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
 
   do_conversion();
 
   status() << "Running " << prop_conv.decision_procedure_text() << eom;
 
   decision_proceduret::resultt dec_result=prop_conv.dec_solve();
-  // output runtime
 
   {
-    absolute_timet sat_stop=current_time();
-    status() << "Runtime decision procedure: "
-             << (sat_stop-sat_start) << "s" << eom;
+    now = std::chrono::steady_clock::now();
+    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
+    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+             << "s" << eom;
   }
 
   return dec_result;

src/cbmc/bmc_cover.cpp

@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "bmc.h"
 
-#include <util/time_stopping.h>
+#include <chrono>
+
 #include <util/xml.h>
 #include <util/xml_expr.h>
 #include <util/json.h>
@@ -191,8 +192,8 @@ bool bmc_covert::operator()()
 
   solver.set_message_handler(get_message_handler());
 
-  // stop the time
-  absolute_timet sat_start=current_time();
+  auto now = std::chrono::steady_clock::now();
+  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
 
   // Collect _all_ goals in `goal_map'.
   // This maps property IDs to 'goalt'
@@ -251,12 +252,11 @@ bool bmc_covert::operator()()
 
   cover_goals();
 
-  // output runtime
-
   {
-    absolute_timet sat_stop=current_time();
-    status() << "Runtime decision procedure: "
-             << (sat_stop-sat_start) << "s" << eom;
+    now = std::chrono::steady_clock::now();
+    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
+    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+             << "s" << eom;
   }
 
   // report

src/cbmc/cbmc_parse_options.cpp

@@ -1029,6 +1029,7 @@ void cbmc_parse_optionst::help()
     " --json-ui                    use JSON-formatted output\n"
     HELP_GOTO_TRACE
     " --verbosity #                verbosity level\n"
+    HELP_TIMESTAMP
     "\n";
   // clang-format on
 }

src/cbmc/cbmc_parse_options.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/timestamper.h>
 
 #include <langapi/language.h>
 
@@ -62,6 +63,7 @@ class optionst;
   "(version)" \
   "(cover):(symex-coverage-report):" \
   "(mm):" \
+  OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
   "(ppc-macos)(unsigned-char)" \
   "(arrays-uf-always)(arrays-uf-never)" \

src/cbmc/fault_localization.cpp

@@ -11,12 +11,13 @@ Author: Peter Schrammel
 
 #include "fault_localization.h"
 
+#include <chrono>
+
 #include <util/threeval.h>
 #include <util/arith_tools.h>
 #include <util/symbol.h>
 #include <util/std_expr.h>
 #include <util/message.h>
-#include <util/time_stopping.h>
 #include <util/xml_expr.h>
 
 #include <solvers/prop/minimize.h>
@@ -245,8 +246,8 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
 
   prop_conv.set_message_handler(bmc.get_message_handler());
 
-  // stop the time
-  absolute_timet sat_start=current_time();
+  auto now = std::chrono::steady_clock::now();
+  auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
 
   bmc.do_conversion();
 
@@ -259,9 +260,10 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
   // output runtime
 
   {
-    absolute_timet sat_stop=current_time();
-    status() << "Runtime decision procedure: "
-             << (sat_stop-sat_start) << "s" << eom;
+    now = std::chrono::steady_clock::now();
+    auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
+    status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
+             << "s" << eom;
   }
 
   return dec_result;

src/cbmc/symex_coverage.cpp

@@ -13,11 +13,11 @@ Date: March 2016
 
 #include "symex_coverage.h"
 
+#include <chrono>
 #include <iostream>
 #include <fstream>
 #include <sstream>
 
-#include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/string2int.h>
 #include <util/cprover_prefix.h>
@@ -387,6 +387,10 @@ void symex_coveraget::build_cobertura(
   std::string overall_branch_rate_str=
     rate(overall_cov.branches_covered, overall_cov.branches_total);
 
+  auto now = std::chrono::system_clock::now();
+  auto current_time = std::chrono::time_point_cast<std::chrono::seconds>(now);
+  std::time_t tt = std::chrono::system_clock::to_time_t(current_time);
+
   // <coverage line-rate="0.0" branch-rate="0.0" lines-covered="1"
   //           lines-valid="1" branches-covered="1"
   //           branches-valid="1" complexity="0.0"
@@ -404,7 +408,7 @@ void symex_coveraget::build_cobertura(
   xml_coverage.set_attribute("complexity", "0.0");
   xml_coverage.set_attribute("version", "2.1.1");
   xml_coverage.set_attribute("timestamp",
-                             std::to_string(current_time().get_t()));
+                             std::to_string(tt));
 
   xmlt &packages=xml_coverage.new_element("packages");
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -906,5 +906,6 @@ void goto_analyzer_parse_optionst::help()
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
+    HELP_TIMESTAMP
     "\n";
 }

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -103,6 +103,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/timestamper.h>
 
 #include <langapi/language.h>
 
@@ -135,6 +136,7 @@ class optionst;
   "(show-local-may-alias)" \
   "(json):(xml):" \
   "(text):(dot):" \
+  OPT_TIMESTAMP \
   "(unreachable-instructions)(unreachable-functions)" \
   "(reachable-functions)" \
   "(intervals)(show-intervals)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -501,5 +501,6 @@ void goto_diff_parse_optionst::help()
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_TIMESTAMP
     "\n";
 }