diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index 89916e317d3..c8ef2a1a3f3 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/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 diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 8c96798bade..e8b302a0e86 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -17,6 +17,7 @@ Date: April 2016 #include #include +#include #include 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 +{ +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 +{ +public: + /// Maps class identifiers onto node indices + typedef std::unordered_map + 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 diff --git a/unit/Makefile b/unit/Makefile index 752300fc0c4..0be65a71b80 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/goto-programs/class_hierarchy_graph.cpp b/unit/goto-programs/class_hierarchy_graph.cpp new file mode 100644 index 00000000000..e2caef0bad9 --- /dev/null +++ b/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 +#include + +#include + +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); +}