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 
143  const changesett &get_inserted() const
144  {
145  return inserted;
146  }
147  const changesett &get_updated() const
148  {
149  return updated;
150  }
151  const changesett &get_removed() const
152  {
153  return removed;
154  }
155 
156 private:
157  void on_insert(const irep_idt &id)
158  {
159  if(removed.erase(id) == 0)
160  inserted.insert(id);
161  updated.insert(id);
162  }
163 
164  void on_update(const irep_idt &id)
165  {
166  updated.insert(id);
167  }
168 
169  void on_remove(const irep_idt &id)
170  {
171  if(inserted.erase(id) == 0)
172  removed.insert(id);
173  updated.erase(id);
174  }
175 };
176 
177 #endif // CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
irep_idt name
The unique identifier.
Definition: symbol.h:40
journalling_symbol_tablet(symbol_table_baset &base_symbol_table)
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
journalling_symbol_tablet(journalling_symbol_tablet &&other)
const symbol_base_mapt & symbol_base_map
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void on_update(const irep_idt &id)
virtual symbolt * get_writeable(const irep_idt &identifier) override
Find a symbol in the symbol table for read-write access.
STL namespace.
Symbol table entry.
Definition: symbol.h:27
void on_insert(const irep_idt &id)
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
virtual const symbol_tablet & get_symbol_table() const override
symbol_table_baset & base_symbol_table
const changesett & get_updated() const
const changesett & get_inserted() const
The symbol table.
Definition: symbol_table.h:19
const symbol_module_mapt & symbol_module_map
const changesett & get_removed() const
std::size_t next_unused_suffix(const std::string &prefix) const override
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
virtual iteratort begin()=0
virtual iteratort end() override
const symbolst & symbols
virtual iteratort end()=0
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Move or copy a new symbol to the symbol table.
void on_remove(const irep_idt &id)
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
The symbol table base class interface.
std::unordered_set< irep_idt > changesett
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...
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual void erase(const symbol_tablet::symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
virtual const symbol_tablet & get_symbol_table() const =0
virtual iteratort begin() override
virtual void clear()=0
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override