A floating point expression on a given format. More...

#include <Floating_Point_Expression.defs.hh>

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

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.
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.
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.
Static Public Member Functions
static bool	overflows (const FP_Linear_Form &lf)
	Verifies if a given linear form overflows.
static void	relative_error (const FP_Linear_Form &lf, FP_Linear_Form &result)
	Computes the relative error of a given linear form.
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`.
Static Public Attributes
static FP_Interval_Type	absolute_error = compute_absolute_error()
	Absolute error.
Static Private Member Functions
static FP_Interval_Type	compute_absolute_error ()
	Computes the absolute error.

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.

Definition at line 56 of file Floating_Point_Expression.defs.hh.

Member Typedef Documentation

template<typename FP_Interval_Type, typename FP_Format>

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

The floating point format used by the analyzer.

Reimplemented in Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Sum_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >, and Parma_Polyhedra_Library::Constant_Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 82 of file Floating_Point_Expression.defs.hh.

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.

Definition at line 71 of file Floating_Point_Expression.defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

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

Alias for a linear form with template argument FP_Interval_Type.

Definition at line 61 of file Floating_Point_Expression.defs.hh.

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.

Definition at line 79 of file Floating_Point_Expression.defs.hh.

template<typename FP_Interval_Type, typename FP_Format>

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

The interval policy used by FP_Interval_Type.

Reimplemented in Parma_Polyhedra_Library::Multiplication_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Division_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Difference_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Sum_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Opposite_Floating_Point_Expression< FP_Interval_Type, FP_Format >, Parma_Polyhedra_Library::Variable_Floating_Point_Expression< FP_Interval_Type, FP_Format >, and Parma_Polyhedra_Library::Constant_Floating_Point_Expression< FP_Interval_Type, FP_Format >.

Definition at line 85 of file Floating_Point_Expression.defs.hh.

Constructor & Destructor Documentation

template<typename FP_Interval_Type , typename FP_Format >

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

inlinevirtual

Destructor.

Definition at line 35 of file Floating_Point_Expression.inlines.hh.

{}

Member Function Documentation

template<typename FP_Interval_Type , typename FP_Format >

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

staticprivate

Computes the absolute error.

Static helper method that is used to compute the value of the public static field absolute_error.

Returns:: The interval $[-\omega, \omega]$ corresponding to the value of absolute_error

Definition at line 95 of file Floating_Point_Expression.templates.hh.

References Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::i_constraint(), and Parma_Polyhedra_Library::LESS_OR_EQUAL.

                         {
  typedef typename Floating_Point_Expression<FP_Interval_Type, FP_Format>
    ::boundary_type Boundary;
  boundary_type omega;
  omega = std::max(pow(static_cast<Boundary>(FP_Format::BASE),
                       static_cast<Boundary>(1 - FP_Format::EXPONENT_BIAS
                                             - FP_Format::MANTISSA_BITS)),
                   std::numeric_limits<Boundary>::denorm_min());
  FP_Interval_Type result;
  result.build(i_constraint(GREATER_OR_EQUAL, -omega),
               i_constraint(LESS_OR_EQUAL, omega));
  return result;
}

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)$

Definition at line 76 of file Floating_Point_Expression.templates.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::coefficient(), Parma_Polyhedra_Library::Box< ITV >::get_interval(), Parma_Polyhedra_Library::Linear_Form< C >::inhomogeneous_term(), Parma_Polyhedra_Library::Linear_Form< C >::space_dimension(), and Parma_Polyhedra_Library::Box< ITV >::space_dimension().

                                        {
  result = FP_Interval_Type(lf.inhomogeneous_term());
  dimension_type dimension = lf.space_dimension();
  assert(dimension <= store.space_dimension());
  for (dimension_type i = 0; i < dimension; ++i) {
    FP_Interval_Type current_addend = lf.coefficient(Variable(i));
    const FP_Interval_Type& curr_int = store.get_interval(Variable(i));
    current_addend *= curr_int;
    result += current_addend;
  }

  return;
}

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.

Definition at line 40 of file Floating_Point_Expression.inlines.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::coefficient(), Parma_Polyhedra_Library::Linear_Form< C >::inhomogeneous_term(), and Parma_Polyhedra_Library::Linear_Form< C >::space_dimension().

                                    {
  if (!lf.inhomogeneous_term().is_bounded())
    return true;

  dimension_type dimension = lf.space_dimension();
  for (dimension_type i = 0; i < dimension; ++i) {
    if (!lf.coefficient(Variable(i)).is_bounded())
      return true;
  }

  return false;
}

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.

Definition at line 36 of file Floating_Point_Expression.templates.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::coefficient(), Parma_Polyhedra_Library::GREATER_OR_EQUAL, Parma_Polyhedra_Library::i_constraint(), Parma_Polyhedra_Library::Linear_Form< C >::inhomogeneous_term(), Parma_Polyhedra_Library::LESS_OR_EQUAL, and Parma_Polyhedra_Library::Linear_Form< C >::space_dimension().

                                                                 {

  FP_Interval_Type error_propagator;
  boundary_type lb = -pow(FP_Format::BASE,
  -static_cast<typename Floating_Point_Expression<FP_Interval_Type, FP_Format>
  ::boundary_type>(FP_Format::MANTISSA_BITS));
  error_propagator.build(i_constraint(GREATER_OR_EQUAL, lb),
                         i_constraint(LESS_OR_EQUAL, -lb));

  // Handle the inhomogeneous term.
  const FP_Interval_Type* current_term = &lf.inhomogeneous_term();
  assert(current_term->is_bounded());

  FP_Interval_Type
    current_multiplier(std::max(std::abs(current_term->lower()),
                                std::abs(current_term->upper())));
  FP_Linear_Form current_result_term(current_multiplier);
  current_result_term *= error_propagator;
  result = FP_Linear_Form(current_result_term);

  // Handle the other terms.
  dimension_type dimension = lf.space_dimension();
  for (dimension_type i = 0; i < dimension; ++i) {
    current_term = &lf.coefficient(Variable(i));
    assert(current_term->is_bounded());
    current_multiplier
      = FP_Interval_Type(std::max(std::abs(current_term->lower()),
                                  std::abs(current_term->upper())));
    current_result_term = FP_Linear_Form(Variable(i));
    current_result_term *= current_multiplier;
    current_result_term *= error_propagator;
    result += current_result_term;
  }

  return;
}

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.

Definition at line 127 of file Floating_Point_Expression.defs.hh.

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

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Static Private Member Functions

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

Constructor & Destructor 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 >