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 
29 
34 class journalling_symbol_tablet : public symbol_table_baset
35 {
36 public:
37  typedef std::unordered_set<irep_idt> changesett;
38 
39 private:
40  symbol_table_baset &base_symbol_table;
41  // Symbols originally in the table will never be marked inserted
42  changesett inserted;
43  // get_writeable marks an existing symbol updated
44  // Inserted symbols are marked updated, removed ones aren't
45  changesett updated;
46  // Symbols not originally in the table will never be marked removed
47  changesett removed;
48 
49 private:
50  explicit journalling_symbol_tablet(symbol_table_baset &base_symbol_table)
52  base_symbol_table.symbols,
53  base_symbol_table.symbol_base_map,
54  base_symbol_table.symbol_module_map),
55  base_symbol_table(base_symbol_table)
56  {
57  }
58 
59 public:
60  journalling_symbol_tablet(const journalling_symbol_tablet &other) = delete;
61 
62  journalling_symbol_tablet(journalling_symbol_tablet &&other)
64  other.symbols,
65  other.symbol_base_map,
66  other.symbol_module_map),
67  base_symbol_table(other.base_symbol_table),
68  inserted(std::move(other.inserted)),
69  updated(std::move(other.updated)),
70  removed(std::move(other.removed))
71  {
72  }
73 
74  virtual const symbol_tablet &get_symbol_table() const override
75  {
76  return base_symbol_table.get_symbol_table();
77  }
78 
79  static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
80  {
81  return journalling_symbol_tablet(base_symbol_table);
82  }
83 
84  virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
85  {
86  bool ret = base_symbol_table.move(symbol, new_symbol);
87  if(!ret)
88  on_insert(symbol.name);
89  else
90  on_update(symbol.name);
91  return ret;
92  }
93 
94  virtual symbolt *get_writeable(const irep_idt &identifier) override
95  {
96  symbolt *result = base_symbol_table.get_writeable(identifier);
97  if(result)
98  on_update(identifier);
99  return result;
100  }
101 
102  virtual std::pair<symbolt &, bool> insert(symbolt symbol) override
103  {
104  std::pair<symbolt &, bool> result =
105  base_symbol_table.insert(std::move(symbol));
106  if(result.second)
107  on_insert(result.first.name);
108  return result;
109  }
110 
111  virtual void
112  erase(const symbol_tablet::symbolst::const_iterator &entry) override
113  {
114  const irep_idt entry_name = entry->first;
115  base_symbol_table.erase(entry);
116  on_remove(entry_name);
117  }
118 
119  virtual void clear() override
120  {
121  for(const auto &named_symbol : base_symbol_table.symbols)
122  on_remove(named_symbol.first);
123  base_symbol_table.clear();
124  }
125 
126  virtual iteratort begin() override
127  {
128  return iteratort(
129  base_symbol_table.begin(), [this](const irep_idt &id) { on_update(id); });
130  }
131  virtual iteratort end() override
132  {
133  return iteratort(
134  base_symbol_table.end(), [this](const irep_idt &id) { on_update(id); });
135  }
136 
137  const changesett &get_inserted() const
138  {
139  return inserted;
140  }
141  const changesett &get_updated() const
142  {
143  return updated;
144  }
145  const changesett &get_removed() const
146  {
147  return removed;
148  }
149 
150 private:
151  void on_insert(const irep_idt &id)
152  {
153  if(removed.erase(id) == 0)
154  inserted.insert(id);
155  updated.insert(id);
156  }
157 
158  void on_update(const irep_idt &id)
159  {
160  updated.insert(id);
161  }
162 
163  void on_remove(const irep_idt &id)
164  {
165  if(inserted.erase(id) == 0)
166  removed.insert(id);
167  updated.erase(id);
168  }
169 };
170 
171 #endif // CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
irep_idt name
The unique identifier.
Definition: symbol.h:43
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
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
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
The symbol table.
Definition: symbol_table.h:19
Author: Diffblue Ltd.
virtual iteratort begin()=0
const symbolst & symbols
virtual iteratort end()=0
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual const symbol_tablet & get_symbol_table() const =0
virtual void clear()=0