JSON output

src/cbmc/bmc.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/source_location.h>
 #include <util/time_stopping.h>
 #include <util/message_stream.h>
+#include <util/json.h>
 
 #include <langapi/mode.h>
 #include <langapi/languages.h>
@@ -87,8 +88,14 @@ void bmct::error_trace()
     }
     break;
 
-  default:
-    assert(false);
+  case ui_message_handlert::JSON_UI:
+    {
+      json_objectt counterexample;
+      jsont &json_trace=counterexample["counterexample"];
+      convert(ns, goto_trace, json_trace);
+      std::cout << ",\n" << counterexample << "\n";
+    }
+    break;
   }
 
   const std::string graphml=options.get_option("graphml-cex");
@@ -105,22 +112,6 @@ void bmct::error_trace()
       write_graphml(cex_graph, out);
     }
   }
-
-  if(options.get_option("json-cex")!="")
-  {
-    jsont json_trace;
-    convert(ns, goto_trace, json_trace);
-
-    if(options.get_option("json-cex")=="-")
-    {
-      std::cout << json_trace;
-    }
-    else
-    {
-      std::ofstream out(options.get_option("json-cex").c_str());
-      out << json_trace << '\n';
-    }
-  }  
 }
 
 /*******************************************************************\
@@ -223,9 +214,14 @@ void bmct::report_success()
       std::cout << "\n";
     }
     break;
-
-  default:
-    assert(false);
+
+  case ui_message_handlert::JSON_UI:
+    {
+      json_objectt json_result;
+      json_result["cProverStatus"]=json_stringt("success");
+      std::cout << ",\n" << json_result;
+    }
+    break;
   }
 }
 
@@ -258,9 +254,14 @@ void bmct::report_failure()
       std::cout << "\n";
     }
     break;
-
-  default:
-    assert(false);
+
+  case ui_message_handlert::JSON_UI:
+    {
+      json_objectt json_result;
+      json_result["cProverStatus"]=json_stringt("failure");
+      std::cout << ",\n" << json_result;
+    }
+    break;
   }
 }
 

src/cbmc/cbmc_parse_options.cpp

@@ -38,6 +38,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
@@ -442,9 +443,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("graphml-cex"))
     options.set_option("graphml-cex", cmdline.get_value("graphml-cex"));
-
-  if(cmdline.isset("json-cex"))
-    options.set_option("json-cex", cmdline.get_value("json-cex"));
 }
 
 /*******************************************************************\
@@ -652,15 +650,17 @@ int cbmc_parse_optionst::get_goto_program(
 
       if(!infile)
       {
-        error() << "failed to open input file `" << filename << "'" << eom;
+        error() << "failed to open input file `" 
+                << filename << "'" << eom;
         return 6;
       }
 
       languaget *language=get_language_from_filename(filename);
 
       if(language==NULL)
       {
-        error() << "failed to figure out type of file `" <<  filename << "'" << eom;
+        error() << "failed to figure out type of file `" 
+                <<  filename << "'" << eom;
         return 6;
       }
 
@@ -715,7 +715,8 @@ int cbmc_parse_optionst::get_goto_program(
     {
       status() << "Reading GOTO program from file " << eom;
 
-      if(read_object_and_link(*it, symbol_table, goto_functions, get_message_handler()))
+      if(read_object_and_link(*it, symbol_table, goto_functions, 
+                              get_message_handler()))
         return 6;
     }
 
@@ -964,7 +965,8 @@ bool cbmc_parse_optionst::process_goto_program(
     // show it?
     if(cmdline.isset("show-goto-functions"))
     {
-      goto_functions.output(ns, std::cout);
+      namespacet ns(symbol_table);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return true;
     }
   }
@@ -1164,5 +1166,6 @@ void cbmc_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
+    " --json-ui                    use JSON-formatted output\n"
     "\n";
 }

src/cbmc/cbmc_parse_options.h

@@ -31,7 +31,7 @@ class optionst;
   "(bounds-check)(pointer-check)(div-by-zero-check)(memory-leak-check)" \
   "(signed-overflow-check)(unsigned-overflow-check)(float-overflow-check)(nan-check)" \
   "(no-assertions)(no-assumptions)" \
-  "(xml-ui)(xml-interface)" \
+  "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
@@ -52,7 +52,7 @@ class optionst;
   "(arrays-uf-always)(arrays-uf-never)" \
   "(string-abstraction)(no-arch)(arch):" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
-  "(graphml-cex):(json-cex):" \
+  "(graphml-cex):" \
   "(floatbv)(all-claims)(all-properties)(decide)" // legacy, and will eventually disappear
 
 class cbmc_parse_optionst:

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/parameter_assignments.h>
+#include <goto-programs/show_goto_functions.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -470,7 +471,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("show-goto-functions"))
     {
       namespacet ns(symbol_table);
-      goto_functions.output(ns, std::cout);
+      show_goto_functions(ns, get_ui(), goto_functions);
       return 0;
     }
 
@@ -1347,5 +1348,6 @@ void goto_instrument_parse_optionst::help()
     " --use-system-headers         with --dump-c/--dump-cpp: generate C source with includes\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
+    " --json-ui                    use JSON-formatted output\n"
     "\n";
 }

src/goto-instrument/goto_instrument_parse_options.h

@@ -54,7 +54,7 @@ Author: Daniel Kroening, [email protected]
   "(cav11)" \
   "(show-natural-loops)(accelerate)(havoc-loops)" \
   "(error-label):(string-abstraction)" \
-  "(verbosity):(version)(xml-ui)(show-loops)" \
+  "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \
   "(accelerate)(constant-propagator)" \
   "(k-induction):(step-case)(base-case)" \
   "(show-call-sequences)(check-call-sequence)" \

src/goto-programs/Makefile

@@ -16,7 +16,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
       graphml_goto_trace.cpp remove_virtual_functions.cpp \
-      class_hierarchy.cpp
+      class_hierarchy.cpp show_goto_functions.cpp
 
 INCLUDES= -I ..
 

src/goto-programs/read_goto_binary.cpp

@@ -370,7 +370,8 @@ bool read_object_and_link(
   goto_functionst &functions,
   message_handlert &message_handler)
 {
-  message_handler.print(8, "Reading: " + file_name);
+  messaget(message_handler).statistics() << "Reading: " 
+                                         << file_name << messaget::eom;
 
   // we read into a temporary model
   goto_modelt temp_model;

src/goto-programs/show_properties.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 
 #include <util/xml.h>
+#include <util/json.h>
 #include <util/i2string.h>
 #include <util/xml_expr.h>
 
@@ -89,6 +90,10 @@ void show_properties(
         std::cout << xml_property << std::endl;
       }
       break;
+
+    case ui_message_handlert::JSON_UI:
+      assert(false);
+      break;
 
     case ui_message_handlert::PLAIN:
       std::cout << "Property " << property_id << ":" << std::endl;
@@ -106,9 +111,10 @@ void show_properties(
   }
 }
 
+
 /*******************************************************************\
 
-Function: show_properties
+Function: cbmc_parseoptionst::show_properties_json
 
   Inputs:
 
@@ -118,17 +124,99 @@ Function: show_properties
 
 \*******************************************************************/
 
-void show_properties(
+void show_properties_json(
+  json_arrayt &json_properties,
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const goto_programt &goto_program)
+{
+  for(goto_programt::instructionst::const_iterator
+      it=goto_program.instructions.begin();
+      it!=goto_program.instructions.end();
+      it++)
+  {
+    if(!it->is_assert())
+      continue;
+
+    const source_locationt &source_location=it->source_location;
+
+    const irep_idt &comment=source_location.get_comment();
+    //const irep_idt &function=location.get_function();
+    const irep_idt &property_class=source_location.get_property_class();
+    const irep_idt description=
+      (comment==""?"assertion":comment);
+
+    irep_idt property_id=source_location.get_property_id();
+
+    json_objectt &json_property=
+      json_properties.push_back(jsont()).make_object();
+    json_property["name"]=json_stringt(id2string(property_id));
+    json_property["class"]=json_stringt(id2string(property_class));
+#if 0 //TODO
+    json_property["location"]=json(it->source_location);
+#endif
+    json_property["description"]=json_stringt(id2string(description));
+    json_property["expression"]=
+      json_stringt(from_expr(ns, identifier, it->guard));
+  }
+}
+
+/*******************************************************************\
+
+Function: show_properties_json
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_properties_json(
   const namespacet &ns,
-  ui_message_handlert::uit ui,
   const goto_functionst &goto_functions)
 {
+  json_arrayt json_properties;
   for(goto_functionst::function_mapt::const_iterator
       it=goto_functions.function_map.begin();
       it!=goto_functions.function_map.end();
       it++)
+  {
     if(!it->second.is_inlined())
-      show_properties(ns, it->first, ui, it->second.body);
+      show_properties_json(json_properties, ns, it->first, it->second.body);
+  }
+  json_objectt json_result;
+  json_result["properties"] = json_properties;
+  std::cout << ",\n" << json_result;
+}
+
+/*******************************************************************\
+
+Function: show_properties
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_properties(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions)
+{
+  if(ui == ui_message_handlert::JSON_UI)
+    show_properties_json(ns, goto_functions);
+  else
+    for(goto_functionst::function_mapt::const_iterator
+	  it=goto_functions.function_map.begin();
+	it!=goto_functions.function_map.end();
+	it++)
+      if(!it->second.is_inlined())
+	show_properties(ns, it->first, ui, it->second.body);
 }
 
 /*******************************************************************\
@@ -148,6 +236,9 @@ void show_properties(
   ui_message_handlert::uit ui)
 {
   const namespacet ns(goto_model.symbol_table);
-  show_properties(ns, ui, goto_model.goto_functions);
+  if(ui == ui_message_handlert::JSON_UI)
+    show_properties_json(ns, goto_model.goto_functions);
+  else
+    show_properties(ns, ui, goto_model.goto_functions);
 }
 

src/langapi/language_ui.cpp

@@ -36,6 +36,9 @@ static ui_message_handlert::uit get_ui_cmdline(const cmdlinet &cmdline)
   if(cmdline.isset("xml-ui"))
     return ui_message_handlert::XML_UI;
 
+  if(cmdline.isset("json-ui"))
+    return ui_message_handlert::JSON_UI;
+
   return ui_message_handlert::PLAIN;
 }