Print XML and JSON objects on message stream

peterschrammel · peterschrammel · commit ad6484eea011 · 2017-09-18T11:14:07.000+01:00
diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "all_properties_class.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/json.h>
@@ -176,10 +174,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         for(const auto &g : goal_map)
           if(g.second.status==goalt::statust::FAILURE)
           {
-            std::cout << "\n" << "Trace for " << g.first << ":" << "\n";
-            show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);
+            result() << "\n" << "Trace for " << g.first << ":" << "\n";
+            show_goto_trace(result(), bmc.ns, g.second.goto_trace);
           }
       }
+      result() << eom;
 
       status() << "\n** " << cover_goals.number_covered()
                << " of " << cover_goals.size() << " failed ("
@@ -200,7 +199,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         if(g.second.status==goalt::statust::FAILURE)
           convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -224,7 +223,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
         }
       }
 
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -64,24 +64,24 @@ void bmct::error_trace()
     {
       xmlt xml;
       convert(ns, goto_trace, xml);
-      status() << xml << eom;
+      status() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_arrayt &result_array=json_result["results"].make_array();
-      json_objectt &result=result_array.push_back().make_object();
+      json_objectt json;
+      json_arrayt &result_array=json["results"].make_array();
+      json_objectt &json_result=result_array.push_back().make_object();
       const goto_trace_stept &step=goto_trace.steps.back();
-      result["property"]=
+      json_result["property"]=
         json_stringt(id2string(step.pc->source_location.get_property_id()));
-      result["description"]=
+      json_result["description"]=
         json_stringt(id2string(step.pc->source_location.get_comment()));
-      result["status"]=json_stringt("failed");
-      jsont &json_trace=result["trace"];
+      json_result["status"]=json_stringt("failed");
+      jsont &json_trace=json_result["trace"];
       convert(ns, goto_trace, json_trace);
-      status() << ",\n" << json_result << eom;
+      status() << json_result;
     }
     break;
   }
@@ -173,16 +173,15 @@ void bmct::report_success()
     {
       xmlt xml("cprover-status");
       xml.data="SUCCESS";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("success");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
@@ -201,16 +200,15 @@ void bmct::report_failure()
     {
       xmlt xml("cprover-status");
       xml.data="FAILURE";
-      std::cout << xml;
-      std::cout << "\n";
+      result() << xml;
     }
     break;
 
   case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["cProverStatus"]=json_stringt("failure");
-      std::cout << ",\n" << json_result;
+      result() << json_result;
     }
     break;
   }
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bmc.h"
 
-#include <iostream>
-
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/xml_expr.h>
@@ -185,10 +183,6 @@ void bmc_covert::satisfying_assignment()
       goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
       break;
     }
-
-  #if 0
-  show_goto_trace(std::cout, bmc.ns, test.goto_trace);
-  #endif
 }
 
 bool bmc_covert::operator()()
@@ -223,8 +217,6 @@ bool bmc_covert::operator()()
 
   bmc.do_conversion();
 
-  // bmc.equation.output(std::cout);
-
   // get the conditions for these goals from formula
   // collect all 'instances' of the goals
   for(auto it = bmc.equation.SSA_steps.begin();
@@ -317,7 +309,7 @@ bool bmc_covert::operator()()
         if(goal.source_location.is_not_nil())
           xml_result.new_element()=xml(goal.source_location);
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
 
       for(const auto &test : tests)
@@ -350,7 +342,7 @@ bool bmc_covert::operator()()
           xml_goal.set_attribute("id", id2string(goal_id));
         }
 
-        std::cout << xml_result << "\n";
+        result() << xml_result;
       }
       break;
     }
@@ -406,7 +398,8 @@ bool bmc_covert::operator()()
           goal_refs.push_back(json_stringt(id2string(goal_id)));
         }
       }
-      std::cout << ",\n" << json_result;
+
+      result() << json_result;
       break;
     }
   }
@@ -424,10 +417,12 @@ bool bmc_covert::operator()()
 
   if(bmc.ui==ui_message_handlert::uit::PLAIN)
   {
-    std::cout << "Test suite:" << '\n';
+    result() << "Test suite:" << '\n';
 
     for(const auto &test : tests)
-      std::cout << get_test(test.goto_trace) << '\n';
+      result() << get_test(test.goto_trace) << '\n';
+
+    result() << eom;
   }
 
   return false;
diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp
@@ -301,7 +301,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
       xmlt dest("fault-localization");
       xmlt xml_diagnosis=report_xml(ID_nil);
       dest.new_element().swap(xml_diagnosis);
-      status() << preformatted_output << dest << eom;
+      status() << dest;
       break;
     }
     case ui_message_handlert::uit::JSON_UI:
@@ -379,7 +379,7 @@ void fault_localizationt::report(
         xmlt xml_diagnosis=report_xml(goal_pair.first);
         dest.new_element().swap(xml_diagnosis);
       }
-      status() << preformatted_output << dest << eom;
+      status() << dest;
     }
     break;
   case ui_message_handlert::uit::JSON_UI:
diff --git a/src/util/message.h b/src/util/message.h
@@ -15,7 +15,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 
 #include "invariant.h"
+#include "json.h"
 #include "source_location.h"
+#include "xml.h"
 
 class message_handlert
 {
@@ -24,7 +26,17 @@ class message_handlert
   {
   }
 
-  virtual void print(unsigned level, const std::string &message) = 0;
+  virtual void print(unsigned level, const std::string &message)=0;
+
+  virtual void print(unsigned level, const xmlt &xml)
+  {
+    // no-op by default
+  }
+
+  virtual void print(unsigned level, const jsont &json)
+  {
+    // no-op by default
+  }
 
   virtual void print(
     unsigned level,
@@ -176,6 +188,26 @@ class messaget
     messaget &message;
     source_locationt source_location;
 
+    mstreamt &operator << (const xmlt &data)
+    {
+      *this << eom; // force end of previous message
+      if(message.message_handler)
+      {
+        message.message_handler->print(message_level, data);
+      }
+      return *this;
+    }
+
+    mstreamt &operator << (const json_objectt &data)
+    {
+      *this << eom; // force end of previous message
+      if(message.message_handler)
+      {
+        message.message_handler->print(message_level, data);
+      }
+      return *this;
+    }
+
     template <class T>
     mstreamt &operator << (const T &x)
     {
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
@@ -115,6 +115,50 @@ void ui_message_handlert::print(
   }
 }
 
+void ui_message_handlert::print(
+  unsigned level,
+  const xmlt &data)
+{
+  if(verbosity>=level)
+  {
+    switch(get_ui())
+    {
+    case uit::PLAIN:
+      INVARIANT(false, "Cannot print xml data on PLAIN UI");
+      break;
+    case uit::XML_UI:
+      std::cout << data << '\n';
+      flush(level);
+      break;
+    case uit::JSON_UI:
+      INVARIANT(false, "Cannot print xml data on JSON UI");
+      break;
+    }
+  }
+}
+
+void ui_message_handlert::print(
+  unsigned level,
+  const jsont &data)
+{
+  if(verbosity>=level)
+  {
+    switch(get_ui())
+    {
+    case uit::PLAIN:
+      INVARIANT(false, "Cannot print json data on PLAIN UI");
+      break;
+    case uit::XML_UI:
+      INVARIANT(false, "Cannot print json data on XML UI");
+      break;
+    case uit::JSON_UI:
+      std::cout << ',' << '\n' << data;
+      flush(level);
+      break;
+    }
+  }
+}
+
 void ui_message_handlert::print(
   unsigned level,
   const std::string &message,
diff --git a/src/util/ui_message.h b/src/util/ui_message.h
@@ -36,22 +36,28 @@ class ui_message_handlert:public message_handlert
     _ui=__ui;
   }
 
-  virtual void flush(unsigned level);
+  virtual void flush(unsigned level) override;
 
 protected:
   uit _ui;
 
-  // overloading
   virtual void print(
     unsigned level,
-    const std::string &message);
+    const std::string &message) override;
 
-  // overloading
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location);
+    const source_locationt &location) override;
+
+  virtual void print(
+    unsigned level,
+    const xmlt &data) override;
+
+  virtual void print(
+    unsigned level,
+    const jsont &data) override;
 
   virtual void xml_ui_msg(
     const std::string &type,

Original file line number	Diff line number	Diff line change
`@@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]`
`11`	`11`
`12`	`12`	`#include "all_properties_class.h"`
`13`	`13`
`14`		`-#include <iostream>`
`15`		`-`
`16`	`14`	`#include <util/time_stopping.h>`
`17`	`15`	`#include <util/xml.h>`
`18`	`16`	`#include <util/json.h>`
`@@ -176,10 +174,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`176`	`174`	`for(const auto &g : goal_map)`
`177`	`175`	`if(g.second.status==goalt::statust::FAILURE)`
`178`	`176`	`{`
`179`		`- std::cout << "\n" << "Trace for " << g.first << ":" << "\n";`
`180`		`- show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);`
	`177`	`+ result() << "\n" << "Trace for " << g.first << ":" << "\n";`
	`178`	`+ show_goto_trace(result(), bmc.ns, g.second.goto_trace);`
`181`	`179`	`}`
`182`	`180`	`}`
	`181`	`+ result() << eom;`
`183`	`182`
`184`	`183`	`status() << "\n** " << cover_goals.number_covered()`
`185`	`184`	`<< " of " << cover_goals.size() << " failed ("`
`@@ -200,7 +199,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`200`	`199`	`if(g.second.status==goalt::statust::FAILURE)`
`201`	`200`	`convert(bmc.ns, g.second.goto_trace, xml_result.new_element());`
`202`	`201`
`203`		`- std::cout << xml_result << "\n";`
	`202`	`+ result() << xml_result;`
`204`	`203`	`}`
`205`	`204`	`break;`
`206`	`205`	`}`
`@@ -224,7 +223,7 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)`
`224`	`223`	`}`
`225`	`224`	`}`
`226`	`225`
`227`		`- std::cout << ",\n" << json_result;`
	`226`	`+ result() << json_result;`
`228`	`227`	`}`
`229`	`228`	`break;`
`230`	`229`	`}`
Original file line number	Diff line number	Diff line change
`@@ -64,24 +64,24 @@ void bmct::error_trace()`
`64`	`64`	`{`
`65`	`65`	`xmlt xml;`
`66`	`66`	`convert(ns, goto_trace, xml);`
`67`		`- status() << xml << eom;`
	`67`	`+ status() << xml;`
`68`	`68`	`}`
`69`	`69`	`break;`
`70`	`70`
`71`	`71`	`case ui_message_handlert::uit::JSON_UI:`
`72`	`72`	`{`
`73`		`- json_objectt json_result;`
`74`		`- json_arrayt &result_array=json_result["results"].make_array();`
`75`		`- json_objectt &result=result_array.push_back().make_object();`
	`73`	`+ json_objectt json;`
	`74`	`+ json_arrayt &result_array=json["results"].make_array();`
	`75`	`+ json_objectt &json_result=result_array.push_back().make_object();`
`76`	`76`	`const goto_trace_stept &step=goto_trace.steps.back();`
`77`		`- result["property"]=`
	`77`	`+ json_result["property"]=`
`78`	`78`	`json_stringt(id2string(step.pc->source_location.get_property_id()));`
`79`		`- result["description"]=`
	`79`	`+ json_result["description"]=`
`80`	`80`	`json_stringt(id2string(step.pc->source_location.get_comment()));`
`81`		`- result["status"]=json_stringt("failed");`
`82`		`- jsont &json_trace=result["trace"];`
	`81`	`+ json_result["status"]=json_stringt("failed");`
	`82`	`+ jsont &json_trace=json_result["trace"];`
`83`	`83`	`convert(ns, goto_trace, json_trace);`
`84`		`- status() << ",\n" << json_result << eom;`
	`84`	`+ status() << json_result;`
`85`	`85`	`}`
`86`	`86`	`break;`
`87`	`87`	`}`
`@@ -173,16 +173,15 @@ void bmct::report_success()`
`173`	`173`	`{`
`174`	`174`	`xmlt xml("cprover-status");`
`175`	`175`	`xml.data="SUCCESS";`
`176`		`- std::cout << xml;`
`177`		`- std::cout << "\n";`
	`176`	`+ result() << xml;`
`178`	`177`	`}`
`179`	`178`	`break;`
`180`	`179`
`181`	`180`	`case ui_message_handlert::uit::JSON_UI:`
`182`	`181`	`{`
`183`	`182`	`json_objectt json_result;`
`184`	`183`	`json_result["cProverStatus"]=json_stringt("success");`
`185`		`- std::cout << ",\n" << json_result;`
	`184`	`+ result() << json_result;`
`186`	`185`	`}`
`187`	`186`	`break;`
`188`	`187`	`}`
`@@ -201,16 +200,15 @@ void bmct::report_failure()`
`201`	`200`	`{`
`202`	`201`	`xmlt xml("cprover-status");`
`203`	`202`	`xml.data="FAILURE";`
`204`		`- std::cout << xml;`
`205`		`- std::cout << "\n";`
	`203`	`+ result() << xml;`
`206`	`204`	`}`
`207`	`205`	`break;`
`208`	`206`
`209`	`207`	`case ui_message_handlert::uit::JSON_UI:`
`210`	`208`	`{`
`211`	`209`	`json_objectt json_result;`
`212`	`210`	`json_result["cProverStatus"]=json_stringt("failure");`
`213`		`- std::cout << ",\n" << json_result;`
	`211`	`+ result() << json_result;`
`214`	`212`	`}`
`215`	`213`	`break;`
`216`	`214`	`}`
Original file line number	Diff line number	Diff line change
`@@ -301,7 +301,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()`
`301`	`301`	`xmlt dest("fault-localization");`
`302`	`302`	`xmlt xml_diagnosis=report_xml(ID_nil);`
`303`	`303`	`dest.new_element().swap(xml_diagnosis);`
`304`		`- status() << preformatted_output << dest << eom;`
	`304`	`+ status() << dest;`
`305`	`305`	`break;`
`306`	`306`	`}`
`307`	`307`	`case ui_message_handlert::uit::JSON_UI:`
`@@ -379,7 +379,7 @@ void fault_localizationt::report(`
`379`	`379`	`xmlt xml_diagnosis=report_xml(goal_pair.first);`
`380`	`380`	`dest.new_element().swap(xml_diagnosis);`
`381`	`381`	`}`
`382`		`- status() << preformatted_output << dest << eom;`
	`382`	`+ status() << dest;`
`383`	`383`	`}`
`384`	`384`	`break;`
`385`	`385`	`case ui_message_handlert::uit::JSON_UI:`