CBMC
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 
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  {
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 
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 '",
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 
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 
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  {
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  {
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(
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 }
bool empty() const
Definition: dstring.h:89
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.
Definition: symbol_table.h:14
bool operator==(const symbol_tablet &other) const
symbolst internal_symbols
Value referenced by symbol_table_baset::symbols.
Definition: symbol_table.h:17
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.
Definition: symbol_table.h:21
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.
Definition: symbol_table.h:19
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 base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
Author: Diffblue Ltd.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition: validate.h:37
validation_modet