#include <ppl.hh>

Inheritance diagram for Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >:

[legend]

Public Types
typedef Linear_Form< FP_Interval_Type >	FP_Linear_Form
	Alias for a linear form with template argument `FP_Interval_Type`.

typedef Box< FP_Interval_Type >	FP_Interval_Abstract_Store
	Alias for a map that associates a variable index to an interval. More...

typedef std::map< dimension_type, FP_Linear_Form >	FP_Linear_Form_Abstract_Store
	Alias for a map that associates a variable index to a linear form. More...

typedef FP_Interval_Type::boundary_type	boundary_type
	The floating point format used by the analyzer.

typedef FP_Interval_Type::info_type	info_type
	The interval policy used by `FP_Interval_Type`.

Public Member Functions
virtual	~Floating_Point_Expression ()
	Destructor.

virtual bool	linearize (const FP_Interval_Abstract_Store &int_store, const FP_Linear_Form_Abstract_Store &lf_store, FP_Linear_Form &result) const =0
	Linearizes a floating point expression. More...

Static Public Member Functions
static bool	overflows (const FP_Linear_Form &lf)
	Verifies if a given linear form overflows. More...

static void	relative_error (const FP_Linear_Form &lf, FP_Linear_Form &result)
	Computes the relative error of a given linear form. More...

static void	intervalize (const FP_Linear_Form &lf, const FP_Interval_Abstract_Store &store, FP_Interval_Type &result)
	Makes `result` become an interval that overapproximates all the possible values of `lf` in the interval abstract store `store`. More...

Static Public Attributes
static FP_Interval_Type	absolute_error = compute_absolute_error()
	Absolute error. More...

Detailed Description

template<typename FP_Interval_Type, typename FP_Format>
class Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >

\ A floating point expression on a given format.

This class represents a concrete floating point expression. This includes constants, floating point variables, binary and unary arithmetic operators.

Template type parameters

The class template type parameter FP_Interval_Type represents the type of the intervals used in the abstract domain. The interval bounds should have a floating point type.
The class template type parameter FP_Format represents the floating point format used in the concrete domain. This parameter must be a struct similar to the ones defined in file Float_defs.hh, even though it is sufficient to define the three fields BASE, MANTISSA_BITS and EXPONENT_BIAS.

Member Typedef Documentation

template<typename FP_Interval_Type , typename FP_Format >

typedef Box<FP_Interval_Type> Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Interval_Abstract_Store

Alias for a map that associates a variable index to an interval.

Alias for a Box storing lower and upper bounds for floating point variables.

The type a linear form abstract store associating each variable with an interval that correctly approximates its value.

template<typename FP_Interval_Type , typename FP_Format >

typedef std::map<dimension_type, FP_Linear_Form> Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form_Abstract_Store

Alias for a map that associates a variable index to a linear form.

The type a linear form abstract store associating each variable with a linear form that correctly approximates its value.

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

virtual bool Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::linearize	(	const FP_Interval_Abstract_Store &	int_store,
		const FP_Linear_Form_Abstract_Store &	lf_store,
		FP_Linear_Form &	result
	)		const

pure virtual

Linearizes a floating point expression.

Makes result become a linear form that correctly approximates the value of the floating point expression in the given composite abstract store.

Parameters

int_store	The interval abstract store.
lf_store	The linear form abstract store.
result	Becomes the linearized expression.

Returns: true if the linearization succeeded, false otherwise.

Formally, if *this represents the expression $e$ , int_store represents the interval abstract store $\rho^{\#}$ and lf_store represents the linear form abstract store $\rho^{\#}_l$ , then result will become $\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l}$ if the linearization succeeds.

All variables occurring in the floating point expression MUST have an associated interval in int_store. If this precondition is not met, calling the method causes an undefined behavior.

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::overflows ( const FP_Linear_Form & lf )

inlinestatic

Verifies if a given linear form overflows.

Parameters

lf	The linear form to verify.

Returns: Returns false if all coefficients in lf are bounded, true otherwise.

template<typename FP_Interval_Type , typename FP_Format >

void Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::relative_error	(	const FP_Linear_Form &	lf,
		FP_Linear_Form &	result
	)

static

Computes the relative error of a given linear form.

Static helper method that is used by linearize to account for the relative errors on lf.

Parameters

lf	The linear form used to compute the relative error.
result	Becomes the linear form corresponding to a relative error committed on `lf`.

This method makes result become a linear form obtained by evaluating the function $\varepsilon_{\mathbf{f}}(l)$ on the linear form lf. This function is defined such as:

$\varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right) \defeq (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}]) + \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v$

where p is the fraction size in bits for the format $\mathbf{f}$ and $\beta$ the base.

template<typename FP_Interval_Type , typename FP_Format >

void Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::intervalize	(	const FP_Linear_Form &	lf,
		const FP_Interval_Abstract_Store &	store,
		FP_Interval_Type &	result
	)

static

Makes result become an interval that overapproximates all the possible values of lf in the interval abstract store store.

Parameters

lf	The linear form to aproximate.
store	The abstract store.
result	The linear form that will be modified.

This method makes result become $\iota(lf)\rho^{\#}$ , that is an interval defined as:

$\iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{\#} \defeq i \asifp \left(\bigoplus_{v \in \cV}{}^{\#}i_{v} \amifp \rho^{\#}(v)\right)$

Member Data Documentation

template<typename FP_Interval_Type , typename FP_Format >

FP_Interval_Type Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >::absolute_error = compute_absolute_error()

static

Absolute error.

Represents the interval $[-\omega, \omega]$ where $\omega$ is the smallest non-zero positive number in the less precise floating point format between the analyzer format and the analyzed format.

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

ppl.hh

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Detailed Description

template<typename FP_Interval_Type, typename FP_Format> class Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >

Member Typedef Documentation

Member Function Documentation

Member Data Documentation

template<typename FP_Interval_Type, typename FP_Format>
class Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >