Base JSON UI message handler upon json_streamt

Author: peterschrammel

src/util/message.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "invariant.h"
 #include "json.h"
+#include "json_stream.h"
 #include "source_location.h"
 #include "xml.h"
 
@@ -38,6 +39,11 @@ class message_handlert
     // no-op by default
   }
 
+  virtual json_stream_arrayt &get_json_stream()
+  {
+    UNREACHABLE;
+  }
+
   virtual void print(
     unsigned level,
     const std::string &message,
@@ -232,6 +238,12 @@ class messaget
       return func(*this);
     }
 
+    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,36 +15,36 @@ 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(
-  uit __ui, const std::string &program):_ui(__ui)
+  uit __ui, const std::string &program):ui_message_handlert()
 {
-  switch(__ui)
+  set_ui(__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;
+      INVARIANT(json_stream, "JSON stream must be initialized before use");
+      json_stream->push_back().make_object()["program"] = json_stringt(program);
     }
     break;
   }
@@ -61,16 +61,24 @@ ui_message_handlert::ui_message_handlert(
 {
 }
 
+ui_message_handlert::ui_message_handlert():
+  _ui(uit::PLAIN), out(std::cout), json_stream(nullptr)
+{
+}
+
 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:
@@ -127,7 +135,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:
@@ -152,7 +160,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;
     }
@@ -233,8 +242,8 @@ void ui_message_handlert::xml_ui_msg(
   result.new_element("text").data=msg1;
   result.set_attribute("type", type);
 
-  std::cout << result;
-  std::cout << '\n';
+  out << result;
+  out << '\n';
 }
 
 void ui_message_handlert::json_ui_msg(
@@ -243,19 +252,15 @@ 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())
     result["sourceLocation"] = json(location);
 
   result["messageType"] = json_stringt(type);
   result["messageText"] = json_stringt(msg1);
-
-  // By convention a leading comma is created by every new array entry.
-  // The first entry is generated in the constructor and does not have
-  //  a trailing comma.
-  std::cout << ",\n" << result;
 }
 
 void ui_message_handlert::flush(unsigned level)
@@ -272,7 +277,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

@@ -12,17 +12,16 @@ Author: Daniel Kroening, [email protected]
 
 #include "message.h"
 
+class json_stream_arrayt;
+
 class ui_message_handlert:public message_handlert
 {
 public:
   enum class uit { PLAIN, XML_UI, JSON_UI };
 
   ui_message_handlert(uit, const std::string &program);
   ui_message_handlert(const class cmdlinet &, const std::string &program);
-  ui_message_handlert():
-    _ui(uit::PLAIN)
-  {
-  }
+  ui_message_handlert();
 
   virtual ~ui_message_handlert();
 
@@ -34,12 +33,23 @@ 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::ostream &out;
+  std::unique_ptr<json_stream_arrayt> json_stream;
 
   virtual void print(
     unsigned level,