The abstract state of the computer (abstract domain). More...

#include <otawa/data/clp/ClpState.h>

Classes
class	Iter

class	Node
	A node in the memory list. More...

Public Member Functions
	State (const Value &def=Value::all)
	Constructors of a new State. More...

	State (const State &state)
	Copy constructor. More...

	~State (void)
	Destructor. More...

State &	operator= (const State &state)

bool	operator== (const State &state) const

void	copy (const State &state)
	Change the state to be a copy of the given one. More...

void	clear (void)
	Remove all nodes from the state. More...

void	set (const Value &addr, const Value &val)
	Define a value into a register or the memory. More...

void	clear (t::uint32 base, t::uint32 size)
	Set to T the memories on the given area. More...

bool	equals (const State &state) const

void	join (const State &state)
	Merge a state with the current one. More...

void	widening (const State &state, int loopBound)
	Perform a widening. More...

void	print (io::Output &out, const hard::Platform *pf=0) const
	Print the state. More...

const Value &	get (const Value &addr) const
	Return a stored value. More...

Static Public Attributes
static const State	EMPTY

static const State	FULL

Protected Attributes
Node	first

genstruct::Vector< Value >	registers

genstruct::Vector< Value >	tmpreg

Detailed Description

The abstract state of the computer (abstract domain).

state for the CLP Analysis analysis.

The abstract state is a list of register states and memory states.

Constructor & Destructor Documentation

otawa::clp::State::State ( const Value & def = Value::all )

inline

Constructors of a new State.

otawa::clp::State::State ( const State & state )

inline

Copy constructor.

References copy().

otawa::clp::State::~State ( void )

inline

Destructor.

References clear().

Member Function Documentation

void otawa::clp::State::clear ( void )

Remove all nodes from the state.

References otawa::clp::State::Node::next.

Referenced by ~State().

void otawa::clp::State::clear	(	t::uint32	base,
		t::uint32	size
	)

Set to T the memories on the given area.

Parameters

base	Base address of the area.
size	Size of the area.

References otawa::clp::State::Node::getNext().

void otawa::clp::State::copy ( const State & state )

Change the state to be a copy of the given one.

Parameters

state the state to be copied

References elm::cerr, clear(), elm::io::endl, first, otawa::clp::State::Node::next, otawa::p::print(), print(), registers, tmpreg, and TRACED.

Referenced by operator=(), and State().

bool otawa::clp::State::equals ( const State & state ) const

Returns: if a state is equals to the current one

References otawa::clp::State::Node::addr, first, otawa::clp::Value::kind(), otawa::clp::State::Node::next, registers, and otawa::clp::State::Node::val.

Referenced by operator==().

const Value & otawa::clp::State::get ( const Value & addr ) const

Return a stored value.

Parameters

addr	is the addresse to get the value of. The kind of the value can be REG for a register, or VAL for memory. The address is considered as constant, the lower() attribute is the value.

Returns: the stored value

References otawa::clp::State::Node::addr, otawa::clp::Value::isConst(), otawa::clp::Value::kind(), otawa::clp::Value::lower(), otawa::clp::State::Node::next, otawa::clp::REG, and otawa::clp::State::Node::val.

Referenced by otawa::se::getFilterForAddr(), otawa::se::getFilterForReg(), and otawa::dcache::CLPBlockBuilder::processBB().

void otawa::clp::State::join ( const State & state )

Merge a state with the current one.

References otawa::clp::ALL, elm::cerr, copy(), elm::io::endl, first, otawa::clp::Value::join(), otawa::clp::State::Node::next, otawa::p::print(), print(), registers, tmpreg, TRACED, TRACEJ, and otawa::clp::State::Node::val.

State& otawa::clp::State::operator= ( const State & state )

inline

References copy().

bool otawa::clp::State::operator== ( const State & state ) const

inline

References equals().

void otawa::clp::State::print	(	io::Output &	out,
		const hard::Platform *	pf = `0`
	)		const

Print the state.

References CLP_END, CLP_START, otawa::hard::Platform::findReg(), otawa::clp::Value::kind(), otawa::hard::Register::name(), otawa::clp::State::Node::next, and otawa::clp::VAL.

Referenced by copy(), join(), otawa::clp::operator<<(), and widening().

void otawa::clp::State::set	(	const Value &	addr,
		const Value &	val
	)

Define a value into a register or the memory.

Parameters

addr	a value of kind REG for a register, VAL for the memory. The value must be a constant (only the lower() attribute will be used) or all.
val	the value to store at the given address

References otawa::clp::ALL, elm::cerr, clear(), elm::io::endl, otawa::clp::Value::isConst(), otawa::clp::Value::kind(), otawa::clp::Value::lower(), otawa::clp::State::Node::next, otawa::p::print(), otawa::clp::REG, and TRACED.

void otawa::clp::State::widening	(	const State &	state,
		int	loopBound
	)

Perform a widening.

Parameters

state	the state of the next iteration
loopBound	is the number of iteration of the loop. A different widening operation will be used if the loopBound is known (>=0) or not.

References otawa::clp::ALL, elm::cerr, copy(), elm::io::endl, otawa::clp::Value::ffwidening(), first, otawa::clp::State::Node::next, otawa::p::print(), print(), registers, tmpreg, TRACED, and otawa::clp::State::Node::val.