cprover
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 <map>
10 #include <unordered_map>
11 
12 #include "symbol.h"
13 
14 typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
15 typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
16 
17 class symbol_tablet;
18 
22 {
23 public:
24  typedef std::unordered_map<irep_idt, symbolt> symbolst;
25 
26 public:
30  const symbolst &symbols;
39 
40 public:
42  const symbolst &symbols,
45  : symbols(symbols),
48  {
49  }
50 
51  symbol_table_baset(const symbol_table_baset &other) = delete;
52  symbol_table_baset &operator=(const symbol_table_baset &other) = delete;
53 
54  virtual ~symbol_table_baset();
55 
62  std::size_t
63  next_unused_suffix(const std::string &prefix, std::size_t start_number) const
64  {
65  while(this->symbols.find(prefix + std::to_string(start_number)) !=
66  symbols.end())
67  ++start_number;
68 
69  return start_number;
70  }
71 
72  virtual std::size_t next_unused_suffix(const std::string &prefix) const
73  {
74  return next_unused_suffix(prefix, 0);
75  }
76 
78  operator const symbol_tablet &() const
79  {
80  return get_symbol_table();
81  }
82  virtual const symbol_tablet &get_symbol_table() const = 0;
83 
87  bool has_symbol(const irep_idt &name) const
88  {
89  return symbols.find(name) != symbols.end();
90  }
91 
95  const symbolt *lookup(const irep_idt &name) const
96  {
97  symbolst::const_iterator it = symbols.find(name);
98  return it != symbols.end() ? &it->second : nullptr;
99  }
100 
104  const symbolt &lookup_ref(const irep_idt &name) const
105  {
106  const symbolt *const symbol = lookup(name);
107  INVARIANT(
108  symbol, "`" + id2string(name) + "' must exist in the symbol table.");
109  return *symbol;
110  }
111 
115  virtual symbolt *get_writeable(const irep_idt &name) = 0;
116 
122  {
123  symbolt *symbol = get_writeable(name);
124  if(symbol == nullptr)
125  throw std::out_of_range("name not found in symbol_table");
126  return *symbol;
127  }
128 
129  bool add(const symbolt &symbol);
139  virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
140  virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
141 
142  bool remove(const irep_idt &name);
145  virtual void erase(const symbolst::const_iterator &entry) = 0;
146  virtual void clear() = 0;
147 
148  void show(std::ostream &out) const;
149 
152  std::vector<irep_idt> sorted_symbol_names() const;
153 
154  class iteratort
155  {
156  private:
157  symbolst::iterator it;
158  std::function<void(const irep_idt &id)> on_get_writeable;
159 
160  public:
161  explicit iteratort(symbolst::iterator it) : it(std::move(it))
162  {
163  }
164 
166  const iteratort &it,
167  std::function<void(const irep_idt &id)> on_get_writeable)
169  {
170  }
171 
172  // The following typedefs are NOLINT as they are needed by the STL
173  typedef symbolst::iterator::difference_type difference_type; // NOLINT
174  typedef symbolst::const_iterator::value_type value_type; // NOLINT
175  typedef symbolst::const_iterator::pointer pointer; // NOLINT
176  typedef symbolst::const_iterator::reference reference; // NOLINT
177  typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
178 
179  bool operator!=(const iteratort &other) const
180  {
181  return it != other.it;
182  }
183 
184  bool operator==(const iteratort &other) const
185  {
186  return it == other.it;
187  }
188 
192  {
193  ++it;
194  return *this;
195  }
196 
200  {
201  iteratort copy(*this);
202  this->operator++();
203  return copy;
204  }
205 
209  {
210  return *it;
211  }
212 
216  {
217  return &**this;
218  }
219 
228  {
229  if(on_get_writeable)
230  on_get_writeable((*this)->first);
231  return it->second;
232  }
233  };
234 
235  virtual iteratort begin() = 0;
236  virtual iteratort end() = 0;
237 
238  using const_iteratort = symbolst::const_iterator;
239 
240  virtual const_iteratort begin() const;
241  virtual const_iteratort end() const;
242 };
243 
244 std::ostream &
245 operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
246 
247 #endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H
symbol_table_baset::iteratort::operator==
bool operator==(const iteratort &other) const
Definition: symbol_table_base.h:184
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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
symbol_table_baset::iteratort::operator->
pointer operator->() const
Dereference operator (member access)
Definition: symbol_table_base.h:215
symbol_table_baset::get_writeable
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
symbol_table_baset::iteratort::operator!=
bool operator!=(const iteratort &other) const
Definition: symbol_table_base.h:179
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_table_baset::clear
virtual void clear()=0
symbol_table_baset::symbol_table_baset
symbol_table_baset(const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map)
Definition: symbol_table_base.h:41
symbol_table_baset::sorted_symbol_names
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...
Definition: symbol_table_base.cpp:36
operator<<
std::ostream & operator<<(std::ostream &out, const symbol_table_baset &symbol_table)
Print the contents of the symbol table.
Definition: symbol_table_base.cpp:77
symbol_table_baset::show
void show(std::ostream &out) const
Print the contents of the symbol table.
Definition: symbol_table_base.cpp:54
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
symbol_base_mapt
std::multimap< irep_idt, irep_idt > symbol_base_mapt
Definition: symbol_table_base.h:14
symbol_table_baset::iteratort::iterator_category
symbolst::iterator::iterator_category iterator_category
Definition: symbol_table_base.h:177
symbol_table_baset::erase
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
symbol_module_mapt
std::multimap< irep_idt, irep_idt > symbol_module_mapt
Definition: symbol_table_base.h:15
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
symbol_table_baset::iteratort::it
symbolst::iterator it
Definition: symbol_table_base.h:157
symbol_table_baset::~symbol_table_baset
virtual ~symbol_table_baset()
Author: Diffblue Ltd.
Definition: symbol_table_base.cpp:9
symbol_table_baset::next_unused_suffix
virtual std::size_t next_unused_suffix(const std::string &prefix) const
Definition: symbol_table_base.h:72
symbol_table_baset::iteratort::pointer
symbolst::const_iterator::pointer pointer
Definition: symbol_table_base.h:175
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_baset::const_iteratort
symbolst::const_iterator const_iteratort
Definition: symbol_table_base.h:238
symbol_table_baset::iteratort::get_writeable_symbol
symbolt & get_writeable_symbol()
Whereas the dereference operator gives a constant reference to the current symbol,...
Definition: symbol_table_base.h:227
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
symbol_table_baset::end
virtual iteratort end()=0
symbol_table_baset::iteratort::operator*
reference operator*() const
Dereference operator.
Definition: symbol_table_base.h:208
symbol.h
Symbol table entry.
symbol_table_baset::iteratort::operator++
iteratort operator++(int)
Post-increment operator.
Definition: symbol_table_base.h:199
symbol_table_baset::iteratort::on_get_writeable
std::function< void(const irep_idt &id)> on_get_writeable
Definition: symbol_table_base.h:158
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
symbol_table_baset::iteratort::reference
symbolst::const_iterator::reference reference
Definition: symbol_table_base.h:176
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
symbol_table_baset::iteratort
Definition: symbol_table_base.h:154
symbol_table_baset::begin
virtual iteratort begin()=0
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbol_table_baset::symbolst
std::unordered_map< irep_idt, symbolt > symbolst
Definition: symbol_table_base.h:24
symbol_table_baset::iteratort::difference_type
symbolst::iterator::difference_type difference_type
Definition: symbol_table_base.h:173
symbol_table_baset::iteratort::iteratort
iteratort(const iteratort &it, std::function< void(const irep_idt &id)> on_get_writeable)
Definition: symbol_table_base.h:165
symbol_table_baset::operator=
symbol_table_baset & operator=(const symbol_table_baset &other)=delete
symbol_table_baset::iteratort::iteratort
iteratort(symbolst::iterator it)
Definition: symbol_table_base.h:161
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
symbol_table_baset::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbol_table_baset::next_unused_suffix
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.
Definition: symbol_table_base.h:63
symbol_table_baset::iteratort::operator++
iteratort & operator++()
Preincrement operator Do not call on the end() iterator.
Definition: symbol_table_base.h:191
symbol_table_baset::iteratort::value_type
symbolst::const_iterator::value_type value_type
Definition: symbol_table_base.h:174
validation_modet::INVARIANT
symbol_table_baset::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0