From 3f6965b78999a475eff1ad6187ebee5496790ff6 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 14 Feb 2018 06:43:28 +0000 Subject: [PATCH 1/2] 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. --- src/cbmc/all_properties.cpp | 17 ++--- src/cbmc/bmc.cpp | 14 ++-- src/cbmc/bmc_cover.cpp | 16 ++--- src/cbmc/fault_localization.cpp | 14 ++-- src/cbmc/symex_coverage.cpp | 8 ++- src/util/Makefile | 2 - src/util/time_stopping.cpp | 69 -------------------- src/util/time_stopping.h | 110 -------------------------------- src/util/timer.cpp | 45 ------------- src/util/timer.h | 76 ---------------------- 10 files changed, 38 insertions(+), 333 deletions(-) delete mode 100644 src/util/time_stopping.cpp delete mode 100644 src/util/time_stopping.h delete mode 100644 src/util/timer.cpp delete mode 100644 src/util/timer.h diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 2a67d388caf..05490c613c7 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "all_properties_class.h" -#include +#include + #include #include @@ -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(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(now); + + status() << "Runtime decision procedure: " << (sat_stop - sat_start).count() + << "s" << eom; } // report diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 2abd76f7383..71d096b25bb 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "bmc.h" +#include #include #include #include @@ -18,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -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(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(now); + status() << "Runtime decision procedure: " << (sat_stop - sat_start).count() + << "s" << eom; } return dec_result; diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index a91eeed2c9a..2afc70a59d8 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "bmc.h" -#include +#include + #include #include #include @@ -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(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(now); + status() << "Runtime decision procedure: " << (sat_stop - sat_start).count() + << "s" << eom; } // report diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 31a1673f0ca..b29be8ed588 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -11,12 +11,13 @@ Author: Peter Schrammel #include "fault_localization.h" +#include + #include #include #include #include #include -#include #include #include @@ -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(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(now); + status() << "Runtime decision procedure: " << (sat_stop - sat_start).count() + << "s" << eom; } return dec_result; diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index dc9fef60567..c6a9e3cd419 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -13,11 +13,11 @@ Date: March 2016 #include "symex_coverage.h" +#include #include #include #include -#include #include #include #include @@ -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(now); + std::time_t tt = std::chrono::system_clock::to_time_t(current_time); + // - -#if defined(_WIN32) && !defined(__MINGW32__) -#include -#include -#else -#include -#endif - -#if defined(_WIN32) && !defined(__MINGW32__) -// NOLINTNEXTLINE(readability/identifiers) -struct timezone -{ - int dummy; -}; - -// NOLINTNEXTLINE(readability/identifiers) -void gettimeofday(struct timeval* p, struct timezone *tz) -{ - union - { - long long ns100; /*time since 1 Jan 1601 in 100ns units */ - FILETIME ft; - } _now; - - GetSystemTimeAsFileTime(&(_now.ft)); - p->tv_usec=(long)((_now.ns100 / 10LL) % 1000000LL); - p->tv_sec= (long)((_now.ns100-(116444736000000000LL))/10000000LL); -} -#endif - -absolute_timet current_time() -{ - // NOLINTNEXTLINE(readability/identifiers) - struct timeval tv; - // NOLINTNEXTLINE(readability/identifiers) - struct timezone tz; - - gettimeofday(&tv, &tz); - - return absolute_timet(tv.tv_usec/1000+(unsigned long long)tv.tv_sec*1000); -} - -std::ostream &operator << (std::ostream &out, const time_periodt &period) -{ - return out << static_cast(period.get_t())/1000; -} - -std::string time_periodt::as_string() const -{ - std::ostringstream out; - out << *this; - return out.str(); -} diff --git a/src/util/time_stopping.h b/src/util/time_stopping.h deleted file mode 100644 index 7a7dcd20014..00000000000 --- a/src/util/time_stopping.h +++ /dev/null @@ -1,110 +0,0 @@ -/*******************************************************************\ - -Module: Time Stopping - -Author: Daniel Kroening - -Date: February 2004 - -\*******************************************************************/ - -/// \file -/// Time Stopping - -#ifndef CPROVER_UTIL_TIME_STOPPING_H -#define CPROVER_UTIL_TIME_STOPPING_H - -#include -#include - -class fine_timet -{ -public: - fine_timet():t(0) - { - } - - explicit fine_timet(unsigned long long _t):t(_t) - { - } - - unsigned long long get_t() const - { - return t; - } - - void clear() - { - t=0; - } - -protected: - unsigned long long t; -}; - -class time_periodt:public fine_timet -{ -public: - time_periodt() - { - } - - explicit time_periodt(unsigned long long _t):fine_timet(_t) - { - } - - std::string as_string() const; - - time_periodt &operator+=(const time_periodt &other) - { - t+=other.t; - return *this; - } - - time_periodt operator+(const time_periodt &other) - { - time_periodt tmp=*this; - tmp.t+=other.t; - return tmp; - } - - time_periodt operator-(const time_periodt &other) - { - return time_periodt(t-other.t); - } - - friend class absolute_timet; -}; - -class absolute_timet:public fine_timet -{ -public: - absolute_timet() - { - } - - explicit absolute_timet(unsigned long long _t):fine_timet(_t) - { - } - - time_periodt operator-(const absolute_timet &other) - { - return time_periodt(t-other.t); - } - - absolute_timet operator+(const time_periodt &other) - { - return absolute_timet(t+other.t); - } - - bool operator>=(const absolute_timet &other) - { - return t>=other.t; - } -}; - -absolute_timet current_time(); - -std::ostream &operator << (std::ostream &, const time_periodt &); - -#endif // CPROVER_UTIL_TIME_STOPPING_H diff --git a/src/util/timer.cpp b/src/util/timer.cpp deleted file mode 100644 index 095947a65d3..00000000000 --- a/src/util/timer.cpp +++ /dev/null @@ -1,45 +0,0 @@ -/*******************************************************************\ - -Module: Time Stopping - -Author: - -Date: - -\*******************************************************************/ - -/// \file -/// Time Stopping - -#include "timer.h" - -#include -#include - -timert::~timert() -{ -} - -void timert::start() -{ - assert(!started); - started = true; - - _start_time = current_time(); - nr_starts++; -} - -void timert::stop() -{ - assert(started); - started = false; - - _latest_time = current_time() - _start_time; - _total_time += _latest_time; -} - -void timert::clear() -{ - _total_time.clear(); - _start_time.clear(); -} diff --git a/src/util/timer.h b/src/util/timer.h deleted file mode 100644 index 79d60082f65..00000000000 --- a/src/util/timer.h +++ /dev/null @@ -1,76 +0,0 @@ -/*******************************************************************\ - -Module: Time Stopping - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Time Stopping - -#ifndef CPROVER_UTIL_TIMER_H -#define CPROVER_UTIL_TIMER_H - -#include -#include - -#include "time_stopping.h" - -class timert -{ -private: - time_periodt _total_time; - absolute_timet _start_time; - time_periodt _latest_time; - long nr_starts; - bool started; - -public: - timert(): - _total_time(0), - _start_time(0), - _latest_time(0), - nr_starts(0), - started(false) - { - } - - virtual ~timert(); - - virtual void start(); - virtual void stop(); - virtual void clear(); - - virtual time_periodt total_time() const - { - return _total_time; - } - - virtual fine_timet latest_time() const - { - return _latest_time; - } - - virtual long number_starts() const - { - return nr_starts; - } - - std::string output_total_time() const - { - return _total_time.as_string(); - } - - std::string output_latest_time() const - { - return _latest_time.as_string(); - } -}; - -std::ostream &operator<<(std::ostream &out, const timert &timer) -{ - return out << timer.total_time(); -} - -#endif // CPROVER_UTIL_TIMER_H From 82549de2a0c7e3e6c5d4680a5b9958ad126cf1e8 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Thu, 8 Feb 2018 03:42:22 +0000 Subject: [PATCH 2/2] Emit timestamps on each line of output This commit adds the --timestamp command line option to allow cprover tools to emit timestamps before each line of output. The timestamps are either pretty-formatted wall-clock times (which may decrease as time passes in the event of a leap-second or daylight savings time event), or raw numbers that are guaranteed to increase. In either case, the timestamps have microsecond precision if supported by the underlying platform. --- src/cbmc/cbmc_parse_options.cpp | 1 + src/cbmc/cbmc_parse_options.h | 2 + .../goto_analyzer_parse_options.cpp | 1 + .../goto_analyzer_parse_options.h | 2 + src/goto-diff/goto_diff_parse_options.cpp | 1 + src/goto-diff/goto_diff_parse_options.h | 2 + .../goto_instrument_parse_options.cpp | 1 + .../goto_instrument_parse_options.h | 2 + src/jbmc/jbmc_parse_options.cpp | 1 + src/jbmc/jbmc_parse_options.h | 2 + src/util/Makefile | 1 + src/util/timestamper.cpp | 73 ++++++++++++++++ src/util/timestamper.h | 84 +++++++++++++++++++ src/util/ui_message.cpp | 28 +++++-- src/util/ui_message.h | 15 +++- 15 files changed, 204 insertions(+), 12 deletions(-) create mode 100644 src/util/timestamper.cpp create mode 100644 src/util/timestamper.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c6f0edfc9ee..3496c6bf8ec 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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 } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 60e112da456..658c552c22e 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -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)" \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index fc37947e56a..2e4a97b3b0e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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"; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index dc5c8cdf80d..d47f4ae91d3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -103,6 +103,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -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)" \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 2f5701dde02..87e8c98e5d2 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/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"; } diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index a79cd064706..8eb8e58f1c2 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/src/goto-diff/goto_diff_parse_options.h @@ -14,6 +14,7 @@ Author: Peter Schrammel #include #include +#include #include #include @@ -27,6 +28,7 @@ class optionst; "(json-ui)" \ OPT_SHOW_GOTO_FUNCTIONS \ "(verbosity):(version)" \ + OPT_TIMESTAMP \ "u(unified)(change-impact)(forward-impact)(backward-impact)" \ "(compact-output)" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 12259330c49..a98acd741f6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1568,5 +1568,6 @@ void goto_instrument_parse_optionst::help() " --version show version and exit\n" " --xml-ui use XML-formatted output\n" " --json-ui use JSON-formatted output\n" + HELP_TIMESTAMP "\n"; } diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5f17c96fca1..19acc24b44f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -66,6 +67,7 @@ Author: Daniel Kroening, kroening@kroening.com "(show-claims)(show-properties)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ "(cav11)" \ + OPT_TIMESTAMP \ "(show-natural-loops)(accelerate)(havoc-loops)" \ "(error-label):(string-abstraction)" \ "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index b0889adb4cb..f397bbaf812 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -956,5 +956,6 @@ void jbmc_parse_optionst::help() " --json-ui use JSON-formatted output\n" HELP_GOTO_TRACE " --verbosity # verbosity level\n" + HELP_TIMESTAMP "\n"; } diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index aa221424d9c..362011b8f33 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -60,6 +61,7 @@ class optionst; "(verbosity):" \ "(version)" \ "(cover):(symex-coverage-report):" \ + OPT_TIMESTAMP \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \ "(ppc-macos)" \ "(arrays-uf-always)(arrays-uf-never)" \ diff --git a/src/util/Makefile b/src/util/Makefile index 39daadcf024..f347bd73aae 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -84,6 +84,7 @@ SRC = arith_tools.cpp \ tempdir.cpp \ tempfile.cpp \ threeval.cpp \ + timestamper.cpp \ type.cpp \ type_eq.cpp \ typecheck.cpp \ diff --git a/src/util/timestamper.cpp b/src/util/timestamper.cpp new file mode 100644 index 00000000000..8ffb05ea1b3 --- /dev/null +++ b/src/util/timestamper.cpp @@ -0,0 +1,73 @@ +/*******************************************************************\ + +Module: Timestamps + +Author: Kareem Khazem + +\*******************************************************************/ + +#include "timestamper.h" + +#include +#include +#include +#include + +#include "invariant.h" + +std::unique_ptr +timestampert::make(timestampert::clockt clock_type) +{ +#ifdef _WIN32 + return std::unique_ptr(new timestampert()); +#else + switch(clock_type) + { + case timestampert::clockt::NONE: + return std::unique_ptr(new timestampert()); + case timestampert::clockt::MONOTONIC: + return std::unique_ptr( + new monotonic_timestampert()); + case timestampert::clockt::WALL_CLOCK: + return std::unique_ptr( + new wall_clock_timestampert()); + } + UNREACHABLE; +#endif +} + +#ifndef _WIN32 +std::string monotonic_timestampert::stamp() const +{ + std::chrono::time_point + time_stamp = std::chrono::time_point_cast( + std::chrono::steady_clock::now()); + + auto cnt = time_stamp.time_since_epoch().count(); + std::lldiv_t divmod = lldiv(cnt, 1000000); + + std::stringstream ss; + ss << divmod.quot << "." << std::setfill('0') << std::setw(6) << divmod.rem + << " "; + return ss.str(); +} + +#define WALL_FORMAT "%Y-%m-%dT%H:%M:%S." + +std::string wall_clock_timestampert::stamp() const +{ + std::chrono::time_point + time_stamp = std::chrono::time_point_cast( + std::chrono::system_clock::now()); + + unsigned u_seconds = time_stamp.time_since_epoch().count() % 1000000; + + std::time_t tt = std::chrono::system_clock::to_time_t(time_stamp); + std::tm local = *std::localtime(&tt); + + std::stringstream ss; + ss << std::put_time(&local, WALL_FORMAT) << std::setfill('0') << std::setw(6) + << u_seconds << " "; + return ss.str(); +} +#endif diff --git a/src/util/timestamper.h b/src/util/timestamper.h new file mode 100644 index 00000000000..9adc0beb8c7 --- /dev/null +++ b/src/util/timestamper.h @@ -0,0 +1,84 @@ +/// \file timestamper.h +/// \brief Emit timestamps +/// \author Kareem Khazem + +#ifndef CPROVER_UTIL_TIMESTAMPER_H +#define CPROVER_UTIL_TIMESTAMPER_H + +#ifdef _WIN32 +#define OPT_TIMESTAMP "" +#define HELP_TIMESTAMP "" +#else +#define OPT_TIMESTAMP "(timestamp):" + +#define HELP_TIMESTAMP \ + " --timestamp print microsecond-precision timestamps.\n" \ + " monotonic: stamps increase monotonically.\n" \ + " wall: ISO-8601 wall clock timestamps.\n" +#endif + +#include +#include + +/// \brief Timestamp class hierarchy +/// +/// This class hierarchy supports generation of timestamps in various textual +/// formats. The timestamps returned by instances of this class are empty; more +/// meaningful timestamps are returned by derived classes. +/// +/// Instances of this class can be instantiated to emit empty timestamps, in +/// case the user did not specify `--timestamp` on the command line. The +/// intended use of this class hierarchy is to create a pointer or +/// std::unique_ptr called `time` to a timestampert, and to initialize `time` +/// with either an actual \ref timestampert object or one of the derived +/// classes based on whether the user has asked for timestamps to be emitted. +/// Clients can thus unconditionally call `time->stamp()` and prepend that +/// string to any logging messages; if the user didn't ask for timestamps, then +/// the object pointed to by `time` will be a \ref timestampert and thus +/// timestampert::stamp() will return only an empty string. Derived classes +/// emit an actual timestamp followed by a space, so no conditional checking is +/// needed by the client. +class timestampert +{ +public: + /// \brief Derived types of \ref timestampert + enum class clockt + { + /// \ref timestampert + NONE, + /// monotonic_timestampert + MONOTONIC, + /// wall_clock_timestampert + WALL_CLOCK + }; + virtual ~timestampert() = default; + + /// \brief Default timestamp: the empty string + virtual std::string stamp() const + { + return ""; + } + + /// \brief Factory method to build timestampert subclasses + static std::unique_ptr make(clockt clock_type); +}; + +#ifndef _WIN32 +class monotonic_timestampert : public timestampert +{ +public: + /// \brief See \ref HELP_TIMESTAMP in util/timestamper.h for time + /// stamp format + virtual std::string stamp() const override; +}; + +class wall_clock_timestampert : public timestampert +{ +public: + /// \brief See \ref HELP_TIMESTAMP in util/timestamper.h for time + /// stamp format + virtual std::string stamp() const override; +}; +#endif + +#endif /* CPROVER_UTIL_TIMESTAMPER_H */ diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 9aa7a3749d3..1ba79f34db4 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -19,7 +19,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "cmdline.h" ui_message_handlert::ui_message_handlert( - uit __ui, const std::string &program):_ui(__ui) + uit __ui, + const std::string &program, + timestampert::clockt clock_type) + : _ui(__ui), time(timestampert::make(clock_type)) { switch(__ui) { @@ -52,12 +55,19 @@ ui_message_handlert::ui_message_handlert( ui_message_handlert::ui_message_handlert( const class cmdlinet &cmdline, - const std::string &program): - ui_message_handlert( - cmdline.isset("xml-ui")?uit::XML_UI: - cmdline.isset("json-ui")?uit::JSON_UI: - uit::PLAIN, - program) + const std::string &program) + : ui_message_handlert( + cmdline.isset("xml-ui") ? uit::XML_UI : cmdline.isset("json-ui") + ? uit::JSON_UI + : uit::PLAIN, + program, + cmdline.isset("timestamp") + ? cmdline.get_value("timestamp") == "monotonic" + ? timestampert::clockt::MONOTONIC + : cmdline.get_value("timestamp") == "wall" + ? timestampert::clockt::WALL_CLOCK + : timestampert::clockt::NONE + : timestampert::clockt::NONE) { } @@ -99,7 +109,9 @@ void ui_message_handlert::print( case uit::PLAIN: { console_message_handlert console_message_handler; - console_message_handler.print(level, message); + std::stringstream ss; + ss << time->stamp() << message; + console_message_handler.print(level, ss.str()); } break; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 422633e1f40..e3886961385 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -11,16 +11,22 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_UI_MESSAGE_H #include "message.h" +#include "timestamper.h" -class ui_message_handlert:public message_handlert +class ui_message_handlert : public message_handlert { public: enum class uit { PLAIN, XML_UI, JSON_UI }; - ui_message_handlert(uit, const std::string &program); + ui_message_handlert( + uit, + const std::string &program, + timestampert::clockt clock_type); + ui_message_handlert(const class cmdlinet &, const std::string &program); - ui_message_handlert(): - _ui(uit::PLAIN) + + ui_message_handlert() + : _ui(uit::PLAIN), time(timestampert::make(timestampert::clockt::NONE)) { } @@ -40,6 +46,7 @@ class ui_message_handlert:public message_handlert protected: uit _ui; + std::unique_ptr time; virtual void print( unsigned level,