More JSON output

src/cbmc/all_properties.cpp

@@ -10,13 +10,15 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/time_stopping.h>
 #include <util/xml.h>
+#include <util/json.h>
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/prop/cover_goals.h>
 #include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/json_goto_trace.h>
 
 #include "bmc.h"
 #include "bv_cbmc.h"
@@ -183,8 +185,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       else if(it->source.pc->is_goto())
       {
         // this is likely an unwinding assertion
-        property_id=id2string(it->source.pc->source_location.get_function())+".unwind."+
-                    i2string(it->source.pc->loop_number);
+        property_id=id2string(
+          it->source.pc->source_location.get_function())+".unwind."+
+          i2string(it->source.pc->loop_number);
         goal_map[property_id].description=it->comment;
       }
       else
@@ -211,7 +214,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   status() << "Running " << solver.decision_procedure_text() << eom;
 
-  cover_goals();  
+  cover_goals();
 
   // output runtime
 
@@ -222,43 +225,75 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
   }
 
   // report
-  if(bmc.ui!=ui_message_handlert::XML_UI)
+  switch(bmc.ui)
   {
-    status() << eom;
-    status() << "** Results:" << eom;
-  }
+    case ui_message_handlert::PLAIN:
+    {
+      status() << eom;
+      status() << "** Results:" << eom;
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        status() << "[" << it->first << "] "
+                 << it->second.description << ": "
+                 << (it->second.failed?"FAILURE":"SUCCESS")
+                 << eom;
+      }
+      status() << eom;
 
-  for(goal_mapt::const_iterator
-      it=goal_map.begin();
-      it!=goal_map.end();
-      it++)
-  {
-    if(bmc.ui==ui_message_handlert::XML_UI)
+      status() << "** " << cover_goals.number_covered()
+               << " of " << cover_goals.size() << " failed ("
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
+               << ")" << eom;
+      break;
+    }
+    case ui_message_handlert::XML_UI:
     {
-      xmlt xml_result("result");
-      xml_result.set_attribute("property", id2string(it->first));
-      xml_result.set_attribute("status", it->second.failed?"FAILURE":"SUCCESS");
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        xmlt xml_result("results");
+        xml_result.set_attribute("property", id2string(it->first));
+        xml_result.set_attribute("status",
+                                 it->second.failed?"FAILURE":"SUCCESS");
 
-      if(it->second.failed)
-        convert(bmc.ns, it->second.goto_trace, xml_result.new_element());
+        if(it->second.failed)
+          convert(bmc.ns, it->second.goto_trace, xml_result.new_element());
 
-      std::cout << xml_result << "\n";
+        std::cout << xml_result << "\n";
+      }
+      break;
     }
-    else
+    case ui_message_handlert::JSON_UI:
     {
-      status() << "[" << it->first << "] "
-               << it->second.description << ": " << (it->second.failed?"FAILURE":"SUCCESS")
-               << eom;
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["result"].make_array();
+      for(goal_mapt::const_iterator
+            it=goal_map.begin();
+          it!=goal_map.end();
+          it++)
+      {
+        json_objectt &result=result_array.push_back().make_object();
+        result["property"]=json_stringt(id2string(it->first));
+        result["description"]=json_stringt(id2string(it->second.description));
+        result["status"]=json_stringt(it->second.failed?"failure":"success");
+
+        if(it->second.failed)
+        {
+          jsont &json_trace=result["trace"];
+          convert(bmc.ns, it->second.goto_trace, json_trace);
+        }
+      }
+      std::cout << ",\n" << json_result;
+      break;
     }
   }
 
-  status() << eom;
-
-  status() << "** " << cover_goals.number_covered()
-           << " of " << cover_goals.size() << " failed ("
-           << cover_goals.iterations() << " iteration"
-           << (cover_goals.iterations()==1?"":"s")
-           << ")" << eom;
 
   bool safe=(cover_goals.number_covered()==0);
 

src/cbmc/bmc.cpp

@@ -90,10 +90,18 @@ void bmct::error_trace()
 
   case ui_message_handlert::JSON_UI:
     {
-      json_objectt counterexample;
-      jsont &json_trace=counterexample["counterexample"];
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["results"].make_array();
+      json_objectt &result=result_array.push_back().make_object();
+      const goto_trace_stept &step=goto_trace.steps.back();
+      result["property"]=
+        json_stringt(id2string(step.pc->source_location.get_property_id()));
+      result["description"]=
+        json_stringt(id2string(step.pc->source_location.get_comment()));
+      result["status"]=json_stringt("failed");
+      jsont &json_trace=result["trace"];
       convert(ns, goto_trace, json_trace);
-      std::cout << ",\n" << counterexample << "\n";
+      std::cout << ",\n" << json_result;
     }
     break;
   }

src/cbmc/bmc_cover.cpp

@@ -11,12 +11,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/time_stopping.h>
 #include <util/xml.h>
 #include <util/xml_expr.h>
+#include <util/json.h>
+#include <util/json_expr.h>
 
 #include <solvers/prop/cover_goals.h>
 #include <solvers/prop/literal_expr.h>
 
 #include <goto-symex/build_goto_trace.h>
 #include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/json_goto_trace.h>
 
 #include "bmc.h"
 #include "bv_cbmc.h"
@@ -315,60 +318,104 @@ bool bmc_covert::operator()()
   }
 
   // report
-  if(bmc.ui!=ui_message_handlert::XML_UI)
-  {
-    status() << eom;
-    status() << "** coverage results:" << eom;
-  }
-
   unsigned goals_covered=0;
-
-  for(const auto & it : goal_map)
+  switch(bmc.ui)
   {
-    const goalt &goal=it.second;
-
-    if(goal.satisfied) goals_covered++;
-
-    if(bmc.ui==ui_message_handlert::XML_UI)
+    case ui_message_handlert::PLAIN:
     {
-      xmlt xml_result("result");
-      xml_result.set_attribute("goal", id2string(it.first));
-      xml_result.set_attribute("description", goal.description);
-      xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
-
-      if(goal.source_location.is_not_nil())
-        xml_result.new_element()=xml(goal.source_location);
+      status() << eom;
+      status() << "** coverage results:" << eom;
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
 
-      if(goal.satisfied)
-        convert(bmc.ns, goal.goto_trace, xml_result.new_element());
+        if(goal.satisfied) goals_covered++;
 
-      std::cout << xml_result << "\n";
+        status() << "[" << it.first << "]";
+
+        if(goal.source_location.is_not_nil())
+          status() << ' ' << goal.source_location;
+
+        if(!goal.description.empty()) status() << ' ' << goal.description;
+
+        status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+                 << eom;
+      }
+      status() << eom;
+      status() << "** " << goals_covered
+               << " of " << goal_map.size() << " covered ("
+               << std::fixed << std::setw(1) << std::setprecision(1)
+               << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
+               << "%), using "
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
+               << eom;
+      break;
     }
-    else
+    case ui_message_handlert::XML_UI:
     {
-      status() << "[" << it.first << "]";
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
 
-      if(goal.source_location.is_not_nil())
-        status() << ' ' << goal.source_location;
-
-      if(!goal.description.empty()) status() << ' ' << goal.description;
+        if(goal.satisfied) goals_covered++;
 
-      status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
+        xmlt xml_result("result");
+        xml_result.set_attribute("goal", id2string(it.first));
+        xml_result.set_attribute("description", goal.description);
+        xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
+
+        if(goal.source_location.is_not_nil())
+          xml_result.new_element()=xml(goal.source_location);
+
+        if(goal.satisfied)
+          convert(bmc.ns, goal.goto_trace, xml_result.new_element());
+
+        std::cout << xml_result << "\n";
+      }
+
+      status() << eom;
+      status() << "** " << goals_covered
+               << " of " << goal_map.size() << " covered ("
+               << std::fixed << std::setw(1) << std::setprecision(1)
+               << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
+               << "%), using "
+               << cover_goals.iterations() << " iteration"
+               << (cover_goals.iterations()==1?"":"s")
                << eom;
+      break;
+    }
+    case ui_message_handlert::JSON_UI:
+    {
+      json_objectt json_result;
+      json_arrayt &result_array=json_result["results"].make_array();
+      for(const auto & it : goal_map)
+      {
+        const goalt &goal=it.second;
+
+        if(goal.satisfied) goals_covered++;
+
+        json_objectt &result=result_array.push_back().make_object();
+        result["status"]=json_stringt(goal.satisfied?"satisfied":"failed");
+        result["goal"]=json_stringt(id2string(it.first));
+        result["description"]=json_stringt(goal.description);
+
+        if(goal.source_location.is_not_nil())
+          result["sourceLocation"]=json(goal.source_location);
+
+        if(goal.satisfied)
+        {
+          jsont &json_trace=result["trace"];
+          convert(bmc.ns, goal.goto_trace, json_trace);
+        }
+      }
+      json_result["totalGoals"]=json_numbert(i2string(goal_map.size()));
+      json_result["goalsCovered"]=json_numbert(i2string(goals_covered));
+      std::cout << ",\n" << json_result;
+      break;
     }
   }
 
-  status() << eom;
-
-  status() << "** " << goals_covered
-           << " of " << goal_map.size() << " covered ("
-           << std::fixed << std::setw(1) << std::setprecision(1)
-           << (goal_map.empty()?0.0:100.0*goals_covered/goal_map.size())
-           << "%), using "
-           << cover_goals.iterations() << " iteration"
-           << (cover_goals.iterations()==1?"":"s")
-           << eom;
-
   return false;
 }