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

@@ -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/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";
 }

src/goto-diff/goto_diff_parse_options.h

@@ -14,6 +14,7 @@ Author: Peter Schrammel
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/timestamper.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
@@ -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)"
 

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";
 }

src/goto-instrument/goto_instrument_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 <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
@@ -66,6 +67,7 @@ Author: Daniel Kroening, [email protected]
   "(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)" \

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";
 }

src/jbmc/jbmc_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>
 
@@ -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)" \

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 \

src/util/timestamper.cpp

@@ -0,0 +1,73 @@
+/*******************************************************************\
+
+Module: Timestamps
+
+Author: Kareem Khazem <[email protected]>
+
+\*******************************************************************/
+
+#include "timestamper.h"
+
+#include <chrono>
+#include <cstdlib>
+#include <iomanip>
+#include <sstream>
+
+#include "invariant.h"
+
+std::unique_ptr<const timestampert>
+timestampert::make(timestampert::clockt clock_type)
+{
+#ifdef _WIN32
+  return std::unique_ptr<const timestampert>(new timestampert());
+#else
+  switch(clock_type)
+  {
+  case timestampert::clockt::NONE:
+    return std::unique_ptr<const timestampert>(new timestampert());
+  case timestampert::clockt::MONOTONIC:
+    return std::unique_ptr<const monotonic_timestampert>(
+      new monotonic_timestampert());
+  case timestampert::clockt::WALL_CLOCK:
+    return std::unique_ptr<const wall_clock_timestampert>(
+      new wall_clock_timestampert());
+  }
+  UNREACHABLE;
+#endif
+}
+
+#ifndef _WIN32
+std::string monotonic_timestampert::stamp() const
+{
+  std::chrono::time_point<std::chrono::steady_clock, std::chrono::microseconds>
+    time_stamp = std::chrono::time_point_cast<std::chrono::microseconds>(
+      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<std::chrono::system_clock, std::chrono::microseconds>
+    time_stamp = std::chrono::time_point_cast<std::chrono::microseconds>(
+      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

src/util/timestamper.h

@@ -0,0 +1,84 @@
+/// \file timestamper.h
+/// \brief Emit timestamps
+/// \author Kareem Khazem <[email protected]>
+
+#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 <monotonic|wall> print microsecond-precision timestamps.\n"    \
+  "                              monotonic: stamps increase monotonically.\n"  \
+  "                              wall: ISO-8601 wall clock timestamps.\n"
+#endif
+
+#include <memory>
+#include <string>
+
+/// \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<const timestampert> 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 */

src/util/ui_message.cpp

@@ -19,7 +19,10 @@ Author: Daniel Kroening, [email protected]
 #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;
 

src/util/ui_message.h

@@ -11,16 +11,22 @@ Author: Daniel Kroening, [email protected]
 #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<const timestampert> time;
 
   virtual void print(
     unsigned level,