Add symbol table writer
This wraps a symbol table, providing an interface matching its write side (but not type-compatible, to avoid implicit casts between the two), and journals modifcations such that callers can determine what changes were made by code using this wrapper to add, update and remove symbols
This commit is contained in:
Chris Smowton
parent
62675bb28f
commit
c3c24e2d98
|
|
@ -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 <utility>
|
||||
#include <unordered_set>
|
||||
#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<irep_idt, irep_id_hash> 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<symbolt &, bool> insert(symbolt symbol)
|
||||
{
|
||||
std::pair<symbolt &, bool> 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
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,250 @@
|
|||
// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
|
||||
|
||||
/// \file Tests for symbol_tablet
|
||||
|
||||
#include <testing-utils/catch.hpp>
|
||||
#include <util/symbol_table_writer.h>
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
Loading…
Reference in New Issue