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-analyzer/goto_analyzer_parse_options.cpp

@@ -905,6 +905,7 @@ void goto_analyzer_parse_optionst::help()
     "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
+    HELP_FLUSH
     HELP_TIMESTAMP
     "\n";
   // clang-format on

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -139,6 +139,7 @@ class optionst;
   "(show-local-may-alias)" \
   "(json):(xml):" \
   "(text):(dot):" \
+  OPT_FLUSH \
   OPT_TIMESTAMP \
   "(unreachable-instructions)(unreachable-functions)" \
   "(reachable-functions)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -537,6 +537,7 @@ void goto_diff_parse_optionst::help()
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"
+    HELP_FLUSH
     HELP_TIMESTAMP
     "\n";
   // clang-format on

src/goto-diff/goto_diff_parse_options.h

@@ -35,6 +35,7 @@ class optionst;
   OPT_GOTO_CHECK \
   "(cover):" \
   "(verbosity):(version)" \
+  OPT_FLUSH \
   OPT_TIMESTAMP \
   "u(unified)(change-impact)(forward-impact)(backward-impact)" \
   "(compact-output)"

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, [email protected]
   "(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, [email protected]
 
 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;
 
@@ -144,6 +150,8 @@ void ui_message_handlert::print(
       source_locationt location;
       location.make_nil();
       print(level, message, -1, location);
+      if(always_flush)
+        flush(level);
     }
     break;
     }
@@ -225,14 +233,15 @@ void ui_message_handlert::print(
       std::string sequence_number_str=
         sequence_number>=0?std::to_string(sequence_number):"";
 
-      ui_msg(type, tmp_message, sequence_number_str, location);
+      ui_msg(level, type, tmp_message, sequence_number_str, location);
     }
     break;
     }
   }
 }
 
 void ui_message_handlert::ui_msg(
+  const unsigned level,
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
@@ -244,7 +253,7 @@ void ui_message_handlert::ui_msg(
     break;
 
   case uit::XML_UI:
-    xml_ui_msg(type, msg1, msg2, location);
+    xml_ui_msg(level, type, msg1, msg2, location);
     break;
 
   case uit::JSON_UI:
@@ -254,6 +263,7 @@ void ui_message_handlert::ui_msg(
 }
 
 void ui_message_handlert::xml_ui_msg(
+  const unsigned level,
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
@@ -274,6 +284,8 @@ void ui_message_handlert::xml_ui_msg(
 
   out << result;
   out << '\n';
+  if(always_flush)
+    flush(level);
 }
 
 void ui_message_handlert::json_ui_msg(
@@ -302,7 +314,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,
+    const 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;
@@ -80,6 +82,7 @@ class ui_message_handlert : public message_handlert
     const jsont &data) override;
 
   virtual void xml_ui_msg(
+    const unsigned level,
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
@@ -92,6 +95,7 @@ class ui_message_handlert : public message_handlert
     const source_locationt &location);
 
   virtual void ui_msg(
+    const unsigned level,
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
@@ -100,4 +104,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