Skip to content

Commit bbf0d02

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #2482 from antlechner/antonia/direct-children-of-class
Make direct children of a class publicly available
2 parents c982c21 + 9af7ef1 commit bbf0d02

File tree

4 files changed

+204
-34
lines changed

4 files changed

+204
-34
lines changed

‎jbmc/unit/java_bytecode/goto-programs/class_hierarchy_graph.cpp

Lines changed: 89 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ void require_parent_child_relationship(
2727
}
2828

2929
SCENARIO(
30-
"Output a simple class hierarchy"
30+
"Output a simple class hierarchy graph",
3131
"[core][goto-programs][class_hierarchy_graph]")
3232
{
3333
symbol_tablet symbol_table =
@@ -46,3 +46,91 @@ SCENARIO(
4646
require_parent_child_relationship(
4747
"HierarchyTestInterface2", "HierarchyTestGrandchild", hierarchy);
4848
}
49+
50+
SCENARIO(
51+
"class_hierarchy_graph",
52+
"[core][goto-programs][class_hierarchy_graph]")
53+
{
54+
symbol_tablet symbol_table =
55+
load_java_class("HierarchyTest", "./java_bytecode/goto-programs/");
56+
class_hierarchy_grapht hierarchy;
57+
hierarchy.populate(symbol_table);
58+
59+
WHEN("Retrieving direct children of a given class")
60+
{
61+
const class_hierarchy_grapht::idst ht_direct_children =
62+
hierarchy.get_direct_children("java::HierarchyTest");
63+
THEN("The correct list of direct children should be returned")
64+
{
65+
REQUIRE(ht_direct_children.size() == 2);
66+
REQUIRE(
67+
find(
68+
ht_direct_children.begin(),
69+
ht_direct_children.end(),
70+
"java::HierarchyTestChild1") != ht_direct_children.end());
71+
REQUIRE(
72+
find(
73+
ht_direct_children.begin(),
74+
ht_direct_children.end(),
75+
"java::HierarchyTestChild2") != ht_direct_children.end());
76+
}
77+
}
78+
WHEN("Retrieving all children of a given class")
79+
{
80+
const class_hierarchy_grapht::idst ht_all_children =
81+
hierarchy.get_children_trans("java::HierarchyTest");
82+
THEN("The correct list of children should be returned")
83+
{
84+
REQUIRE(ht_all_children.size() == 3);
85+
REQUIRE(
86+
find(
87+
ht_all_children.begin(),
88+
ht_all_children.end(),
89+
"java::HierarchyTestChild1") != ht_all_children.end());
90+
REQUIRE(
91+
find(
92+
ht_all_children.begin(),
93+
ht_all_children.end(),
94+
"java::HierarchyTestChild2") != ht_all_children.end());
95+
REQUIRE(
96+
find(
97+
ht_all_children.begin(),
98+
ht_all_children.end(),
99+
"java::HierarchyTestGrandchild") != ht_all_children.end());
100+
}
101+
}
102+
WHEN("Retrieving all parents of a given class")
103+
{
104+
const class_hierarchy_grapht::idst htg_all_parents =
105+
hierarchy.get_parents_trans("java::HierarchyTestGrandchild");
106+
THEN("The correct list of parents should be returned")
107+
{
108+
REQUIRE(htg_all_parents.size() == 5);
109+
REQUIRE(
110+
find(
111+
htg_all_parents.begin(),
112+
htg_all_parents.end(),
113+
"java::HierarchyTestChild1") != htg_all_parents.end());
114+
REQUIRE(
115+
find(
116+
htg_all_parents.begin(),
117+
htg_all_parents.end(),
118+
"java::HierarchyTest") != htg_all_parents.end());
119+
REQUIRE(
120+
find(
121+
htg_all_parents.begin(),
122+
htg_all_parents.end(),
123+
"java::HierarchyTestInterface1") != htg_all_parents.end());
124+
REQUIRE(
125+
find(
126+
htg_all_parents.begin(),
127+
htg_all_parents.end(),
128+
"java::HierarchyTestInterface2") != htg_all_parents.end());
129+
REQUIRE(
130+
find(
131+
htg_all_parents.begin(),
132+
htg_all_parents.end(),
133+
"java::java.lang.Object") != htg_all_parents.end());
134+
}
135+
}
136+
}

‎jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ void require_parent_child_relationship(
3030
}
3131

3232
SCENARIO(
33-
"Output a simple class hierarchy"
33+
"Output a simple class hierarchy",
3434
"[core][goto-programs][class_hierarchy]")
3535
{
3636
symbol_tablet symbol_table =

‎src/goto-programs/class_hierarchy.cpp

Lines changed: 96 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -13,43 +13,13 @@ Date: April 2016
1313

1414
#include "class_hierarchy.h"
1515

16+
#include <iterator>
1617
#include <ostream>
1718

1819
#include <util/json_stream.h>
1920
#include <util/std_types.h>
2021
#include <util/symbol_table.h>
2122

22-
/// Looks for all the struct types in the symbol table and construct a map from
23-
/// class names to a data structure that contains lists of parent and child
24-
/// classes for each struct type (ie class).
25-
/// \param symbol_table: The symbol table to analyze
26-
void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
27-
{
28-
for(const auto &symbol_pair : symbol_table.symbols)
29-
{
30-
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
31-
{
32-
const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
33-
34-
class_map[symbol_pair.first].is_abstract =
35-
struct_type.get_bool(ID_abstract);
36-
37-
const irept::subt &bases=
38-
struct_type.find(ID_bases).get_sub();
39-
40-
for(const auto &base : bases)
41-
{
42-
irep_idt parent=base.find(ID_type).get(ID_identifier);
43-
if(parent.empty())
44-
continue;
45-
46-
class_map[parent].children.push_back(symbol_pair.first);
47-
class_map[symbol_pair.first].parents.push_back(parent);
48-
}
49-
}
50-
}
51-
}
52-
5323
/// Populate the class hierarchy graph, such that there is a node for every
5424
/// struct type in the symbol table and an edge representing each superclass
5525
/// <-> subclass relationship, pointing from parent to child.
@@ -88,6 +58,70 @@ void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
8858
}
8959
}
9060

61+
/// Helper function that converts a vector of node_indext to a vector of ids
62+
/// that are stored in the corresponding nodes in the graph.
63+
class_hierarchy_grapht::idst class_hierarchy_grapht::ids_from_indices(
64+
const std::vector<node_indext> &node_indices) const
65+
{
66+
idst result;
67+
std::transform(
68+
node_indices.begin(),
69+
node_indices.end(),
70+
back_inserter(result),
71+
[&](const node_indext &node_index) {
72+
return (*this)[node_index].class_identifier;
73+
});
74+
return result;
75+
}
76+
77+
/// Get all the classes that directly (i.e. in one step) inherit from class c.
78+
/// \param c: The class to consider
79+
/// \return A list containing ids of all direct children of c.
80+
class_hierarchy_grapht::idst
81+
class_hierarchy_grapht::get_direct_children(const irep_idt &c) const
82+
{
83+
const node_indext &node_index = nodes_by_name.at(c);
84+
const auto &child_indices = get_successors(node_index);
85+
return ids_from_indices(child_indices);
86+
}
87+
88+
/// Helper function for `get_children_trans` and `get_parents_trans`
89+
class_hierarchy_grapht::idst class_hierarchy_grapht::get_other_reachable_ids(
90+
const irep_idt &c,
91+
bool forwards) const
92+
{
93+
idst direct_child_ids;
94+
const node_indext &node_index = nodes_by_name.at(c);
95+
const auto &reachable_indices = get_reachable(node_index, forwards);
96+
auto reachable_ids = ids_from_indices(reachable_indices);
97+
// Remove c itself from the list
98+
// TODO Adding it first and then removing it is not ideal. It would be
99+
// better to define a function grapht::get_other_reachable and directly use
100+
// that here.
101+
reachable_ids.erase(
102+
std::remove(reachable_ids.begin(), reachable_ids.end(), c),
103+
reachable_ids.end());
104+
return reachable_ids;
105+
}
106+
107+
/// Get all the classes that inherit (directly or indirectly) from class c.
108+
/// \param c: The class to consider
109+
/// \return A list containing ids of all classes that eventually inherit from c.
110+
class_hierarchy_grapht::idst
111+
class_hierarchy_grapht::get_children_trans(const irep_idt &c) const
112+
{
113+
return get_other_reachable_ids(c, true);
114+
}
115+
116+
/// Get all the classes that class c inherits from (directly or indirectly).
117+
/// \param c: The class to consider
118+
/// \return A list of class ids that c eventually inherits from.
119+
class_hierarchy_grapht::idst
120+
class_hierarchy_grapht::get_parents_trans(const irep_idt &c) const
121+
{
122+
return get_other_reachable_ids(c, false);
123+
}
124+
91125
void class_hierarchyt::get_children_trans_rec(
92126
const irep_idt &c,
93127
idst &dest) const
@@ -105,7 +139,37 @@ void class_hierarchyt::get_children_trans_rec(
105139
get_children_trans_rec(child, dest);
106140
}
107141

108-
/// Get all the classes that inherit (directly or indirectly) from class c. The
142+
/// Looks for all the struct types in the symbol table and construct a map from
143+
/// class names to a data structure that contains lists of parent and child
144+
/// classes for each struct type (ie class).
145+
/// \param symbol_table: The symbol table to analyze
146+
void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
147+
{
148+
for(const auto &symbol_pair : symbol_table.symbols)
149+
{
150+
if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
151+
{
152+
const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
153+
154+
class_map[symbol_pair.first].is_abstract =
155+
struct_type.get_bool(ID_abstract);
156+
157+
const irept::subt &bases = struct_type.find(ID_bases).get_sub();
158+
159+
for(const auto &base : bases)
160+
{
161+
irep_idt parent = base.find(ID_type).get(ID_identifier);
162+
if(parent.empty())
163+
continue;
164+
165+
class_map[parent].children.push_back(symbol_pair.first);
166+
class_map[symbol_pair.first].parents.push_back(parent);
167+
}
168+
}
169+
}
170+
}
171+
172+
/// Get all the classes that class c inherits from (directly or indirectly). The
109173
/// first element(s) will be the immediate parents of c, though after this
110174
/// the order is all the parents of the first immediate parent
111175
/// \param c: The class to consider

‎src/goto-programs/class_hierarchy.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,12 @@ class symbol_tablet;
3434
class json_stream_arrayt;
3535
class message_handlert;
3636

37+
/// Non-graph-based representation of the class hierarchy.
38+
/// \deprecated `class_hierarchy_grapht` is a more advanced graph-based
39+
/// representation of the class hierarchy and its use is preferred over
40+
/// `class_hierarchy_classt`.
41+
/// \todo Implement missing functions from `class_hierarchyt` in
42+
/// `class_hierarchy_grapht` so that `class_hierarchyt` can be fully replaced.
3743
class class_hierarchyt
3844
{
3945
public:
@@ -89,6 +95,8 @@ class class_hierarchy_graph_nodet : public graph_nodet<empty_edget>
8995
class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
9096
{
9197
public:
98+
typedef std::vector<irep_idt> idst;
99+
92100
/// Maps class identifiers onto node indices
93101
typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;
94102

@@ -101,9 +109,19 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
101109
return nodes_by_name;
102110
}
103111

112+
idst get_direct_children(const irep_idt &c) const;
113+
114+
idst get_children_trans(const irep_idt &c) const;
115+
116+
idst get_parents_trans(const irep_idt &c) const;
117+
104118
private:
105119
/// Maps class identifiers onto node indices
106120
nodes_by_namet nodes_by_name;
121+
122+
idst ids_from_indices(const std::vector<node_indext> &nodes) const;
123+
124+
idst get_other_reachable_ids(const irep_idt &c, bool forwards) const;
107125
};
108126

109127
/// Output the class hierarchy

0 commit comments

Comments
 (0)