cprover
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 
23 #include "goto_model.h"
24 
26 {
27 }
28 
30  const symbol_tablet &symbol_table,
31  std::ostream &out)
32 {
33  // we want to sort alphabetically
34  const namespacet ns(symbol_table);
35 
36  for(const auto &id : symbol_table.sorted_symbol_names())
37  {
38  const symbolt &symbol=ns.lookup(id);
39 
40  std::unique_ptr<languaget> ptr;
41 
42  if(symbol.mode.empty())
44  else
45  {
46  ptr=get_language_from_mode(symbol.mode);
47  if(ptr==nullptr)
48  throw "symbol "+id2string(symbol.name)+" has unknown mode";
49  }
50 
51  std::string type_str;
52 
53  if(symbol.type.is_not_nil())
54  ptr->from_type(symbol.type, type_str, ns);
55 
56  out << symbol.name << " " << type_str << '\n';
57  }
58 }
59 
61  const symbol_tablet &symbol_table,
62  std::ostream &out)
63 {
64  out << '\n' << "Symbols:" << '\n' << '\n';
65 
66  const namespacet ns(symbol_table);
67 
68  // we want to sort alphabetically
69  for(const irep_idt &id : symbol_table.sorted_symbol_names())
70  {
71  const symbolt &symbol=ns.lookup(id);
72 
73  std::unique_ptr<languaget> ptr;
74 
75  if(symbol.mode.empty())
76  {
78  }
79  else
80  {
81  ptr=get_language_from_mode(symbol.mode);
82  }
83 
84  if(!ptr)
85  throw "symbol "+id2string(symbol.name)+" has unknown mode";
86 
87  std::string type_str, value_str;
88 
89  if(symbol.type.is_not_nil())
90  ptr->from_type(symbol.type, type_str, ns);
91 
92  if(symbol.value.is_not_nil())
93  ptr->from_expr(symbol.value, value_str, ns);
94 
95  out << "Symbol......: " << symbol.name << '\n' << std::flush;
96  out << "Pretty name.: " << symbol.pretty_name << '\n';
97  out << "Module......: " << symbol.module << '\n';
98  out << "Base name...: " << symbol.base_name << '\n';
99  out << "Mode........: " << symbol.mode << '\n';
100  out << "Type........: " << type_str << '\n';
101  out << "Value.......: " << value_str << '\n';
102  out << "Flags.......:";
103 
104  if(symbol.is_lvalue)
105  out << " lvalue";
106  if(symbol.is_static_lifetime)
107  out << " static_lifetime";
108  if(symbol.is_thread_local)
109  out << " thread_local";
110  if(symbol.is_file_local)
111  out << " file_local";
112  if(symbol.is_type)
113  out << " type";
114  if(symbol.is_extern)
115  out << " extern";
116  if(symbol.is_input)
117  out << " input";
118  if(symbol.is_output)
119  out << " output";
120  if(symbol.is_macro)
121  out << " macro";
122  if(symbol.is_parameter)
123  out << " parameter";
124  if(symbol.is_auxiliary)
125  out << " auxiliary";
126  if(symbol.is_weak)
127  out << " weak";
128  if(symbol.is_property)
129  out << " property";
130  if(symbol.is_state_var)
131  out << " state_var";
132  if(symbol.is_exported)
133  out << " exported";
134  if(symbol.is_volatile)
135  out << " volatile";
136 
137  out << '\n';
138  out << "Location....: " << symbol.location << '\n';
139 
140  out << '\n' << std::flush;
141  }
142 }
143 
145  const symbol_tablet &symbol_table,
146  ui_message_handlert &message_handler)
147 {
148  json_stream_arrayt &out = message_handler.get_json_stream();
149 
150  json_stream_objectt &result_wrapper = out.push_back_stream_object();
151  json_stream_objectt &result =
152  result_wrapper.push_back_stream_object("symbolTable");
153 
154  const namespacet ns(symbol_table);
155  json_irept irep_converter(true);
156 
157  for(const auto &id_and_symbol : symbol_table.symbols)
158  {
159  const symbolt &symbol = id_and_symbol.second;
160 
161  std::unique_ptr<languaget> ptr;
162 
163  if(symbol.mode.empty())
164  {
165  ptr=get_default_language();
166  }
167  else
168  {
169  ptr=get_language_from_mode(symbol.mode);
170  }
171 
172  if(!ptr)
173  throw "symbol "+id2string(symbol.name)+" has unknown mode";
174 
175  std::string type_str, value_str;
176 
177  if(symbol.type.is_not_nil())
178  ptr->from_type(symbol.type, type_str, ns);
179 
180  if(symbol.value.is_not_nil())
181  ptr->from_expr(symbol.value, value_str, ns);
182 
183  json_objectt symbol_json{
184  {"prettyName", json_stringt(symbol.pretty_name)},
185  {"name", json_stringt(symbol.name)},
186  {"baseName", json_stringt(symbol.base_name)},
187  {"mode", json_stringt(symbol.mode)},
188  {"module", json_stringt(symbol.module)},
189 
190  {"prettyType", json_stringt(type_str)},
191  {"prettyValue", json_stringt(value_str)},
192 
193  {"type", irep_converter.convert_from_irep(symbol.type)},
194  {"value", irep_converter.convert_from_irep(symbol.value)},
195  {"location", irep_converter.convert_from_irep(symbol.location)},
196 
197  {"isType", jsont::json_boolean(symbol.is_type)},
198  {"isMacro", jsont::json_boolean(symbol.is_macro)},
199  {"isExported", jsont::json_boolean(symbol.is_exported)},
200  {"isInput", jsont::json_boolean(symbol.is_input)},
201  {"isOutput", jsont::json_boolean(symbol.is_output)},
202  {"isStateVar", jsont::json_boolean(symbol.is_state_var)},
203  {"isProperty", jsont::json_boolean(symbol.is_property)},
204  {"isStaticLifetime", jsont::json_boolean(symbol.is_static_lifetime)},
205  {"isThreadLocal", jsont::json_boolean(symbol.is_thread_local)},
206  {"isLvalue", jsont::json_boolean(symbol.is_lvalue)},
207  {"isFileLocal", jsont::json_boolean(symbol.is_file_local)},
208  {"isExtern", jsont::json_boolean(symbol.is_extern)},
209  {"isVolatile", jsont::json_boolean(symbol.is_volatile)},
210  {"isParameter", jsont::json_boolean(symbol.is_parameter)},
211  {"isAuxiliary", jsont::json_boolean(symbol.is_auxiliary)},
212  {"isWeak", jsont::json_boolean(symbol.is_weak)}};
213 
214  result.push_back(id2string(symbol.name), std::move(symbol_json));
215  }
216 }
217 
219  const symbol_tablet &symbol_table,
220  ui_message_handlert &message_handler)
221 {
222  json_stream_arrayt &out = message_handler.get_json_stream();
223 
224  json_stream_objectt &result_wrapper = out.push_back_stream_object();
225  json_stream_objectt &result =
226  result_wrapper.push_back_stream_object("symbolTable");
227 
228  const namespacet ns(symbol_table);
229  json_irept irep_converter(true);
230 
231  for(const auto &id_and_symbol : symbol_table.symbols)
232  {
233  const symbolt &symbol = id_and_symbol.second;
234 
235  std::unique_ptr<languaget> ptr;
236 
237  if(symbol.mode.empty())
238  {
239  ptr=get_default_language();
240  }
241  else
242  {
243  ptr=get_language_from_mode(symbol.mode);
244  }
245 
246  if(!ptr)
247  throw "symbol "+id2string(symbol.name)+" has unknown mode";
248 
249  std::string type_str, value_str;
250 
251  if(symbol.type.is_not_nil())
252  ptr->from_type(symbol.type, type_str, ns);
253 
254  json_objectt symbol_json{
255  {"prettyName", json_stringt(symbol.pretty_name)},
256  {"baseName", json_stringt(symbol.base_name)},
257  {"mode", json_stringt(symbol.mode)},
258  {"module", json_stringt(symbol.module)},
259 
260  {"prettyType", json_stringt(type_str)},
261 
262  {"type", irep_converter.convert_from_irep(symbol.type)}};
263 
264  result.push_back(id2string(symbol.name), std::move(symbol_json));
265  }
266 }
267 
269  const symbol_tablet &symbol_table,
271 {
272  switch(ui.get_ui())
273  {
275  show_symbol_table_plain(symbol_table, std::cout);
276  break;
277 
280  break;
281 
283  show_symbol_table_json_ui(symbol_table, ui);
284  break;
285  }
286 }
287 
289  const goto_modelt &goto_model,
291 {
292  show_symbol_table(goto_model.symbol_table, ui);
293 }
294 
296  const symbol_tablet &symbol_table,
298 {
299  switch(ui.get_ui())
300  {
302  show_symbol_table_brief_plain(symbol_table, std::cout);
303  break;
304 
307  break;
308 
310  show_symbol_table_brief_json_ui(symbol_table, ui);
311  break;
312  }
313 }
314 
316  const goto_modelt &goto_model,
318 {
319  show_symbol_table_brief(goto_model.symbol_table, ui);
320 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
ui_message_handlert
Definition: ui_message.h:20
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:25
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
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:50
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
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:268
json_irep.h
Util.
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ui_message_handlert::get_json_stream
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
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:140
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
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:295
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:46
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:37
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:93
show_symbol_table.h
Show the symbol table.
language.h
Abstract interface to support a programming language.
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:33
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:218
show_symbol_table_brief_plain
void show_symbol_table_brief_plain(const symbol_tablet &symbol_table, std::ostream &out)
Definition: show_symbol_table.cpp:29
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
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:28
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:21
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:60
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:144
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
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:138
json_stringt
Definition: json.h:270