#include <otawa/dfa/hai/WideningFixPoint.h>

Classes
class	FixPointState

Public Types
typedef Listener::Problem	Problem

typedef Problem::Domain	Domain

Public Member Functions
FixPointState *	newState (void)

	WideningFixPoint (Listener &_list)

	~WideningFixPoint ()

void	init (HalfAbsInt< WideningFixPoint > *_ai)
	Is called by HalfAbsInt for fixpoint object initializeation. More...

void	fixPoint (BasicBlock *bb, bool &fixpoint, Domain &in, bool firstTime) const
	Main fixPoint function: is called by HalfAbsInt whenever the analysis reaches a loop header. More...

void	markEdge (PropList *e, const Domain &s)
	Marks a proplist (typically an edge) e with state s. More...

void	unmarkEdge (PropList *e)
	Unmark a proplist (typically an edge) More...

Domain *	getMark (PropList *e)
	Get the mark of a proplist (typically an edge) More...

void	updateEdge (Edge *edge, Domain &dom)

const Domain &	bottom (void) const
	This function gets the bottom of the problem's lattice This is usually delegated to the Problem. More...

const Domain &	entry (void) const
	This function returns the entry state of the whole program to be analyzed. More...

void	lub (Domain &a, const Domain &b) const
	Performs operation: a = a lub b This is delegated to the Problem. More...

void	assign (Domain &a, const Domain &b) const
	Performs operation a = b This is delegated to the Problem. More...

bool	equals (const Domain &a, const Domain &b) const
	Tests a and b for equality. More...

void	update (Domain &out, const Domain &in, BasicBlock *bb)
	Is called whenever the analysis needs to get the Output state for a basic block, given its input state. More...

void	blockInterpreted (BasicBlock bb, const Domain &in, const Domain &out, CFG cur_cfg, elm::genstruct::Vector< Edge * > *callStack) const
	This listener is called whenever HalfAbsInt has processed a basic block. More...

void	fixPointReached (BasicBlock *bb) const
	This listener is called whenever a fixpoint is reached for a loop. More...

void	enterContext (Domain &dom, BasicBlock *bb, hai_context_t ctx) const
	This is called whenever we enter a loop. More...

void	leaveContext (Domain &dom, BasicBlock *bb, hai_context_t ctx) const
	This is called whenever we leave a loop. More...

Private Attributes
Problem &	prob

Listener &	list

HalfAbsInt< WideningFixPoint > *	ai

Static Private Attributes
static Identifier< Domain * >	STATE

Member Typedef Documentation

template<class Listener>

typedef Problem::Domain otawa::dfa::hai::WideningFixPoint< Listener >::Domain

template<class Listener>

typedef Listener::Problem otawa::dfa::hai::WideningFixPoint< Listener >::Problem

Constructor & Destructor Documentation

template<class Listener>

otawa::dfa::hai::WideningFixPoint< Listener >::WideningFixPoint ( Listener & _list )

inline

template<class Listener>

otawa::dfa::hai::WideningFixPoint< Listener >::~WideningFixPoint ( )

inline

Member Function Documentation

template<class Listener>

void otawa::dfa::hai::WideningFixPoint< Listener >::assign	(	Domain &	a,
		const Domain &	b
	)		const

inline

Performs operation a = b This is delegated to the Problem.

Parameters

a	State a
b	State b

template<class Listener>

void otawa::dfa::hai::WideningFixPoint< Listener >::blockInterpreted	(	BasicBlock *	bb,
		const Domain &	in,
		const Domain &	out,
		CFG *	cur_cfg,
		elm::genstruct::Vector< Edge * > *	callStack
	)		const

inline

This listener is called whenever HalfAbsInt has processed a basic block.

The listener must gather and store the information for the user. This is delegated to the Listener.

Parameters

bb	The basic block
in	The input state
out	The output state
cur_cfg	Current CFG.

template<class Listener >

const Domain & otawa::dfa::hai::WideningFixPoint< Listener >::bottom ( void ) const

inline

This function gets the bottom of the problem's lattice This is usually delegated to the Problem.

Returns: Bottom

Referenced by otawa::dfa::hai::WideningFixPoint< Listener >::newState().

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::enterContext	(	Domain &	dom,
		BasicBlock *	bb,
		hai_context_t	ctx
	)		const

inline

This is called whenever we enter a loop.

Parameters

dom	State (optionnally to be modified according to the new context)
bb	Loop header

template<class Listener >

const Domain & otawa::dfa::hai::WideningFixPoint< Listener >::entry ( void ) const

inline

This function returns the entry state of the whole program to be analyzed.

This is usually delegated to the Problem.

Returns: Entry state

template<class Listener>

bool otawa::dfa::hai::WideningFixPoint< Listener >::equals	(	const Domain &	a,
		const Domain &	b
	)		const

inline

Tests a and b for equality.

This is delegated to the Problem.

Parameters

a	State a
b	State b

Returns: True if equal

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::fixPoint	(	BasicBlock *	bb,
		bool &	fixpoint,
		Domain &	in,
		bool	firstTime
	)		const

Main fixPoint function: is called by HalfAbsInt whenever the analysis reaches a loop header.

Its purpose is to detect if the fixpoint's reached, and compute the new loop entry state. It may store state information into the HalfAbsInt's FixPointState object.

Parameters

bb	loop header basic block
fixpoint	fixPoint() must store True here when the fixpoint is reached.
in	fixPoint() must store here the new loop entry state.
fistTime	is True if it's the first time we call fixPoint for this loop.

References HAIW_TRACE, and otawa::dfa::hai::WideningFixPoint< Listener >::FixPointState::headerState.

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::fixPointReached ( BasicBlock * bb ) const

inline

This listener is called whenever a fixpoint is reached for a loop.

This is delegated to the Listener.

Parameters

bb	The loop header.

template<class Listener >

Domain * otawa::dfa::hai::WideningFixPoint< Listener >::getMark ( PropList * e )

inline

Get the mark of a proplist (typically an edge)

Parameters

e	The proplist to getmark

References otawa::stack::STATE.

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::init ( util::HalfAbsInt< WideningFixPoint< Listener > > * _ai )

inline

Is called by HalfAbsInt for fixpoint object initializeation.

Parameters

_ai	HalfAbsint object.

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::leaveContext	(	Domain &	dom,
		BasicBlock *	bb,
		hai_context_t	ctx
	)		const

inline

This is called whenever we leave a loop.

Parameters

dom	State (optionally to be modified according to the new context)
bb	Loop header

template<class Listener>

void otawa::dfa::hai::WideningFixPoint< Listener >::lub	(	Domain &	a,
		const Domain &	b
	)		const

inline

Performs operation: a = a lub b This is delegated to the Problem.

with lub = Lowest Upper Bound.

Parameters

a	State a
b	State b

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::markEdge	(	PropList *	e,
		const Domain &	s
	)

inline

Marks a proplist (typically an edge) e with state s.

Parameters

e	Proplist to mark
s	State

References otawa::stack::STATE.

template<class Listener>

FixPointState* otawa::dfa::hai::WideningFixPoint< Listener >::newState ( void )

inline

References otawa::dfa::hai::WideningFixPoint< Listener >::bottom().

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::unmarkEdge ( PropList * e )

inline

Unmark a proplist (typically an edge)

Parameters

e	Proplist to unmark

References otawa::stack::STATE.

template<class Listener>

void otawa::dfa::hai::WideningFixPoint< Listener >::update	(	Domain &	out,
		const Domain &	in,
		BasicBlock *	bb
	)

inline

Is called whenever the analysis needs to get the Output state for a basic block, given its input state.

This is delegated to the Problem.

Parameters

out	Output state
in	Input state
bb	Basic Block

template<class Listener >

void otawa::dfa::hai::WideningFixPoint< Listener >::updateEdge	(	Edge *	edge,
		Domain &	dom
	)

inline

Member Data Documentation

template<class Listener>

HalfAbsInt<WideningFixPoint>* otawa::dfa::hai::WideningFixPoint< Listener >::ai

private

template<class Listener>

Listener& otawa::dfa::hai::WideningFixPoint< Listener >::list

private

template<class Listener>

Problem& otawa::dfa::hai::WideningFixPoint< Listener >::prob

private

template<class Listener>

Identifier< typename Listener::Problem::Domain * > otawa::dfa::hai::WideningFixPoint< Listener >::STATE

staticprivate

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

include/otawa/dfa/hai/WideningFixPoint.h
src/prog/dfa_hai_WideningFixPoint.cpp

Classes

Public Types

Public Member Functions

Private Attributes

Static Private Attributes

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation