goto_cse Class Reference

Global Common Subexpression Elimination algorithm. More...

#include <gcse.h>

Inheritance diagram for goto_cse:

Public Member Functions
	goto_cse (contextt &ns, std::shared_ptr< value_setst > &vsa)
virtual bool	runOnProgram (goto_functionst &) override
virtual bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F) override
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Member Functions
expr2tc	obtain_max_sub_expr (const expr2tc &e, const cse_domaint &state) const
void	replace_max_sub_expr (expr2tc &e, const std::unordered_map< expr2tc, expr2tc, irep2_hash > &expr2symbol, const goto_programt::const_targett &to, std::unordered_set< expr2tc, irep2_hash > &matched_expressions) const
void	replace_in_lvalue (expr2tc &lhs, const std::unordered_map< expr2tc, expr2tc, irep2_hash > &expr2symbol, const goto_programt::const_targett &to, std::unordered_set< expr2tc, irep2_hash > &matched_expressions) const
	Like replace_max_sub_expr, but only in the value operands of an lvalue.
symbolt	create_cse_symbol (const type2tc &t, const goto_programt::const_targett &to)
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnLoop (loopst &loop, goto_programt &goto_program)

Protected Attributes
ait< cse_domaint >	available_expressions
contextt &	context
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Detailed Description

Global Common Subexpression Elimination algorithm.

Compute all common subexpression in a goto program. For each common subexpression, a new intermediate variable __ESBMC_cse_symbol$ is created and assigned to the common value.

In ESBMC, the main advantage is for sequential dereferences/with statements. They generate lots of boilerplate to be dereferenced during symex.

Before: X = a + b + c; Y = a + b + d;

After: __ESBMC_cse_symbol$0 = a + b; X = __ESBMC_cse_symbol$0 + c; Y = __ESBMC_cse_symbol$0 + d;

Constructor & Destructor Documentation

goto_cse()

goto_cse::goto_cse ( contextt & ns, std::shared_ptr< value_setst > & vsa )

inline

Member Function Documentation

create_cse_symbol()

symbolt goto_cse::create_cse_symbol ( const type2tc & t, const goto_programt::const_targett & to )

inlineprotected

obtain_max_sub_expr()

expr2tc goto_cse::obtain_max_sub_expr ( const expr2tc & e, const cse_domaint & state ) const

protected

replace_in_lvalue()

void goto_cse::replace_in_lvalue ( expr2tc & lhs, const std::unordered_map< expr2tc, expr2tc, irep2_hash > & expr2symbol, const goto_programt::const_targett & to, std::unordered_set< expr2tc, irep2_hash > & matched_expressions ) const

protected

Like replace_max_sub_expr, but only in the value operands of an lvalue.

replace_max_sub_expr()

void goto_cse::replace_max_sub_expr ( expr2tc & e, const std::unordered_map< expr2tc, expr2tc, irep2_hash > & expr2symbol, const goto_programt::const_targett & to, std::unordered_set< expr2tc, irep2_hash > & matched_expressions ) const

protected

runOnFunction()

bool goto_cse::runOnFunction ( std::pair< const irep_idt, goto_functiont > & F )

overridevirtual

Reimplemented from goto_functions_algorithm.

runOnProgram()

bool goto_cse::runOnProgram ( goto_functionst & F )

overridevirtual

Reimplemented from goto_functions_algorithm.

Member Data Documentation

available_expressions

ait<cse_domaint> goto_cse::available_expressions

protected

context

contextt& goto_cse::context

protected

---

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

• src/goto-programs/abstract-interpretation/gcse.h
• src/goto-programs/abstract-interpretation/gcse.cpp