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 struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
47 
48  for(const auto &base : struct_type.bases())
49  {
50  const irep_idt &parent = 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  for(const auto &base : struct_type.bases())
161  {
162  const irep_idt &parent = base.type().get_identifier();
163  if(parent.empty())
164  continue;
165 
166  class_map[parent].children.push_back(symbol_pair.first);
167  class_map[symbol_pair.first].parents.push_back(parent);
168  }
169  }
170  }
171 }
172 
179  const irep_idt &c,
180  idst &dest) const
181 {
182  class_mapt::const_iterator it=class_map.find(c);
183  if(it==class_map.end())
184  return;
185  const entryt &entry=it->second;
186 
187  for(const auto &child : entry.parents)
188  dest.push_back(child);
189 
190  // recursive calls
191  for(const auto &child : entry.parents)
192  get_parents_trans_rec(child, dest);
193 }
194 
198 void class_hierarchyt::output(std::ostream &out, bool children_only) const
199 {
200  for(const auto &c : class_map)
201  {
202  out << c.first << (c.second.is_abstract ? " (abstract)" : "") << ":\n";
203  if(!children_only)
204  {
205  out << " parents:\n";
206  for(const auto &pa : c.second.parents)
207  out << " " << pa << '\n';
208  }
209  out << " children:\n";
210  for(const auto &ch : c.second.children)
211  out << " " << ch << '\n';
212  }
213 }
214 
217 void class_hierarchyt::output_dot(std::ostream &ostr) const
218 {
219  ostr << "digraph class_hierarchy {\n"
220  << " rankdir=BT;\n"
221  << " node [fontsize=12 shape=box];\n";
222  for(const auto &c : class_map)
223  {
224  for(const auto &ch : c.second.parents)
225  {
226  ostr << " \"" << c.first << "\" -> "
227  << "\"" << ch << "\" "
228  << " [arrowhead=\"vee\"];"
229  << "\n";
230  }
231  }
232  ostr << "}\n";
233 }
234 
239  json_stream_arrayt &json_stream,
240  bool children_only) const
241 {
242  for(const auto &c : class_map)
243  {
244  json_stream_objectt &json_class = json_stream.push_back_stream_object();
245  json_class["name"] = json_stringt(c.first);
246  json_class["isAbstract"] = jsont::json_boolean(c.second.is_abstract);
247  if(!children_only)
248  {
249  json_stream_arrayt &json_parents =
250  json_class.push_back_stream_array("parents");
251  for(const auto &pa : c.second.parents)
252  json_parents.push_back(json_stringt(pa));
253  }
254  json_stream_arrayt &json_children =
255  json_class.push_back_stream_array("children");
256  for(const auto &ch : c.second.children)
257  json_children.push_back(json_stringt(ch));
258  }
259 }
260 
262  const class_hierarchyt &hierarchy,
263  ui_message_handlert &message_handler,
264  bool children_only)
265 {
266  messaget msg(message_handler);
267  switch(message_handler.get_ui())
268  {
270  hierarchy.output(msg.result(), children_only);
271  msg.result() << messaget::eom;
272  break;
274  if(msg.result().tellp() > 0)
275  msg.result() << messaget::eom; // force end of previous message
276  hierarchy.output(message_handler.get_json_stream(), children_only);
277  break;
280  }
281 }
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.
uit get_ui() const
Definition: ui_message.h:30
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.
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
void get_parents_trans_rec(const irep_idt &, idst &) const
Get all the classes that class c inherits from (directly or indirectly).
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
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.
json_stream_arrayt & get_json_stream()
Definition: ui_message.h:37
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:303
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:174
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:938
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
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 typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
const symbolst & symbols
std::vector< irep_idt > idst
static eomt eom
Definition: message.h:284
Pre-defined types.
#define UNIMPLEMENTED
Definition: invariant.h:497
mstreamt & result() const
Definition: message.h:396
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:232
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
bool empty() const
Definition: dstring.h:75
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:598