cprover
journalling_symbol_tablet Class Reference

A symbol table wrapper that records which entries have been updated/removedA caller can pass a journalling_symbol_tablet 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. More...

#include <journalling_symbol_table.h>

+ Inheritance diagram for journalling_symbol_tablet:
+ Collaboration diagram for journalling_symbol_tablet:

Public Types

typedef std::unordered_set< irep_idtchangesett
 
- Public Types inherited from symbol_table_baset
typedef std::unordered_map< irep_idt, symboltsymbolst
 

Public Member Functions

 journalling_symbol_tablet (const journalling_symbol_tablet &other)=delete
 
 journalling_symbol_tablet (journalling_symbol_tablet &&other)
 
virtual const symbol_tabletget_symbol_table () const override
 
virtual bool move (symbolt &symbol, symbolt *&new_symbol) override
 
virtual symboltget_writeable (const irep_idt &identifier) override
 Find a symbol in the symbol table for read-write access. More...
 
virtual std::pair< symbolt &, bool > insert (symbolt symbol) override
 Move or copy a new symbol to the symbol table. More...
 
virtual void erase (const symbol_tablet::symbolst::const_iterator &entry) override
 Remove a symbol from the symbol table. More...
 
virtual void clear () override
 
virtual iteratort begin () override
 
virtual iteratort end () override
 
const changesettget_inserted () const
 
const changesettget_updated () const
 
const changesettget_removed () const
 
- Public Member Functions inherited from symbol_table_baset
 symbol_table_baset (const symbolst &symbols, const symbol_base_mapt &symbol_base_map, const symbol_module_mapt &symbol_module_map)
 
 symbol_table_baset (const symbol_table_baset &other)=delete
 
symbol_table_basetoperator= (const symbol_table_baset &other)=delete
 
virtual ~symbol_table_baset ()
 Author: Diffblue Ltd. More...
 
 operator const symbol_tablet & () const
 Permits implicit cast to const symbol_tablet &. More...
 
bool has_symbol (const irep_idt &name) const
 Check whether a symbol exists in the symbol table. More...
 
const symboltlookup (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
const symboltlookup_ref (const irep_idt &name) const
 Find a symbol in the symbol table for read-only access. More...
 
symboltget_writeable_ref (const irep_idt &name)
 Find a symbol in the symbol table for read-write access. More...
 
bool add (const symbolt &symbol)
 Add a new symbol to the symbol table. More...
 
bool remove (const irep_idt &name)
 Remove a symbol from the symbol table. More...
 
void show (std::ostream &out) const
 Print the contents of the symbol table. More...
 

Static Public Member Functions

static journalling_symbol_tablet wrap (symbol_table_baset &base_symbol_table)
 

Private Member Functions

 journalling_symbol_tablet (symbol_table_baset &base_symbol_table)
 
void on_insert (const irep_idt &id)
 
void on_update (const irep_idt &id)
 
void on_remove (const irep_idt &id)
 

Private Attributes

symbol_table_basetbase_symbol_table
 
changesett inserted
 
changesett updated
 
changesett removed
 

Additional Inherited Members

- Public Attributes inherited from symbol_table_baset
const symbolstsymbols
 
const symbol_base_maptsymbol_base_map
 
const symbol_module_maptsymbol_module_map
 

Detailed Description

A symbol table wrapper that records which entries have been updated/removed

A caller can pass a journalling_symbol_tablet 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_tablet journal(actual_table); // Wraps real_table
alter_table(journal);
for(const auto &added : journal.added())
{
printf("%s was added\n", added.name);
}

Definition at line 35 of file journalling_symbol_table.h.

Member Typedef Documentation

◆ changesett

typedef std::unordered_set<irep_idt> journalling_symbol_tablet::changesett

Definition at line 38 of file journalling_symbol_table.h.

Constructor & Destructor Documentation

◆ journalling_symbol_tablet() [1/3]

journalling_symbol_tablet::journalling_symbol_tablet ( symbol_table_baset base_symbol_table)
inlineexplicitprivate

Definition at line 51 of file journalling_symbol_table.h.

◆ journalling_symbol_tablet() [2/3]

journalling_symbol_tablet::journalling_symbol_tablet ( const journalling_symbol_tablet other)
delete

◆ journalling_symbol_tablet() [3/3]

journalling_symbol_tablet::journalling_symbol_tablet ( journalling_symbol_tablet &&  other)
inline

Definition at line 63 of file journalling_symbol_table.h.

Member Function Documentation

◆ begin()

virtual iteratort journalling_symbol_tablet::begin ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 127 of file journalling_symbol_table.h.

◆ clear()

virtual void journalling_symbol_tablet::clear ( void  )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 120 of file journalling_symbol_table.h.

◆ end()

virtual iteratort journalling_symbol_tablet::end ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 132 of file journalling_symbol_table.h.

◆ erase()

virtual void journalling_symbol_tablet::erase ( const symbol_tablet::symbolst::const_iterator &  entry)
inlineoverridevirtual

Remove a symbol from the symbol table.

Parameters
entryan iterator pointing at the symbol to remove

Implements symbol_table_baset.

Definition at line 113 of file journalling_symbol_table.h.

◆ get_inserted()

const changesett& journalling_symbol_tablet::get_inserted ( ) const
inline

Definition at line 138 of file journalling_symbol_table.h.

◆ get_removed()

const changesett& journalling_symbol_tablet::get_removed ( ) const
inline

Definition at line 146 of file journalling_symbol_table.h.

◆ get_symbol_table()

virtual const symbol_tablet& journalling_symbol_tablet::get_symbol_table ( ) const
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 75 of file journalling_symbol_table.h.

◆ get_updated()

const changesett& journalling_symbol_tablet::get_updated ( ) const
inline

Definition at line 142 of file journalling_symbol_table.h.

◆ get_writeable()

virtual symbolt* journalling_symbol_tablet::get_writeable ( const irep_idt name)
inlineoverridevirtual

Find a symbol in the symbol table for read-write access.

Parameters
nameThe name of the symbol to look for
Returns
a pointer to the found symbol if it exists, nullptr otherwise.

Implements symbol_table_baset.

Definition at line 95 of file journalling_symbol_table.h.

◆ insert()

virtual std::pair<symbolt &, bool> journalling_symbol_tablet::insert ( symbolt  symbol)
inlineoverridevirtual

Move or copy a new symbol to the symbol table.

Remarks
: This is a nicer interface than move and achieves the same result as both move and add
Parameters
symbolThe symbol to be added to the symbol table - can be moved or copied in
Returns
Returns a reference to the newly inserted symbol or to the existing symbol if a symbol with the same name already exists in the symbol table, along with a bool that is true if a new symbol was inserted.

Implements symbol_table_baset.

Definition at line 103 of file journalling_symbol_table.h.

◆ move()

virtual bool journalling_symbol_tablet::move ( symbolt symbol,
symbolt *&  new_symbol 
)
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 85 of file journalling_symbol_table.h.

◆ on_insert()

void journalling_symbol_tablet::on_insert ( const irep_idt id)
inlineprivate

Definition at line 152 of file journalling_symbol_table.h.

◆ on_remove()

void journalling_symbol_tablet::on_remove ( const irep_idt id)
inlineprivate

Definition at line 164 of file journalling_symbol_table.h.

◆ on_update()

void journalling_symbol_tablet::on_update ( const irep_idt id)
inlineprivate

Definition at line 159 of file journalling_symbol_table.h.

◆ wrap()

static journalling_symbol_tablet journalling_symbol_tablet::wrap ( symbol_table_baset base_symbol_table)
inlinestatic

Definition at line 80 of file journalling_symbol_table.h.

Member Data Documentation

◆ base_symbol_table

symbol_table_baset& journalling_symbol_tablet::base_symbol_table
private

Definition at line 41 of file journalling_symbol_table.h.

◆ inserted

changesett journalling_symbol_tablet::inserted
private

Definition at line 43 of file journalling_symbol_table.h.

◆ removed

changesett journalling_symbol_tablet::removed
private

Definition at line 48 of file journalling_symbol_table.h.

◆ updated

changesett journalling_symbol_tablet::updated
private

Definition at line 46 of file journalling_symbol_table.h.


The documentation for this class was generated from the following file: