#include <renaming.h>

Inheritance diagram for renaming::level2t:

Classes
class	name_record
struct	name_rec_hash
struct	valuet

Public Types
typedef persistent_map< name_record, valuet, name_rec_hash >	current_namest

Public Member Functions
virtual void	make_assignment (expr2tc &lhs_symbol, const expr2tc &constant_value, const expr2tc &assigned_value)
void	rename (expr2tc &expr) override
virtual void	rename (expr2tc &expr, unsigned count)=0
void	get_ident_name (expr2tc &symbol) const override
void	remove (const expr2tc &symbol) override
valuet	current_value (const name_record &rec) const
	Get-or-default then re-store: the persistent map hands out immutable values, so a "modify the entry in place" site reads a copy, mutates it, and sets it back.
void	retire (const name_record &rec)
	Retire a name whose storage has gone out of scope.
void	declare (const name_record &rec)
	Record rec at its initial version.
void	get_original_name (expr2tc &expr) const override
void	set_constant (const name_record &rec, const expr2tc &value)
	Complete an assignment make_assignment has just made, whose value only its caller can build: #7597 re-offers a refused member write as a read of the L2 name make_assignment mints.
unsigned	current_number (const expr2tc &sym) const
unsigned	current_number (const name_record &rec) const
	level2t ()=default
	~level2t () override=default
virtual std::shared_ptr< level2t >	clone () const =0
virtual void	print (std::ostream &out) const
virtual void	dump () const
Public Member Functions inherited from renaming::renaming_levelt
virtual	~renaming_levelt ()=default

Static Public Member Functions
static void	rename_to_record (expr2tc &sym, const name_record &rec)
Static Public Member Functions inherited from renaming::renaming_levelt
static void	get_original_name (expr2tc &expr, symbol2t::renaming_level lev)

Public Attributes
current_namest	current_names

Protected Member Functions
virtual void	coveredinbees (expr2tc &lhs_sym, unsigned count, unsigned node_id)

Friends
void	build_goto_symex_classes ()

Member Typedef Documentation

◆ current_namest

typedef persistent_map<name_record, valuet, name_rec_hash> renaming::level2t::current_namest

Constructor & Destructor Documentation

◆ level2t()

renaming::level2t::level2t ( )

default

◆ ~level2t()

renaming::level2t::~level2t ( )

overridedefault

Member Function Documentation

◆ clone()

virtual std::shared_ptr< level2t > renaming::level2t::clone ( ) const

pure virtual

Implemented in execution_statet::ex_state_level2t, and execution_statet::state_hashing_level2t.

◆ coveredinbees()

void renaming::level2t::coveredinbees	(	expr2tc &	lhs_sym,
		unsigned	count,
		unsigned	node_id )

protectedvirtual

◆ current_number() [1/2]

unsigned renaming::level2t::current_number ( const expr2tc & sym ) const

◆ current_number() [2/2]

unsigned renaming::level2t::current_number ( const name_record & rec ) const

◆ current_value()

valuet renaming::level2t::current_value ( const name_record & rec ) const

inline

Get-or-default then re-store: the persistent map hands out immutable values, so a "modify the entry in place" site reads a copy, mutates it, and sets it back.

◆ declare()

void renaming::level2t::declare ( const name_record & rec )

inline

Record rec at its initial version.

phi_function merges only names that already had a record when the branch was taken, so storage first written inside a branch would otherwise keep that branch's version on both paths (#6798). get_ident_name numbers a count-0 record exactly as it numbers an absent one, so declaring costs no SSA renumbering.

◆ dump()

void renaming::level2t::dump ( ) const

virtual

◆ get_ident_name()

void renaming::level2t::get_ident_name ( expr2tc & symbol ) const

overridevirtual

Implements renaming::renaming_levelt.

◆ get_original_name()

void renaming::level2t::get_original_name ( expr2tc & expr ) const

inlineoverridevirtual

Implements renaming::renaming_levelt.

◆ make_assignment()

void renaming::level2t::make_assignment	(	expr2tc &	lhs_symbol,
		const expr2tc &	constant_value,
		const expr2tc &	assigned_value )

virtual

Reimplemented in execution_statet::state_hashing_level2t.

◆ print()

void renaming::level2t::print ( std::ostream & out ) const

virtual

◆ remove()

void renaming::level2t::remove ( const expr2tc & symbol )

inlineoverridevirtual

Implements renaming::renaming_levelt.

◆ rename() [1/2]

void renaming::level2t::rename ( expr2tc & expr )

overridevirtual

Implements renaming::renaming_levelt.

◆ rename() [2/2]

virtual void renaming::level2t::rename	(	expr2tc &	expr,
		unsigned	count )

pure virtual

Implemented in execution_statet::ex_state_level2t.

◆ rename_to_record()

void renaming::level2t::rename_to_record	(	expr2tc &	sym,
		const name_record &	rec )

static

◆ retire()

void renaming::level2t::retire ( const name_record & rec )

inline

Retire a name whose storage has gone out of scope.

L1 names are never reused across frames (symex_decl's counter is monotone), so a popped frame's local can still be named – through a dangling pointer – after teardown. Erasing the record restarts the counter, letting such a write re-issue an index the declaration already defined and so define one SSA name twice (I10). Advancing past the last live index instead leaves the current name undefined, which keeps a read of the expired storage unconstrained exactly as erasure did.

◆ set_constant()

void renaming::level2t::set_constant	(	const name_record &	rec,
		const expr2tc &	value )

inline

Complete an assignment make_assignment has just made, whose value only its caller can build: #7597 re-offers a refused member write as a read of the L2 name make_assignment mints.

Narrow on purpose – an entry that is absent or already carries a value means the caller keyed the wrong record, which would otherwise be a silent no-op.

◆ build_goto_symex_classes

void build_goto_symex_classes ( )

friend

Member Data Documentation

◆ current_names

current_namest renaming::level2t::current_names

The documentation for this struct was generated from the following files:

src/goto-symex/state/renaming.h
src/goto-symex/state/renaming.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Friends

Member Typedef Documentation

◆ current_namest

Constructor & Destructor Documentation

◆ level2t()

◆ ~level2t()

Member Function Documentation

◆ clone()

◆ coveredinbees()

◆ current_number() [1/2]

◆ current_number() [2/2]

◆ current_value()

◆ declare()

◆ dump()

◆ get_ident_name()

◆ get_original_name()

◆ make_assignment()

◆ print()

◆ remove()

◆ rename() [1/2]

◆ rename() [2/2]

◆ rename_to_record()

◆ retire()

◆ set_constant()

Friends And Related Symbol Documentation

◆ build_goto_symex_classes

Member Data Documentation

◆ current_names