diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp index ec41314eb92..bd952615c56 100644 --- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp @@ -27,7 +27,7 @@ void require_parent_child_relationship( } SCENARIO( - "Output a simple class hierarchy" + "Output a simple class hierarchy graph", "[core][goto-programs][class_hierarchy_graph]") { symbol_tablet symbol_table = @@ -46,3 +46,91 @@ SCENARIO( require_parent_child_relationship( "HierarchyTestInterface2", "HierarchyTestGrandchild", hierarchy); } + +SCENARIO( + "class_hierarchy_graph", + "[core][goto-programs][class_hierarchy_graph]") +{ + symbol_tablet symbol_table = + load_java_class("HierarchyTest", "./java_bytecode/goto-programs/"); + class_hierarchy_grapht hierarchy; + hierarchy.populate(symbol_table); + + WHEN("Retrieving direct children of a given class") + { + const class_hierarchy_grapht::idst ht_direct_children = + hierarchy.get_direct_children("java::HierarchyTest"); + THEN("The correct list of direct children should be returned") + { + REQUIRE(ht_direct_children.size() == 2); + REQUIRE( + find( + ht_direct_children.begin(), + ht_direct_children.end(), + "java::HierarchyTestChild1") != ht_direct_children.end()); + REQUIRE( + find( + ht_direct_children.begin(), + ht_direct_children.end(), + "java::HierarchyTestChild2") != ht_direct_children.end()); + } + } + WHEN("Retrieving all children of a given class") + { + const class_hierarchy_grapht::idst ht_all_children = + hierarchy.get_children_trans("java::HierarchyTest"); + THEN("The correct list of children should be returned") + { + REQUIRE(ht_all_children.size() == 3); + REQUIRE( + find( + ht_all_children.begin(), + ht_all_children.end(), + "java::HierarchyTestChild1") != ht_all_children.end()); + REQUIRE( + find( + ht_all_children.begin(), + ht_all_children.end(), + "java::HierarchyTestChild2") != ht_all_children.end()); + REQUIRE( + find( + ht_all_children.begin(), + ht_all_children.end(), + "java::HierarchyTestGrandchild") != ht_all_children.end()); + } + } + WHEN("Retrieving all parents of a given class") + { + const class_hierarchy_grapht::idst htg_all_parents = + hierarchy.get_parents_trans("java::HierarchyTestGrandchild"); + THEN("The correct list of parents should be returned") + { + REQUIRE(htg_all_parents.size() == 5); + REQUIRE( + find( + htg_all_parents.begin(), + htg_all_parents.end(), + "java::HierarchyTestChild1") != htg_all_parents.end()); + REQUIRE( + find( + htg_all_parents.begin(), + htg_all_parents.end(), + "java::HierarchyTest") != htg_all_parents.end()); + REQUIRE( + find( + htg_all_parents.begin(), + htg_all_parents.end(), + "java::HierarchyTestInterface1") != htg_all_parents.end()); + REQUIRE( + find( + htg_all_parents.begin(), + htg_all_parents.end(), + "java::HierarchyTestInterface2") != htg_all_parents.end()); + REQUIRE( + find( + htg_all_parents.begin(), + htg_all_parents.end(), + "java::java.lang.Object") != htg_all_parents.end()); + } + } +} diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp index cb8566296f8..c170d481527 100644 --- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp @@ -30,7 +30,7 @@ void require_parent_child_relationship( } SCENARIO( - "Output a simple class hierarchy" + "Output a simple class hierarchy", "[core][goto-programs][class_hierarchy]") { symbol_tablet symbol_table = diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index e5fbb743019..cb9106c818d 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -13,43 +13,13 @@ Date: April 2016 #include "class_hierarchy.h" +#include #include #include #include #include -/// Looks for all the struct types in the symbol table and construct a map from -/// class names to a data structure that contains lists of parent and child -/// classes for each struct type (ie class). -/// \param symbol_table: The symbol table to analyze -void class_hierarchyt::operator()(const symbol_tablet &symbol_table) -{ - for(const auto &symbol_pair : symbol_table.symbols) - { - if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct) - { - const struct_typet &struct_type = to_struct_type(symbol_pair.second.type); - - class_map[symbol_pair.first].is_abstract = - struct_type.get_bool(ID_abstract); - - const irept::subt &bases= - struct_type.find(ID_bases).get_sub(); - - for(const auto &base : bases) - { - irep_idt parent=base.find(ID_type).get(ID_identifier); - if(parent.empty()) - continue; - - class_map[parent].children.push_back(symbol_pair.first); - class_map[symbol_pair.first].parents.push_back(parent); - } - } - } -} - /// 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. @@ -88,6 +58,70 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table) } } +/// Helper function that converts a vector of node_indext to a vector of ids +/// that are stored in the corresponding nodes in the graph. +class_hierarchy_grapht::idst class_hierarchy_grapht::ids_from_indices( + const std::vector &node_indices) const +{ + idst result; + std::transform( + node_indices.begin(), + node_indices.end(), + back_inserter(result), + [&](const node_indext &node_index) { + return (*this)[node_index].class_identifier; + }); + return result; +} + +/// Get all the classes that directly (i.e. in one step) inherit from class c. +/// \param c: The class to consider +/// \return A list containing ids of all direct children of c. +class_hierarchy_grapht::idst +class_hierarchy_grapht::get_direct_children(const irep_idt &c) const +{ + const node_indext &node_index = nodes_by_name.at(c); + const auto &child_indices = get_successors(node_index); + return ids_from_indices(child_indices); +} + +/// Helper function for `get_children_trans` and `get_parents_trans` +class_hierarchy_grapht::idst class_hierarchy_grapht::get_other_reachable_ids( + const irep_idt &c, + bool forwards) const +{ + idst direct_child_ids; + const node_indext &node_index = nodes_by_name.at(c); + const auto &reachable_indices = get_reachable(node_index, forwards); + auto reachable_ids = ids_from_indices(reachable_indices); + // Remove c itself from the list + // TODO Adding it first and then removing it is not ideal. It would be + // better to define a function grapht::get_other_reachable and directly use + // that here. + reachable_ids.erase( + std::remove(reachable_ids.begin(), reachable_ids.end(), c), + reachable_ids.end()); + return reachable_ids; +} + +/// Get all the classes that inherit (directly or indirectly) from class c. +/// \param c: The class to consider +/// \return A list containing ids of all classes that eventually inherit from c. +class_hierarchy_grapht::idst +class_hierarchy_grapht::get_children_trans(const irep_idt &c) const +{ + return get_other_reachable_ids(c, true); +} + +/// Get all the classes that class c inherits from (directly or indirectly). +/// \param c: The class to consider +/// \return A list of class ids that c eventually inherits from. +class_hierarchy_grapht::idst +class_hierarchy_grapht::get_parents_trans(const irep_idt &c) const +{ + return get_other_reachable_ids(c, false); +} + void class_hierarchyt::get_children_trans_rec( const irep_idt &c, idst &dest) const @@ -105,7 +139,37 @@ void class_hierarchyt::get_children_trans_rec( get_children_trans_rec(child, dest); } -/// Get all the classes that inherit (directly or indirectly) from class c. The +/// Looks for all the struct types in the symbol table and construct a map from +/// class names to a data structure that contains lists of parent and child +/// classes for each struct type (ie class). +/// \param symbol_table: The symbol table to analyze +void class_hierarchyt::operator()(const symbol_tablet &symbol_table) +{ + for(const auto &symbol_pair : symbol_table.symbols) + { + if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct) + { + const struct_typet &struct_type = to_struct_type(symbol_pair.second.type); + + class_map[symbol_pair.first].is_abstract = + struct_type.get_bool(ID_abstract); + + const irept::subt &bases = struct_type.find(ID_bases).get_sub(); + + for(const auto &base : bases) + { + irep_idt parent = base.find(ID_type).get(ID_identifier); + if(parent.empty()) + continue; + + class_map[parent].children.push_back(symbol_pair.first); + class_map[symbol_pair.first].parents.push_back(parent); + } + } + } +} + +/// Get all the classes that class c inherits from (directly or indirectly). The /// first element(s) will be the immediate parents of c, though after this /// the order is all the parents of the first immediate parent /// \param c: The class to consider diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index daf071451bf..eae38a47a80 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -34,6 +34,12 @@ class symbol_tablet; class json_stream_arrayt; class message_handlert; +/// Non-graph-based representation of the class hierarchy. +/// \deprecated `class_hierarchy_grapht` is a more advanced graph-based +/// representation of the class hierarchy and its use is preferred over +/// `class_hierarchy_classt`. +/// \todo Implement missing functions from `class_hierarchyt` in +/// `class_hierarchy_grapht` so that `class_hierarchyt` can be fully replaced. class class_hierarchyt { public: @@ -89,6 +95,8 @@ class class_hierarchy_graph_nodet : public graph_nodet class class_hierarchy_grapht : public grapht { public: + typedef std::vector idst; + /// Maps class identifiers onto node indices typedef std::unordered_map nodes_by_namet; @@ -101,9 +109,19 @@ class class_hierarchy_grapht : public grapht return nodes_by_name; } + idst get_direct_children(const irep_idt &c) const; + + idst get_children_trans(const irep_idt &c) const; + + idst get_parents_trans(const irep_idt &c) const; + private: /// Maps class identifiers onto node indices nodes_by_namet nodes_by_name; + + idst ids_from_indices(const std::vector &nodes) const; + + idst get_other_reachable_ids(const irep_idt &c, bool forwards) const; }; /// Output the class hierarchy