Class hierarchy: add DOT output, unit tests

This also adds a goto-instrument command to output the class hierarchy in text or
DOT format. This is currently not usable with vanilla cbmc because none of its tools
can produce GOTO binaries from Java class files, but out-of-tree tools can, and JBMC
will surely gain support for GBF or its successors in the near future.

Author: smowton

regression/goto-instrument/class-hierarchy/dot.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--class-hierarchy --dot
+digraph class_hierarchy
+^EXIT=0$
+^SIGNAL=0$

regression/goto-instrument/class-hierarchy/main.c

@@ -0,0 +1,4 @@
+
+void main()
+{
+}

regression/goto-instrument/class-hierarchy/plain.desc

@@ -0,0 +1,5 @@
+CORE
+main.c
+--class-hierarchy
+^EXIT=0$
+^SIGNAL=0$

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/json.h>
 #include <util/exit_codes.h>
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
@@ -675,6 +676,18 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("class-hierarchy"))
+    {
+      class_hierarchyt hierarchy;
+      hierarchy(goto_model.symbol_table);
+      if(cmdline.isset("dot"))
+        hierarchy.output_dot(std::cout);
+      else
+        hierarchy.output(std::cout);
+
+      return 0;
+    }
+
     if(cmdline.isset("dot"))
     {
       namespacet ns(goto_model.symbol_table);
@@ -1474,6 +1487,7 @@ void goto_instrument_parse_optionst::help()
     " --call-graph                 show graph of function calls\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --reachable-call-graph       show graph of function calls potentially reachable from main function\n"
+    " --class-hierarchy            show class hierarchy\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -44,6 +44,7 @@ Author: Daniel Kroening, [email protected]
   "(max-var):(max-po-trans):(ignore-arrays)" \
   "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)(reachable-call-graph)" \
+  "(class-hierarchy)" \
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \

src/goto-programs/class_hierarchy.cpp

@@ -99,3 +99,23 @@ void class_hierarchyt::output(std::ostream &out) const
           << ch << '\n';
   }
 }
+
+/// Output class hierarchy in Graphviz DOT format
+/// \param ostr: stream to write DOT to
+void class_hierarchyt::output_dot(std::ostream &ostr) const
+{
+  ostr << "digraph class_hierarchy {\n"
+       << "  rankdir=BT;\n"
+       << "  node [fontsize=12 shape=box];\n";
+  for(const auto &c : class_map)
+  {
+    for(const auto &ch : c.second.parents)
+    {
+      ostr << "  \"" << c.first << "\" -> "
+           << "\"" << ch << "\" "
+           << " [arrowhead=\"vee\"];"
+           << "\n";
+    }
+  }
+  ostr << "}\n";
+}

src/goto-programs/class_hierarchy.h

@@ -52,6 +52,7 @@ class class_hierarchyt
   }
 
   void output(std::ostream &) const;
+  void output_dot(std::ostream &) const;
 
 protected:
   void get_children_trans_rec(const irep_idt &, idst &) const;

unit/Makefile

@@ -17,6 +17,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
+       goto-programs/class_hierarchy_output.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \

unit/goto-programs/HierarchyTest.class

@@ -0,0 +1,12 @@
+public class HierarchyTest {
+  // These fields exist only so the classloader will load all test classes:
+  HierarchyTestGrandchild field1;
+  HierarchyTestChild2 field2;
+}
+
+class HierarchyTestChild1 extends HierarchyTest {}
+
+class HierarchyTestChild2 extends HierarchyTest {}
+
+class HierarchyTestGrandchild extends HierarchyTestChild1
+  implements HierarchyTestInterface1, HierarchyTestInterface2 {}