cprover
Loading...
Searching...
No Matches
symbol_table_base.h
Go to the documentation of this file.
1
2
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 <map>
12#include <unordered_map>
13
14typedef std::multimap<irep_idt, irep_idt> symbol_base_mapt;
15typedef std::multimap<irep_idt, irep_idt> symbol_module_mapt;
16
17class symbol_tablet;
18
22{
23public:
24 typedef std::unordered_map<irep_idt, symbolt> symbolst;
25
26public:
39
40public:
50
51 symbol_table_baset(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())
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
114 std::list<symbolst::const_iterator>
116 {
117 std::list<symbolst::const_iterator> results;
118
119 auto name_it = symbols.find(id);
120 if(name_it != symbols.end())
121 results.push_back(name_it);
122
123 auto base_name_it_pair = symbol_base_map.equal_range(id);
124 for(auto base_name_it = base_name_it_pair.first;
126 ++base_name_it)
127 {
128 name_it = symbols.find(base_name_it->second);
129 CHECK_RETURN(name_it != symbols.end());
130 // don't add entries where name and base name match as this amounts to the
131 // case already covered above
132 if(base_name_it->first != base_name_it->second)
133 results.push_back(name_it);
134 }
135
136 return results;
137 }
138
142 virtual symbolt *get_writeable(const irep_idt &name) = 0;
143
149 {
150 symbolt *symbol = get_writeable(name);
151 if(symbol == nullptr)
152 throw std::out_of_range("name not found in symbol_table");
153 return *symbol;
154 }
155
156 bool add(const symbolt &symbol);
166 virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
167 virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
168
169 bool remove(const irep_idt &name);
172 virtual void erase(const symbolst::const_iterator &entry) = 0;
173 virtual void clear() = 0;
174
175 void show(std::ostream &out) const;
176
179 std::vector<irep_idt> sorted_symbol_names() const;
180
182 {
183 private:
184 symbolst::iterator it;
185 std::function<void(const irep_idt &id)> on_get_writeable;
186
187 public:
188 explicit iteratort(symbolst::iterator it) : it(std::move(it))
189 {
190 }
191
193 const iteratort &it,
194 std::function<void(const irep_idt &id)> on_get_writeable)
196 {
197 }
198
199 operator symbolst::const_iterator() const
200 {
201 return symbolst::const_iterator{it};
202 }
203
204 // The following typedefs are NOLINT as they are needed by the STL
205 typedef symbolst::iterator::difference_type difference_type; // NOLINT
206 typedef symbolst::const_iterator::value_type value_type; // NOLINT
207 typedef symbolst::const_iterator::pointer pointer; // NOLINT
208 typedef symbolst::const_iterator::reference reference; // NOLINT
209 typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
210
211 bool operator!=(const iteratort &other) const
212 {
213 return it != other.it;
214 }
215
216 bool operator==(const iteratort &other) const
217 {
218 return it == other.it;
219 }
220
224 {
225 ++it;
226 return *this;
227 }
228
232 {
233 iteratort copy(*this);
234 this->operator++();
235 return copy;
236 }
237
241 {
242 return *it;
243 }
244
248 {
249 return &**this;
250 }
251
260 {
262 on_get_writeable((*this)->first);
263 return it->second;
264 }
265 };
266
267 virtual iteratort begin() = 0;
268 virtual iteratort end() = 0;
269
270 using const_iteratort = symbolst::const_iterator;
271
272 virtual const_iteratort begin() const;
273 virtual const_iteratort end() const;
274
275 virtual void
277};
278
279std::ostream &
280operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
281
282#endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool operator==(const iteratort &other) const
std::function< void(const irep_idt &id)> on_get_writeable
iteratort operator++(int)
Post-increment operator.
iteratort & operator++()
Preincrement operator Do not call on the end() iterator.
bool operator!=(const iteratort &other) const
symbolst::iterator::iterator_category iterator_category
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
symbolt & get_writeable_symbol()
Whereas the dereference operator gives a constant reference to the current symbol,...
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
symbol_table_baset & operator=(const symbol_table_baset &other)=delete
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy 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 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
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.
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.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
virtual const symbol_tablet & get_symbol_table() const =0
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual ~symbol_table_baset()
Author: Diffblue Ltd.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual std::size_t next_unused_suffix(const std::string &prefix) const
symbol_table_baset(const symbol_table_baset &other)=delete
The symbol table.
Symbol table entry.
Definition symbol.h:28
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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