From f06b5632ea0bab3e34ed0e0db9d48c0cdd1ced1a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Sep 2018 16:22:04 +0100 Subject: [PATCH 1/5] ui_message_handlert retains console_message_handlert object --- src/util/ui_message.cpp | 52 ++++++++++++++--------------------------- src/util/ui_message.h | 3 ++- 2 files changed, 20 insertions(+), 35 deletions(-) diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 2e99eec0dd7..e3a9ea4903e 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -11,21 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "xml.h" +#include "cmdline.h" #include "json.h" -#include "xml_expr.h" #include "json_expr.h" #include "json_stream.h" -#include "cout_message.h" -#include "cmdline.h" +#include "make_unique.h" +#include "xml.h" +#include "xml_expr.h" ui_message_handlert::ui_message_handlert( - message_handlert *message_handler, + message_handlert *_message_handler, uit __ui, const std::string &program, bool always_flush, timestampert::clockt clock_type) - : message_handler(message_handler), + : message_handler(_message_handler), _ui(__ui), always_flush(always_flush), time(timestampert::make(clock_type)), @@ -80,6 +80,12 @@ ui_message_handlert::ui_message_handlert( : timestampert::clockt::NONE : timestampert::clockt::NONE) { + if(get_ui() == uit::PLAIN) + { + console_message_handler = + util_make_unique(always_flush); + message_handler = &*console_message_handler; + } } ui_message_handlert::ui_message_handlert(message_handlert &message_handler) @@ -132,19 +138,9 @@ void ui_message_handlert::print( std::stringstream ss; const std::string timestamp = time->stamp(); ss << timestamp << (timestamp.empty() ? "" : " ") << message; - if(message_handler) - { - message_handler->print(level, ss.str()); - if(always_flush) - message_handler->flush(level); - } - else - { - console_message_handlert msg(always_flush); - msg.print(level, ss.str()); - if(always_flush) - msg.flush(level); - } + message_handler->print(level, ss.str()); + if(always_flush) + message_handler->flush(level); } break; @@ -306,24 +302,12 @@ void ui_message_handlert::flush(unsigned level) switch(get_ui()) { case uit::PLAIN: - { - if(message_handler) - { - message_handler->flush(level); - } - else - { - console_message_handlert msg(always_flush); - msg.flush(level); - } - } - break; + message_handler->flush(level); + break; case uit::XML_UI: case uit::JSON_UI: - { out << std::flush; - } - break; + break; } } diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 8278eaa4937..ab00b82e370 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "message.h" +#include "cout_message.h" #include "json_stream.h" #include "timestamper.h" @@ -41,6 +41,7 @@ class ui_message_handlert : public message_handlert } protected: + std::unique_ptr console_message_handler; message_handlert *message_handler; uit _ui; const bool always_flush; From 33569fa0adbdd651378dda99dba8f45f826f92be Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Sep 2018 14:33:14 +0100 Subject: [PATCH 2/5] added a message color API This enables colorful formatting of any message printed through the messaget API. Server-side implementation is provided for Windows and Unix consoles. --- src/util/cout_message.cpp | 36 ++++++++++++++++++++++++++ src/util/cout_message.h | 15 +++++++---- src/util/message.h | 53 +++++++++++++++++++++++++++++++++++++++ src/util/ui_message.h | 8 ++++++ 4 files changed, 107 insertions(+), 5 deletions(-) diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index ca85873dacc..beaa6a2c244 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#else +#include #endif #include "unicode.h" @@ -35,6 +37,40 @@ cerr_message_handlert::cerr_message_handlert(): { } +console_message_handlert::console_message_handlert(bool _always_flush) + : always_flush(_always_flush), is_a_tty(false), use_SGR(false) +{ +#ifdef _WIN32 + HANDLE out_handle=GetStdHandle(STD_OUTPUT_HANDLE); + + DWORD consoleMode; + if(GetConsoleMode(out_handle, &consoleMode)) + { + is_a_tty = true; + +#ifdef ENABLE_VIRTUAL_TERMINAL_PROCESSING + consoleMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING; + if(SetConsoleMode(out_handle, consoleMode)) + use_SGR = true; +#endif + } +#else + is_a_tty = isatty(STDOUT_FILENO); + use_SGR = is_a_tty; +#endif +} + +/// Create an ECMA-48 SGR (Select Graphic Rendition) command with +/// given code. +/// \param c: ECMA-48 command code +std::string console_message_handlert::command(unsigned c) const +{ + if(!use_SGR) + return std::string(); + + return "\x1b[" + std::to_string(c) + 'm'; +} + void console_message_handlert::print( unsigned level, const std::string &message) diff --git a/src/util/cout_message.h b/src/util/cout_message.h index 913de68fd2c..ce870b07b2d 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -36,17 +36,22 @@ class console_message_handlert : public message_handlert virtual void flush(unsigned level) override; - console_message_handlert() : always_flush(false) + console_message_handlert() : console_message_handlert(false) { } - explicit console_message_handlert(bool always_flush) - : always_flush(always_flush) - { - } + explicit console_message_handlert(bool always_flush); + + std::string command(unsigned c) const override; protected: const bool always_flush; + + /// true if we are outputting to a proper console + bool is_a_tty; + + /// true if we use ECMA-48 SGR to render colors + bool use_SGR; }; class gcc_message_handlert : public message_handlert diff --git a/src/util/message.h b/src/util/message.h index 09f3e098f7d..556f0d13bc1 100644 --- a/src/util/message.h +++ b/src/util/message.h @@ -65,6 +65,13 @@ class message_handlert return message_count[level]; } + /// \brief Create an ECMA-48 SGR (Select Graphic Rendition) command. + /// The default behavior is no action. + virtual std::string command(unsigned) const + { + return std::string(); + } + protected: unsigned verbosity; std::vector message_count; @@ -275,6 +282,52 @@ class messaget return m; } + /// \brief Create an ECMA-48 SGR (Select Graphic Rendition) command. + std::string command(unsigned c) const + { + if(message_handler) + return message_handler->command(c); + else + return std::string(); + } + + /// return to default formatting, + /// as defined by the terminal + std::string reset() const + { + return command(0); + } + + /// render text with red foreground color + std::string red() const + { + return command(31); + } + + /// render text with green foreground color + std::string green() const + { + return command(32); + } + + /// render text with yellow foreground color + std::string yellow() const + { + return command(33); + } + + /// render text with blue foreground color + std::string blue() const + { + return command(34); + } + + /// render text with bold font + std::string bold() const + { + return command(1); + } + mstreamt &get_mstream(unsigned message_level) const { mstream.message_level=message_level; diff --git a/src/util/ui_message.h b/src/util/ui_message.h index ab00b82e370..5abe1a2fb32 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -89,6 +89,14 @@ class ui_message_handlert : public message_handlert const source_locationt &location); const char *level_string(unsigned level); + + std::string command(unsigned c) const override + { + if(message_handler) + return message_handler->command(c); + else + return std::string(); + } }; #define OPT_FLUSH "(flush)" From f133a25f9361067e6cd20fc7db6a89e362184255 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Sep 2018 15:44:39 +0100 Subject: [PATCH 3/5] use colors in BMC status reporting Failed properties are red, passing ones are green, and the overall result is in bold. --- src/cbmc/all_properties.cpp | 13 ++++++++++--- src/cbmc/bmc.cpp | 4 ++-- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 126be18cf3d..babce3bed60 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -159,10 +159,17 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) result() << "\n** Results:" << eom; for(const auto &goal_pair : goal_map) + { result() << "[" << goal_pair.first << "] " - << goal_pair.second.description << ": " - << goal_pair.second.status_string() - << eom; + << goal_pair.second.description << ": "; + + if(goal_pair.second.status == goalt::statust::SUCCESS) + result() << green(); + else + result() << red(); + + result() << goal_pair.second.status_string() << reset() << eom; + } if(bmc.options.get_bool_option("trace")) { diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 48a8e2784d3..a574426cd73 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -153,7 +153,7 @@ bmct::run_decision_procedure(prop_convt &prop_conv) void bmct::report_success() { - result() << "VERIFICATION SUCCESSFUL" << eom; + result() << bold() << "VERIFICATION SUCCESSFUL" << reset() << eom; switch(ui_message_handler.get_ui()) { @@ -180,7 +180,7 @@ void bmct::report_success() void bmct::report_failure() { - result() << "VERIFICATION FAILED" << eom; + result() << bold() << "VERIFICATION FAILED" << reset() << eom; switch(ui_message_handler.get_ui()) { From b27c1e86bd4b0105255c636b63dae1cdde85accd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Sep 2018 16:30:54 +0100 Subject: [PATCH 4/5] use colors in gcc personality This mimicks what newer versions of gcc do. --- src/util/cout_message.cpp | 10 +++++++--- src/util/cout_message.h | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp index beaa6a2c244..3973d243ed9 100644 --- a/src/util/cout_message.cpp +++ b/src/util/cout_message.cpp @@ -154,7 +154,7 @@ void gcc_message_handlert::print( if(!function.empty()) { if(!file.empty()) - dest+=id2string(file)+":"; + dest += command(1) + id2string(file) + ":" + command(0); // bold if(dest!="") dest+=' '; dest+="In function '"+id2string(function)+"':\n"; @@ -162,6 +162,8 @@ void gcc_message_handlert::print( if(!line.empty()) { + dest += command(1); // bold + if(!file.empty()) dest+=id2string(file)+":"; @@ -173,9 +175,11 @@ void gcc_message_handlert::print( dest+=id2string(column)+": "; if(level==messaget::M_ERROR) - dest+="error: "; + dest += command(31) + "error: "; // red else if(level==messaget::M_WARNING) - dest+="warning: "; + dest += command(95) + "warning: "; // bright magenta + + dest += command(0); // reset } dest+=message; diff --git a/src/util/cout_message.h b/src/util/cout_message.h index ce870b07b2d..e41451d05fd 100644 --- a/src/util/cout_message.h +++ b/src/util/cout_message.h @@ -54,7 +54,7 @@ class console_message_handlert : public message_handlert bool use_SGR; }; -class gcc_message_handlert : public message_handlert +class gcc_message_handlert : public console_message_handlert { public: // aims to imitate the messages gcc prints From d999a3e6f9b7fe55f0228e257f3a46dcd3d90f83 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 21 Sep 2018 19:48:42 +0100 Subject: [PATCH 5/5] use formatting in goto-analyzer the summary result is now bold --- src/goto-analyzer/static_verifier.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index d73880f1bd5..8abca993966 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -232,22 +232,22 @@ bool static_verifier( if(e.is_true()) { - m.result() << "Success"; + m.result() << m.green() << "Success" << m.reset(); pass++; } else if(e.is_false()) { - m.result() << "Failure (if reachable)"; + m.result() << m.red() << "Failure" << m.reset() << " (if reachable)"; fail++; } else if(domain.is_bottom()) { - m.result() << "Success (unreachable)"; + m.result() << m.green() << "Success" << m.reset() << " (unreachable)"; pass++; } else { - m.result() << "Unknown"; + m.result() << m.yellow() << "Unknown" << m.reset(); unknown++; } @@ -258,10 +258,11 @@ bool static_verifier( } } - m.status() << "Summary: " + m.status() << m.bold() << "Summary: " << pass << " pass, " << fail << " fail if reachable, " - << unknown << " unknown\n"; + << unknown << " unknown" + << m.reset() << messaget::eom; return false; }