diff --git a/src/util/symbol_table_writer.h b/src/util/symbol_table_writer.h new file mode 100644 index 00000000000..e502a097371 --- /dev/null +++ b/src/util/symbol_table_writer.h @@ -0,0 +1,163 @@ + +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. + +/// \file +/// A symbol table writer that records which entries have been updated + +#ifndef CPROVER_UTIL_SYMBOL_TABLE_WRITER_H +#define CPROVER_UTIL_SYMBOL_TABLE_WRITER_H + +#include +#include +#include "irep.h" +#include "symbol_table.h" + +/// \brief A symbol table wrapper that records which entries have been +/// updated/removed +/// \ingroup gr_symbol_table +/// A caller can pass a `journalling_symbol_table_writert` into a callee that is +/// expected to mutate it somehow, then after it has run inspect the recording +/// table's journal to determine what has changed more cheaply than examining +/// every symbol. +/// +/// Example of usage: +/// ``` +/// symbol_tablet real_table; +/// init_table(real_table); +/// +/// journalling_symbol_table_writert journal(actual_table); // Wraps real_table +/// alter_table(journal); + +/// for(const auto &added : journal.added()) +/// { +/// printf("%s was added\n", added.name); +/// } +class journalling_symbol_table_writert +{ +public: + typedef std::unordered_set changesett; +private: + symbol_tablet &base_symbol_table; + // Symbols originally in the table will never be marked inserted + changesett inserted; + // get_writeable marks an existing symbol updated + // Inserted symbols are marked updated, removed ones aren't + changesett updated; + // Symbols not originally in the table will never be marked removed + changesett removed; + +private: + explicit journalling_symbol_table_writert(symbol_tablet &base_symbol_table): + base_symbol_table(base_symbol_table) + { + } + +public: + journalling_symbol_table_writert( + const journalling_symbol_table_writert &other): + base_symbol_table(other.base_symbol_table) + { + } + + /// Permits implicit cast to const symbol_tablet & + operator const symbol_tablet &() const + { + return base_symbol_table; + } + + static journalling_symbol_table_writert wrap( + symbol_tablet &base_symbol_table) + { + return journalling_symbol_table_writert(base_symbol_table); + } + + bool add(const symbolt &symbol) + { + bool ret=base_symbol_table.add(symbol); + if(!ret) + on_insert(symbol.name); + return ret; + } + + bool move(symbolt &symbol, symbolt *&new_symbol) + { + bool ret=base_symbol_table.move(symbol, new_symbol); + if(!ret) + on_insert(symbol.name); + else + on_update(symbol.name); + return ret; + } + + symbolt *get_writeable(const irep_idt &identifier) + { + symbolt *result=base_symbol_table.get_writeable(identifier); + if(result) + on_update(identifier); + return result; + } + + symbolt &get_writeable_ref(const irep_idt &identifier) + { + // Run on_update *after* the get-ref operation in case it throws + symbolt &result=base_symbol_table.get_writeable_ref(identifier); + on_update(identifier); + return result; + } + + std::pair insert(symbolt symbol) + { + std::pair result= + base_symbol_table.insert(std::move(symbol)); + if(result.second) + on_insert(result.first.name); + return result; + } + + bool remove(const irep_idt &id) + { + bool ret=base_symbol_table.remove(id); + if(!ret) + on_remove(id); + return ret; + } + + void erase(const symbol_tablet::symbolst::const_iterator &entry) + { + base_symbol_table.erase(entry); + on_remove(entry->first); + } + + void clear() + { + for(const auto &named_symbol : base_symbol_table.symbols) + on_remove(named_symbol.first); + base_symbol_table.clear(); + } + + const changesett &get_inserted() const { return inserted; } + const changesett &get_updated() const { return updated; } + const changesett &get_removed() const { return removed; } + +private: + void on_insert(const irep_idt &id) + { + if(removed.erase(id)==0) + inserted.insert(id); + updated.insert(id); + } + + void on_update(const irep_idt &id) + { + updated.insert(id); + } + + void on_remove(const irep_idt &id) + { + if(inserted.erase(id)==0) + removed.insert(id); + updated.erase(id); + } +}; + +#endif // CPROVER_UTIL_SYMBOL_TABLE_WRITER_H diff --git a/unit/Makefile b/unit/Makefile index 379918fa56f..d667c199036 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -31,6 +31,7 @@ SRC += unit_tests.cpp \ util/expr_iterator.cpp \ util/message.cpp \ util/simplify_expr.cpp \ + util/symbol_table.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp new file mode 100644 index 00000000000..981a86b8b2a --- /dev/null +++ b/unit/util/symbol_table.cpp @@ -0,0 +1,250 @@ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. + +/// \file Tests for symbol_tablet + +#include +#include + +SCENARIO("journalling_symbol_table_writer", + "[core][utils][journalling_symbol_table_writer]") +{ + GIVEN("A journalling_symbol_table_writert wrapping an empty symbol_tablet") + { + symbol_tablet base_symbol_table; + journalling_symbol_table_writert symbol_table= + journalling_symbol_table_writert::wrap(base_symbol_table); + const symbol_tablet &read_symbol_table=symbol_table; + + irep_idt symbol_name="Test"; + symbolt symbol; + symbol.name=symbol_name; + + WHEN("A symbol is inserted into the symbol table") + { + auto result=symbol_table.insert(symbol); + THEN("The insert should succeed") + { + REQUIRE(result.second); + } + THEN("The inserted symbol should have the same name") + { + REQUIRE(result.first.name==symbol_name); + } + THEN( + "The symbol table should return a symbol from a lookup of that name") + { + REQUIRE(read_symbol_table.lookup(symbol_name)!=nullptr); + } + THEN("The symbol table should return the same symbol from a lookup") + { + REQUIRE(&result.first==read_symbol_table.lookup(symbol_name)); + } + THEN("The added symbol should appear in the updated collection") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==1); + } + THEN("The added symbol should not appear in the removed collection") + { + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + WHEN("Adding the same symbol again") + { + symbolt symbol; + symbol.name=symbol_name; + auto result=symbol_table.insert(symbol); + THEN("The insert should fail") + { + REQUIRE(!result.second); + } + } + } + WHEN("Moving a symbol into the symbol table") + { + symbolt *symbol_in_table; + auto result=symbol_table.move(symbol, symbol_in_table); + THEN("The move should succeed") + { + REQUIRE(!result); + } + THEN( + "The symbol table should return a symbol from a lookup of that name") + { + REQUIRE(read_symbol_table.lookup(symbol_name)!=nullptr); + } + THEN("The symbol table should return the same symbol from a lookup") + { + REQUIRE(symbol_in_table==read_symbol_table.lookup(symbol_name)); + } + THEN("The added symbol should appear in the updated collection") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==1); + } + THEN("The added symbol should not appear in the removed collection") + { + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + WHEN("Moving the same symbol again") + { + symbolt symbol; + symbol.name=symbol_name; + symbolt *symbol_in_table2; + auto result=symbol_table.move(symbol, symbol_in_table2); + THEN("The move should fail") + { + REQUIRE(result); + } + THEN("The returned pointer should match the previous move result") + { + REQUIRE(symbol_in_table==symbol_in_table2); + } + } + } + WHEN("Adding a symbol to the symbol table") + { + auto result=symbol_table.add(symbol); + THEN("The add should succeed") + { + REQUIRE(!result); + } + THEN( + "The symbol table should return a symbol from a lookup of that name") + { + REQUIRE(read_symbol_table.lookup(symbol_name)!=nullptr); + } + THEN("The symbol table should return the same symbol from a lookup") + { + REQUIRE(symbol.name==read_symbol_table.lookup(symbol_name)->name); + } + THEN("The added symbol should appear in the updated collection") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==1); + } + THEN("The added symbol should not appear in the removed collection") + { + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + WHEN("Adding the same symbol again") + { + symbolt symbol; + symbol.name=symbol_name; + auto result=symbol_table.add(symbol); + THEN("The insert should fail") + { + REQUIRE(result); + } + } + } + WHEN("Updating an existing symbol") + { + base_symbol_table.add(symbol); + symbolt *writeable=symbol_table.get_writeable(symbol_name); + + THEN("get_writeable should succeed") + { + REQUIRE(writeable!=nullptr); + } + THEN("get_writeable should return the same pointer " + "as the underlying table") + { + symbolt *writeable2=base_symbol_table.get_writeable(symbol_name); + REQUIRE(writeable==writeable2); + } + THEN("get_writeable_ref should not throw") + { + symbol_table.get_writeable_ref(symbol_name); + } + THEN("The updated symbol should appear in the updated collection") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==1); + } + THEN("The updated symbol should not appear in the removed collection") + { + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + } + WHEN("Removing a non-existent symbol") + { + irep_idt symbol_name="DoesNotExist"; + bool ret=symbol_table.remove(symbol_name); + THEN("The remove operation should fail") + { + REQUIRE(ret); + } + THEN("The symbol we failed to remove should appear in neither journal") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==0); + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + } + WHEN("Removing an existing symbol added via the journalling writer") + { + symbol_table.add(symbol); + bool ret=symbol_table.remove(symbol_name); + THEN("The remove operation should succeed") + { + REQUIRE(!ret); + } + THEN("The symbol should appear in neither journal") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==0); + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + } + WHEN("Removing an existing symbol added outside the journalling writer") + { + base_symbol_table.add(symbol); + bool ret=symbol_table.remove(symbol_name); + THEN("The remove operation should succeed") + { + REQUIRE(!ret); + } + THEN("The symbol we removed should be journalled as removed " + "but not updated") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==0); + REQUIRE(symbol_table.get_removed().count(symbol_name)==1); + } + } + WHEN("Removing an existing symbol using an iterator (added via writer)") + { + symbol_table.add(symbol); + auto erase_iterator=read_symbol_table.symbols.find(symbol_name); + symbol_table.erase(erase_iterator); + THEN("The symbol should appear in neither journal") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==0); + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + } + WHEN("Removing an existing symbol using an iterator (added via base)") + { + base_symbol_table.add(symbol); + auto erase_iterator=read_symbol_table.symbols.find(symbol_name); + symbol_table.erase(erase_iterator); + THEN("The symbol should be journalled as removed") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==0); + REQUIRE(symbol_table.get_removed().count(symbol_name)==1); + } + } + WHEN("Re-adding a symbol previously removed") + { + auto result=symbol_table.add(symbol); + symbol_table.remove(symbol.name); + auto result2=symbol_table.add(symbol); + THEN("The first add should succeed") + { + REQUIRE(!result); + } + THEN("The second add should succeed") + { + REQUIRE(!result); + } + THEN("The symbol should be journalled as updated but not removed") + { + REQUIRE(symbol_table.get_updated().count(symbol_name)==1); + REQUIRE(symbol_table.get_removed().count(symbol_name)==0); + } + } + } +}