Add class-hierarchy variant based on grapht

src/goto-programs/class_hierarchy.cpp

@@ -47,6 +47,41 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
   }
 }
 
+/// Populate the class hierarchy graph, such that there is a node for every
+/// struct type in the symbol table and an edge representing each superclass
+/// <-> subclass relationship, pointing from parent to child.
+/// \param symbol_table: global symbol table, which will be searched for struct
+///   types.
+void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
+{
+  // Add nodes for all classes:
+  forall_symbols(it, symbol_table.symbols)
+  {
+    if(it->second.is_type && it->second.type.id() == ID_struct)
+    {
+      node_indext new_node_index = add_node();
+      nodes_by_name[it->first] = new_node_index;
+      (*this)[new_node_index].class_identifier = it->first;
+    }
+  }
+
+  // Add parent -> child edges:
+  forall_symbols(it, symbol_table.symbols)
+  {
+    if(it->second.is_type && it->second.type.id() == ID_struct)
+    {
+      const class_typet &class_type = to_class_type(it->second.type);
+
+      for(const auto &base : class_type.bases())
+      {
+        const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
+        if(!parent.empty())
+          add_edge(nodes_by_name.at(parent), nodes_by_name.at(it->first));
+      }
+    }
+  }
+}
+
 void class_hierarchyt::get_children_trans_rec(
   const irep_idt &c,
   idst &dest) const

src/goto-programs/class_hierarchy.h

@@ -17,6 +17,7 @@ Date: April 2016
 #include <iosfwd>
 #include <map>
 
+#include <util/graph.h>
 #include <util/namespace.h>
 
 class class_hierarchyt
@@ -59,4 +60,35 @@ class class_hierarchyt
   void get_parents_trans_rec(const irep_idt &, idst &) const;
 };
 
+/// Class hierarchy graph node: simply contains a class identifier.
+class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
+{
+public:
+  /// Class ID for this node
+  irep_idt class_identifier;
+};
+
+/// Class hierarchy, represented using grapht and therefore suitable for use
+/// with generic graph algorithms.
+class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
+{
+public:
+  /// Maps class identifiers onto node indices
+  typedef std::unordered_map<irep_idt, node_indext, irep_id_hash>
+    nodes_by_namet;
+
+  void populate(const symbol_tablet &);
+
+  /// Get map from class identifier to node index
+  /// \return map from class identifier to node index
+  const nodes_by_namet &get_nodes_by_class_identifier() const
+  {
+    return nodes_by_name;
+  }
+
+private:
+  /// Maps class identifiers onto node indices
+  nodes_by_namet nodes_by_name;
+};
+
 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H

unit/Makefile

@@ -18,6 +18,7 @@ SRC += unit_tests.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 \
+       goto-programs/class_hierarchy_graph.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/class_hierarchy_graph.cpp

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+ Module: Unit tests for class_hierarchy_grapht
+
+ Author: Diffblue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <testing-utils/load_java_class.h>
+
+#include <goto-programs/class_hierarchy.h>
+
+void require_parent_child_relationship(
+  const std::string &parent_raw,
+  const std::string &child_raw,
+  const class_hierarchy_grapht &hierarchy)
+{
+  irep_idt parent = "java::" + parent_raw;
+  irep_idt child = "java::" + child_raw;
+
+  const class_hierarchy_grapht::nodes_by_namet &nodes_map =
+    hierarchy.get_nodes_by_class_identifier();
+  REQUIRE(nodes_map.count(parent) != 0);
+  REQUIRE(nodes_map.count(child) != 0);
+  REQUIRE(hierarchy.has_edge(nodes_map.at(parent), nodes_map.at(child)));
+}
+
+SCENARIO(
+  "Output a simple class hierarchy"
+  "[core][goto-programs][class_hierarchy_graph]")
+{
+  symbol_tablet symbol_table =
+    load_java_class("HierarchyTest", "goto-programs/");
+  class_hierarchy_grapht hierarchy;
+  hierarchy.populate(symbol_table);
+
+  require_parent_child_relationship(
+    "HierarchyTest", "HierarchyTestChild1", hierarchy);
+  require_parent_child_relationship(
+    "HierarchyTest", "HierarchyTestChild2", hierarchy);
+  require_parent_child_relationship(
+    "HierarchyTestChild1", "HierarchyTestGrandchild", hierarchy);
+  require_parent_child_relationship(
+    "HierarchyTestInterface1", "HierarchyTestGrandchild", hierarchy);
+  require_parent_child_relationship(
+    "HierarchyTestInterface2", "HierarchyTestGrandchild", hierarchy);
+}