CBMC
show_symbol_table.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show the symbol table
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_symbol_table.h"
13 
14 #include <algorithm>
15 #include <iostream>
16 #include <memory>
17 
18 #include <langapi/language.h>
19 #include <langapi/mode.h>
20 
21 #include <util/json_irep.h>
22 #include <util/json_stream.h>
23 #include <util/ui_message.h>
24 
25 #include "goto_model.h"
26 
35 static std::unique_ptr<languaget>
37 {
38  if(!symbol.mode.empty())
39  if(auto language_from_mode = get_language_from_mode(symbol.mode))
40  return language_from_mode;
41  return get_default_language();
42 }
43 
45 {
46 }
47 
49  const symbol_tablet &symbol_table,
50  std::ostream &out)
51 {
52  // we want to sort alphabetically
53  const namespacet ns(symbol_table);
54 
55  for(const auto &id : symbol_table.sorted_symbol_names())
56  {
57  const symbolt &symbol=ns.lookup(id);
58 
59  const std::unique_ptr<languaget> ptr = get_show_symbol_language(symbol);
60 
61  std::string type_str;
62 
63  if(symbol.type.is_not_nil())
64  ptr->from_type(symbol.type, type_str, ns);
65 
66  out << symbol.name << " " << type_str << '\n';
67  }
68 }
69 
71  const symbol_tablet &symbol_table,
72  std::ostream &out)
73 {
74  out << '\n' << "Symbols:" << '\n' << '\n';
75 
76  const namespacet ns(symbol_table);
77 
78  // we want to sort alphabetically
79  for(const irep_idt &id : symbol_table.sorted_symbol_names())
80  {
81  const symbolt &symbol=ns.lookup(id);
82 
83  const std::unique_ptr<languaget> ptr = get_show_symbol_language(symbol);
84 
85  std::string type_str, value_str;
86 
87  if(symbol.type.is_not_nil())
88  ptr->from_type(symbol.type, type_str, ns);
89 
90  if(symbol.value.is_not_nil())
91  ptr->from_expr(symbol.value, value_str, ns);
92 
93  out << "Symbol......: " << symbol.name << '\n' << std::flush;
94  out << "Pretty name.: " << symbol.pretty_name << '\n';
95  out << "Module......: " << symbol.module << '\n';
96  out << "Base name...: " << symbol.base_name << '\n';
97  out << "Mode........: " << symbol.mode << '\n';
98  out << "Type........: " << type_str << '\n';
99  out << "Value.......: " << value_str << '\n';
100  out << "Flags.......:";
101 
102  if(symbol.is_lvalue)
103  out << " lvalue";
104  if(symbol.is_static_lifetime)
105  out << " static_lifetime";
106  if(symbol.is_thread_local)
107  out << " thread_local";
108  if(symbol.is_file_local)
109  out << " file_local";
110  if(symbol.is_type)
111  out << " type";
112  if(symbol.is_extern)
113  out << " extern";
114  if(symbol.is_input)
115  out << " input";
116  if(symbol.is_output)
117  out << " output";
118  if(symbol.is_macro)
119  out << " macro";
120  if(symbol.is_parameter)
121  out << " parameter";
122  if(symbol.is_auxiliary)
123  out << " auxiliary";
124  if(symbol.is_weak)
125  out << " weak";
126  if(symbol.is_property)
127  out << " property";
128  if(symbol.is_state_var)
129  out << " state_var";
130  if(symbol.is_exported)
131  out << " exported";
132  if(symbol.is_volatile)
133  out << " volatile";
134 
135  out << '\n';
136  out << "Location....: " << symbol.location << '\n';
137 
138  out << '\n' << std::flush;
139  }
140 }
141 
143  const symbol_tablet &symbol_table,
145 {
146  json_stream_arrayt &out = message_handler.get_json_stream();
147 
148  json_stream_objectt &result_wrapper = out.push_back_stream_object();
149  json_stream_objectt &result =
150  result_wrapper.push_back_stream_object("symbolTable");
151 
152  const namespacet ns(symbol_table);
153  json_irept irep_converter(true);
154 
155  for(const auto &id_and_symbol : symbol_table.symbols)
156  {
157  const symbolt &symbol = id_and_symbol.second;
158 
159  const std::unique_ptr<languaget> ptr = get_show_symbol_language(symbol);
160 
161  std::string type_str, value_str;
162 
163  if(symbol.type.is_not_nil())
164  ptr->from_type(symbol.type, type_str, ns);
165 
166  if(symbol.value.is_not_nil())
167  ptr->from_expr(symbol.value, value_str, ns);
168 
169  json_objectt symbol_json{
170  {"prettyName", json_stringt(symbol.pretty_name)},
171  {"name", json_stringt(symbol.name)},
172  {"baseName", json_stringt(symbol.base_name)},
173  {"mode", json_stringt(symbol.mode)},
174  {"module", json_stringt(symbol.module)},
175 
176  {"prettyType", json_stringt(type_str)},
177  {"prettyValue", json_stringt(value_str)},
178 
179  {"type", irep_converter.convert_from_irep(symbol.type)},
180  {"value", irep_converter.convert_from_irep(symbol.value)},
181  {"location", irep_converter.convert_from_irep(symbol.location)},
182 
183  {"isType", jsont::json_boolean(symbol.is_type)},
184  {"isMacro", jsont::json_boolean(symbol.is_macro)},
185  {"isExported", jsont::json_boolean(symbol.is_exported)},
186  {"isInput", jsont::json_boolean(symbol.is_input)},
187  {"isOutput", jsont::json_boolean(symbol.is_output)},
188  {"isStateVar", jsont::json_boolean(symbol.is_state_var)},
189  {"isProperty", jsont::json_boolean(symbol.is_property)},
190  {"isStaticLifetime", jsont::json_boolean(symbol.is_static_lifetime)},
191  {"isThreadLocal", jsont::json_boolean(symbol.is_thread_local)},
192  {"isLvalue", jsont::json_boolean(symbol.is_lvalue)},
193  {"isFileLocal", jsont::json_boolean(symbol.is_file_local)},
194  {"isExtern", jsont::json_boolean(symbol.is_extern)},
195  {"isVolatile", jsont::json_boolean(symbol.is_volatile)},
196  {"isParameter", jsont::json_boolean(symbol.is_parameter)},
197  {"isAuxiliary", jsont::json_boolean(symbol.is_auxiliary)},
198  {"isWeak", jsont::json_boolean(symbol.is_weak)}};
199 
200  result.push_back(id2string(symbol.name), std::move(symbol_json));
201  }
202 }
203 
205  const symbol_tablet &symbol_table,
207 {
208  json_stream_arrayt &out = message_handler.get_json_stream();
209 
210  json_stream_objectt &result_wrapper = out.push_back_stream_object();
211  json_stream_objectt &result =
212  result_wrapper.push_back_stream_object("symbolTable");
213 
214  const namespacet ns(symbol_table);
215  json_irept irep_converter(true);
216 
217  for(const auto &id_and_symbol : symbol_table.symbols)
218  {
219  const symbolt &symbol = id_and_symbol.second;
220 
221  const std::unique_ptr<languaget> ptr = get_show_symbol_language(symbol);
222 
223  std::string type_str, value_str;
224 
225  if(symbol.type.is_not_nil())
226  ptr->from_type(symbol.type, type_str, ns);
227 
228  json_objectt symbol_json{
229  {"prettyName", json_stringt(symbol.pretty_name)},
230  {"baseName", json_stringt(symbol.base_name)},
231  {"mode", json_stringt(symbol.mode)},
232  {"module", json_stringt(symbol.module)},
233 
234  {"prettyType", json_stringt(type_str)},
235 
236  {"type", irep_converter.convert_from_irep(symbol.type)}};
237 
238  result.push_back(id2string(symbol.name), std::move(symbol_json));
239  }
240 }
241 
243  const symbol_tablet &symbol_table,
245 {
246  switch(ui.get_ui())
247  {
249  show_symbol_table_plain(symbol_table, std::cout);
250  break;
251 
254  break;
255 
257  show_symbol_table_json_ui(symbol_table, ui);
258  break;
259  }
260 }
261 
263  const goto_modelt &goto_model,
265 {
266  show_symbol_table(goto_model.symbol_table, ui);
267 }
268 
270  const symbol_tablet &symbol_table,
272 {
273  switch(ui.get_ui())
274  {
276  show_symbol_table_brief_plain(symbol_table, std::cout);
277  break;
278 
281  break;
282 
284  show_symbol_table_brief_json_ui(symbol_table, ui);
285  break;
286  }
287 }
288 
290  const goto_modelt &goto_model,
292 {
293  show_symbol_table_brief(goto_model.symbol_table, ui);
294 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
ui_message_handlert
Definition: ui_message.h:21
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
ui_message_handlert::uit::XML_UI
@ XML_UI
show_symbol_table_xml_ui
void show_symbol_table_xml_ui()
Definition: show_symbol_table.cpp:44
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
json_stream.h
symbolt::is_input
bool is_input
Definition: symbol.h:62
symbol_table_baset::sorted_symbol_names
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
Definition: symbol_table_base.cpp:36
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
goto_model.h
goto_modelt
Definition: goto_model.h:25
mode.h
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
show_symbol_table
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:242
json_irep.h
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
json_objectt
Definition: json.h:299
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
get_show_symbol_language
static std::unique_ptr< languaget > get_show_symbol_language(const symbolt &symbol)
Gets the language which should be used for showing the type and value of the supplied symbol.
Definition: show_symbol_table.cpp:36
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
show_symbol_table_brief
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
Definition: show_symbol_table.cpp:269
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
languaget::from_type
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition: language.cpp:41
ui_message_handlert::uit::JSON_UI
@ JSON_UI
languaget::from_expr
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition: language.cpp:32
ui_message_handlert::out
std::ostream & out
Definition: ui_message.h:53
json_stream_objectt::push_back_stream_object
json_stream_objectt & push_back_stream_object(const std::string &key)
Add a JSON object stream for a specific key.
Definition: json_stream.cpp:106
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
show_symbol_table.h
language.h
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
dstringt::empty
bool empty() const
Definition: dstring.h:88
json_irept::convert_from_irep
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
Definition: json_irep.cpp:31
show_symbol_table_brief_json_ui
static void show_symbol_table_brief_json_ui(const symbol_tablet &symbol_table, ui_message_handlert &message_handler)
Definition: show_symbol_table.cpp:204
show_symbol_table_brief_plain
void show_symbol_table_brief_plain(const symbol_tablet &symbol_table, std::ostream &out)
Definition: show_symbol_table.cpp:48
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_output
bool is_output
Definition: symbol.h:62
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
ui_message_handlert::uit::PLAIN
@ PLAIN
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:67
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
json_irept
Definition: json_irep.h:20
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
show_symbol_table_plain
void show_symbol_table_plain(const symbol_tablet &symbol_table, std::ostream &out)
Definition: show_symbol_table.cpp:70
show_symbol_table_json_ui
static void show_symbol_table_json_ui(const symbol_tablet &symbol_table, ui_message_handlert &message_handler)
Definition: show_symbol_table.cpp:142
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
json_stream_objectt::push_back
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
Definition: json_stream.h:178
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:97
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:62
ui_message_handlert::message_handler
message_handlert * message_handler
Definition: ui_message.h:49
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:139
json_stringt
Definition: json.h:269
ui_message.h