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 <ostream>
17 
18 #include <util/json_stream.h>
19 #include <util/std_types.h>
20 #include <util/symbol_table.h>
21 
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 
59 {
60  // Add nodes for all classes:
61  for(const auto &symbol_pair : symbol_table.symbols)
62  {
63  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
64  {
65  node_indext new_node_index = add_node();
66  nodes_by_name[symbol_pair.first] = new_node_index;
67  (*this)[new_node_index].class_identifier = symbol_pair.first;
68  }
69  }
70 
71  // Add parent -> child edges:
72  for(const auto &symbol_pair : symbol_table.symbols)
73  {
74  if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
75  {
76  const class_typet &class_type = to_class_type(symbol_pair.second.type);
77 
78  for(const auto &base : class_type.bases())
79  {
80  const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
81  if(!parent.empty())
82  {
83  add_edge(
84  nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));
85  }
86  }
87  }
88  }
89 }
90 
92  const irep_idt &c,
93  idst &dest) const
94 {
95  class_mapt::const_iterator it=class_map.find(c);
96  if(it==class_map.end())
97  return;
98  const entryt &entry=it->second;
99 
100  for(const auto &child : entry.children)
101  dest.push_back(child);
102 
103  // recursive calls
104  for(const auto &child : entry.children)
105  get_children_trans_rec(child, dest);
106 }
107 
114  const irep_idt &c,
115  idst &dest) const
116 {
117  class_mapt::const_iterator it=class_map.find(c);
118  if(it==class_map.end())
119  return;
120  const entryt &entry=it->second;
121 
122  for(const auto &child : entry.parents)
123  dest.push_back(child);
124 
125  // recursive calls
126  for(const auto &child : entry.parents)
127  get_parents_trans_rec(child, dest);
128 }
129 
133 void class_hierarchyt::output(std::ostream &out, bool children_only) const
134 {
135  for(const auto &c : class_map)
136  {
137  out << c.first << (c.second.is_abstract ? " (abstract)" : "") << ":\n";
138  if(!children_only)
139  {
140  out << " parents:\n";
141  for(const auto &pa : c.second.parents)
142  out << " " << pa << '\n';
143  }
144  out << " children:\n";
145  for(const auto &ch : c.second.children)
146  out << " " << ch << '\n';
147  }
148 }
149 
152 void class_hierarchyt::output_dot(std::ostream &ostr) const
153 {
154  ostr << "digraph class_hierarchy {\n"
155  << " rankdir=BT;\n"
156  << " node [fontsize=12 shape=box];\n";
157  for(const auto &c : class_map)
158  {
159  for(const auto &ch : c.second.parents)
160  {
161  ostr << " \"" << c.first << "\" -> "
162  << "\"" << ch << "\" "
163  << " [arrowhead=\"vee\"];"
164  << "\n";
165  }
166  }
167  ostr << "}\n";
168 }
169 
174  json_stream_arrayt &json_stream,
175  bool children_only) const
176 {
177  for(const auto &c : class_map)
178  {
179  json_stream_objectt &json_class = json_stream.push_back_stream_object();
180  json_class["name"] = json_stringt(c.first);
181  json_class["isAbstract"] = jsont::json_boolean(c.second.is_abstract);
182  if(!children_only)
183  {
184  json_stream_arrayt &json_parents =
185  json_class.push_back_stream_array("parents");
186  for(const auto &pa : c.second.parents)
187  json_parents.push_back(json_stringt(pa));
188  }
189  json_stream_arrayt &json_children =
190  json_class.push_back_stream_array("children");
191  for(const auto &ch : c.second.children)
192  json_children.push_back(json_stringt(ch));
193  }
194 }
195 
197  const class_hierarchyt &hierarchy,
200  bool children_only)
201 {
203  switch(ui)
204  {
206  hierarchy.output(msg.result(), children_only);
207  msg.result() << messaget::eom;
208  break;
210  hierarchy.output(msg.result().json_stream(), children_only);
211  break;
214  }
215 }
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.
std::vector< irept > subt
Definition: irep.h:90
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 inherit (directly or indirectly) from class c.
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:245
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
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
Author: Diffblue Ltd.
const symbolst & symbols
std::vector< irep_idt > idst
API to type classes.
#define UNIMPLEMENTED
Definition: invariant.h:266
mstreamt & result() const
Definition: message.h:312
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
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
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:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285