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,