Basic implementation for the XML class

Produces an XML version of the show-goto-functions flag (i.e. when
running a tool with the --xml-ui flag).

Author: thk123

src/goto-programs/Makefile

@@ -17,7 +17,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.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 show_goto_functions_json.cpp
+      slice_global_inits.cpp goto_inline_class.cpp show_goto_functions_json.cpp \
+      show_goto_functions_xml.cpp
 
 INCLUDES= -I ..
 

src/goto-programs/show_goto_functions.cpp

@@ -17,6 +17,7 @@ Author: Peter Schrammel
 
 #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"
@@ -43,15 +44,8 @@ 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.print_goto_functions(goto_functions, std::cout);
   }
   break;
 

src/goto-programs/show_goto_functions_xml.cpp

@@ -0,0 +1,146 @@
+/*******************************************************************\
+
+Module: Goto Program
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#include <goto-programs/show_goto_functions_xml.h>
+#include <iostream>
+#include <sstream>
+
+
+#include <util/xml_expr.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+
+#include <langapi/language_util.h>
+
+#include "goto_functions.h"
+#include "goto_model.h"
+
+/*******************************************************************\
+
+Function: show_goto_functions_xmlt::show_goto_functions_xmlt
+
+  Inputs:
+   ns - the namespace to use to resolve names with
+
+ Outputs:
+
+ Purpose: For outputing the GOTO program in a readable xml format.
+
+\*******************************************************************/
+
+show_goto_functions_xmlt::show_goto_functions_xmlt(const namespacet &ns)
+  : ns(ns)
+{}
+
+/*******************************************************************\
+
+Function: show_goto_functions_xmlt::show_goto_functions
+
+  Inputs:
+   goto_functions - the goto functions that make up the program
+
+ Outputs:
+
+ Purpose: Walks through all of the functions in the program and returns
+          an xml object representing all their functions. Produces output
+          like this:
+          <functions>
+            <function name=main, isBodyAvaliable=true, isInternal=false>
+              <instructions>
+                <instruction id=ASSIGN>
+                  <location file="main.c" line="14"/>
+                  <instructionValue>// adsakjsdl
+                     x=y</instructionValue>
+                </instruction>
+              </instructions>
+            </function>
+          </functions>
+
+\*******************************************************************/
+
+xmlt show_goto_functions_xmlt::get_goto_functions(
+  const goto_functionst &goto_functions)
+{
+  xmlt xml_functions=xmlt("functions");
+  for(const auto &function_entry : goto_functions.function_map)
+  {
+    const irep_idt &function_name=function_entry.first;
+    const goto_functionst::goto_functiont &function=function_entry.second;
+
+    xmlt &xml_function=xml_functions.new_element("function");
+    xml_function.set_attribute("name", id2string(function_name));
+    xml_function.set_attribute_bool(
+      "isBodyAvailable", function.body_available());
+    bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
+                      function_name==ID__start);
+    xml_function.set_attribute_bool("isInternal", is_internal);
+
+    if(function.body_available())
+    {
+      xmlt &xml_instructions=xml_function.new_element("instructions");
+      for(const goto_programt::instructiont &instruction :
+        function.body.instructions)
+      {
+        xmlt &instruction_entry=xml_instructions.new_element("instruction");
+
+        std::ostringstream instruction_id_builder;
+        instruction_id_builder << instruction.type;
+
+        instruction_entry.set_attribute(
+          "instructionId", instruction_id_builder.str());
+
+        if(instruction.code.source_location().is_not_nil())
+        {
+          instruction_entry.new_element(
+            xml(instruction.code.source_location()));
+        }
+
+        std::ostringstream instruction_builder;
+        function.body.output_instruction(
+          ns, function_name, instruction_builder, instruction);
+
+        xmlt &instruction_value=
+          instruction_entry.new_element("instructionValue");
+        instruction_value.data=instruction_builder.str();
+        instruction_value.elements.clear();
+      }
+    }
+  }
+  return xml_functions;
+}
+
+/*******************************************************************\
+
+Function: show_goto_functions_xmlt::print_goto_functions
+
+  Inputs:
+   goto_functions - the goto functions that make up the program
+   out - the stream to write the object to
+   append - should a command and newline be appended to the stream
+            before writing the xml object. Defaults to true
+
+ Outputs:
+
+ Purpose: Print the xml object generated by
+          show_goto_functions_xmlt::show_goto_functions to the provided
+          stream (e.g. std::cout)
+
+\*******************************************************************/
+
+void show_goto_functions_xmlt::print_goto_functions(
+  const goto_functionst &goto_functions,
+  std::ostream &out,
+  bool append /*=true*/)
+{
+  const xmlt &function_output=get_goto_functions(goto_functions);
+  if(append)
+  {
+    out << "\n";
+  }
+  out << get_goto_functions(goto_functions);
+}

src/goto-programs/show_goto_functions_xml.h

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Goto Program
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H
+#define CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H
+
+#include <util/xml.h>
+
+class goto_functionst;
+class namespacet;
+
+class show_goto_functions_xmlt
+{
+public:
+  explicit show_goto_functions_xmlt(const namespacet &ns);
+
+  xmlt get_goto_functions(const goto_functionst &goto_functions);
+  void print_goto_functions(
+    const goto_functionst &goto_functions, std::ostream &out, bool append=true);
+
+private:
+  const namespacet &ns;
+};
+
+#endif // CPROVER_GOTO_PROGRAMS_SHOW_GOTO_FUNCTIONS_XML_H