Base JSON UI message handler upon json_streamt

Author: NlightNFotis

src/util/message.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, [email protected]
 #include "source_location.h"
 #include "xml.h"
 
+class json_stream_arrayt;
+
 class message_handlert
 {
 public:
@@ -33,6 +35,12 @@ class message_handlert
     // no-op by default
   }
 
+  /// Return the underlying JSON stream
+  virtual json_stream_arrayt &get_json_stream()
+  {
+    UNREACHABLE;
+  }
+
   virtual void print(unsigned level, const jsont &json)
   {
     // no-op by default
@@ -232,6 +240,13 @@ class messaget
       return func(*this);
     }
 
+    /// Returns a reference to the top-level JSON array stream
+    json_stream_arrayt &json_stream()
+    {
+      *this << eom; // force end of previous message
+      return message.message_handler->get_json_stream();
+    }
+
   private:
     void assign_from(const mstreamt &other)
     {

src/util/ui_message.cpp

@@ -15,39 +15,57 @@ Author: Daniel Kroening, [email protected]
 #include "json.h"
 #include "xml_expr.h"
 #include "json_expr.h"
+#include "json_stream.h"
 #include "cout_message.h"
 #include "cmdline.h"
 
+ui_message_handlert::ui_message_handlert()
+  : _ui(uit::PLAIN),
+    time(timestampert::make(timestampert::clockt::NONE)),
+    out(std::cout),
+    json_stream(nullptr)
+{
+}
+
 ui_message_handlert::ui_message_handlert(
   uit __ui,
   const std::string &program,
   timestampert::clockt clock_type)
-  : _ui(__ui), time(timestampert::make(clock_type))
+  : _ui(__ui),
+    time(timestampert::make(clock_type)),
+    out(std::cout),
+    json_stream(nullptr)
 {
-  switch(__ui)
+  switch(_ui)
   {
   case uit::PLAIN:
     break;
 
   case uit::XML_UI:
-    std::cout << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" << "\n";
-    std::cout << "<cprover>" << "\n";
+    out << "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
+        << "\n";
+    out << "<cprover>"
+        << "\n";
 
     {
       xmlt program_xml;
       program_xml.name="program";
       program_xml.data=program;
 
-      std::cout << program_xml;
+      out << program_xml;
     }
     break;
 
   case uit::JSON_UI:
     {
-      std::cout << "[\n";
-      json_objectt json_program;
-      json_program["program"] = json_stringt(program);
-      std::cout << json_program;
+      if(!json_stream)
+      {
+        json_stream =
+          std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
+      }
+
+      INVARIANT(json_stream, "JSON stream must be initialized before use");
+      json_stream->push_back().make_object()["program"] = json_stringt(program);
     }
     break;
   }
@@ -76,11 +94,15 @@ ui_message_handlert::~ui_message_handlert()
   switch(get_ui())
   {
   case uit::XML_UI:
-    std::cout << "</cprover>" << "\n";
+
+    out << "</cprover>"
+        << "\n";
     break;
 
   case uit::JSON_UI:
-    std::cout << "\n]\n";
+    INVARIANT(json_stream, "JSON stream must be initialized before use");
+    json_stream->close();
+    out << '\n';
     break;
 
   case uit::PLAIN:
@@ -140,7 +162,7 @@ void ui_message_handlert::print(
       INVARIANT(false, "Cannot print xml data on PLAIN UI");
       break;
     case uit::XML_UI:
-      std::cout << data << '\n';
+      out << data << '\n';
       flush(level);
       break;
     case uit::JSON_UI:
@@ -165,7 +187,8 @@ void ui_message_handlert::print(
       INVARIANT(false, "Cannot print json data on XML UI");
       break;
     case uit::JSON_UI:
-      std::cout << ',' << '\n' << data;
+      INVARIANT(json_stream, "JSON stream must be initialized before use");
+      json_stream->push_back(data);
       flush(level);
       break;
     }
@@ -249,8 +272,8 @@ void ui_message_handlert::xml_ui_msg(
   if(!timestamp.empty())
     result.set_attribute("timestamp", timestamp);
 
-  std::cout << result;
-  std::cout << '\n';
+  out << result;
+  out << '\n';
 }
 
 void ui_message_handlert::json_ui_msg(
@@ -259,7 +282,8 @@ void ui_message_handlert::json_ui_msg(
   const std::string &msg2,
   const source_locationt &location)
 {
-  json_objectt result;
+  INVARIANT(json_stream, "JSON stream must be initialized before use");
+  json_objectt &result = json_stream->push_back().make_object();
 
   if(location.is_not_nil() &&
      !location.get_file().empty())
@@ -291,7 +315,7 @@ void ui_message_handlert::flush(unsigned level)
   case uit::XML_UI:
   case uit::JSON_UI:
   {
-    std::cout << std::flush;
+    out << std::flush;
   }
   break;
   }

src/util/ui_message.h

@@ -10,7 +10,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_UI_MESSAGE_H
 #define CPROVER_UTIL_UI_MESSAGE_H
 
+#include <memory>
+
 #include "message.h"
+#include "json_stream.h"
 #include "timestamper.h"
 
 class ui_message_handlert : public message_handlert
@@ -25,10 +28,8 @@ class ui_message_handlert : public message_handlert
 
   ui_message_handlert(const class cmdlinet &, const std::string &program);
 
-  ui_message_handlert()
-    : _ui(uit::PLAIN), time(timestampert::make(timestampert::clockt::NONE))
-  {
-  }
+  /// Default constructor; implementation is in .cpp file
+  ui_message_handlert();
 
   virtual ~ui_message_handlert();
 
@@ -40,13 +41,25 @@ class ui_message_handlert : public message_handlert
   void set_ui(uit __ui)
   {
     _ui=__ui;
+    if(_ui == uit::JSON_UI && !json_stream)
+    {
+      json_stream =
+        std::unique_ptr<json_stream_arrayt>(new json_stream_arrayt(out));
+    }
   }
 
   virtual void flush(unsigned level) override;
 
+  json_stream_arrayt &get_json_stream() override
+  {
+    return *json_stream;
+  }
+
 protected:
   uit _ui;
   std::unique_ptr<const timestampert> time;
+  std::ostream &out;
+  std::unique_ptr<json_stream_arrayt> json_stream;
 
   virtual void print(
     unsigned level,