Fast implementation of abstract domain on the functional state of a microprocessor including the registers and the memory content. More...

#include <otawa/dfa/FastState.h>

Classes
struct	node_t

struct	state_t

Public Types
typedef t::uint32	address_t

typedef t::uint32	register_t

typedef D::t	value_t

typedef state_t *	t

Public Member Functions
	FastState (D d, dfa::State state, StackAllocator &alloc)
	Build a state. More...

int	getMultiMax (void) const
	Get the max number of multiple load/store before jumping to top. More...

void	setMultiMax (int new_multi_max)
	Set the maximum number of multiple load/store before approximating to top. More...

value_t	get (t s, register_t r)
	Get register value. More...

t	set (t s, register_t r, value_t v)
	Set a register value. More...

t	store (t s, address_t a, value_t v)
	Perform a store to memory. More...

value_t	load (t s, address_t a)
	Perform a load at the given address. More...

t	store (t s, address_t a, address_t b, ot::size off, value_t v)
	Perform a multiple-store (joining on all memories that are modified). More...

t	storeAtTop (t s)
	Store to T address (set all memory to T). More...

value_t	load (t s, address_t a, address_t b, ot::size off)
	Load multiple values from a memory area. More...

t	join (t s1, t s2)
	Perform join of both states. More...

template<class W >
t	map (t s, W &w)
	Apply a function to transform a state. More...

bool	equals (t s1, t s2)
	Test if both states are equal. More...

void	print (io::Output &out, t s)
	Display the state. More...

template<class W >
t	combine (t s1, t s2, W &w)
	Apply a function to combine two states. More...

Public Attributes
t	top

t	bot

Private Types
typedef struct otawa::dfa::FastState::node_t	node_t

typedef struct otawa::dfa::FastState::state_t	stat_t

Private Member Functions
t	make (bool bot)
	Make a basic state. More...

Private Attributes
D *	dom

elm::t::size	nrblock

StackAllocator &	allocator

int	multi_max

dfa::State *	istate

Static Private Attributes
static const elm::t::size	rblock_shift = 3

static const elm::t::size	rblock_mask = (1 << rblock_shift) - 1

static const elm::t::size	rblock_size = 1 << rblock_shift

Detailed Description

template<class D>
class otawa::dfa::FastState< D >

Fast implementation of abstract domain on the functional state of a microprocessor including the registers and the memory content.

Parameters

D	Domain of values.

Member Typedef Documentation

template<class D >

typedef t::uint32 otawa::dfa::FastState< D >::address_t

template<class D >

typedef struct otawa::dfa::FastState::node_t otawa::dfa::FastState< D >::node_t

private

template<class D >

typedef t::uint32 otawa::dfa::FastState< D >::register_t

template<class D >

typedef struct otawa::dfa::FastState::state_t otawa::dfa::FastState< D >::stat_t

private

template<class D >

typedef state_t* otawa::dfa::FastState< D >::t

template<class D >

typedef D::t otawa::dfa::FastState< D >::value_t

Constructor & Destructor Documentation

template<class D >

otawa::dfa::FastState< D >::FastState	(	D *	d,
		dfa::State *	state,
		StackAllocator &	alloc
	)

inline

Build a state.

Parameters

d	Domain manager.
proc	Analyzed process.
alloc	Stack allocator to use.

Member Function Documentation

template<class D >

template<class W >

FastState::t otawa::dfa::FastState< D >::combine	(	t	s1,
		t	s2,
		W &	w
	)

inline

Apply a function to combine two states.

This function assumes that the applied operation is idempotent and monotonic and use it to speed up the combination.

The worker object must match the following concept:

class Worker {
public:
                value_t process(value_t v1, value_t v2);
};

Parameters

s1	First state.
s2	Second state.
w	Worker object.

Returns: Output state.

References otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

FastState::bool otawa::dfa::FastState< D >::equals	(	t	s1,
		t	s2
	)

inline

Test if both states are equal.

Parameters

s1	First state.
s2	Second state.

Returns: True if they equal, false else.

References otawa::dfa::FastState< D >::node_t::a, otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, otawa::dfa::FastState< D >::state_t::regs, and otawa::dfa::FastState< D >::node_t::v.

template<class D >

FastState::value_t otawa::dfa::FastState< D >::get	(	t	s,
		register_t	r
	)

inline

Get register value.

Parameters

s	State to look at.
r	Register to get.

Returns: Register value.

template<class D >

int otawa::dfa::FastState< D >::getMultiMax ( void ) const

inline

Get the max number of multiple load/store before jumping to top.

Returns: Maximum number of effective load/store.

template<class D >

FastState::t otawa::dfa::FastState< D >::join	(	t	s1,
		t	s2
	)

inline

Perform join of both states.

References otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

value_t otawa::dfa::FastState< D >::load	(	t	s,
		address_t	a
	)

inline

Perform a load at the given address.

Parameters

s	Current state.
a	Address to load from.

Returns: Load value.

References otawa::dfa::FastState< D >::state_t::mem, and otawa::dfa::FastState< D >::node_t::n.

template<class D >

FastState::value_t otawa::dfa::FastState< D >::load	(	t	s,
		address_t	a,
		address_t	b,
		ot::size	off
	)

inline

Load multiple values from a memory area.

Parameters

s	State to load from.
a	First address of the area.
b	Last address past the area.
off	Offset of objects between the area.

Returns: Union of found objects.

References otawa::dfa::FastState< D >::node_t::a, and otawa::dfa::FastState< D >::state_t::mem.

template<class D >

t otawa::dfa::FastState< D >::make ( bool bot )

inlineprivate

Make a basic state.

Parameters

bot	True if it is a bottom state, false else.

Returns: Created state (must not be released by the user).

template<class D >

template<class W >

FastState::t otawa::dfa::FastState< D >::map	(	t	s,
		W &	w
	)

inline

Apply a function to transform a state.

The worker object must match the following concept:

class Worker {
public:
                value_t process(value_t v);
};

Parameters

in	Input state.
w	Worker object.

Returns: Output state.

The worker object must match the following concept:

class Worker {
public:
                value_t process(value_t v);
};

Parameters

W	Type of the worker.
in	Input state.
w	Worker object.

Returns: Output state.

References otawa::dfa::FastState< D >::node_t::a, copy(), otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, otawa::dfa::FastState< D >::state_t::regs, and otawa::dfa::FastState< D >::node_t::v.

template<class D >

void otawa::dfa::FastState< D >::print	(	io::Output &	out,
		t	s
	)

inline

Display the state.

Parameters

out	Stream to display to.
s	State to display.

References otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

FastState::t otawa::dfa::FastState< D >::set	(	t	s,
		register_t	r,
		value_t	v
	)

inline

Set a register value.

Parameters

s	State to change.
r	Register to set.
v	Value to set.

Returns: State after change.

References elm::array::copy(), otawa::dfa::FastState< D >::state_t::mem, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

void otawa::dfa::FastState< D >::setMultiMax ( int new_multi_max )

inline

Set the maximum number of multiple load/store before approximating to top.

Parameters

new_multi_max New maximum number of multiple load/store.

template<class D >

FastState::t otawa::dfa::FastState< D >::store	(	t	s,
		address_t	a,
		value_t	v
	)

inline

Perform a store to memory.

Parameters

s	State to change.
a	Address to store to.
v	Value to store.

Returns: New state with store performed.

References otawa::dfa::FastState< D >::node_t::a, otawa::dfa::FastState< D >::state_t::mem, otawa::dfa::FastState< D >::node_t::n, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

FastState::t otawa::dfa::FastState< D >::store	(	t	s,
		address_t	a,
		address_t	b,
		ot::size	off,
		value_t	v
	)

inline

Perform a multiple-store (joining on all memories that are modified).

FastState::value_t FastState::load(t s, address_t a); Perform a load at the given address.

Parameters

s	State to store in.
a	Start address of the area.
b	Last address past the area.
off	Offset between stored objects.
v	Value to set.

Returns: New state.

Parameters

s	Current state.
a	Address to load from.

Returns: Load value.

Perform a multiple-store (joining on all memories that are modified).

Parameters

s	State to store in.
a	Start address of the area.
b	Last address past the area.
off	Offset between stored objects.
v	Value to set.

Returns: New state.

References otawa::dfa::FastState< D >::node_t::a, otawa::dfa::FastState< D >::state_t::mem, and otawa::dfa::FastState< D >::state_t::regs.

template<class D >

FastState::t otawa::dfa::FastState< D >::storeAtTop ( t s )

inline

Store to T address (set all memory to T).

Parameters

s	State to store to.

Returns: s with memory set to T.

References otawa::dfa::FastState< D >::state_t::regs.

Member Data Documentation

template<class D >

StackAllocator& otawa::dfa::FastState< D >::allocator

private

template<class D >

t otawa::dfa::FastState< D >::bot

template<class D >

D* otawa::dfa::FastState< D >::dom

private

template<class D >

dfa::State* otawa::dfa::FastState< D >::istate

private

template<class D >

int otawa::dfa::FastState< D >::multi_max

private

template<class D >

elm::t::size otawa::dfa::FastState< D >::nrblock

private

template<class D >

const elm::t::size otawa::dfa::FastState< D >::rblock_mask = (1 << rblock_shift) - 1

staticprivate

template<class D >

const elm::t::size otawa::dfa::FastState< D >::rblock_shift = 3

staticprivate

template<class D >

const elm::t::size otawa::dfa::FastState< D >::rblock_size = 1 << rblock_shift

staticprivate

template<class D >

t otawa::dfa::FastState< D >::top

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

include/otawa/dfa/FastState.h
src/prog/dfa_FastState.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Private Types

Private Member Functions

Private Attributes

Static Private Attributes

Detailed Description

template<class D> class otawa::dfa::FastState< D >

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation

template<class D>
class otawa::dfa::FastState< D >