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