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 
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  try
30  {
31  internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name);
32  }
33  catch(...)
34  {
35  internal_symbol_base_map.erase(base_result);
36  throw;
37  }
38  }
39  catch(...)
40  {
41  internal_symbols.erase(result.first);
42  throw;
43  }
44  }
45  return std::make_pair(std::ref(new_symbol), result.second);
46 }
47 
63 bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
64 {
65  // Add an empty symbol to the table or retrieve existing symbol with same name
66  symbolt temp_symbol;
67  // This is not copying the symbol, this is passing the three required
68  // parameters to insert (just in the symbol)
69  temp_symbol.name=symbol.name;
70  temp_symbol.base_name=symbol.base_name;
71  temp_symbol.module=symbol.module;
72  std::pair<symbolt &, bool> result=insert(std::move(temp_symbol));
73  if(result.second)
74  {
75  // Move the provided symbol into the symbol table, this can't be done
76  // earlier
77  result.first.swap(symbol);
78  }
79  // Return the address of the symbol in the table
80  new_symbol=&result.first;
81  return !result.second;
82 }
83 
86 void symbol_tablet::erase(const symbolst::const_iterator &entry)
87 {
88  const symbolt &symbol=entry->second;
89 
90  symbol_base_mapt::const_iterator
91  base_it=symbol_base_map.lower_bound(entry->second.base_name);
92  symbol_base_mapt::const_iterator
93  base_it_end=symbol_base_map.upper_bound(entry->second.base_name);
94  while(base_it!=base_it_end && base_it->second!=symbol.name)
95  ++base_it;
96  INVARIANT(
97  base_it!=base_it_end,
98  "symbolt::base_name should not be changed "
99  "after it is added to the symbol_table "
100  "(name: "+id2string(symbol.name)+", "
101  "current base_name: "+id2string(symbol.base_name)+")");
102  internal_symbol_base_map.erase(base_it);
103 
104  symbol_module_mapt::const_iterator
105  module_it=symbol_module_map.lower_bound(entry->second.module),
106  module_it_end=symbol_module_map.upper_bound(entry->second.module);
107  while(module_it!=module_it_end && module_it->second!=symbol.name)
108  ++module_it;
109  INVARIANT(
110  module_it!=module_it_end,
111  "symbolt::module should not be changed "
112  "after it is added to the symbol_table "
113  "(name: "+id2string(symbol.name)+", "
114  "current module: "+id2string(symbol.module)+")");
115  internal_symbol_module_map.erase(module_it);
116 
117  internal_symbols.erase(entry);
118 }
119 
124 {
125  // Check that identifiers are mapped to the correct symbol
126  for(const auto &elem : symbols)
127  {
128  const auto symbol_key = elem.first;
129  const auto &symbol = elem.second;
130 
131  // First of all, ensure symbol well-formedness
133  vm, symbol.is_well_formed(), "Symbol is malformed: ", symbol_key);
134 
135  // Check that symbols[id].name == id
137  vm,
138  symbol.name == symbol_key,
139  "Symbol table entry must map to a symbol with the correct identifier",
140  "Symbol table key '",
141  symbol_key,
142  "' maps to symbol '",
143  symbol.name,
144  "'");
145 
146  // Check that the symbol basename is mapped to its full name
147  if(!symbol.base_name.empty())
148  {
149  const auto base_map_search =
150  symbol_base_map.equal_range(symbol.base_name);
151  const bool base_map_matches_symbol =
152  std::find_if(
153  base_map_search.first,
154  base_map_search.second,
155  [&symbol_key](const typename symbol_base_mapt::value_type &match) {
156  return match.second == symbol_key;
157  }) != symbol_base_map.end();
158 
160  vm,
161  base_map_matches_symbol,
162  "The base_name of a symbol should map to itself",
163  "Symbol table key '",
164  symbol_key,
165  "' has a base_name '",
166  symbol.base_name,
167  "' which does not map to itself");
168  }
169 
170  // Check that the module name of the symbol is mapped to the full name
171  if(!symbol.module.empty())
172  {
173  auto module_map_search = symbol_module_map.equal_range(symbol.module);
174  bool module_map_matches_symbol =
175  std::find_if(
176  module_map_search.first,
177  module_map_search.second,
178  [&symbol_key](const typename symbol_module_mapt::value_type &match) {
179  return match.second == symbol_key;
180  }) != symbol_module_map.end();
181 
183  vm,
184  module_map_matches_symbol,
185  "Symbol table module map should map to symbol",
186  "Symbol table key '",
187  symbol_key,
188  "' has a module name of '",
189  symbol.module,
190  "' which does not map to itself");
191  }
192  }
193 
194  // Check that all base name map entries point to a symbol entry
195  for(auto base_map_entry : symbol_base_map)
196  {
198  vm,
199  has_symbol(base_map_entry.second),
200  "Symbol table base_name map entries must map to a symbol name",
201  "base_name map entry '",
202  base_map_entry.first,
203  "' maps to non-existant symbol name '",
204  base_map_entry.second,
205  "'");
206  }
207 
208  // Check that all module map entries point to a symbol entry
209  for(auto module_map_entry : symbol_module_map)
210  {
212  vm,
213  has_symbol(module_map_entry.second),
214  "Symbol table module map entries must map to a symbol name",
215  "base_name map entry '",
216  module_map_entry.first,
217  "' maps to non-existant symbol name '",
218  module_map_entry.second,
219  "'");
220  }
221 }
symbol_tablet::internal_symbol_module_map
symbol_module_mapt internal_symbol_module_map
Definition: symbol_table.h:24
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:78
symbol_table_baset::symbol_base_map
const symbol_base_mapt & symbol_base_map
Definition: symbol_table_base.h:28
symbol_tablet::internal_symbol_base_map
symbol_base_mapt internal_symbol_base_map
Definition: symbol_table.h:23
symbol_table_baset::symbol_module_map
const symbol_module_mapt & symbol_module_map
Definition: symbol_table_base.h:29
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
invariant.h
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:123
symbol_tablet::internal_symbols
symbolst internal_symbols
Definition: symbol_table.h:22
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:17
validation_modet
validation_modet
Definition: validation_mode.h:12
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:63
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
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:86
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
validation_modet::INVARIANT
@ INVARIANT