cprover
class_hierarchy.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Class Hierarchy
4 
5 Author: Daniel Kroening
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "class_hierarchy.h"
15 
16 #include <iterator>
17 #include <ostream>
18 
19 #include <util/json_stream.h>
20 #include <util/std_types.h>
21 #include <util/symbol_table.h>
22 
29 {
30  // Add nodes for all classes:
31  for(const auto &symbol_pair : symbol_table.symbols)
32  {
33  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
34  {
35  node_indext new_node_index = add_node();
36  nodes_by_name[symbol_pair.first] = new_node_index;
37  (*this)[new_node_index].class_identifier = symbol_pair.first;
38  }
39  }
40 
41  // Add parent -> child edges:
42  for(const auto &symbol_pair : symbol_table.symbols)
43  {
44  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
45  {
46  const class_typet &class_type = to_class_type(symbol_pair.second.type);
47 
48  for(const auto &base : class_type.bases())
49  {
50  const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
51  if(!parent.empty())
52  {
53  const auto parent_node_it = nodes_by_name.find(parent);
55  parent_node_it != nodes_by_name.end(),
56  "parent class not in symbol table");
57  add_edge(parent_node_it->second, nodes_by_name.at(symbol_pair.first));
58  }
59  }
60  }
61  }
62 }
63 
67  const std::vector<node_indext> &node_indices) const
68 {
69  idst result;
70  std::transform(
71  node_indices.begin(),
72  node_indices.end(),
73  back_inserter(result),
74  [&](const node_indext &node_index) {
75  return (*this)[node_index].class_identifier;
76  });
77  return result;
78 }
79 
85 {
86  const node_indext &node_index = nodes_by_name.at(c);
87  const auto &child_indices = get_successors(node_index);
88  return ids_from_indices(child_indices);
89 }
90 
93  const irep_idt &c,
94  bool forwards) const
95 {
96  idst direct_child_ids;
97  const node_indext &node_index = nodes_by_name.at(c);
98  const auto &reachable_indices = get_reachable(node_index, forwards);
99  auto reachable_ids = ids_from_indices(reachable_indices);
100  // Remove c itself from the list
101  // TODO Adding it first and then removing it is not ideal. It would be
102  // better to define a function grapht::get_other_reachable and directly use
103  // that here.
104  reachable_ids.erase(
105  std::remove(reachable_ids.begin(), reachable_ids.end(), c),
106  reachable_ids.end());
107  return reachable_ids;
108 }
109 
115 {
116  return get_other_reachable_ids(c, true);
117 }
118 
124 {
125  return get_other_reachable_ids(c, false);
126 }
127 
129  const irep_idt &c,
130  idst &dest) const
131 {
132  class_mapt::const_iterator it=class_map.find(c);
133  if(it==class_map.end())
134  return;
135  const entryt &entry=it->second;
136 
137  for(const auto &child : entry.children)
138  dest.push_back(child);
139 
140  // recursive calls
141  for(const auto &child : entry.children)
142  get_children_trans_rec(child, dest);
143 }
144 
150 {
151  for(const auto &symbol_pair : symbol_table.symbols)
152  {
153  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
154  {
155  const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
156 
157  class_map[symbol_pair.first].is_abstract =
158  struct_type.get_bool(ID_abstract);
159 
160  const irept::subt &bases = struct_type.find(ID_bases).get_sub();
161 
162  for(const auto &base : bases)
163  {
164  irep_idt parent = base.find(ID_type).get(ID_identifier);
165  if(parent.empty())
166  continue;
167 
168  class_map[parent].children.push_back(symbol_pair.first);
169  class_map[symbol_pair.first].parents.push_back(parent);
170  }
171  }
172  }
173 }
174 
181  const irep_idt &c,
182  idst &dest) const
183 {
184  class_mapt::const_iterator it=class_map.find(c);
185  if(it==class_map.end())
186  return;
187  const entryt &entry=it->second;
188 
189  for(const auto &child : entry.parents)
190  dest.push_back(child);
191 
192  // recursive calls
193  for(const auto &child : entry.parents)
194  get_parents_trans_rec(child, dest);
195 }
196 
200 void class_hierarchyt::output(std::ostream &out, bool children_only) const
201 {
202  for(const auto &c : class_map)
203  {
204  out << c.first << (c.second.is_abstract ? " (abstract)" : "") << ":\n";
205  if(!children_only)
206  {
207  out << " parents:\n";
208  for(const auto &pa : c.second.parents)
209  out << " " << pa << '\n';
210  }
211  out << " children:\n";
212  for(const auto &ch : c.second.children)
213  out << " " << ch << '\n';
214  }
215 }
216 
219 void class_hierarchyt::output_dot(std::ostream &ostr) const
220 {
221  ostr << "digraph class_hierarchy {\n"
222  << " rankdir=BT;\n"
223  << " node [fontsize=12 shape=box];\n";
224  for(const auto &c : class_map)
225  {
226  for(const auto &ch : c.second.parents)
227  {
228  ostr << " \"" << c.first << "\" -> "
229  << "\"" << ch << "\" "
230  << " [arrowhead=\"vee\"];"
231  << "\n";
232  }
233  }
234  ostr << "}\n";
235 }
236 
241  json_stream_arrayt &json_stream,
242  bool children_only) const
243 {
244  for(const auto &c : class_map)
245  {
246  json_stream_objectt &json_class = json_stream.push_back_stream_object();
247  json_class["name"] = json_stringt(c.first);
248  json_class["isAbstract"] = jsont::json_boolean(c.second.is_abstract);
249  if(!children_only)
250  {
251  json_stream_arrayt &json_parents =
252  json_class.push_back_stream_array("parents");
253  for(const auto &pa : c.second.parents)
254  json_parents.push_back(json_stringt(pa));
255  }
256  json_stream_arrayt &json_children =
257  json_class.push_back_stream_array("children");
258  for(const auto &ch : c.second.children)
259  json_children.push_back(json_stringt(ch));
260  }
261 }
262 
264  const class_hierarchyt &hierarchy,
267  bool children_only)
268 {
270  switch(ui)
271  {
273  hierarchy.output(msg.result(), children_only);
274  msg.result() << messaget::eom;
275  break;
277  hierarchy.output(msg.result().json_stream(), children_only);
278  break;
281  }
282 }
idst ids_from_indices(const std::vector< node_indext > &nodes) const
Helper function that converts a vector of node_indext to a vector of ids that are stored in the corre...
void get_children_trans_rec(const irep_idt &, idst &) const
void operator()(const symbol_tablet &)
Looks for all the struct types in the symbol table and construct a map from class names to a data str...
void output(std::ostream &, bool children_only) const
Output the class hierarchy in plain text.
Non-graph-based representation of the class hierarchy.
std::vector< irept > subt
Definition: irep.h:160
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
nodes_by_namet nodes_by_name
Maps class identifiers onto node indices.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
static jsont json_boolean(bool value)
Definition: json.h:85
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:435
void get_parents_trans_rec(const irep_idt &, idst &) const
Get all the classes that class c inherits from (directly or indirectly).
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
subt & get_sub()
Definition: irep.h:317
idst get_children_trans(const irep_idt &c) const
Get all the classes that inherit (directly or indirectly) from class c.
idst get_direct_children(const irep_idt &c) const
Get all the classes that directly (i.e.
Class Hierarchy.
The symbol table.
Definition: symbol_table.h:19
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
class_mapt class_map
nodet::node_indext node_indext
Definition: graph.h:140
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:891
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
const symbolst & symbols
std::vector< irep_idt > idst
API to type classes.
#define UNIMPLEMENTED
Definition: invariant.h:287
mstreamt & result() const
Definition: message.h:312
std::vector< irep_idt > idst
idst get_other_reachable_ids(const irep_idt &c, bool forwards) const
Helper function for get_children_trans and get_parents_trans
void add_edge(node_indext a, node_indext b)
Definition: graph.h:198
void show_class_hierarchy(const class_hierarchyt &hierarchy, message_handlert &message_handler, ui_message_handlert::uit ui, bool children_only)
Output the class hierarchy.
const basest & bases() const
Definition: std_types.h:386
idst get_parents_trans(const irep_idt &c) const
Get all the classes that class c inherits from (directly or indirectly).
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
C++ class type.
Definition: std_types.h:341
json_stream_arrayt & json_stream()
Returns a reference to the top-level JSON array stream.
Definition: message.h:252
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
bool empty() const
Definition: dstring.h:73
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
std::vector< node_indext > get_reachable(node_indext src, bool forwards) const
Run depth-first search on the graph, starting from a single source node.
Definition: graph.h:555