cprover
Loading...
Searching...
No Matches
journalling_symbol_table.h
Go to the documentation of this file.
1
2
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{
37public:
38 typedef std::unordered_set<irep_idt> changesett;
39
40private:
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
50private:
59
60public:
62
74
75 virtual const symbol_tablet &get_symbol_table() const override
76 {
78 }
79
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 {
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;
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
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
159private:
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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
static journalling_symbol_tablet wrap(symbol_table_baset &base_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.
journalling_symbol_tablet(journalling_symbol_tablet &&other)
const changesett & get_inserted() const
void on_insert(const irep_idt &id)
const changesett & get_removed() const
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)
symbol_table_baset & base_symbol_table
std::size_t next_unused_suffix(const std::string &prefix) const override
const changesett & get_updated() const
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Move or copy a new symbol to the symbol table.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
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 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
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 iteratort end()=0
virtual const symbol_tablet & get_symbol_table() const =0
The symbol table.
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
STL namespace.
Author: Diffblue Ltd.