Merge pull request #448 from thk123/feature/goto2json

Support for outputting JSON version of the GOTO program

Author: Daniel Kroening

src/goto-programs/Makefile

@@ -18,6 +18,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       graphml_witness.cpp remove_virtual_functions.cpp \
       class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \
       slice_global_inits.cpp goto_inline_class.cpp class_identifier.cpp \
+      show_goto_functions_json.cpp \
+      show_goto_functions_xml.cpp \
       remove_static_init_loops.cpp remove_instanceof.cpp
 
 INCLUDES= -I ..

src/goto-programs/goto_program.cpp

@@ -19,10 +19,15 @@ Author: Daniel Kroening, kroening@kroening.com
 Function: goto_programt::output_instruction
 
   Inputs:
+   ns - the namespace to resolve the expressions in
+   identifier - the identifier used to find a symbol to identify the
+                source language
+   out - the stream to write the goto string to
+   it - an iterator pointing to the instruction to convert
 
- Outputs:
+ Outputs: See below.
 
- Purpose:
+ Purpose: See below.
 
 \*******************************************************************/
 
@@ -32,51 +37,81 @@ std::ostream& goto_programt::output_instruction(
   std::ostream& out,
   instructionst::const_iterator it) const
 {
-  out << "        // " << it->location_number << " ";
+  return output_instruction(ns, identifier, out, *it);
+}
+
+/*******************************************************************\
+
+Function: goto_programt::output_instruction
+
+  Inputs:
+   ns - the namespace to resolve the expressions in
+   identifier - the identifier used to find a symbol to identify the
+                source language
+   out - the stream to write the goto string to
+   instruction - the instruction to convert
 
-  if(!it->source_location.is_nil())
-    out << it->source_location.as_string();
+ Outputs: Appends to out a two line representation of the instruction
+
+ Purpose: Writes to out a two line string representation of the specific
+          instruction. It is of the format:
+          // {location} file {source file} line {line in source file}
+          {representation of the instruction}
+
+\*******************************************************************/
+
+std::ostream &goto_programt::output_instruction(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  std::ostream &out,
+  const goto_program_templatet::instructiont &instruction) const
+{
+  out << "        // " << instruction.location_number << " ";
+
+  if(!instruction.source_location.is_nil())
+    out << instruction.source_location.as_string();
   else
     out << "no location";
 
   out << "\n";
 
-  if(!it->labels.empty())
+  if(!instruction.labels.empty())
   {
     out << "        // Labels:";
-    for(const auto &label : it->labels)
+    for(const auto &label : instruction.labels)
       out << " " << label;
 
     out << '\n';
   }
 
-  if(it->is_target())
-    out << std::setw(6) << it->target_number << ": ";
+  if(instruction.is_target())
+    out << std::setw(6) << instruction.target_number << ": ";
   else
     out << "        ";
 
-  switch(it->type)
+  switch(instruction.type)
   {
   case NO_INSTRUCTION_TYPE:
     out << "NO INSTRUCTION TYPE SET" << '\n';
     break;
 
   case GOTO:
-    if(!it->guard.is_true())
+    if(!instruction.guard.is_true())
     {
       out << "IF "
-          << from_expr(ns, identifier, it->guard)
+          << from_expr(ns, identifier, instruction.guard)
           << " THEN ";
     }
 
     out << "GOTO ";
 
     for(instructiont::targetst::const_iterator
-        gt_it=it->targets.begin();
-        gt_it!=it->targets.end();
+        gt_it=instruction.targets.begin();
+        gt_it!=instruction.targets.end();
         gt_it++)
     {
-      if(gt_it!=it->targets.begin()) out << ", ";
+      if(gt_it!=instruction.targets.begin())
+        out << ", ";
       out << (*gt_it)->target_number;
     }
 
@@ -89,20 +124,20 @@ std::ostream& goto_programt::output_instruction(
   case DEAD:
   case FUNCTION_CALL:
   case ASSIGN:
-    out << from_expr(ns, identifier, it->code) << '\n';
+    out << from_expr(ns, identifier, instruction.code) << '\n';
     break;
 
   case ASSUME:
   case ASSERT:
-    if(it->is_assume())
+    if(instruction.is_assume())
       out << "ASSUME ";
     else
       out << "ASSERT ";
 
     {
-      out << from_expr(ns, identifier, it->guard);
+      out << from_expr(ns, identifier, instruction.guard);
 
-      const irep_idt &comment=it->source_location.get_comment();
+      const irep_idt &comment=instruction.source_location.get_comment();
       if(comment!="") out << " // " << comment;
     }
 
@@ -126,34 +161,35 @@ std::ostream& goto_programt::output_instruction(
 
     {
       const irept::subt &exception_list=
-        it->code.find(ID_exception_list).get_sub();
+        instruction.code.find(ID_exception_list).get_sub();
 
       for(const auto &ex : exception_list)
         out << " " << ex.id();
     }
 
-    if(it->code.operands().size()==1)
-      out << ": " << from_expr(ns, identifier, it->code.op0());
+    if(instruction.code.operands().size()==1)
+      out << ": " << from_expr(ns, identifier, instruction.code.op0());
 
     out << '\n';
     break;
 
   case CATCH:
-    if(!it->targets.empty())
+    if(!instruction.targets.empty())
     {
       out << "CATCH-PUSH ";
 
       unsigned i=0;
       const irept::subt &exception_list=
-        it->code.find(ID_exception_list).get_sub();
-      assert(it->targets.size()==exception_list.size());
+        instruction.code.find(ID_exception_list).get_sub();
+      assert(instruction.targets.size()==exception_list.size());
       for(instructiont::targetst::const_iterator
-          gt_it=it->targets.begin();
-          gt_it!=it->targets.end();
+          gt_it=instruction.targets.begin();
+          gt_it!=instruction.targets.end();
           gt_it++,
           i++)
       {
-        if(gt_it!=it->targets.begin()) out << ", ";
+        if(gt_it!=instruction.targets.begin())
+          out << ", ";
         out << exception_list[i].id() << "->"
             << (*gt_it)->target_number;
       }
@@ -175,8 +211,8 @@ std::ostream& goto_programt::output_instruction(
   case START_THREAD:
     out << "START THREAD ";
 
-    if(it->targets.size()==1)
-      out << it->targets.front()->target_number;
+    if(instruction.targets.size()==1)
+      out << instruction.targets.front()->target_number;
 
     out << '\n';
     break;

src/goto-programs/goto_program.h

@@ -28,6 +28,12 @@ class goto_programt:public goto_program_templatet<codet, exprt>
     std::ostream &out,
     instructionst::const_iterator it) const;
 
+  std::ostream &output_instruction(
+    const class namespacet &ns,
+    const irep_idt &identifier,
+    std::ostream &out,
+    const instructiont &instruction) const;
+
   goto_programt() { }
 
   // get the variables in decl statements

src/goto-programs/goto_program_template.h

@@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 #include <set>
 #include <limits>
+#include <sstream>
+#include <string>
 
 #include <util/namespace.h>
 #include <util/symbol_table.h>
@@ -240,6 +242,13 @@ class goto_program_templatet
 
       return false;
     }
+
+    std::string to_string() const
+    {
+      std::ostringstream instruction_id_builder;
+      instruction_id_builder << type;
+      return instruction_id_builder.str();
+    }
   };
 
   typedef std::list<class instructiont> instructionst;

src/goto-programs/show_goto_functions.cpp

@@ -10,11 +10,14 @@ Author: Peter Schrammel
 
 #include <util/xml.h>
 #include <util/json.h>
+#include <util/json_expr.h>
 #include <util/xml_expr.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 
 #include <langapi/language_util.h>
+#include <goto-programs/show_goto_functions_json.h>
+#include <goto-programs/show_goto_functions_xml.h>
 
 #include "show_goto_functions.h"
 #include "goto_functions.h"
@@ -41,36 +44,15 @@ void show_goto_functions(
   {
   case ui_message_handlert::XML_UI:
   {
-    //This only prints the list of functions
-    xmlt xml_functions("functions");
-    forall_goto_functions(it, goto_functions)
-    {
-      xmlt &xml_function=xml_functions.new_element("function");
-      xml_function.set_attribute("name", id2string(it->first));
-    }
-
-    std::cout << xml_functions << std::endl;
+    show_goto_functions_xmlt xml_show_functions(ns);
+    xml_show_functions(goto_functions, std::cout);
   }
   break;
 
   case ui_message_handlert::JSON_UI:
   {
-    //This only prints the list of functions
-    json_arrayt json_functions;
-    forall_goto_functions(it, goto_functions)
-    {
-      json_objectt &json_function=
-        json_functions.push_back(jsont()).make_object();
-      json_function["name"]=json_stringt(id2string(it->first));
-      json_function["isBodyAvailable"]=
-        jsont::json_boolean(it->second.body_available());
-      bool is_internal=(has_prefix(id2string(it->first), CPROVER_PREFIX) ||
-                        it->first==ID__start);
-      json_function["isInternal"]=jsont::json_boolean(is_internal);
-    }
-    json_objectt json_result;
-    json_result["functions"]=json_functions;
-    std::cout << ",\n" << json_result;
+    show_goto_functions_jsont json_show_functions(ns);
+    json_show_functions(goto_functions, std::cout);
   }
   break;