PPL  1.2
Related Functions | List of all members
Parma_Polyhedra_Library::Concrete_Expression< Target > Class Template Reference

The base class of all concrete expressions. More...

#include <Concrete_Expression_types.hh>

Related Functions

(Note that these are not member functions.)

template<typename Target , typename FP_Interval_Type >
static bool add_linearize (const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 
template<typename Target , typename FP_Interval_Type >
static bool sub_linearize (const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 
template<typename Target , typename FP_Interval_Type >
static bool mul_linearize (const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 
template<typename Target , typename FP_Interval_Type >
static bool div_linearize (const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 
template<typename Target , typename FP_Interval_Type >
static bool cast_linearize (const Cast_Operator< Target > &cast_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 
template<typename Target , typename FP_Interval_Type >
bool linearize (const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
 Linearizes a floating point expression. More...
 

Detailed Description

template<typename Target>
class Parma_Polyhedra_Library::Concrete_Expression< Target >

The base class of all concrete expressions.

Definition at line 28 of file Concrete_Expression_types.hh.

Friends And Related Function Documentation

template<typename Target , typename FP_Interval_Type >
static bool add_linearize ( const Binary_Operator< Target > &  bop_expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Helper function used by linearize to linearize a sum of floating point expressions.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
bop_exprThe binary operator concrete expression to linearize. Its binary operator type must be ADD.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultThe modified linear form.
Linearization of sum 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 and $\aslf$ a sound abstract operator 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. \]

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

\[ \linexprenv{e_{1} \oplus e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \aslf \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf mf_{\mathbf{f}}[-1, 1] \]

where $\varepsilon_{\mathbf{f}}(l)$ is the relative error associated to $l$ (see method relative_error of class Linear_Form) and $mf_{\mathbf{f}}$ is a rounding error computed by function compute_absolute_error.

Definition at line 110 of file linearize.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and Parma_Polyhedra_Library::Linear_Form< C >::relative_error().

114  {
115  PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::ADD);
116 
117  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
118 
119  if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
120  return false;
121  }
122 
123  Floating_Point_Format analyzed_format =
124  bop_expr.type().floating_point_format();
125  FP_Linear_Form rel_error;
126  result.relative_error(analyzed_format, rel_error);
127  result += rel_error;
128  FP_Linear_Form linearized_second_operand;
129  if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
130  linearized_second_operand)) {
131  return false;
132  }
133 
134  result += linearized_second_operand;
135  linearized_second_operand.relative_error(analyzed_format, rel_error);
136  result += rel_error;
137  FP_Interval_Type absolute_error =
138  compute_absolute_error<FP_Interval_Type>(analyzed_format);
139  result += absolute_error;
140  return !result.overflows();
141 }
Parma_Polyhedra_Library::Floating_Point_Format
Floating_Point_Format
Definition: globals_types.hh:187
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
template<typename Target , typename FP_Interval_Type >
static bool cast_linearize ( const Cast_Operator< Target > &  cast_expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Helper function used by linearize to linearize a cast floating point expression.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
cast_exprThe cast operator concrete expression to linearize.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultThe modified linear form.

Definition at line 635 of file linearize.hh.

References Parma_Polyhedra_Library::FP_Oracle< Target, FP_Interval_Type >::get_integer_expr_value(), Parma_Polyhedra_Library::is_less_precise_than(), Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and Parma_Polyhedra_Library::Linear_Form< C >::relative_error().

638  {
639  typedef typename FP_Interval_Type::boundary_type analyzer_format;
640  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
641 
642  Floating_Point_Format analyzed_format =
643  cast_expr.type().floating_point_format();
644  const Concrete_Expression<Target>* cast_arg = cast_expr.argument();
645  if (cast_arg->type().is_floating_point()) {
646  if (!linearize(*cast_arg, oracle, lf_store, result)) {
647  return false;
648  }
649  if (!is_less_precise_than(analyzed_format,
650  cast_arg->type().floating_point_format())
651  || result == FP_Linear_Form(FP_Interval_Type(0))
652  || result == FP_Linear_Form(FP_Interval_Type(1))) {
653  /*
654  FIXME: find a general way to check if the casted constant
655  is exactly representable in the less precise format.
656  */
657  /*
658  We are casting to a more precise format or casting
659  a definitely safe value: do not add errors.
660  */
661  return true;
662  }
663  }
664  else {
665  FP_Interval_Type expr_value;
666  if (!oracle.get_integer_expr_value(*cast_arg, expr_value))
667  return false;
668  result = FP_Linear_Form(expr_value);
669  if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format)
670  || result == FP_Linear_Form(FP_Interval_Type(0))
671  || result == FP_Linear_Form(FP_Interval_Type(1))) {
672  /*
673  FIXME: find a general way to check if the casted constant
674  is exactly representable in the less precise format.
675  */
676  /*
677  We are casting to a more precise format or casting
678  a definitely safe value: do not add errors.
679  */
680  return true;
681  }
682  }
683 
684  FP_Linear_Form rel_error;
685  result.relative_error(analyzed_format, rel_error);
686  result += rel_error;
687  FP_Interval_Type absolute_error =
688  compute_absolute_error<FP_Interval_Type>(analyzed_format);
689  result += absolute_error;
690  return !result.overflows();
691 }
Parma_Polyhedra_Library::is_less_precise_than
bool is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2)
Definition: Float_inlines.hh:513
Parma_Polyhedra_Library::Floating_Point_Format
Floating_Point_Format
Definition: globals_types.hh:187
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
template<typename Target , typename FP_Interval_Type >
static bool div_linearize ( const Binary_Operator< Target > &  bop_expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Helper function used by linearize to linearize a division of floating point expressions.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
bop_exprThe binary operator concrete expression to linearize. Its binary operator type must be DIV.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultThe modified linear form.
Linearization of division 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 $\adivlf$ two sound abstract operator 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, \]

\[ \left(i + \sum_{v \in \cV}i_{v}v\right) \adivlf i' = \left(i \adivifp i'\right) + \sum_{v \in \cV}\left(i_{v} \adivifp i'\right)v. \]

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

\[ \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l} = \left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \adivlf [a, b]\right) \aslf \left(\varepsilon_{\mathbf{f}}\left( \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right) \adivlf [a, b]\right) \aslf mf_{\mathbf{f}}[-1, 1], \]

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

\[ \linexprenv{e_{1} \oslash e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e_{1} \oslash \iota\left( \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right)\rho^{\#}}{\rho^{\#}}{\rho^{\#}_l}, \]

where $\varepsilon_{\mathbf{f}}(l)$ is the relative error associated to $l$ (see method relative_error of class Linear_Form), $\iota(l)\rho^{\#}$ is the intervalization of $l$ (see method intervalize of class Linear_Form), and $mf_{\mathbf{f}}$ is a rounding error computed by function compute_absolute_error.

Definition at line 560 of file linearize.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and Parma_Polyhedra_Library::Linear_Form< C >::relative_error().

563  {
564  PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::DIV);
565 
566  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
567 
568  FP_Linear_Form linearized_second_operand;
569  if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
570  linearized_second_operand)) {
571  return false;
572  }
573  FP_Interval_Type intervalized_second_operand;
574  if (!linearized_second_operand.intervalize(oracle,
575  intervalized_second_operand)) {
576  return false;
577  }
578  // Check if we may divide by zero.
579  if ((intervalized_second_operand.lower_is_boundary_infinity()
580  || intervalized_second_operand.lower() <= 0) &&
581  (intervalized_second_operand.upper_is_boundary_infinity()
582  || intervalized_second_operand.upper() >= 0)) {
583  return false;
584  }
585  if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
586  return false;
587  }
588 
589  Floating_Point_Format analyzed_format =
590  bop_expr.type().floating_point_format();
591  FP_Linear_Form rel_error;
592  result.relative_error(analyzed_format, rel_error);
593  result /= intervalized_second_operand;
594  rel_error /= intervalized_second_operand;
595  result += rel_error;
596  FP_Interval_Type absolute_error =
597  compute_absolute_error<FP_Interval_Type>(analyzed_format);
598  result += absolute_error;
599  return !result.overflows();
600 }
Parma_Polyhedra_Library::Floating_Point_Format
Floating_Point_Format
Definition: globals_types.hh:187
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
template<typename Target , typename FP_Interval_Type >
bool linearize ( const Concrete_Expression< Target > &  expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Linearizes a floating point expression.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
exprThe concrete expression to linearize.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultBecomes the linearized expression.

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

Definition at line 729 of file linearize.hh.

References Parma_Polyhedra_Library::EMPTY, Parma_Polyhedra_Library::FP_Oracle< Target, FP_Interval_Type >::get_associated_dimensions(), Parma_Polyhedra_Library::FP_Oracle< Target, FP_Interval_Type >::get_fp_constant_value(), Parma_Polyhedra_Library::FP_Oracle< Target, FP_Interval_Type >::get_interval(), Parma_Polyhedra_Library::Linear_Form< C >::negate(), Parma_Polyhedra_Library::not_a_dimension(), Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and PPL_COMPILE_TIME_CHECK.

732  {
733  typedef typename FP_Interval_Type::boundary_type analyzer_format;
734  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
735  typedef std::map<dimension_type, FP_Linear_Form>
736  FP_Linear_Form_Abstract_Store;
737 
738  PPL_ASSERT(expr.type().is_floating_point());
739  // Check that analyzer_format is a floating point type.
740  PPL_COMPILE_TIME_CHECK(!std::numeric_limits<analyzer_format>::is_exact,
741  "linearize<Target, FP_Interval_Type>:"
742  " FP_Interval_Type is not the type of an interval with floating point boundaries.");
743 
744  switch(expr.kind()) {
745  case Integer_Constant<Target>::KIND:
746  PPL_UNREACHABLE;
747  break;
748  case Floating_Point_Constant<Target>::KIND:
749  {
750  const Floating_Point_Constant<Target>* fpc_expr =
751  expr.template as<Floating_Point_Constant>();
752  FP_Interval_Type constant_value;
753  if (!oracle.get_fp_constant_value(*fpc_expr, constant_value)) {
754  return false;
755  }
756  result = FP_Linear_Form(constant_value);
757  return true;
758  }
759  case Unary_Operator<Target>::KIND:
760  {
761  const Unary_Operator<Target>* uop_expr =
762  expr.template as<Unary_Operator>();
763  switch (uop_expr->unary_operator()) {
764  case Unary_Operator<Target>::UPLUS:
765  return linearize(*(uop_expr->argument()), oracle, lf_store, result);
766  case Unary_Operator<Target>::UMINUS:
767  if (!linearize(*(uop_expr->argument()), oracle, lf_store, result)) {
768  return false;
769  }
770 
771  result.negate();
772  return true;
773  case Unary_Operator<Target>::BNOT:
774  throw std::runtime_error("PPL internal error: unimplemented");
775  break;
776  default:
777  PPL_UNREACHABLE;
778  break;
779  }
780  break;
781  }
782  case Binary_Operator<Target>::KIND:
783  {
784  const Binary_Operator<Target>* bop_expr =
785  expr.template as<Binary_Operator>();
786  switch (bop_expr->binary_operator()) {
787  case Binary_Operator<Target>::ADD:
788  return add_linearize(*bop_expr, oracle, lf_store, result);
789  case Binary_Operator<Target>::SUB:
790  return sub_linearize(*bop_expr, oracle, lf_store, result);
791  case Binary_Operator<Target>::MUL:
792  return mul_linearize(*bop_expr, oracle, lf_store, result);
793  case Binary_Operator<Target>::DIV:
794  return div_linearize(*bop_expr, oracle, lf_store, result);
795  case Binary_Operator<Target>::REM:
796  case Binary_Operator<Target>::BAND:
797  case Binary_Operator<Target>::BOR:
798  case Binary_Operator<Target>::BXOR:
799  case Binary_Operator<Target>::LSHIFT:
800  case Binary_Operator<Target>::RSHIFT:
801  // FIXME: can we do better?
802  return false;
803  default:
804  PPL_UNREACHABLE;
805  return false;
806  }
807  break;
808  }
809  case Approximable_Reference<Target>::KIND:
810  {
811  const Approximable_Reference<Target>* ref_expr =
812  expr.template as<Approximable_Reference>();
813  std::set<dimension_type> associated_dimensions;
814  if (!oracle.get_associated_dimensions(*ref_expr, associated_dimensions)
815  || associated_dimensions.empty()) {
816  /*
817  We were unable to find any associated space dimension:
818  linearization fails.
819  */
820  return false;
821  }
822 
823  if (associated_dimensions.size() == 1) {
824  /* If a linear form associated to the only referenced
825  space dimension exists in lf_store, return that form.
826  Otherwise, return the simplest linear form. */
827  dimension_type variable_index = *associated_dimensions.begin();
828  PPL_ASSERT(variable_index != not_a_dimension());
829 
830  typename FP_Linear_Form_Abstract_Store::const_iterator
831  variable_value = lf_store.find(variable_index);
832  if (variable_value == lf_store.end()) {
833  result = FP_Linear_Form(Variable(variable_index));
834  return true;
835  }
836 
837  result = FP_Linear_Form(variable_value->second);
838  /* FIXME: do we really need to contemplate the possibility
839  that an unbounded linear form was saved into lf_store? */
840  return !result.overflows();
841  }
842 
843  /*
844  Here associated_dimensions.size() > 1. Try to return the LUB
845  of all intervals associated to each space dimension.
846  */
847  PPL_ASSERT(associated_dimensions.size() > 1);
848  std::set<dimension_type>::const_iterator i
849  = associated_dimensions.begin();
850  std::set<dimension_type>::const_iterator i_end
851  = associated_dimensions.end();
852  FP_Interval_Type lub(EMPTY);
853  for (; i != i_end; ++i) {
854  FP_Interval_Type curr_int;
855  PPL_ASSERT(*i != not_a_dimension());
856  if (!oracle.get_interval(*i, curr_int)) {
857  return false;
858  }
859 
860  lub.join_assign(curr_int);
861  }
862 
863  result = FP_Linear_Form(lub);
864  return !result.overflows();
865  }
866  case Cast_Operator<Target>::KIND:
867  {
868  const Cast_Operator<Target>* cast_expr =
869  expr.template as<Cast_Operator>();
870  return cast_linearize(*cast_expr, oracle, lf_store, result);
871  }
872  default:
873  PPL_UNREACHABLE;
874  break;
875  }
876 
877  PPL_UNREACHABLE;
878  return false;
879 }
Parma_Polyhedra_Library::EMPTY
The empty element, i.e., the empty set.
Definition: globals_types.hh:34
Parma_Polyhedra_Library::dimension_type
size_t dimension_type
An unsigned integral type for representing space dimensions.
Definition: globals_types.hh:22
Parma_Polyhedra_Library::Concrete_Expression::cast_linearize
static bool cast_linearize(const Cast_Operator< Target > &cast_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Definition: linearize.hh:635
Parma_Polyhedra_Library::not_a_dimension
dimension_type not_a_dimension()
Returns a value that does not designate a valid dimension.
Definition: globals_inlines.hh:38
Parma_Polyhedra_Library::Concrete_Expression::sub_linearize
static bool sub_linearize(const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Definition: linearize.hh:224
PPL_COMPILE_TIME_CHECK
#define PPL_COMPILE_TIME_CHECK(e, msg)
Produces a compilation error if the compile-time constant e does not evaluate to true ...
Definition: meta_programming.hh:133
Parma_Polyhedra_Library::Concrete_Expression::add_linearize
static bool add_linearize(const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Definition: linearize.hh:110
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
Parma_Polyhedra_Library::Concrete_Expression::mul_linearize
static bool mul_linearize(const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Definition: linearize.hh:366
Parma_Polyhedra_Library::Concrete_Expression::div_linearize
static bool div_linearize(const Binary_Operator< Target > &bop_expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Definition: linearize.hh:560
template<typename Target , typename FP_Interval_Type >
static bool mul_linearize ( const Binary_Operator< Target > &  bop_expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Helper function used by linearize to linearize a product of floating point expressions.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
bop_exprThe binary operator concrete expression to linearize. Its binary operator type must be MUL.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultThe modified linear form.
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 relative error associated to $l$ (see method relative_error of class Linear_Form), $\iota(l)\rho^{\#}$ is the intervalization of $l$ (see method intervalize of class Linear_Form), and $mf_{\mathbf{f}}$ is a rounding error computed by function compute_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 366 of file linearize.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and Parma_Polyhedra_Library::Linear_Form< C >::relative_error().

369  {
370  PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::MUL);
371 
372  typedef typename FP_Interval_Type::boundary_type analyzer_format;
373  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
374 
375  /*
376  FIXME: We currently adopt the "Interval-Size Local" strategy in order to
377  decide which of the two linear forms must be intervalized, as described
378  in Section 6.2.4 ("Multiplication Strategies") of Antoine Mine's Ph.D.
379  thesis "Weakly Relational Numerical Abstract Domains".
380  In this Section are also described other multiplication strategies, such
381  as All-Cases, Relative-Size Local, Simplification-Driven Global and
382  Homogeneity Global.
383  */
384 
385  // Here we choose which of the two linear forms must be intervalized.
386 
387  // true if we intervalize the first form, false if we intervalize the second.
388  bool intervalize_first;
389  FP_Linear_Form linearized_first_operand;
390  if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store,
391  linearized_first_operand)) {
392  return false;
393  }
394  FP_Interval_Type intervalized_first_operand;
395  if (!linearized_first_operand.intervalize(oracle,
396  intervalized_first_operand)) {
397  return false;
398  }
399  FP_Linear_Form linearized_second_operand;
400  if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
401  linearized_second_operand)) {
402  return false;
403  }
404  FP_Interval_Type intervalized_second_operand;
405  if (!linearized_second_operand.intervalize(oracle,
406  intervalized_second_operand)) {
407  return false;
408  }
409 
410  // FIXME: we are not sure that what we do here is policy-proof.
411  if (intervalized_first_operand.is_bounded()) {
412  if (intervalized_second_operand.is_bounded()) {
413  analyzer_format first_interval_size
414  = intervalized_first_operand.upper()
415  - intervalized_first_operand.lower();
416  analyzer_format second_interval_size
417  = intervalized_second_operand.upper()
418  - intervalized_second_operand.lower();
419  if (first_interval_size <= second_interval_size) {
420  intervalize_first = true;
421  }
422  else {
423  intervalize_first = false;
424  }
425  }
426  else {
427  intervalize_first = true;
428  }
429  }
430  else {
431  if (intervalized_second_operand.is_bounded()) {
432  intervalize_first = false;
433  }
434  else {
435  return false;
436  }
437  }
438 
439  // Here we do the actual computation.
440  // For optimizing, we store the relative error directly into result.
441  Floating_Point_Format analyzed_format =
442  bop_expr.type().floating_point_format();
443  if (intervalize_first) {
444  linearized_second_operand.relative_error(analyzed_format, result);
445  linearized_second_operand *= intervalized_first_operand;
446  result *= intervalized_first_operand;
447  result += linearized_second_operand;
448  }
449  else {
450  linearized_first_operand.relative_error(analyzed_format, result);
451  linearized_first_operand *= intervalized_second_operand;
452  result *= intervalized_second_operand;
453  result += linearized_first_operand;
454  }
455 
456  FP_Interval_Type absolute_error =
457  compute_absolute_error<FP_Interval_Type>(analyzed_format);
458  result += absolute_error;
459  return !result.overflows();
460 }
Parma_Polyhedra_Library::Floating_Point_Format
Floating_Point_Format
Definition: globals_types.hh:187
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
template<typename Target , typename FP_Interval_Type >
static bool sub_linearize ( const Binary_Operator< Target > &  bop_expr,
const FP_Oracle< Target, FP_Interval_Type > &  oracle,
const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &  lf_store,
Linear_Form< FP_Interval_Type > &  result 
)
related

Helper function used by linearize to linearize a difference of floating point expressions.

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

Template Parameters
TargetA type template parameter specifying the instantiation of Concrete_Expression to be used.
FP_Interval_TypeA type template parameter for the intervals used in the abstract domain. The interval bounds should have a floating point type.
Returns
true if the linearization succeeded, false otherwise.
Parameters
bop_exprThe binary operator concrete expression to linearize. Its binary operator type must be SUB.
oracleThe FP_Oracle to be queried.
lf_storeThe linear form abstract store.
resultThe modified linear form.
Linearization of difference 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 $\adlf$ two sound abstract operators on linear form 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, \]

\[ \left(i + \sum_{v \in \cV}i_{v}v\right) \adlf \left(i' + \sum_{v \in \cV}i'_{v}v\right) = \left(i \adifp i'\right) + \sum_{v \in \cV}\left(i_{v} \adifp i'_{v}\right)v. \]

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

\[ \linexprenv{e_{1} \ominus e_{2}}{\rho^{\#}}{\rho^{\#}_l} = \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \adlf \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l} \right) \aslf mf_{\mathbf{f}}[-1, 1] \]

where $\varepsilon_{\mathbf{f}}(l)$ is the relative error associated to $l$ (see method relative_error of class Linear_Form) and $mf_{\mathbf{f}}$ is a rounding error computed by function compute_absolute_error.

Definition at line 224 of file linearize.hh.

References Parma_Polyhedra_Library::Linear_Form< C >::overflows(), and Parma_Polyhedra_Library::Linear_Form< C >::relative_error().

227  {
228  PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::SUB);
229 
230  typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
231 
232  if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
233  return false;
234  }
235 
236  Floating_Point_Format analyzed_format =
237  bop_expr.type().floating_point_format();
238  FP_Linear_Form rel_error;
239  result.relative_error(analyzed_format, rel_error);
240  result += rel_error;
241  FP_Linear_Form linearized_second_operand;
242  if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
243  linearized_second_operand)) {
244  return false;
245  }
246 
247  result -= linearized_second_operand;
248  linearized_second_operand.relative_error(analyzed_format, rel_error);
249  result += rel_error;
250  FP_Interval_Type absolute_error =
251  compute_absolute_error<FP_Interval_Type>(analyzed_format);
252  result += absolute_error;
253  return !result.overflows();
254 }
Parma_Polyhedra_Library::Floating_Point_Format
Floating_Point_Format
Definition: globals_types.hh:187
Parma_Polyhedra_Library::Concrete_Expression::linearize
bool linearize(const Concrete_Expression< Target > &expr, const FP_Oracle< Target, FP_Interval_Type > &oracle, const std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Linear_Form< FP_Interval_Type > &result)
Linearizes a floating point expression.
Definition: linearize.hh:729
The documentation for this class was generated from the following files: