From 1ef0f418377888ac164324a5811e3a5ec4f01210 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Mon, 11 Dec 2017 15:36:43 -0500 Subject: [PATCH] Add --flush option to flush all output --- src/cbmc/cbmc_parse_options.cpp | 1 + src/cbmc/cbmc_parse_options.h | 1 + src/goto-analyzer/goto_analyzer_parse_options.cpp | 1 + src/goto-analyzer/goto_analyzer_parse_options.h | 1 + src/goto-diff/goto_diff_parse_options.cpp | 1 + src/goto-diff/goto_diff_parse_options.h | 1 + .../goto_instrument_parse_options.cpp | 1 + src/goto-instrument/goto_instrument_parse_options.h | 1 + src/jbmc/jbmc_parse_options.cpp | 1 + src/jbmc/jbmc_parse_options.h | 1 + src/util/cout_message.cpp | 2 +- src/util/cout_message.h | 12 ++++++++++++ src/util/ui_message.cpp | 12 ++++++++++-- src/util/ui_message.h | 6 ++++++ 14 files changed, 39 insertions(+), 3 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 100c83c2abf..b6fcdd40bd2 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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"; diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 9a47b4eed2c..a26eb567bf5 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/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) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 2e7cddeb793..423ff55c7a9 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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 diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index ab1ff8b90cf..f4cc5447f12 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/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)" \ diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 232ebf029b3..7a404c27f0e 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/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 diff --git a/src/goto-diff/goto_diff_parse_options.h b/src/goto-diff/goto_diff_parse_options.h index 48dcb89aa43..2992b1ab615 100644 --- a/src/goto-diff/goto_diff_parse_options.h +++ b/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)" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d5224337440..697a31ad529 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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 diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 4c9ead8d0dc..b5582e579a0 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/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 diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 25cce4cacd1..ab544f481b6 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/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"; diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 32f7e269465..dbb9cf7253e 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/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):" \ diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index 5221fda0f21..44203df75fb 100644 --- a/src/util/cout_message.cpp +++ b/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 diff --git a/src/util/cout_message.h b/src/util/cout_message.h index 39d4bddd349..d17f67e3eec 100644 --- a/src/util/cout_message.h +++ b/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 diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 83c5473fe78..f97aa30deeb 100644 --- a/src/util/ui_message.cpp +++ b/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; @@ -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; } @@ -302,7 +310,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; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 62756df777e..abccf9504a7 100644 --- a/src/util/ui_message.h +++ b/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 time; std::ostream &out; std::unique_ptr 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