Replace util/timer* with std::chrono

The old timer API was written in 2004 and is superseded by std::chrono.
All clients of the old API are updated to use std::chrono, and the old
API classes are removed. This is in preparation for a commit that uses
features of chrono that are not present in the old time API.

Author: karkhaz

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/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/util/Makefile

@@ -84,8 +84,6 @@ SRC = arith_tools.cpp \
       tempdir.cpp \
       tempfile.cpp \
       threeval.cpp \
-      time_stopping.cpp \
-      timer.cpp \
       type.cpp \
       type_eq.cpp \
       typecheck.cpp \