Abstract domain to obtain all available expressions (AE). More...

#include <gcse.h>

Inheritance diagram for cse_domaint:

Public Member Functions
	cse_domaint ()=default
virtual void	transform (goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) override
	how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)
virtual void	output (std::ostream &out) const override
virtual void	make_bottom () override
	no states
virtual void	make_entry () override
	Entry has nothing available yet, but is reachable — distinct from bottom.
virtual void	make_top () override
	all states – the analysis doesn't use this, and domains may refuse to implement it.
virtual bool	is_bottom () const override
virtual bool	is_top () const override
virtual bool	ai_simplify (expr2tc &, const namespacet &) const override
	also add
bool	merge (const cse_domaint &b, goto_programt::const_targett, goto_programt::const_targett)
Public Member Functions inherited from ai_domain_baset
virtual	~ai_domain_baset ()
virtual bool	ai_simplify_lhs (expr2tc &condition, const namespacet &ns) const
	Simplifies the expression but keeps it as an l-value.
virtual expr2tc	to_predicate (void) const
	Gives a Boolean condition that is true for all values represented by the domain.

Public Attributes
std::unordered_set< expr2tc, irep2_hash >	available_expressions
	All expressions available.
bool	bottom = true
	Unreachable-so-far marker.

Static Public Attributes
static std::shared_ptr< value_setst >	vsa = nullptr

Protected Member Functions
void	make_expression_available (const expr2tc &e)
	Add non-primitive expression e (and its sub-expressions) into available_expressions.
void	havoc_expr (const expr2tc &e, const goto_programt::const_targett &)
	Remove expression e (and everything that it depends on) from available_expressions.
void	havoc_symbol (const irep_idt &sym)
	Remove every expression from available_expressions that depends on symbol sym.
void	havoc_pointee (expr2tc ptr, const goto_programt::const_targett &)
	Remove every expression that may read the object ptr points to, which is about to be deallocated.
bool	should_remove_expr (const expr2tc &taint, const expr2tc &src) const
bool	should_remove_expr (const irep_idt &sym, const expr2tc &src) const
Protected Member Functions inherited from ai_domain_baset
	ai_domain_baset ()
	The constructor is expected to produce 'false' or 'bottom'.

Detailed Description

Abstract domain to obtain all available expressions (AE).

The domain is the set of expressions that were already computed up to this point.

... // AE: [] int x = a + b + c // AE: [a + b, a + b + c] int y = a + b + d // AE: [a + b, a + b + c, a + b + d] c = 42 // AE: [a + b, a + b + d]

There are some level of precision to be considered. We shouldn't track constants or symbols as there is no point in saying that something like '42' is available. However, '42 + a' will be cached. This opens a path for canonization algorithms as '42 + a' = 'a + 42'

TODO: add a canonization method for expr2tc.

In Summary, the abstract domain is implemented as:

TOP --> all expressions possible for the program (not needed)
BOTTOM --> no expressions are available
Meet operator: prev meet new: If we are dealing with a basic edge (no split/join in the CFG) then just replace the abstract state with "new". Otherwise, compute the intersection between "prev" and "new".
Transform operator:
- RETURN: the returned expression (and sub-expressions) is now available
- ASSIGN: RHS (and sub-expressions) is now available, LHS (and dependencies) is not available anymore
- GOTO/ASSERT/ASSUME: guard (and sub-expressions) is now available
- DECL/DEAD: variable is no longer available
- FUNCTION_CALL: same as assign

Constructor & Destructor Documentation

◆ cse_domaint()

cse_domaint::cse_domaint ( )

default

Member Function Documentation

◆ ai_simplify()

virtual bool cse_domaint::ai_simplify	(	expr2tc &	condition,
		const namespacet &	ns ) const

inlineoverridevirtual

also add

bool merge(const T &b, const_targett from, const_targett to);

This computes the join between "this" and "b". Return true if "this" has changed. In the usual case, "b" is the updated state after "from" and "this" is the state before "to".

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") This method allows an expression to be simplified / evaluated using the current state. It is used to evaluate assertions and in program simplification return true if unchanged

Implements ai_domain_baset.

◆ havoc_expr()

void cse_domaint::havoc_expr	(	const expr2tc &	e,
		const goto_programt::const_targett &	i_it )

protected

Remove expression e (and everything that it depends on) from available_expressions.

◆ havoc_pointee()

void cse_domaint::havoc_pointee	(	expr2tc	ptr,
		const goto_programt::const_targett &	i_it )

protected

Remove every expression that may read the object ptr points to, which is about to be deallocated.

◆ havoc_symbol()

void cse_domaint::havoc_symbol ( const irep_idt & sym )

protected

Remove every expression from available_expressions that depends on symbol sym.

◆ is_bottom()

virtual bool cse_domaint::is_bottom ( ) const

inlineoverridevirtual

Implements ai_domain_baset.

◆ is_top()

virtual bool cse_domaint::is_top ( ) const

inlineoverridevirtual

Implements ai_domain_baset.

◆ make_bottom()

virtual void cse_domaint::make_bottom ( )

inlineoverridevirtual

no states

Implements ai_domain_baset.

◆ make_entry()

virtual void cse_domaint::make_entry ( )

inlineoverridevirtual

Entry has nothing available yet, but is reachable — distinct from bottom.

Conflating the two would let a merge adopt the other side's expressions wholesale, and would make ai_baset treat a function whose exit has no available expression as an unreachable exit point.

Implements ai_domain_baset.

◆ make_expression_available()

void cse_domaint::make_expression_available ( const expr2tc & e )

protected

Add non-primitive expression e (and its sub-expressions) into available_expressions.

◆ make_top()

virtual void cse_domaint::make_top ( )

inlineoverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

◆ merge()

bool cse_domaint::merge	(	const cse_domaint &	b,
		goto_programt::const_targett	from,
		goto_programt::const_targett	to )

◆ output()

void cse_domaint::output ( std::ostream & out ) const

overridevirtual

Implements ai_domain_baset.

◆ should_remove_expr() [1/2]

bool cse_domaint::should_remove_expr	(	const expr2tc &	taint,
		const expr2tc &	src ) const

protected

◆ should_remove_expr() [2/2]

bool cse_domaint::should_remove_expr	(	const irep_idt &	sym,
		const expr2tc &	src ) const

protected

◆ transform()

void cse_domaint::transform	(	goto_programt::const_targett	from,
		goto_programt::const_targett	to,
		ai_baset &	ai,
		const namespacet &	ns )

overridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

"this" is the domain before the instruction "from" "from" is the instruction to be interpreted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

Implements ai_domain_baset.

Member Data Documentation

◆ available_expressions

std::unordered_set<expr2tc, irep2_hash> cse_domaint::available_expressions

All expressions available.

◆ bottom

bool cse_domaint::bottom = true

Unreachable-so-far marker.

A default-constructed domain must be bottom: ai_baset asserts as much for states it has not visited.

◆ vsa

std::shared_ptr< value_setst > cse_domaint::vsa = nullptr

static

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

Public Member Functions

Public Attributes

Static Public Attributes

Protected Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ cse_domaint()

Member Function Documentation

◆ ai_simplify()

◆ havoc_expr()

◆ havoc_pointee()

◆ havoc_symbol()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_expression_available()

◆ make_top()

◆ merge()

◆ output()

◆ should_remove_expr() [1/2]

◆ should_remove_expr() [2/2]

◆ transform()

Member Data Documentation

◆ available_expressions

◆ bottom

◆ vsa