Skip to content

Commit a2b45e3

Browse files
NathanJPhillipsNathanJPhillips
committed
Update to journalling symbol table
Split a common base class out to reduce impact of usage sites
1 parent 7aa80ad commit a2b45e3

8 files changed

+372
-303
lines changed

‎src/util/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,7 @@ SRC = arith_tools.cpp \
8080
string_utils.cpp \
8181
substitute.cpp \
8282
symbol.cpp \
83+
symbol_table_base.cpp \
8384
symbol_table.cpp \
8485
tempdir.cpp \
8586
tempfile.cpp \

‎src/util/journalling_symbol_table.h

+161
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
2+
// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
3+
4+
/// \file
5+
/// A symbol table writer that records which entries have been updated
6+
7+
#ifndef CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
8+
#define CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H
9+
10+
#include <utility>
11+
#include <unordered_set>
12+
#include "irep.h"
13+
#include "symbol_table.h"
14+
15+
/// \brief A symbol table wrapper that records which entries have been
16+
/// updated/removed
17+
/// \ingroup gr_symbol_table
18+
/// A caller can pass a `journalling_symbol_tablet` into a callee that is
19+
/// expected to mutate it somehow, then after it has run inspect the recording
20+
/// table's journal to determine what has changed more cheaply than examining
21+
/// every symbol.
22+
///
23+
/// Example of usage:
24+
/// ```
25+
/// symbol_tablet real_table;
26+
/// init_table(real_table);
27+
///
28+
/// journalling_symbol_tablet journal(actual_table); // Wraps real_table
29+
/// alter_table(journal);
30+
31+
/// for(const auto &added : journal.added())
32+
/// {
33+
/// printf("%s was added\n", added.name);
34+
/// }
35+
class journalling_symbol_tablet : public symbol_table_baset
36+
{
37+
public:
38+
typedef std::unordered_set<irep_idt, irep_id_hash> changesett;
39+
40+
private:
41+
symbol_tablet &base_symbol_table;
42+
// Symbols originally in the table will never be marked inserted
43+
changesett inserted;
44+
// get_writeable marks an existing symbol updated
45+
// Inserted symbols are marked updated, removed ones aren't
46+
changesett updated;
47+
// Symbols not originally in the table will never be marked removed
48+
changesett removed;
49+
50+
private:
51+
explicit journalling_symbol_tablet(symbol_tablet &base_symbol_table)
52+
: symbol_table_baset(
53+
base_symbol_table.symbols,
54+
base_symbol_table.symbol_base_map,
55+
base_symbol_table.symbol_module_map),
56+
base_symbol_table(base_symbol_table)
57+
{
58+
}
59+
60+
public:
61+
journalling_symbol_tablet(const journalling_symbol_tablet &other) = delete;
62+
63+
journalling_symbol_tablet(journalling_symbol_tablet &&other)
64+
: symbol_table_baset(
65+
other.symbols,
66+
other.symbol_base_map,
67+
other.symbol_module_map),
68+
base_symbol_table(other.base_symbol_table),
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+
{
77+
return base_symbol_table;
78+
}
79+
80+
static journalling_symbol_tablet wrap(symbol_tablet &base_symbol_table)
81+
{
82+
return journalling_symbol_tablet(base_symbol_table);
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+
virtual std::pair<symbolt &, bool> insert(symbolt symbol) override
104+
{
105+
std::pair<symbolt &, bool> result =
106+
base_symbol_table.insert(std::move(symbol));
107+
if(result.second)
108+
on_insert(result.first.name);
109+
return result;
110+
}
111+
112+
virtual void
113+
erase(const symbol_tablet::symbolst::const_iterator &entry) override
114+
{
115+
const irep_idt entry_name = entry->first;
116+
base_symbol_table.erase(entry);
117+
on_remove(entry_name);
118+
}
119+
120+
virtual void clear() override
121+
{
122+
for(const auto &named_symbol : base_symbol_table.symbols)
123+
on_remove(named_symbol.first);
124+
base_symbol_table.clear();
125+
}
126+
127+
const changesett &get_inserted() const
128+
{
129+
return inserted;
130+
}
131+
const changesett &get_updated() const
132+
{
133+
return updated;
134+
}
135+
const changesett &get_removed() const
136+
{
137+
return removed;
138+
}
139+
140+
private:
141+
void on_insert(const irep_idt &id)
142+
{
143+
if(removed.erase(id) == 0)
144+
inserted.insert(id);
145+
updated.insert(id);
146+
}
147+
148+
void on_update(const irep_idt &id)
149+
{
150+
updated.insert(id);
151+
}
152+
153+
void on_remove(const irep_idt &id)
154+
{
155+
if(inserted.erase(id) == 0)
156+
removed.insert(id);
157+
updated.erase(id);
158+
}
159+
};
160+
161+
#endif // CPROVER_UTIL_JOURNALLING_SYMBOL_TABLE_H

‎src/util/symbol_table.cpp

-53
Original file line numberDiff line numberDiff line change
@@ -2,19 +2,8 @@
22

33
#include "symbol_table.h"
44

5-
#include <ostream>
6-
#include <algorithm>
75
#include <util/invariant.h>
86

9-
/// Add a new symbol to the symbol table
10-
/// \param symbol: The symbol to be added to the symbol table
11-
/// \return Returns true if the process failed, which should only happen if
12-
/// there is a symbol with the same name already in the symbol table.
13-
bool symbol_tablet::add(const symbolt &symbol)
14-
{
15-
return !insert(symbol).second;
16-
}
17-
187
/// Move or copy a new symbol to the symbol table
198
/// \remark: This is a nicer interface than move and achieves the same
209
/// result as both move and add
@@ -90,19 +79,6 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
9079
return !result.second;
9180
}
9281

93-
/// Remove a symbol from the symbol table
94-
/// \param name: The name of the symbol to remove
95-
/// \return Returns a boolean indicating whether the process failed
96-
/// i.e. false if the symbol was removed, or true if it didn't exist.
97-
bool symbol_tablet::remove(const irep_idt &name)
98-
{
99-
symbolst::const_iterator entry=symbols.find(name);
100-
if(entry==symbols.end())
101-
return true;
102-
erase(entry);
103-
return false;
104-
}
105-
10682
/// Remove a symbol from the symbol table
10783
/// \param entry: an iterator pointing at the symbol to remove
10884
void symbol_tablet::erase(const symbolst::const_iterator &entry)
@@ -138,32 +114,3 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry)
138114

139115
internal_symbols.erase(entry);
140116
}
141-
142-
/// Print the contents of the symbol table
143-
/// \param out: The ostream to direct output to
144-
void symbol_tablet::show(std::ostream &out) const
145-
{
146-
std::vector<irep_idt> sorted_names;
147-
sorted_names.reserve(symbols.size());
148-
for(const auto &elem : symbols)
149-
sorted_names.push_back(elem.first);
150-
std::sort(
151-
sorted_names.begin(),
152-
sorted_names.end(),
153-
[](const irep_idt &a, const irep_idt &b)
154-
{
155-
return as_string(a) < as_string(b);
156-
});
157-
out << "\n" << "Symbols:" << "\n";
158-
for(const auto &name : sorted_names)
159-
out << symbols.at(name);
160-
}
161-
162-
/// Print the contents of the symbol table
163-
/// \param out: The ostream to direct output to
164-
/// \param symbol_table: The symbol table to print out
165-
std::ostream &operator<<(std::ostream &out, const symbol_tablet &symbol_table)
166-
{
167-
symbol_table.show(out);
168-
return out;
169-
}

0 commit comments

Comments
 (0)