Add --flush option to flush all output

Author: karkhaz

src/cbmc/cbmc_parse_options.cpp

@@ -990,6 +990,7 @@ void cbmc_parse_optionst::help()
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
     HELP_GOTO_TRACE
+    HELP_FLUSH
     " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
     "\n";

src/cbmc/cbmc_parse_options.h

@@ -71,6 +71,7 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
+  OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1573,6 +1573,7 @@ void goto_instrument_parse_optionst::help()
     " --use-all-headers            with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
     " --harness                    with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
     " --version                    show version and exit\n"
+    HELP_FLUSH
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
     HELP_TIMESTAMP

src/goto-instrument/goto_instrument_parse_options.h

@@ -85,6 +85,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
+  OPT_FLUSH \
   "(splice-call):" \
   OPT_REMOVE_CALLS_NO_BODY
 // clang-format on

src/jbmc/jbmc_parse_options.cpp

@@ -1083,6 +1083,7 @@ void jbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
     HELP_GOTO_TRACE
+    HELP_FLUSH
     " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
     "\n";

src/jbmc/jbmc_parse_options.h

@@ -71,6 +71,7 @@ class optionst;
   "(ppc-macos)" \
   "(arrays-uf-always)(arrays-uf-never)" \
   "(no-arch)(arch):" \
+  OPT_FLUSH \
   JAVA_BYTECODE_LANGUAGE_OPTIONS \
   "(java-unwind-enum-static)" \
   "(localize-faults)(localize-faults-method):" \

src/util/cout_message.cpp

@@ -90,7 +90,7 @@ void console_message_handlert::flush(unsigned level)
   // in particular when writing to NFS.
   if(level>=4)
   {
-    if(level<=6)
+    if(level <= 6 || always_flush)
       std::cout << std::flush;
   }
   else

src/util/cout_message.h

@@ -35,6 +35,18 @@ class console_message_handlert:public ui_message_handlert
     const std::string &message) override;
 
   virtual void flush(unsigned level) override;
+
+  console_message_handlert() : always_flush(false)
+  {
+  }
+
+  explicit console_message_handlert(bool always_flush)
+    : always_flush(always_flush)
+  {
+  }
+
+protected:
+  const bool always_flush;
 };
 
 class gcc_message_handlert:public ui_message_handlert

src/util/ui_message.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 ui_message_handlert::ui_message_handlert()
   : _ui(uit::PLAIN),
+    always_flush(false),
     time(timestampert::make(timestampert::clockt::NONE)),
     out(std::cout),
     json_stream(nullptr)
@@ -30,8 +31,10 @@ ui_message_handlert::ui_message_handlert()
 ui_message_handlert::ui_message_handlert(
   uit __ui,
   const std::string &program,
+  bool always_flush,
   timestampert::clockt clock_type)
   : _ui(__ui),
+    always_flush(always_flush),
     time(timestampert::make(clock_type)),
     out(std::cout),
     json_stream(nullptr)
@@ -79,6 +82,7 @@ ui_message_handlert::ui_message_handlert(
                                                 ? uit::JSON_UI
                                                 : uit::PLAIN,
       program,
+      cmdline.isset("flush"),
       cmdline.isset("timestamp")
         ? cmdline.get_value("timestamp") == "monotonic"
             ? timestampert::clockt::MONOTONIC
@@ -130,11 +134,13 @@ void ui_message_handlert::print(
     {
     case uit::PLAIN:
     {
-      console_message_handlert console_message_handler;
+      console_message_handlert console_message_handler(always_flush);
       std::stringstream ss;
       const std::string timestamp = time->stamp();
       ss << timestamp << (timestamp.empty() ? "" : " ") << message;
       console_message_handler.print(level, ss.str());
+      if(always_flush)
+        console_message_handler.flush(level);
     }
     break;
 
@@ -274,6 +280,8 @@ void ui_message_handlert::xml_ui_msg(
 
   out << result;
   out << '\n';
+  if(always_flush)
+    flush(1);
 }
 
 void ui_message_handlert::json_ui_msg(
@@ -299,6 +307,8 @@ void ui_message_handlert::json_ui_msg(
   // The first entry is generated in the constructor and does not have
   //  a trailing comma.
   std::cout << ",\n" << result;
+  if(always_flush)
+    flush(1);
 }
 
 void ui_message_handlert::flush(unsigned level)
@@ -307,7 +317,7 @@ void ui_message_handlert::flush(unsigned level)
   {
   case uit::PLAIN:
   {
-    console_message_handlert console_message_handler;
+    console_message_handlert console_message_handler(always_flush);
     console_message_handler.flush(level);
   }
   break;

src/util/ui_message.h

@@ -24,6 +24,7 @@ class ui_message_handlert : public message_handlert
   ui_message_handlert(
     uit,
     const std::string &program,
+    bool always_flush,
     timestampert::clockt clock_type);
 
   ui_message_handlert(const class cmdlinet &, const std::string &program);
@@ -57,6 +58,7 @@ class ui_message_handlert : public message_handlert
 
 protected:
   uit _ui;
+  const bool always_flush;
   std::unique_ptr<const timestampert> time;
   std::ostream &out;
   std::unique_ptr<json_stream_arrayt> json_stream;
@@ -100,4 +102,8 @@ class ui_message_handlert : public message_handlert
   const char *level_string(unsigned level);
 };
 
+#define OPT_FLUSH "(flush)"
+
+#define HELP_FLUSH " --flush                      flush every line of output\n"
+
 #endif // CPROVER_UTIL_UI_MESSAGE_H