CBMC
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
17std::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 {
34 new_symbol.module, new_symbol.name);
35 }
36 catch(...)
37 {
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
67bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
68{
69 // Add an empty symbol to the table or retrieve existing symbol with same name
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
90void 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;
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)+")");
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(
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) + ")");
122 }
123
124 internal_symbols.erase(entry);
125}
126
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
140 vm, symbol.is_well_formed(), "Symbol is malformed: ", symbol_key);
141
142 // Check that symbols[id].name == id
144 vm,
145 symbol.name == symbol_key,
146 "Symbol table entry must map to a symbol with the correct identifier",
147 "Symbol table 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
167 vm,
169 "The base_name of a symbol should map to itself",
170 "Symbol table 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);
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
190 vm,
192 "Symbol table module map should map to symbol",
193 "Symbol table 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
203 {
205 vm,
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
217 {
219 vm,
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
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(
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(
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbol_module_mapt & symbol_module_map
Read-only field, used to look up symbol names given their modules.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
bool operator==(const symbol_tablet &other) const
symbolst internal_symbols
Value referenced by symbol_table_baset::symbols.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
symbol_module_mapt internal_symbol_module_map
Value referenced by symbol_table_baset::symbol_module_map.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
symbol_base_mapt internal_symbol_base_map
Value referenced by symbol_table_baset::symbol_base_map.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
void validate(const validation_modet vm=validation_modet::INVARIANT) const override
Check that the symbol table is well-formed.
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Author: Diffblue Ltd.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition validate.h:37
validation_modet