CBMC
symbol_table_base.h
Go to the documentation of this file.
1 
5 
6 #ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H
7 #define CPROVER_UTIL_SYMBOL_TABLE_BASE_H
8 
9 #include "symbol.h" // IWYU pragma: keep
10 
11 #include <list>
12 #include <map>
13 #include <unordered_map>
14 
15 typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
16 typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
17 
18 class symbol_tablet;
19 
23 {
24 public:
25  typedef std::unordered_map<irep_idt, symbolt> symbolst;
26 
27 public:
31  const symbolst &symbols;
40 
41 public:
43  const symbolst &symbols,
46  : symbols(symbols),
49  {
50  }
51 
52  symbol_table_baset(const symbol_table_baset &other) = delete;
54 
55  virtual ~symbol_table_baset();
56 
63  std::size_t
64  next_unused_suffix(const std::string &prefix, std::size_t start_number) const
65  {
66  while(this->symbols.find(prefix + std::to_string(start_number)) !=
67  symbols.end())
68  ++start_number;
69 
70  return start_number;
71  }
72 
73  virtual std::size_t next_unused_suffix(const std::string &prefix) const
74  {
75  return next_unused_suffix(prefix, 0);
76  }
77 
79  operator const symbol_tablet &() const
80  {
81  return get_symbol_table();
82  }
83  virtual const symbol_tablet &get_symbol_table() const = 0;
84 
88  bool has_symbol(const irep_idt &name) const
89  {
90  return symbols.find(name) != symbols.end();
91  }
92 
96  const symbolt *lookup(const irep_idt &name) const
97  {
98  symbolst::const_iterator it = symbols.find(name);
99  return it != symbols.end() ? &it->second : nullptr;
100  }
101 
105  const symbolt &lookup_ref(const irep_idt &name) const
106  {
107  const symbolt *const symbol = lookup(name);
108  INVARIANT(
109  symbol, "`" + id2string(name) + "' must exist in the symbol table.");
110  return *symbol;
111  }
112 
115  std::list<symbolst::const_iterator>
117  {
118  std::list<symbolst::const_iterator> results;
119 
120  auto name_it = symbols.find(id);
121  if(name_it != symbols.end())
122  results.push_back(name_it);
123 
124  auto base_name_it_pair = symbol_base_map.equal_range(id);
125  for(auto base_name_it = base_name_it_pair.first;
126  base_name_it != base_name_it_pair.second;
127  ++base_name_it)
128  {
129  name_it = symbols.find(base_name_it->second);
130  CHECK_RETURN(name_it != symbols.end());
131  // don't add entries where name and base name match as this amounts to the
132  // case already covered above
133  if(base_name_it->first != base_name_it->second)
134  results.push_back(name_it);
135  }
136 
137  return results;
138  }
139 
143  virtual symbolt *get_writeable(const irep_idt &name) = 0;
144 
150  {
151  symbolt *symbol = get_writeable(name);
152  if(symbol == nullptr)
153  throw std::out_of_range("name not found in symbol_table");
154  return *symbol;
155  }
156 
157  bool add(const symbolt &symbol);
167  virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
168  virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
169 
170  bool remove(const irep_idt &name);
173  virtual void erase(const symbolst::const_iterator &entry) = 0;
174  virtual void clear() = 0;
175 
176  void show(std::ostream &out) const;
177 
180  std::vector<irep_idt> sorted_symbol_names() const;
181 
182  class iteratort
183  {
184  private:
185  symbolst::iterator it;
186  std::function<void(const irep_idt &id)> on_get_writeable;
187 
188  public:
189  explicit iteratort(symbolst::iterator it) : it(std::move(it))
190  {
191  }
192 
194  const iteratort &it,
195  std::function<void(const irep_idt &id)> on_get_writeable)
197  {
198  }
199 
200  operator symbolst::const_iterator() const
201  {
202  return symbolst::const_iterator{it};
203  }
204 
205  // The following typedefs are NOLINT as they are needed by the STL
206  typedef symbolst::iterator::difference_type difference_type; // NOLINT
207  typedef symbolst::const_iterator::value_type value_type; // NOLINT
208  typedef symbolst::const_iterator::pointer pointer; // NOLINT
209  typedef symbolst::const_iterator::reference reference; // NOLINT
210  typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
211 
212  bool operator!=(const iteratort &other) const
213  {
214  return it != other.it;
215  }
216 
217  bool operator==(const iteratort &other) const
218  {
219  return it == other.it;
220  }
221 
225  {
226  ++it;
227  return *this;
228  }
229 
233  {
234  iteratort copy(*this);
235  this->operator++();
236  return copy;
237  }
238 
242  {
243  return *it;
244  }
245 
249  {
250  return &**this;
251  }
252 
261  {
262  if(on_get_writeable)
263  on_get_writeable((*this)->first);
264  return it->second;
265  }
266  };
267 
268  virtual iteratort begin() = 0;
269  virtual iteratort end() = 0;
270 
271  using const_iteratort = symbolst::const_iterator;
272 
273  virtual const_iteratort begin() const;
274  virtual const_iteratort end() const;
275 
276  virtual void
278 };
279 
280 std::ostream &
281 operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
282 
283 #endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
symbolt & get_writeable_symbol()
Whereas the dereference operator gives a constant reference to the current symbol,...
bool operator==(const iteratort &other) const
std::function< void(const irep_idt &id)> on_get_writeable
iteratort operator++(int)
Post-increment operator.
bool operator!=(const iteratort &other) const
symbolst::iterator::iterator_category iterator_category
iteratort & operator++()
Preincrement operator Do not call on the end() iterator.
symbolst::const_iterator::reference reference
symbolst::const_iterator::value_type value_type
symbolst::const_iterator::pointer pointer
iteratort(const iteratort &it, std::function< void(const irep_idt &id)> on_get_writeable)
iteratort(symbolst::iterator it)
pointer operator->() const
Dereference operator (member access)
reference operator*() const
Dereference operator.
symbolst::iterator::difference_type difference_type
The symbol table base class interface.
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
virtual void clear()=0
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
virtual void validate(const validation_modet vm=validation_modet::INVARIANT) const =0
symbol_table_baset(const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map)
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbol_module_mapt & symbol_module_map
Read-only field, used to look up symbol names given their modules.
virtual iteratort begin()=0
symbolst::const_iterator const_iteratort
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::unordered_map< irep_idt, symbolt > symbolst
void show(std::ostream &out) const
Print the contents of the symbol table.
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual const symbol_tablet & get_symbol_table() const =0
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual iteratort end()=0
std::list< symbolst::const_iterator > match_name_or_base_name(const irep_idt &id) const
Collect all symbols the name of which matches id or the base name of which matches id.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual ~symbol_table_baset()
Author: Diffblue Ltd.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_baset & operator=(const symbol_table_baset &other)=delete
virtual std::size_t next_unused_suffix(const std::string &prefix) const
symbol_table_baset(const symbol_table_baset &other)=delete
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Symbol table entry.
std::multimap< irep_idt, irep_idt > symbol_base_mapt
std::ostream & operator<<(std::ostream &out, const symbol_table_baset &symbol_table)
Print the contents of the symbol table.
std::multimap< irep_idt, irep_idt > symbol_module_mapt
validation_modet