A generic Multiplication Floating Point Expression. More...

#include <Multiplication_Floating_Point_Expression_defs.hh>

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

[legend]

Collaboration diagram for Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >:

[legend]

Public Types
typedef Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form	FP_Linear_Form
	Alias for the Linear_Form<FP_Interval_Type> from Floating_Point_Expression. More...

typedef Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Interval_Abstract_Store	FP_Interval_Abstract_Store
	Alias for the Box<FP_Interval_Type> from Floating_Point_Expression. More...

typedef Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form_Abstract_Store	FP_Linear_Form_Abstract_Store
	Alias for the std::map<dimension_type, FP_Linear_Form> from Floating_Point_Expression. More...

typedef Floating_Point_Expression< FP_Interval_Type, FP_Format >::boundary_type	boundary_type
	Alias for the FP_Interval_Type::boundary_type from Floating_Point_Expression. More...

typedef Floating_Point_Expression< FP_Interval_Type, FP_Format >::info_type	info_type
	Alias for the FP_Interval_Type::info_type from Floating_Point_Expression. More...

Public Types inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
typedef Linear_Form< FP_Interval_Type >	FP_Linear_Form
	Alias for a linear form with template argument `FP_Interval_Type`. More...

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. More...

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

Public Member Functions
bool	linearize (const FP_Interval_Abstract_Store &int_store, const FP_Linear_Form_Abstract_Store &lf_store, FP_Linear_Form &result) const
	Linearizes the expression in a given astract store. More...

void	m_swap (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `*this` with `y`. More...

Constructors and Destructor
	Multiplication_Floating_Point_Expression (Floating_Point_Expression< FP_Interval_Type, FP_Format > const x, Floating_Point_Expression< FP_Interval_Type, FP_Format > const y)
	Constructor with two parameters: builds the multiplication floating point expression corresponding to `x` $\otimes$ `y`. More...

	~Multiplication_Floating_Point_Expression ()
	Destructor. More...

Public Member Functions inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
virtual	~Floating_Point_Expression ()
	Destructor. More...

Private Member Functions
	Multiplication_Floating_Point_Expression (const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
	Inhibited copy constructor. More...

Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	operator= (const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &e)
	Inhibited assignment operator. More...

Private Attributes
Floating_Point_Expression< FP_Interval_Type, FP_Format > *	first_operand
	Pointer to the first operand. More...

Floating_Point_Expression< FP_Interval_Type, FP_Format > *	second_operand
	Pointer to the second operand. More...

Related Functions
(Note that these are not member functions.)
template<typename FP_Interval_Type , typename FP_Format >
void	swap (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)
	Swaps `x` with `y`. More...

template<typename FP_Interval_Type , typename FP_Format >
void	swap (Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &x, Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &y)

Additional Inherited Members
Static Public Member Functions inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
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 inherited from Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >
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::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >

A generic Multiplication Floating Point Expression.

Template type parameters

The class template type parameter FP_Interval_Type represents the type of the intervals used in the abstract domain.
The class template type parameter FP_Format represents the floating point format used in the concrete domain.

Linearization of multiplication floating-point expressions

Let $i + \sum_{v \in \cV}i_{v}v$ and $i' + \sum_{v \in \cV}i'_{v}v$ be two linear forms, $\aslf$ and $\amlf$ two sound abstract operators on linear forms such that:

$\left(i + \sum_{v \in \cV}i_{v}v\right) \aslf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \asifp i'\right) + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v,$

$i \amlf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \amifp i'\right) + \sum_{v \in \cV}\left(i \amifp i'_{v}\right)v.$

Given an expression $[a, b] \otimes e_{2}$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$ , we construct the interval linear form $\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}$ as follows:

$\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \left([a, b] \amlf \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}\right) \aslf \left([a, b] \amlf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right)\right) \aslf mf_{\mathbf{f}}[-1, 1].$

.

Given an expression $e_{1} \otimes [a, b]$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$ , we construct the interval linear form $\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}$ as follows:

$\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{[a, b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.$

Given an expression $e_{1} \otimes e_{2}$ and a composite abstract store $\left \llbracket \rho^{\#}, \rho^{\#}_l \right \rrbracket$ , we construct the interval linear form $\linexprenv{e_{1} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}$ as follows:

$\linexprenv{e_{1} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{\iota\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right)\rho^{\#} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l},$

where $\varepsilon_{\mathbf{f}}(l)$ is the linear form computed by calling method Floating_Point_Expression::relative_error on $l$ , $\iota(l)\rho^{\#}$ is the linear form computed by calling method Floating_Point_Expression::intervalize on $l$ and $\rho^{\#}$ , and $mf_{\mathbf{f}}$ is a rounding error defined in Floating_Point_Expression::absolute_error.

Even though we intervalize the first operand in the above example, the actual implementation utilizes an heuristics for choosing which of the two operands must be intervalized in order to obtain the most precise result.

Definition at line 131 of file Multiplication_Floating_Point_Expression_defs.hh.

Member Typedef Documentation

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::boundary_type Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::boundary_type

Alias for the FP_Interval_Type::boundary_type from Floating_Point_Expression.

Definition at line 166 of file Multiplication_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

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

Alias for the Box<FP_Interval_Type> from Floating_Point_Expression.

Definition at line 150 of file Multiplication_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::FP_Linear_Form Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form

Alias for the Linear_Form<FP_Interval_Type> from Floating_Point_Expression.

Definition at line 142 of file Multiplication_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>:: FP_Linear_Form_Abstract_Store Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::FP_Linear_Form_Abstract_Store

Alias for the std::map<dimension_type, FP_Linear_Form> from Floating_Point_Expression.

Definition at line 158 of file Multiplication_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

typedef Floating_Point_Expression<FP_Interval_Type, FP_Format>::info_type Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::info_type

Alias for the FP_Interval_Type::info_type from Floating_Point_Expression.

Definition at line 172 of file Multiplication_Floating_Point_Expression_defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >

Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Multiplication_Floating_Point_Expression	(	Floating_Point_Expression< FP_Interval_Type, FP_Format > *const	x,
		Floating_Point_Expression< FP_Interval_Type, FP_Format > *const	y
	)

inline

Constructor with two parameters: builds the multiplication floating point expression corresponding to x $\otimes$ y.

Definition at line 35 of file Multiplication_Floating_Point_Expression_inlines.hh.

   : first_operand(x), second_operand(y) {
   assert(x != 0);
   assert(y != 0);
 }

template<typename FP_Interval_Type , typename FP_Format >

Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::~Multiplication_Floating_Point_Expression ( )

inline

Destructor.

Definition at line 46 of file Multiplication_Floating_Point_Expression_inlines.hh.

                                             {
   delete first_operand;
   delete second_operand;
 }

template<typename FP_Interval_Type, typename FP_Format>

Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::Multiplication_Floating_Point_Expression ( const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > & e )

private

Inhibited copy constructor.

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

bool Parma_Polyhedra_Library::Multiplication_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

virtual

Linearizes the expression in a given astract store.

Makes result become the linearization of *this in the given composite abstract store.

Parameters

int_store	The interval abstract store.
lf_store	The linear form abstract store.
result	The modified linear form.

Returns: true if the linearization succeeded, false otherwise.

Note that all variables occuring in the expressions represented by first_operand and second_operand MUST have an associated value in int_store. If this precondition is not met, calling the method causes an undefined behavior.

See the class description for a detailed explanation of how result is computed.

Implements Parma_Polyhedra_Library::Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 32 of file Multiplication_Floating_Point_Expression_templates.hh.

                                           {
   /*
     FIXME: We currently adopt the "Interval-Size Local" strategy in order to
     decide which of the two linear forms must be intervalized, as described
     in Section 6.2.4 ("Multiplication Strategies") of Antoine Mine's Ph.D.
     thesis "Weakly Relational Numerical Abstract Domains".
     In this Section are also described other multiplication strategies, such
     as All-Cases, Relative-Size Local, Simplification-Driven Global and
     Homogeneity Global.
   */
 
   // Here we choose which of the two linear forms must be intervalized.
 
   // true if we intervalize the first form, false if we intervalize the second.
   bool intervalize_first;
   FP_Linear_Form linearized_first_operand;
   if (!first_operand->linearize(int_store, lf_store,
                                linearized_first_operand)) {
     return false;
   }
   FP_Interval_Type intervalized_first_operand;
   this->intervalize(linearized_first_operand, int_store,
                     intervalized_first_operand);
   FP_Linear_Form linearized_second_operand;
   if (!second_operand->linearize(int_store, lf_store,
                                 linearized_second_operand)) {
     return false;
   }
   FP_Interval_Type intervalized_second_operand;
   this->intervalize(linearized_second_operand, int_store,
                     intervalized_second_operand);
 
   // FIXME: we are not sure that what we do here is policy-proof.
   if (intervalized_first_operand.is_bounded()) {
     if (intervalized_second_operand.is_bounded()) {
       boundary_type first_interval_size
         = intervalized_first_operand.upper()
         - intervalized_first_operand.lower();
       boundary_type second_interval_size
         = intervalized_second_operand.upper()
         - intervalized_second_operand.lower();
       if (first_interval_size <= second_interval_size) {
         intervalize_first = true;
       }
       else {
         intervalize_first = false;
       }
     }
     else {
       intervalize_first = true;
     }
   }
   else {
     if (intervalized_second_operand.is_bounded()) {
       intervalize_first = false;
     }
     else {
       return false;
     }
   }
 
   // Here we do the actual computation.
   // For optimizing, we store the relative error directly into result.
   if (intervalize_first) {
     relative_error(linearized_second_operand, result);
     linearized_second_operand *= intervalized_first_operand;
     result *= intervalized_first_operand;
     result += linearized_second_operand;
   }
   else {
     relative_error(linearized_first_operand, result);
     linearized_first_operand *= intervalized_second_operand;
     result *= intervalized_second_operand;
     result += linearized_first_operand;
   }
 
   result += this->absolute_error;
   return !this->overflows(result);
 }

template<typename FP_Interval_Type , typename FP_Format >

void Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap ( Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > & y )

inline

Swaps *this with y.

Definition at line 54 of file Multiplication_Floating_Point_Expression_inlines.hh.

References Parma_Polyhedra_Library::swap().

Referenced by Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::swap().

                                                                  {
   using std::swap;
   swap(first_operand, y.first_operand);
   swap(second_operand, y.second_operand);
 }

template<typename FP_Interval_Type, typename FP_Format>

Multiplication_Floating_Point_Expression<FP_Interval_Type, FP_Format>& Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::operator= ( const Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > & e )

private

Inhibited assignment operator.

Friends And Related Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

void swap	(	Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	x,
		Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	y
	)

template<typename FP_Interval_Type , typename FP_Format >

void swap	(	Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	x,
		Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format > &	y
	)

References Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::m_swap().

                                                                                {
   x.m_swap(y);
 }

Member Data Documentation

template<typename FP_Interval_Type, typename FP_Format>

Floating_Point_Expression<FP_Interval_Type, FP_Format>* Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::first_operand

private

Pointer to the first operand.

Definition at line 221 of file Multiplication_Floating_Point_Expression_defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

Floating_Point_Expression<FP_Interval_Type, FP_Format>* Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >::second_operand

private

Pointer to the second operand.

Definition at line 223 of file Multiplication_Floating_Point_Expression_defs.hh.

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

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Related Functions

Additional Inherited Members

Detailed Description

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

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation

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