cprover
Loading...
Searching...
No Matches
show_symbol_table.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Show the symbol table
4
5Author: 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
35static 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,
144 ui_message_handlert &message_handler)
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,
206 ui_message_handlert &message_handler)
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{
294}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
bool is_not_nil() const
Definition irep.h:380
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
Provides methods for streaming JSON arrays.
Definition json_stream.h:93
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Provides methods for streaming JSON objects.
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
json_stream_objectt & push_back_stream_object(const std::string &key)
Add a JSON object stream for a specific key.
static jsont json_boolean(bool value)
Definition json.h:97
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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...
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_auxiliary
Definition symbol.h:67
bool is_volatile
Definition symbol.h:66
bool is_extern
Definition symbol.h:66
bool is_macro
Definition symbol.h:61
bool is_file_local
Definition symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_static_lifetime
Definition symbol.h:65
bool is_property
Definition symbol.h:62
bool is_parameter
Definition symbol.h:67
bool is_thread_local
Definition symbol.h:65
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
bool is_state_var
Definition symbol.h:62
bool is_output
Definition symbol.h:62
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:67
irep_idt name
The unique identifier.
Definition symbol.h:40
bool is_exported
Definition symbol.h:61
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
bool is_lvalue
Definition symbol.h:66
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
bool is_input
Definition symbol.h:62
virtual uit get_ui() const
Definition ui_message.h:33
virtual json_stream_arrayt & get_json_stream()
Definition ui_message.h:40
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition mode.cpp:139
static void show_symbol_table_json_ui(const symbol_tablet &symbol_table, ui_message_handlert &message_handler)
static void show_symbol_table_brief_json_ui(const symbol_tablet &symbol_table, ui_message_handlert &message_handler)
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.
void show_symbol_table_plain(const symbol_tablet &symbol_table, std::ostream &out)
void show_symbol_table(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief(const symbol_tablet &symbol_table, ui_message_handlert &ui)
void show_symbol_table_brief_plain(const symbol_tablet &symbol_table, std::ostream &out)
void show_symbol_table_xml_ui()
Show the symbol table.