cprover
journalling_symbol_table.h
Go to the documentation of this file.
1 
5 
6 #ifndef CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
7 #define CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
8 
9 #include <utility>
10 #include <unordered_set>
11 #include "irep.h"
12 #include "symbol_table.h"
13 
36 {
37 public:
38  typedef std::unordered_set<irep_idt> changesett;
39 
40 private:
42  // Symbols originally in the table will never be marked inserted
44  // get_writeable marks an existing symbol updated
45  // Inserted symbols are marked updated, removed ones aren't
47  // Symbols not originally in the table will never be marked removed
49 
50 private:
57  {
58  }
59 
60 public:
62 
65  other.symbols,
66  other.symbol_base_map,
67  other.symbol_module_map),
69  inserted(std::move(other.inserted)),
70  updated(std::move(other.updated)),
71  removed(std::move(other.removed))
72  {
73  }
74 
75  virtual const symbol_tablet &get_symbol_table() const override
76  {
78  }
79 
81  {
83  }
84 
85  virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
86  {
87  bool ret = base_symbol_table.move(symbol, new_symbol);
88  if(!ret)
89  on_insert(symbol.name);
90  else
91  on_update(symbol.name);
92  return ret;
93  }
94 
95  virtual symbolt *get_writeable(const irep_idt &identifier) override
96  {
97  symbolt *result = base_symbol_table.get_writeable(identifier);
98  if(result)
99  on_update(identifier);
100  return result;
101  }
102 
103  std::size_t next_unused_suffix(const std::string &prefix) const override
104  {
105  return base_symbol_table.next_unused_suffix(prefix);
106  }
107 
108  virtual std::pair<symbolt &, bool> insert(symbolt symbol) override
109  {
110  std::pair<symbolt &, bool> result =
111  base_symbol_table.insert(std::move(symbol));
112  if(result.second)
113  on_insert(result.first.name);
114  return result;
115  }
116 
117  virtual void
118  erase(const symbol_tablet::symbolst::const_iterator &entry) override
119  {
120  const irep_idt entry_name = entry->first;
121  base_symbol_table.erase(entry);
122  on_remove(entry_name);
123  }
124 
125  virtual void clear() override
126  {
127  for(const auto &named_symbol : base_symbol_table.symbols)
128  on_remove(named_symbol.first);
130  }
131 
132  virtual iteratort begin() override
133  {
134  return iteratort(
135  base_symbol_table.begin(), [this](const irep_idt &id) { on_update(id); });
136  }
137  virtual iteratort end() override
138  {
139  return iteratort(
140  base_symbol_table.end(), [this](const irep_idt &id) { on_update(id); });
141  }
142 
145 
146  const changesett &get_inserted() const
147  {
148  return inserted;
149  }
150  const changesett &get_updated() const
151  {
152  return updated;
153  }
154  const changesett &get_removed() const
155  {
156  return removed;
157  }
158 
159 private:
160  void on_insert(const irep_idt &id)
161  {
162  if(removed.erase(id) == 0)
163  inserted.insert(id);
164  updated.insert(id);
165  }
166 
167  void on_update(const irep_idt &id)
168  {
169  updated.insert(id);
170  }
171 
172  void on_remove(const irep_idt &id)
173  {
174  if(inserted.erase(id) == 0)
175  removed.insert(id);
176  updated.erase(id);
177  }
178 };
179 
180 #endif // CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
virtual iteratort begin() override
const changesett & get_updated() const
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Move or copy a new symbol to the symbol table.
journalling_symbol_tablet(const journalling_symbol_tablet &other)=delete
virtual void erase(const symbol_tablet::symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual symbolt * get_writeable(const irep_idt &identifier) override
Find a symbol in the symbol table for read-write access.
virtual const symbol_tablet & get_symbol_table() const override
journalling_symbol_tablet(journalling_symbol_tablet &&other)
void on_insert(const irep_idt &id)
virtual iteratort end() override
void on_remove(const irep_idt &id)
std::unordered_set< irep_idt > changesett
journalling_symbol_tablet(symbol_table_baset &base_symbol_table)
const changesett & get_removed() const
symbol_table_baset & base_symbol_table
std::size_t next_unused_suffix(const std::string &prefix) const override
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
const changesett & get_inserted() const
void on_update(const irep_idt &id)
The symbol table base class interface.
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
virtual void clear()=0
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
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
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
virtual iteratort end()=0
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
Author: Diffblue Ltd.