basic json-ui

Author: Peter Schrammel

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,6 +214,14 @@ void bmct::report_success()
       std::cout << "\n";
     }
     break;
+
+  case ui_message_handlert::JSON_UI:
+    {
+      json_objectt json_result;
+      json_result["cProverStatus"]=json_stringt("success");
+      std::cout << ",\n" << json_result; 
+    }
+    break;
 
   default:
     assert(false);
@@ -258,9 +257,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/remove_unused_functions.cpp

@@ -23,12 +23,17 @@ Function: remove_unused_functions
 \*******************************************************************/
 
 void remove_unused_functions(
+  const irep_idt &start,
   goto_functionst &functions,
   message_handlert &message_handler)
 {
   std::set<irep_idt> used_functions;
   std::list<goto_functionst::function_mapt::iterator> unused_functions;
-  find_used_functions(goto_functionst::entry_point(), functions, used_functions);
+  find_used_functions(start, functions, used_functions);
+
+  //maybe an error should be thrown in this case
+  if(functions.function_map.find(start) == functions.function_map.end())
+    used_functions.clear();
 
   for(goto_functionst::function_mapt::iterator it=
         functions.function_map.begin();
@@ -39,8 +44,11 @@ void remove_unused_functions(
       unused_functions.push_back(it);
   }
 
+  assert(unused_functions.size() + used_functions.size() ==
+	 functions.function_map.size());
+
   messaget message(message_handler);
-  
+
   if(unused_functions.size()>0)
   {
     message.statistics()
@@ -58,6 +66,26 @@ void remove_unused_functions(
 
 /*******************************************************************\
 
+Function: remove_unused_functions
+
+  Inputs: 
+
+ Outputs: 
+
+ Purpose: 
+
+\*******************************************************************/
+
+void remove_unused_functions(
+  goto_functionst &functions,
+  message_handlert &message_handler)
+{
+  remove_unused_functions(goto_functionst::entry_point(), 
+			  functions, message_handler);
+}
+
+/*******************************************************************\
+
 Function: find_used_functions
 
   Inputs: 

src/goto-programs/remove_unused_functions.h

@@ -10,13 +10,19 @@ Author: CM Wintersteiger
 #define CPROVER_GOTO_PROGRAMS_REMOVE_UNUSED_FUNCTIONS_H
 
 #include <util/message.h>
+#include <util/config.h>
 
 #include <goto-programs/goto_functions.h>
 
 void remove_unused_functions( 
   goto_functionst &functions,
   message_handlert &message_handler);
 
+void remove_unused_functions( 
+  const irep_idt &current,
+  goto_functionst &functions,
+  message_handlert &message_handler);
+
 void find_used_functions(
   const irep_idt &current,
   goto_functionst &functions,

src/goto-programs/show_goto_functions.cpp

@@ -0,0 +1,104 @@
+/*******************************************************************\
+
+Module: Show goto functions
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+#include <iostream>
+
+#include <util/xml.h>
+#include <util/json.h>
+#include <util/i2string.h>
+#include <util/xml_expr.h>
+
+#include <langapi/language_util.h>
+
+#include "show_goto_functions.h"
+#include "goto_functions.h"
+#include "goto_model.h"
+
+/*******************************************************************\
+
+Function: cbmc_parseoptionst::show_goto_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_goto_functions(
+  const namespacet &ns,
+  ui_message_handlert::uit ui,
+  const goto_functionst &goto_functions)
+{
+  switch(ui)
+  {
+  case ui_message_handlert::XML_UI:
+  {
+    //This only prints the list of functions
+    xmlt xml_functions("functions");
+    for(goto_functionst::function_mapt::const_iterator
+          it=goto_functions.function_map.begin();
+        it!=goto_functions.function_map.end();
+        it++)
+    {
+      xmlt &xml_function=xml_functions.new_element("function");
+      xml_function.set_attribute("name", id2string(it->first)); 
+    }
+
+    std::cout << xml_functions << std::endl;
+  }
+  break;
+
+  case ui_message_handlert::JSON_UI:
+  {
+    //This only prints the list of functions
+    json_arrayt json_functions;
+    for(goto_functionst::function_mapt::const_iterator
+          it=goto_functions.function_map.begin();
+        it!=goto_functions.function_map.end();
+        it++)
+    {
+      json_objectt &json_function=
+        json_functions.push_back(jsont()).make_object();
+      json_function["name"]=json_stringt(id2string(it->first));
+    }
+    json_objectt json_result;
+    json_result["functions"]=json_functions;
+    std::cout << ",\n" << json_result;
+  }
+  break;
+      
+  case ui_message_handlert::PLAIN:
+    goto_functions.output(ns, std::cout);
+    break;
+  }
+}
+
+/*******************************************************************\
+
+Function: show_goto_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void show_goto_functions(
+  const goto_modelt &goto_model,
+  ui_message_handlert::uit ui)
+{
+  const namespacet ns(goto_model.symbol_table);
+  show_goto_functions(ns, ui, goto_model.goto_functions);
+}
+
+
+