Console colors

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"))
       {

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())
   {

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

src/util/cout_message.cpp

@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <io.h>
 #include <cstdio>
 #include <util/pragma_pop.def>
+#else
+#include <unistd.h>
 #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)
@@ -118,14 +154,16 @@ 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";
   }
 
   if(!line.empty())
   {
+    dest += command(1); // bold
+
     if(!file.empty())
       dest+=id2string(file)+":";
 
@@ -137,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;

src/util/cout_message.h

@@ -36,20 +36,25 @@ 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
+class gcc_message_handlert : public console_message_handlert
 {
 public:
   // aims to imitate the messages gcc prints

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<std::size_t> 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;

src/util/ui_message.cpp

@@ -11,21 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <iostream>
 
-#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<console_message_handlert>(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;
   }
 }

src/util/ui_message.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <memory>
 
-#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_handlert> console_message_handler;
   message_handlert *message_handler;
   uit _ui;
   const bool always_flush;
@@ -88,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)"