CBMC
symbol_table_buildert Class Reference

Author: Diffblue Ltd. More...

#include <symbol_table_builder.h>

+ Inheritance diagram for symbol_table_buildert:
+ Collaboration diagram for symbol_table_buildert:

Public Member Functions

 symbol_table_buildert (symbol_table_baset &base_symbol_table)
 
 symbol_table_buildert (symbol_table_buildert &&other)
 
 symbol_table_buildert (const symbol_table_buildert &)=delete
 
symbol_table_buildertoperator= (const symbol_table_buildert &)=delete
 
symbol_table_buildertoperator= (symbol_table_buildert &&)=delete
 
const symbol_tabletget_symbol_table () const override
 
void erase (const symbolst::const_iterator &entry) override
 Remove a symbol from the symbol table. More...
 
void clear () override
 
bool move (symbolt &symbol, symbolt *&new_symbol) override
 
symboltget_writeable (const irep_idt &identifier) override
 Find a symbol in the symbol table for read-write access. More...
 
std::pair< symbolt &, bool > insert (symbolt symbol) override
 Move or copy a new symbol to the symbol table. More...
 
iteratort begin () override
 
iteratort end () override
 
void validate (const validation_modet vm=validation_modet::INVARIANT) const override
 
std::size_t next_unused_suffix (const std::string &prefix) const override
 Try to find the next free identity for the passed-in prefix in this symbol table. More...
 
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_basetoperator= (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 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...
 
std::list< symbolst::const_iterator > match_name_or_base_name (const irep_idt &id) const
 Collect all symbols the name of which matches id or the base name of which matches id. 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...
 
std::vector< irep_idtsorted_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 symbol_table_buildert wrap (symbol_table_baset &base_symbol_table)
 

Private Attributes

symbol_table_basetbase_symbol_table
 
std::map< std::string, std::size_t > next_free_suffix_for_prefix
 

Additional Inherited Members

- Public Types inherited from symbol_table_baset
typedef std::unordered_map< irep_idt, symboltsymbolst
 
using const_iteratort = symbolst::const_iterator
 
- Public Attributes inherited from symbol_table_baset
const symbolstsymbols
 Read-only field, used to look up symbols given their names. More...
 
const symbol_base_maptsymbol_base_map
 Read-only field, used to look up symbol names given their base names. More...
 
const symbol_module_maptsymbol_module_map
 Read-only field, used to look up symbol names given their modules. More...
 

Detailed Description

Author: Diffblue Ltd.

Wrapper around a symbol table that keeps track of suffixes for faster calculation of the smallest unused suffix.

Definition at line 13 of file symbol_table_builder.h.

Constructor & Destructor Documentation

◆ symbol_table_buildert() [1/3]

symbol_table_buildert::symbol_table_buildert ( symbol_table_baset base_symbol_table)
inlineexplicit

Definition at line 20 of file symbol_table_builder.h.

◆ symbol_table_buildert() [2/3]

symbol_table_buildert::symbol_table_buildert ( symbol_table_buildert &&  other)
inline

Definition at line 29 of file symbol_table_builder.h.

◆ symbol_table_buildert() [3/3]

symbol_table_buildert::symbol_table_buildert ( const symbol_table_buildert )
delete

Member Function Documentation

◆ begin() [1/3]

symbol_table_baset::const_iteratort symbol_table_baset::begin
virtual

Implements symbol_table_baset.

Definition at line 273 of file symbol_table_base.cpp.

◆ begin() [2/3]

iteratort symbol_table_buildert::begin ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 78 of file symbol_table_builder.h.

◆ begin() [3/3]

virtual iteratort symbol_table_baset::begin
virtual

Implements symbol_table_baset.

◆ clear()

void symbol_table_buildert::clear ( void  )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 57 of file symbol_table_builder.h.

◆ end() [1/3]

symbol_table_baset::const_iteratort symbol_table_baset::end
virtual

Implements symbol_table_baset.

Definition at line 274 of file symbol_table_base.cpp.

◆ end() [2/3]

iteratort symbol_table_buildert::end ( )
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 83 of file symbol_table_builder.h.

◆ end() [3/3]

virtual iteratort symbol_table_baset::end
virtual

Implements symbol_table_baset.

◆ erase()

void symbol_table_buildert::erase ( const 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 52 of file symbol_table_builder.h.

◆ get_symbol_table()

const symbol_tablet& symbol_table_buildert::get_symbol_table ( ) const
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 47 of file symbol_table_builder.h.

◆ get_writeable()

symbolt* symbol_table_buildert::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 68 of file symbol_table_builder.h.

◆ insert()

std::pair<symbolt &, bool> symbol_table_buildert::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 73 of file symbol_table_builder.h.

◆ move()

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

Implements symbol_table_baset.

Definition at line 63 of file symbol_table_builder.h.

◆ next_unused_suffix()

std::size_t symbol_table_buildert::next_unused_suffix ( const std::string &  prefix) const
inlineoverridevirtual

Try to find the next free identity for the passed-in prefix in this symbol table.

Remarks
This method needs to generate names deterministically in regards to operations that generate the same prefix (and any other operation shouldn't affect this).

Due to this requirement we don't do anything fancy in regards to attempting to find the absolute earliest free suffix if one has been deleted, only the next free increment from our last stored value.

Reimplemented from symbol_table_baset.

Definition at line 107 of file symbol_table_builder.h.

◆ operator=() [1/2]

symbol_table_buildert& symbol_table_buildert::operator= ( const symbol_table_buildert )
delete

◆ operator=() [2/2]

symbol_table_buildert& symbol_table_buildert::operator= ( symbol_table_buildert &&  )
delete

◆ validate()

void symbol_table_buildert::validate ( const validation_modet  vm = validation_modet::INVARIANT) const
inlineoverridevirtual

Implements symbol_table_baset.

Definition at line 91 of file symbol_table_builder.h.

◆ wrap()

static symbol_table_buildert symbol_table_buildert::wrap ( symbol_table_baset base_symbol_table)
inlinestatic

Definition at line 42 of file symbol_table_builder.h.

Member Data Documentation

◆ base_symbol_table

symbol_table_baset& symbol_table_buildert::base_symbol_table
private

Definition at line 16 of file symbol_table_builder.h.

◆ next_free_suffix_for_prefix

std::map<std::string, std::size_t> symbol_table_buildert::next_free_suffix_for_prefix
mutableprivate

Definition at line 17 of file symbol_table_builder.h.


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