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:
27  const symbolst &symbols;
30 
31 public:
33  const symbolst &symbols,
36  : symbols(symbols),
39  {
40  }
41 
42  symbol_table_baset(const symbol_table_baset &other) = delete;
43  symbol_table_baset &operator=(const symbol_table_baset &other) = delete;
44 
45  virtual ~symbol_table_baset();
46 
47 public:
49  operator const symbol_tablet &() const
50  {
51  return get_symbol_table();
52  }
53  virtual const symbol_tablet &get_symbol_table() const = 0;
54 
58  bool has_symbol(const irep_idt &name) const
59  {
60  return symbols.find(name) != symbols.end();
61  }
62 
66  const symbolt *lookup(const irep_idt &name) const
67  {
68  symbolst::const_iterator it = symbols.find(name);
69  return it != symbols.end() ? &it->second : nullptr;
70  }
71 
76  const symbolt &lookup_ref(const irep_idt &name) const
77  {
78  return symbols.at(name);
79  }
80 
84  virtual symbolt *get_writeable(const irep_idt &name) = 0;
85 
91  {
92  symbolt *symbol = get_writeable(name);
93  if(symbol == nullptr)
94  throw std::out_of_range("name not found in symbol_table");
95  return *symbol;
96  }
97 
98  bool add(const symbolt &symbol);
107  virtual std::pair<symbolt &, bool> insert(symbolt symbol) = 0;
108  virtual bool move(symbolt &symbol, symbolt *&new_symbol) = 0;
109 
110  bool remove(const irep_idt &name);
113  virtual void erase(const symbolst::const_iterator &entry) = 0;
114  virtual void clear() = 0;
115 
116  void show(std::ostream &out) const;
117 
118  class iteratort
119  {
120  private:
121  symbolst::iterator it;
122  std::function<void(const irep_idt &id)> on_get_writeable;
123 
124  public:
125  explicit iteratort(symbolst::iterator it) : it(std::move(it))
126  {
127  }
128 
130  const iteratort &it,
131  std::function<void(const irep_idt &id)> on_get_writeable)
133  {
134  }
135 
136  // The following typedefs are NOLINT as they are needed by the STL
137  typedef symbolst::iterator::difference_type difference_type; // NOLINT
138  typedef symbolst::const_iterator::value_type value_type; // NOLINT
139  typedef symbolst::const_iterator::pointer pointer; // NOLINT
140  typedef symbolst::const_iterator::reference reference; // NOLINT
141  typedef symbolst::iterator::iterator_category iterator_category; // NOLINT
142 
143  bool operator!=(const iteratort &other) const
144  {
145  return it != other.it;
146  }
147 
148  bool operator==(const iteratort &other) const
149  {
150  return it == other.it;
151  }
152 
156  {
157  ++it;
158  return *this;
159  }
160 
164  {
165  iteratort copy(*this);
166  this->operator++();
167  return copy;
168  }
169 
173  {
174  return *it;
175  }
176 
180  {
181  return &**this;
182  }
183 
185  {
186  if(on_get_writeable)
187  on_get_writeable((*this)->first);
188  return it->second;
189  }
190  };
191 
192  virtual iteratort begin() = 0;
193  virtual iteratort end() = 0;
194 };
195 
196 std::ostream &
197 operator<<(std::ostream &out, const symbol_table_baset &symbol_table);
198 
199 #endif // CPROVER_UTIL_SYMBOL_TABLE_BASE_H
reference operator*() const
Dereference operator.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
void show(std::ostream &out) const
Print the contents of the symbol table.
std::ostream & operator<<(std::ostream &out, const symbol_table_baset &symbol_table)
Print the contents of the symbol table.
symbolst::iterator::difference_type difference_type
const symbol_base_mapt & symbol_base_map
std::multimap< irep_idt, irep_idt > symbol_base_mapt
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
bool operator==(const iteratort &other) const
symbolst::const_iterator::pointer pointer
STL namespace.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
symbolst::iterator::iterator_category iterator_category
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
std::multimap< irep_idt, irep_idt > symbol_module_mapt
symbolt & get_writeable_symbol(const irep_idt &identifier)
iteratort operator++(int)
Post-increment operator.
symbol_table_baset(const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map)
std::unordered_map< irep_idt, symbolt > symbolst
The symbol table.
Definition: symbol_table.h:19
const symbol_module_mapt & symbol_module_map
virtual iteratort begin()=0
const symbolst & symbols
virtual iteratort end()=0
symbolst::const_iterator::value_type value_type
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
symbolst::const_iterator::reference reference
iteratort(const iteratort &it, std::function< void(const irep_idt &id)> on_get_writeable)
symbol_table_baset & operator=(const symbol_table_baset &other)=delete
iteratort & operator++()
Preincrement operator Do not call on the end() iterator.
virtual ~symbol_table_baset()
Author: Diffblue Ltd.
The symbol table base class interface.
std::function< void(const irep_idt &id)> on_get_writeable
pointer operator->() const
Dereference operator (member access)
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual const symbol_tablet & get_symbol_table() const =0
bool operator!=(const iteratort &other) const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual void clear()=0
iteratort(symbolst::iterator it)