A symbol table wrapper that records which entries have been updated/removed. 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_idt >	changesett

Public Types inherited from symbol_table_baset
typedef std::unordered_map< irep_idt, symbolt >	symbolst

using	const_iteratort = symbolst::const_iterator

Public Member Functions
	journalling_symbol_tablet (const journalling_symbol_tablet &other)=delete

	journalling_symbol_tablet (journalling_symbol_tablet &&other)

virtual const symbol_tablet &	get_symbol_table () const override

virtual bool	move (symbolt &symbol, symbolt *&new_symbol) override

virtual symbolt *	get_writeable (const irep_idt &identifier) override
	Find a symbol in the symbol table for read-write access. More...

std::size_t	next_unused_suffix (const std::string &prefix) const override

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 changesett &	get_inserted () const

const changesett &	get_updated () const

const changesett &	get_removed () const

virtual iteratort	begin ()=0

virtual const_iteratort	begin () const

virtual iteratort	end ()=0

virtual const_iteratort	end () 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_baset &	operator= (const symbol_table_baset &other)=delete

virtual	~symbol_table_baset ()
	Author: Diffblue Ltd. More...

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`. 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 symbolt *	lookup (const irep_idt &name) const
	Find a symbol in the symbol table for read-only access. More...

const symbolt &	lookup_ref (const irep_idt &name) const
	Find a symbol in the symbol table for read-only access. More...

symbolt &	get_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...

std::vector< irep_idt >	sorted_symbol_names () const
	Build and return a lexicographically sorted vector of symbol names from all symbols stored in this symbol table. More...

virtual const_iteratort	begin () const

virtual const_iteratort	end () const

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_baset &	base_symbol_table

changesett	inserted

changesett	updated

changesett	removed

Additional Inherited Members
Public Attributes inherited from symbol_table_baset
const symbolst &	symbols
	Read-only field, used to look up symbols given their names. More...

const symbol_base_mapt &	symbol_base_map
	Read-only field, used to look up symbol names given their base names. More...

const symbol_module_mapt &	symbol_module_map
	Read-only field, used to look up symbol names given their modules. More...

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() [1/3]

virtual const_iteratort symbol_table_baset::begin

◆ begin() [2/3]

virtual iteratort journalling_symbol_tablet::begin ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 132 of file journalling_symbol_table.h.

◆ begin() [3/3]

symbol_table_baset::const_iteratort symbol_table_baset::begin

Definition at line 68 of file symbol_table_base.cpp.

◆ clear()

virtual void journalling_symbol_tablet::clear ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 125 of file journalling_symbol_table.h.

◆ end() [1/3]

virtual const_iteratort symbol_table_baset::end

◆ end() [2/3]

virtual iteratort journalling_symbol_tablet::end ( )

inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 137 of file journalling_symbol_table.h.

◆ end() [3/3]

symbol_table_baset::const_iteratort symbol_table_baset::end

Definition at line 63 of file symbol_table_base.cpp.

◆ erase()

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

inlineoverridevirtual

Remove a symbol from the symbol table.

Parameters

entry an iterator pointing at the symbol to remove

Implements symbol_table_baset.

Definition at line 118 of file journalling_symbol_table.h.

◆ get_inserted()

const changesett& journalling_symbol_tablet::get_inserted ( ) const

inline

Definition at line 146 of file journalling_symbol_table.h.

◆ get_removed()

const changesett& journalling_symbol_tablet::get_removed ( ) const

inline

Definition at line 154 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 150 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

name	The 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

symbol The 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 108 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.

◆ next_unused_suffix()

std::size_t journalling_symbol_tablet::next_unused_suffix ( const std::string & prefix ) const

inlineoverridevirtual

Reimplemented from symbol_table_baset.

Definition at line 103 of file journalling_symbol_table.h.

◆ on_insert()

void journalling_symbol_tablet::on_insert ( const irep_idt & id )

inlineprivate

Definition at line 160 of file journalling_symbol_table.h.

◆ on_remove()

void journalling_symbol_tablet::on_remove ( const irep_idt & id )

inlineprivate

Definition at line 172 of file journalling_symbol_table.h.

◆ on_update()

void journalling_symbol_tablet::on_update ( const irep_idt & id )

inlineprivate

Definition at line 167 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:

/home/runner/work/cbmc-documentation/cbmc-documentation/src/util/journalling_symbol_table.h

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ changesett

Constructor & Destructor Documentation

◆ journalling_symbol_tablet() [1/3]

◆ journalling_symbol_tablet() [2/3]

◆ journalling_symbol_tablet() [3/3]

Member Function Documentation

◆ begin() [1/3]

◆ begin() [2/3]

◆ begin() [3/3]

◆ clear()

◆ end() [1/3]

◆ end() [2/3]

◆ end() [3/3]

◆ erase()

◆ get_inserted()

◆ get_removed()

◆ get_symbol_table()

◆ get_updated()

◆ get_writeable()

◆ insert()

◆ move()

◆ next_unused_suffix()

◆ on_insert()

◆ on_remove()

◆ on_update()

◆ wrap()

Member Data Documentation

◆ base_symbol_table

◆ inserted

◆ removed

◆ updated