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