cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
symbol_table.cpp
Go to the documentation of this file.
1
2
3
#include "
symbol_table.h
"
4
5
#include <algorithm>
6
#include <
util/invariant.h
>
7
#include <
util/validate.h
>
8
17
std::pair<symbolt &, bool>
symbol_tablet::insert
(
symbolt
symbol)
18
{
19
// Add the symbol to the table or retrieve existing symbol with the same name
20
std::pair<symbolst::iterator, bool> result=
21
internal_symbols
.emplace(symbol.
name
, std::move(symbol));
22
symbolt
&new_symbol=result.first->second;
23
if
(result.second)
24
{
25
try
26
{
27
symbol_base_mapt::iterator base_result=
28
internal_symbol_base_map
.emplace(new_symbol.
base_name
, new_symbol.
name
);
29
if
(!new_symbol.
module
.
empty
())
30
{
31
try
32
{
33
internal_symbol_module_map
.emplace(
34
new_symbol.
module
, new_symbol.
name
);
35
}
36
catch
(...)
37
{
38
internal_symbol_base_map
.erase(base_result);
39
throw
;
40
}
41
}
42
}
43
catch
(...)
44
{
45
internal_symbols
.erase(result.first);
46
throw
;
47
}
48
}
49
return
std::make_pair(std::ref(new_symbol), result.second);
50
}
51
67
bool
symbol_tablet::move
(
symbolt
&symbol,
symbolt
*&new_symbol)
68
{
69
// Add an empty symbol to the table or retrieve existing symbol with same name
70
symbolt
temp_symbol;
71
// This is not copying the symbol, this is passing the three required
72
// parameters to insert (just in the symbol)
73
temp_symbol.
name
=symbol.
name
;
74
temp_symbol.
base_name
=symbol.
base_name
;
75
temp_symbol.
module
=symbol.
module
;
76
std::pair<symbolt &, bool> result=
insert
(std::move(temp_symbol));
77
if
(result.second)
78
{
79
// Move the provided symbol into the symbol table, this can't be done
80
// earlier
81
result.first.swap(symbol);
82
}
83
// Return the address of the symbol in the table
84
new_symbol=&result.first;
85
return
!result.second;
86
}
87
90
void
symbol_tablet::erase
(
const
symbolst::const_iterator &entry)
91
{
92
const
symbolt
&symbol=entry->second;
93
94
auto
base_it =
symbol_base_map
.lower_bound(symbol.
base_name
);
95
const
auto
base_it_end =
symbol_base_map
.upper_bound(symbol.
base_name
);
96
while
(base_it!=base_it_end && base_it->second!=symbol.
name
)
97
++base_it;
98
INVARIANT
(
99
base_it!=base_it_end,
100
"symbolt::base_name should not be changed "
101
"after it is added to the symbol_table "
102
"(name: "
+
id2string
(symbol.
name
)+
", "
103
"current base_name: "
+
id2string
(symbol.
base_name
)+
")"
);
104
internal_symbol_base_map
.erase(base_it);
105
106
if
(!symbol.
module
.
empty
())
107
{
108
auto
module_it =
symbol_module_map
.lower_bound(symbol.
module
);
109
auto
module_it_end =
symbol_module_map
.upper_bound(symbol.
module
);
110
while
(module_it != module_it_end && module_it->second != symbol.
name
)
111
++module_it;
112
INVARIANT
(
113
module_it != module_it_end,
114
"symbolt::module should not be changed "
115
"after it is added to the symbol_table "
116
"(name: "
+
117
id2string
(symbol.
name
) +
118
", "
119
"current module: "
+
120
id2string
(symbol.
module
) +
")"
);
121
internal_symbol_module_map
.erase(module_it);
122
}
123
124
internal_symbols
.erase(entry);
125
}
126
130
void
symbol_tablet::validate
(
const
validation_modet
vm)
const
131
{
132
// Check that identifiers are mapped to the correct symbol
133
for
(
const
auto
&elem :
symbols
)
134
{
135
const
auto
symbol_key = elem.first;
136
const
auto
&symbol = elem.second;
137
138
// First of all, ensure symbol well-formedness
139
DATA_CHECK_WITH_DIAGNOSTICS
(
140
vm, symbol.is_well_formed(),
"Symbol is malformed: "
, symbol_key);
141
142
// Check that symbols[id].name == id
143
DATA_CHECK_WITH_DIAGNOSTICS
(
144
vm,
145
symbol.name == symbol_key,
146
"Symbol table entry must map to a symbol with the correct identifier"
,
147
"Symbol table key '"
,
148
symbol_key,
149
"' maps to symbol '"
,
150
symbol.name,
151
"'"
);
152
153
// Check that the symbol basename is mapped to its full name
154
if
(!symbol.base_name.empty())
155
{
156
const
auto
base_map_search =
157
symbol_base_map
.equal_range(symbol.base_name);
158
const
bool
base_map_matches_symbol =
159
std::find_if(
160
base_map_search.first,
161
base_map_search.second,
162
[&symbol_key](
const
symbol_base_mapt::value_type &match) {
163
return match.second == symbol_key;
164
}) !=
symbol_base_map
.end();
165
166
DATA_CHECK_WITH_DIAGNOSTICS
(
167
vm,
168
base_map_matches_symbol,
169
"The base_name of a symbol should map to itself"
,
170
"Symbol table key '"
,
171
symbol_key,
172
"' has a base_name '"
,
173
symbol.base_name,
174
"' which does not map to itself"
);
175
}
176
177
// Check that the module name of the symbol is mapped to the full name
178
if
(!symbol.module.empty())
179
{
180
auto
module_map_search =
symbol_module_map
.equal_range(symbol.module);
181
bool
module_map_matches_symbol =
182
std::find_if(
183
module_map_search.first,
184
module_map_search.second,
185
[&symbol_key](
const
symbol_module_mapt::value_type &match) {
186
return match.second == symbol_key;
187
}) !=
symbol_module_map
.end();
188
189
DATA_CHECK_WITH_DIAGNOSTICS
(
190
vm,
191
module_map_matches_symbol,
192
"Symbol table module map should map to symbol"
,
193
"Symbol table key '"
,
194
symbol_key,
195
"' has a module name of '"
,
196
symbol.module,
197
"' which does not map to itself"
);
198
}
199
}
200
201
// Check that all base name map entries point to a symbol entry
202
for
(
auto
base_map_entry :
symbol_base_map
)
203
{
204
DATA_CHECK_WITH_DIAGNOSTICS
(
205
vm,
206
has_symbol
(base_map_entry.second),
207
"Symbol table base_name map entries must map to a symbol name"
,
208
"base_name map entry '"
,
209
base_map_entry.first,
210
"' maps to non-existant symbol name '"
,
211
base_map_entry.second,
212
"'"
);
213
}
214
215
// Check that all module map entries point to a symbol entry
216
for
(
auto
module_map_entry :
symbol_module_map
)
217
{
218
DATA_CHECK_WITH_DIAGNOSTICS
(
219
vm,
220
has_symbol
(module_map_entry.second),
221
"Symbol table module map entries must map to a symbol name"
,
222
"base_name map entry '"
,
223
module_map_entry.first,
224
"' maps to non-existant symbol name '"
,
225
module_map_entry.second,
226
"'"
);
227
}
228
}
229
230
bool
symbol_tablet::operator==
(
const
symbol_tablet
&other)
const
231
{
232
// we cannot use == for comparing the multimaps as it compares the items
233
// sequentially, but the order of items with equal keys depends on the
234
// insertion order
235
236
{
237
std::vector<std::pair<irep_idt, irep_idt>> v1(
238
internal_symbol_base_map
.begin(),
internal_symbol_base_map
.end());
239
240
std::vector<std::pair<irep_idt, irep_idt>> v2(
241
other.
internal_symbol_base_map
.begin(),
242
other.
internal_symbol_base_map
.end());
243
244
std::sort(v1.begin(), v1.end());
245
std::sort(v2.begin(), v2.end());
246
247
if
(v1 != v2)
248
return
false
;
249
}
250
251
{
252
std::vector<std::pair<irep_idt, irep_idt>> v1(
253
internal_symbol_module_map
.begin(),
internal_symbol_module_map
.end());
254
255
std::vector<std::pair<irep_idt, irep_idt>> v2(
256
other.
internal_symbol_module_map
.begin(),
257
other.
internal_symbol_module_map
.end());
258
259
std::sort(v1.begin(), v1.end());
260
std::sort(v2.begin(), v2.end());
261
262
if
(v1 != v2)
263
return
false
;
264
}
265
266
return
internal_symbols
== other.
internal_symbols
;
267
}
dstringt::empty
bool empty() const
Definition
dstring.h:89
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
Definition
symbol_table_base.h:34
symbol_table_baset::symbol_module_map
const symbol_module_mapt & symbol_module_map
Read-only field, used to look up symbol names given their modules.
Definition
symbol_table_base.h:39
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition
symbol_table_base.h:31
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition
symbol_table_base.h:88
symbol_tablet::operator==
bool operator==(const symbol_tablet &other) const
Definition
symbol_table.cpp:230
symbol_tablet::internal_symbols
symbolst internal_symbols
Value referenced by symbol_table_baset::symbols.
Definition
symbol_table.h:17
symbol_tablet::symbol_tablet
symbol_tablet()
Definition
symbol_table.h:24
symbol_tablet::erase
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Definition
symbol_table.cpp:90
symbol_tablet::internal_symbol_module_map
symbol_module_mapt internal_symbol_module_map
Value referenced by symbol_table_baset::symbol_module_map.
Definition
symbol_table.h:21
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition
symbol_table.cpp:67
symbol_tablet::internal_symbol_base_map
symbol_base_mapt internal_symbol_base_map
Value referenced by symbol_table_baset::symbol_base_map.
Definition
symbol_table.h:19
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition
symbol_table.cpp:17
symbol_tablet::validate
void validate(const validation_modet vm=validation_modet::INVARIANT) const override
Check that the symbol table is well-formed.
Definition
symbol_table.cpp:130
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition
symbol.h:46
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition
symbol.h:43
symbolt::name
irep_idt name
The unique identifier.
Definition
symbol.h:40
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
invariant.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
symbol_table.h
Author: Diffblue Ltd.
validate.h
DATA_CHECK_WITH_DIAGNOSTICS
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition
validate.h:37
validation_modet
validation_modet
Definition
validation_mode.h:13
util
symbol_table.cpp
Generated by
1.17.0