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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
class_hierarchy_grapht::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:105
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
class_hierarchy_grapht::get_parents_trans
idst get_parents_trans(const irep_idt &c) const
Get all the classes that class c inherits from (directly or indirectly).
Definition: class_hierarchy.cpp:123
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
class_hierarchy_grapht::ids_from_indices
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...
Definition: class_hierarchy.cpp:66
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
ui_message_handlert
Definition: ui_message.h:20
class_hierarchyt::operator()
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...
Definition: class_hierarchy.cpp:149
class_hierarchyt::output
void output(std::ostream &, bool children_only) const
Output the class hierarchy in plain text.
Definition: class_hierarchy.cpp:198
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
ui_message_handlert::uit::XML_UI
@ XML_UI
show_class_hierarchy
void show_class_hierarchy(const class_hierarchyt &hierarchy, ui_message_handlert &message_handler, bool children_only)
Output the class hierarchy.
Definition: class_hierarchy.cpp:261
class_hierarchyt::get_children_trans_rec
void get_children_trans_rec(const irep_idt &, idst &) const
Definition: class_hierarchy.cpp:128
json_stream.h
grapht< class_hierarchy_graph_nodet >::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:181
class_hierarchyt::get_parents_trans_rec
void get_parents_trans_rec(const irep_idt &, idst &) const
Get all the classes that class c inherits from (directly or indirectly).
Definition: class_hierarchy.cpp:178
messaget::eom
static eomt eom
Definition: message.h:297
class_hierarchy_grapht::get_children_trans
idst get_children_trans(const irep_idt &c) const
Get all the classes that inherit (directly or indirectly) from class c.
Definition: class_hierarchy.cpp:114
node_indext
std::size_t node_indext
Definition: destructor_tree.h:15
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
class_hierarchyt::entryt
Definition: class_hierarchy.h:48
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
messaget::result
mstreamt & result() const
Definition: message.h:409
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
ui_message_handlert::uit::JSON_UI
@ JSON_UI
class_hierarchyt::entryt::children
idst children
Definition: class_hierarchy.h:50
class_hierarchy_grapht::nodes_by_name
nodes_by_namet nodes_by_name
Maps class identifiers onto node indices.
Definition: class_hierarchy.h:127
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
std_types.h
Pre-defined types.
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:257
class_hierarchyt::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:45
class_hierarchyt::class_map
class_mapt class_map
Definition: class_hierarchy.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
grapht< class_hierarchy_graph_nodet >::add_edge
void add_edge(node_indext a, node_indext b)
Definition: graph.h:233
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
class_hierarchy.h
Class Hierarchy.
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
ui_message_handlert::uit::PLAIN
@ PLAIN
class_hierarchy_grapht::get_other_reachable_ids
idst get_other_reachable_ids(const irep_idt &c, bool forwards) const
Helper function for get_children_trans and get_parents_trans
Definition: class_hierarchy.cpp:92
grapht< class_hierarchy_graph_nodet >::get_successors
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:940
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
grapht< class_hierarchy_graph_nodet >::get_reachable
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:599
class_hierarchyt::output_dot
void output_dot(std::ostream &) const
Output class hierarchy in Graphviz DOT format.
Definition: class_hierarchy.cpp:217
symbol_table.h
Author: Diffblue Ltd.
class_hierarchyt::entryt::parents
idst parents
Definition: class_hierarchy.h:50
json_stream_arrayt::push_back
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
Definition: json_stream.h:106
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:97
class_hierarchy_grapht::get_direct_children
idst get_direct_children(const irep_idt &c) const
Get all the classes that directly (i.e.
Definition: class_hierarchy.cpp:84
json_stringt
Definition: json.h:270
class_hierarchy_grapht::populate
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
Definition: class_hierarchy.cpp:28