July 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): linearize.hh:
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 77104a92691b2a793fa6e522f7f3d959b594417c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=77104a92691b… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 15:45:20 2010 +0200 linearize.hh: - Fixed mistake when accessing type informations. C_Expr: - Small progress in the implementation. --- src/linearize.hh | 12 ++++++++---- tests/Concrete_Expression/C_Expr.defs.hh | 27 +++++++++++++++++++++++++++ tests/Concrete_Expression/C_Expr.inlines.hh | 27 +++++++++++++++++++++++++++ 3 files changed, 62 insertions(+), 4 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 7883cfa..3bc8f2f 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -117,7 +117,8 @@ add_linearize(const Binary_Operator<Target>& bop_expr, if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; - Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); + Floating_Point_Format analyzed_format = + bop_expr.type().floating_point_format(); FP_Linear_Form rel_error; result.relative_error(analyzed_format, rel_error); result += rel_error; @@ -227,7 +228,8 @@ sub_linearize(const Binary_Operator<Target>& bop_expr, if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; - Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); + Floating_Point_Format analyzed_format = + bop_expr.type().floating_point_format(); FP_Linear_Form rel_error; result.relative_error(analyzed_format, rel_error); result += rel_error; @@ -415,7 +417,8 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, // Here we do the actual computation. // For optimizing, we store the relative error directly into result. - Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); + Floating_Point_Format analyzed_format = + bop_expr.type().floating_point_format(); if (intervalize_first) { linearized_second_operand.relative_error(analyzed_format, result); linearized_second_operand *= intervalized_first_operand; @@ -558,7 +561,8 @@ div_linearize(const Binary_Operator<Target>& bop_expr, if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; - Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); + Floating_Point_Format analyzed_format = + bop_expr.type().floating_point_format(); FP_Linear_Form rel_error; result.relative_error(analyzed_format, rel_error); result /= intervalized_second_operand; diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index 41c2053..073e9a8 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -141,6 +141,15 @@ template <> class Cast_Operator<C_Expr> : public Cast_Operator_Base<C_Expr> { public: + //! Do-nothing destructor. + ~Cast_Operator<C_Expr>(); + + //! Returns the type of \p *this. + Concrete_Expression_Type type() const; + + //! Returns the kind of \p *this. + Concrete_Expression_Kind kind() const; + //! Constant identifying cast nodes. enum { KIND = 3 }; }; @@ -149,6 +158,15 @@ template <> class Integer_Constant<C_Expr> : public Integer_Constant_Base<C_Expr> { public: + //! Do-nothing destructor. + ~Integer_Constant<C_Expr>(); + + //! Returns the type of \p *this. + Concrete_Expression_Type type() const; + + //! Returns the kind of \p *this. + Concrete_Expression_Kind kind() const; + //! Constant identifying integer constant nodes. enum { KIND = 4 }; }; @@ -157,6 +175,15 @@ template <> class Floating_Point_Constant<C_Expr> : public Floating_Point_Constant_Base<C_Expr> { public: + //! Do-nothing destructor. + ~Floating_Point_Constant<C_Expr>(); + + //! Returns the type of \p *this. + Concrete_Expression_Type type() const; + + //! Returns the kind of \p *this. + Concrete_Expression_Kind kind() const; + //! Constant identifying floating constant nodes. enum { KIND = 5 }; }; diff --git a/tests/Concrete_Expression/C_Expr.inlines.hh b/tests/Concrete_Expression/C_Expr.inlines.hh index 43acc0e..900e90f 100644 --- a/tests/Concrete_Expression/C_Expr.inlines.hh +++ b/tests/Concrete_Expression/C_Expr.inlines.hh @@ -87,6 +87,33 @@ Unary_Operator<C_Expr>::argument() const { } inline +Cast_Operator<C_Expr>::~Cast_Operator<C_Expr>() { +} + +inline Concrete_Expression_Kind +Cast_Operator<C_Expr>::kind() const { + return KIND; +} + +inline +Integer_Constant<C_Expr>::~Integer_Constant<C_Expr>() { +} + +inline Concrete_Expression_Kind +Integer_Constant<C_Expr>::kind() const { + return KIND; +} + +inline +Floating_Point_Constant<C_Expr>::~Floating_Point_Constant<C_Expr>() { +} + +inline Concrete_Expression_Kind +Floating_Point_Constant<C_Expr>::kind() const { + return KIND; +} + +inline Approximable_Reference<C_Expr>:: Approximable_Reference(dimension_type var_index) : var_dimension(var_index) {

1 0

[GIT] ppl/ppl(floating_point): Added method associated_dimension.
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: feb014edf63cb2f41c923db0c5fc21097794a4e2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=feb014edf63c… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 15:26:45 2010 +0200 Added method associated_dimension. --- tests/Concrete_Expression/C_Expr.inlines.hh | 5 +++++ 1 files changed, 5 insertions(+), 0 deletions(-) diff --git a/tests/Concrete_Expression/C_Expr.inlines.hh b/tests/Concrete_Expression/C_Expr.inlines.hh index f92c79f..43acc0e 100644 --- a/tests/Concrete_Expression/C_Expr.inlines.hh +++ b/tests/Concrete_Expression/C_Expr.inlines.hh @@ -101,6 +101,11 @@ Approximable_Reference<C_Expr>::kind() const { return KIND; } +inline dimension_type +Approximable_Reference<C_Expr>::associated_dimension() const { + return var_dimension; +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_C_Expr_inlines_hh)

1 0

[GIT] ppl/ppl(floating_point): Concrete_Expression:
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: e34112b360cf60ef5be4c2464d2a40e1e2f4b553 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e34112b360cf… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 15:22:50 2010 +0200 Concrete_Expression: - Added method associated_dimension(). C_Expr: - Small progress in the implementation. --- src/Concrete_Expression.defs.hh | 6 +++++ tests/Concrete_Expression/C_Expr.defs.hh | 30 ++++++++++++++++++++++++-- tests/Concrete_Expression/C_Expr.inlines.hh | 25 ++++++++++++++++++++++ 3 files changed, 58 insertions(+), 3 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index 0442195..f6777cd 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -162,6 +162,12 @@ class Floating_Point_Constant_Base : public Concrete_Expression<Target> { template <typename Target> class Approximable_Reference_Base : public Concrete_Expression<Target> { +public: + /*! \brief + If \p *this is a variable reference, returns the variable's + index. Returns <CODE>not_a_dimension()</CODE> otherwise. + */ + dimension_type associated_dimension() const; }; } // namespace Parma_Polyhedra_Library diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index 2d7b4c2..41c2053 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -54,10 +54,10 @@ public: Concrete_Expression_Type type() const; //! Returns the kind of \p *this. - int kind() const; + Concrete_Expression_Kind kind() const; //! Returns the binary operator of \p *this. - int binary_operator() const; + Concrete_Expression_BOP binary_operator() const; //! Returns the left-hand side of \p *this. const Concrete_Expression<C_Expr>* left_hand_side() const; @@ -97,6 +97,7 @@ private: template <> class Unary_Operator<C_Expr> : public Unary_Operator_Base<C_Expr> { +public: //! Constructor from operator and argument. Unary_Operator<C_Expr>(int unary_operator, const Concrete_Expression<C_Expr>* argument); @@ -111,7 +112,7 @@ class Unary_Operator<C_Expr> : public Unary_Operator_Base<C_Expr> { Concrete_Expression_Kind kind() const; //! Returns the unary operator of \p *this. - int unary_operator() const; + Concrete_Expression_UOP unary_operator() const; //! Returns the argument of \p *this. const Concrete_Expression<C_Expr>* argument() const; @@ -160,12 +161,35 @@ public: enum { KIND = 5 }; }; +// We currently only consider variable references. template <> class Approximable_Reference<C_Expr> : public Approximable_Reference_Base<C_Expr> { public: + //! Builds a reference to the variable having the given index. + Approximable_Reference<C_Expr>(dimension_type var_index); + + //! Do-nothing destructor. + ~Approximable_Reference<C_Expr>(); + + //! Returns the type of \p *this. + Concrete_Expression_Type type() const; + + //! Returns the kind of \p *this. + Concrete_Expression_Kind kind() const; + + /*! \brief + If \p *this is a variable reference, returns the variable's + index. Returns <CODE>not_a_dimension()</CODE> otherwise. + */ + dimension_type associated_dimension() const; + //! Constant identifying approximable reference nodes. enum { KIND = 6 }; + +private: + //! The index of the referenced variable. + dimension_type var_dimension; }; } // namespace Parma_Polyhedra_Library diff --git a/tests/Concrete_Expression/C_Expr.inlines.hh b/tests/Concrete_Expression/C_Expr.inlines.hh index 41fef95..f92c79f 100644 --- a/tests/Concrete_Expression/C_Expr.inlines.hh +++ b/tests/Concrete_Expression/C_Expr.inlines.hh @@ -39,6 +39,11 @@ inline Binary_Operator<C_Expr>::~Binary_Operator<C_Expr>() { } +inline Concrete_Expression_Kind +Binary_Operator<C_Expr>::kind() const { + return KIND; +} + inline Concrete_Expression_BOP Binary_Operator<C_Expr>::binary_operator() const { return bop; @@ -66,6 +71,11 @@ inline Unary_Operator<C_Expr>::~Unary_Operator<C_Expr>() { } +inline Concrete_Expression_Kind +Unary_Operator<C_Expr>::kind() const { + return KIND; +} + inline Concrete_Expression_BOP Unary_Operator<C_Expr>::unary_operator() const { return uop; @@ -76,6 +86,21 @@ Unary_Operator<C_Expr>::argument() const { return arg; } +inline +Approximable_Reference<C_Expr>:: +Approximable_Reference(dimension_type var_index) +: var_dimension(var_index) { +} + +inline +Approximable_Reference<C_Expr>::~Approximable_Reference<C_Expr>() { +} + +inline Concrete_Expression_Kind +Approximable_Reference<C_Expr>::kind() const { + return KIND; +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_C_Expr_inlines_hh)

1 0

[GIT] ppl/ppl(floating_point): Removed an assertion.
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: cf0f3e91a7d00432443ee59354eb8354643c4dc6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cf0f3e91a7d0… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 14:22:00 2010 +0200 Removed an assertion. --- src/linearize.hh | 3 --- 1 files changed, 0 insertions(+), 3 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 2f1171b..7883cfa 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -619,9 +619,6 @@ linearize(const Concrete_Expression<Target>& expr, "linearize<Target, FP_Interval_Type>:" " FP_Interval_Type is not the type of an interval with floating point boundaries."); - // Check that we are dealing with an expression of floating point type. - PPL_ASSERT(expr.is_floating_point()); - switch(expr.kind()) { case Integer_Constant<Target>::KIND: throw std::runtime_error("PPL internal error: unimplemented");

1 0

[GIT] ppl/ppl(floating_point): Added some documentation.
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: e23a7833eaddaa3658132a9163ec022d9d132613 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e23a7833eadd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 14:04:19 2010 +0200 Added some documentation. --- doc/devref.doxyconf-html.in | 1 + doc/devref.doxyconf-latex.in | 1 + src/linearize.hh | 377 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 379 insertions(+), 0 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e23a7833…

1 0

[GIT] ppl/ppl(floating_point): Consistently use the typedefs.
by Roberto Bagnara 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: d1180bb65f43f1fd00788be818cd5266b4dd8096 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d1180bb65f43… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Jul 26 13:49:58 2010 +0200 Consistently use the typedefs. --- src/Concrete_Expression.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Concrete_Expression.defs.hh b/src/Concrete_Expression.defs.hh index f5ca921..0442195 100644 --- a/src/Concrete_Expression.defs.hh +++ b/src/Concrete_Expression.defs.hh @@ -129,7 +129,7 @@ template <typename Target> class Binary_Operator_Base : public Concrete_Expression<Target> { public: //! Returns a constant identifying the operator of \p *this. - int binary_operator() const; + Concrete_Expression_BOP binary_operator() const; //! Returns the left-hand side of \p *this. const Concrete_Expression<Target>* left_hand_side() const; @@ -142,7 +142,7 @@ template <typename Target> class Unary_Operator_Base : public Concrete_Expression<Target> { public: //! Returns a constant identifying the operator of \p *this. - int unary_operator() const; + Concrete_Expression_UOP unary_operator() const; //! Returns the argument \p *this. const Concrete_Expression<Target>* argument() const;

1 0

[GIT] ppl/ppl(floating_point): Adapted to latest changes in Concrete_Expression's
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 7d4c2d096dd5b83034515e107b6ee168c5eee8c7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7d4c2d096dd5… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 11:47:56 2010 +0200 Adapted to latest changes in Concrete_Expression's interface. --- src/linearize.hh | 32 ++++++++++++++++---------------- 1 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 5644a9b..5a8e9ad 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -37,14 +37,14 @@ add_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::ADD); + PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::ADD); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; - if (!linearize(*(bop_expr.get_lhs()), int_store, lf_store, result)) + if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); @@ -52,7 +52,7 @@ add_linearize(const Binary_Operator<Target>& bop_expr, result.relative_error(analyzed_format, rel_error); result += rel_error; FP_Linear_Form linearized_second_operand; - if (!linearize(*(bop_expr.get_rhs()), int_store, lf_store, + if (!linearize(*(bop_expr.right_hand_side()), int_store, lf_store, linearized_second_operand)) return false; @@ -71,14 +71,14 @@ sub_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::SUB); + PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::SUB); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; - if (!linearize(*(bop_expr.get_lhs()), int_store, lf_store, result)) + if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); @@ -86,7 +86,7 @@ sub_linearize(const Binary_Operator<Target>& bop_expr, result.relative_error(analyzed_format, rel_error); result += rel_error; FP_Linear_Form linearized_second_operand; - if (!linearize(*(bop_expr.get_rhs()), int_store, lf_store, + if (!linearize(*(bop_expr.right_hand_side()), int_store, lf_store, linearized_second_operand)) return false; @@ -105,7 +105,7 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::MUL); + PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::MUL); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -127,13 +127,13 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, // true if we intervalize the first form, false if we intervalize the second. bool intervalize_first; FP_Linear_Form linearized_first_operand; - if (!linearize(*(bop_expr.get_lhs()), int_store, lf_store, + if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, linearized_first_operand)) return false; FP_Interval_Type intervalized_first_operand; linearized_first_operand.intervalize(int_store, intervalized_first_operand); FP_Linear_Form linearized_second_operand; - if (!linearize(*(bop_expr.get_rhs()), int_store, lf_store, + if (!linearize(*(bop_expr.right_hand_side()), int_store, lf_store, linearized_second_operand)) return false; FP_Interval_Type intervalized_second_operand; @@ -190,7 +190,7 @@ div_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::DIV); + PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::DIV); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -198,7 +198,7 @@ div_linearize(const Binary_Operator<Target>& bop_expr, typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; FP_Linear_Form linearized_second_operand; - if (!linearize(*(bop_expr.get_rhs()), int_store, lf_store, + if (!linearize(*(bop_expr.right_hand_side()), int_store, lf_store, linearized_second_operand)) return false; FP_Interval_Type intervalized_second_operand; @@ -211,7 +211,7 @@ div_linearize(const Binary_Operator<Target>& bop_expr, intervalized_second_operand.upper() >= 0)) return false; - if (!linearize(*(bop_expr.get_lhs()), int_store, lf_store, result)) + if (!linearize(*(bop_expr.left_hand_side()), int_store, lf_store, result)) return false; Floating_Point_Format analyzed_format = bop_expr.floating_point_format(); @@ -258,12 +258,12 @@ linearize(const Concrete_Expression<Target>& expr, case Unary_Operator<Target>::KIND: Unary_Operator<Target> uop_expr = static_cast<Unary_Operator<Target> >(expr); - switch (uop_expr.get_uop()) { + switch (uop_expr.unary_operator()) { case Unary_Operator<Target>::UPLUS: - return linearize(uop_expr.get_arg(), int_store, lf_store, result); + return linearize(uop_expr.argument(), int_store, lf_store, result); break; case Unary_Operator<Target>::UMINUS: - if (!linearize(uop_expr.get_arg(), int_store, lf_store, result)) + if (!linearize(uop_expr.argument(), int_store, lf_store, result)) return false; result.negate(); @@ -279,7 +279,7 @@ linearize(const Concrete_Expression<Target>& expr, case Binary_Operator<Target>::KIND: Binary_Operator<Target> bop_expr = static_cast<Binary_Operator<Target> >(expr); - switch (bop_expr.get_bop()) { + switch (bop_expr.binary_operator()) { case Binary_Operator<Target>::ADD: return add_linearize(bop_expr, int_store, lf_store, result); break;

1 0

[GIT] ppl/ppl(floating_point): Makefile.am:
by Fabio Bossi 26 Jul '10

26 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 82938f2c47098c92a07a5e958f39e343a463b3d0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=82938f2c4709… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Jul 26 11:24:18 2010 +0200 Makefile.am: - Added linearize.hh to the list of compilation units. linearize.hh: - Fixed a few small mistakes. - Temporarily throw an exception on non-floating point expressions. - Added the variable reference case. --- src/Makefile.am | 1 + src/linearize.hh | 93 ++++++++++++++++++++++-------------------------------- 2 files changed, 39 insertions(+), 55 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index 5f3a962..bfefcb6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -262,6 +262,7 @@ Linear_Expression.inlines.hh \ Linear_Form.defs.hh \ Linear_Form.inlines.hh \ Linear_Form.templates.hh \ +linearize.hh \ Constraint.defs.hh \ Constraint.inlines.hh \ Constraint_System.inlines.hh \ diff --git a/src/linearize.hh b/src/linearize.hh index 681e846..5644a9b 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -33,50 +33,11 @@ namespace Parma_Polyhedra_Library { template <typename Target, typename FP_Interval_Type> static bool -bnot_linearize(const Unary_Operator<Target>& uop_expr, - const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, - Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(uop_expr.get_uop() == BNOT); - - typedef typename FP_Interval_Type::boundary_type analyzer_format; - typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; - typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; - typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; - - if (!linearize(uop_expr.get_arg(), int_store, lf_store, result)) - return false; - - FP_Interval_Type int_r; - result.intervalize(int_store, int_r); - bool lb_is_positive = (!int_r.is_lower_boundary_infinity() && - int_r.lower() > 0); - bool ub_is_negative = (!int_r.is_upper_boundary_infinity() && - int_r.upper() < 0); - if (lb_is_positive || ub_is_negative) { - result = FP_Linear_Form(FP_Interval(0)); - return true; - } - else if (int_r.is_singleton()) { - // Here int_r is the singleton of 0. - // FIXME: Check if the negation of 0 MUST be 1. - result = FP_Linear_Form(FP_Interval(1)); - return true; - } - else - // Here int_r strictly contains 0. - result = FP_Interval_Type(0); - result.join_assign(1); - return true; -} - -template <typename Target, typename FP_Interval_Type> -static bool add_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, + const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == ADD); + PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::ADD); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -108,9 +69,9 @@ template <typename Target, typename FP_Interval_Type> static bool sub_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, + const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == SUB); + PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::SUB); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -142,9 +103,9 @@ template <typename Target, typename FP_Interval_Type> static bool mul_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, + const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == MUL); + PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::MUL); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -177,7 +138,7 @@ mul_linearize(const Binary_Operator<Target>& bop_expr, return false; FP_Interval_Type intervalized_second_operand; linearized_second_operand.intervalize(int_store, intervalized_second_operand); - boundary_type first_interval_size, second_interval_size; + analyzer_format first_interval_size, second_interval_size; // FIXME: we are not sure that what we do here is policy-proof. if (intervalized_first_operand.is_bounded()) { @@ -227,9 +188,9 @@ template <typename Target, typename FP_Interval_Type> static bool div_linearize(const Binary_Operator<Target>& bop_expr, const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, + const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { - PPL_ASSERT(bop_expr.get_bop() == DIV); + PPL_ASSERT(bop_expr.get_bop() == Binary_Operator<Target>::DIV); typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -269,7 +230,7 @@ template <typename Target, typename FP_Interval_Type> bool linearize(const Concrete_Expression<Target>& expr, const Box<FP_Interval_Type>& int_store, - const std::map<dimension_type, Linear_Form<FP_Interval_Type>>& lf_store, + const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store, Linear_Form<FP_Interval_Type>& result) { typedef typename FP_Interval_Type::boundary_type analyzer_format; typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; @@ -286,17 +247,17 @@ linearize(const Concrete_Expression<Target>& expr, switch(expr.kind()) { case Integer_Constant<Target>::KIND: - // TODO. + throw std::runtime_error("PPL internal error: unimplemented"); break; case Floating_Point_Constant<Target>::KIND: Floating_Point_Constant<Target> fpc_expr = - static_cast<Floating_Point_Constant<Target>>(expr); + static_cast<Floating_Point_Constant<Target> >(expr); result = FP_Linear_Form(FP_Interval(fpc_expr.get_value_as_string())); return true; break; case Unary_Operator<Target>::KIND: Unary_Operator<Target> uop_expr = - static_cast<Unary_Operator<Target>>(expr); + static_cast<Unary_Operator<Target> >(expr); switch (uop_expr.get_uop()) { case Unary_Operator<Target>::UPLUS: return linearize(uop_expr.get_arg(), int_store, lf_store, result); @@ -309,7 +270,7 @@ linearize(const Concrete_Expression<Target>& expr, return true; break; case Unary_Operator<Target>::BNOT: - return bnot_linearize(uop_expr, int_store, lf_store, result); + throw std::runtime_error("PPL internal error: unimplemented"); break; default: throw std::runtime_error("PPL internal error"); @@ -317,7 +278,7 @@ linearize(const Concrete_Expression<Target>& expr, break; case Binary_Operator<Target>::KIND: Binary_Operator<Target> bop_expr = - static_cast<Binary_Operator<Target>>(expr); + static_cast<Binary_Operator<Target> >(expr); switch (bop_expr.get_bop()) { case Binary_Operator<Target>::ADD: return add_linearize(bop_expr, int_store, lf_store, result); @@ -345,7 +306,29 @@ linearize(const Concrete_Expression<Target>& expr, } break; case Approximable_Reference<Target>::KIND: - // TODO. + Approximable_Reference<Target> ref_expr = + static_cast<Approximable_Reference<Target> >(expr); + /* Variable references are the only that we are currently + able to analyze */ + dimension_type variable_index = ref_expr.associated_dimension(); + if (variable_index == not_a_dimension()) + return false; + else { + /* If a linear form associated to the referenced variable + exists in lf_store, return that form. Otherwise, return + the simplest linear form. */ + typename FP_Linear_Form_Abstract_Store::const_iterator + variable_value = lf_store.find(variable_index); + if (variable_value == lf_store.end()) { + result = FP_Linear_Form(Variable(variable_index)); + return true; + } + + result = FP_Linear_Form(variable_value->second); + /* FIXME: do we really need to contemplate the possibility + that an unbounded linear form was saved into lf_store? */ + return !result.overflows(); + } break; case Cast_Operator<Target>::KIND: // TODO.

1 0

[GIT] ppl/ppl(floating_point): Started rewriting the incarnation of concrete expression to be used in PPL tests .
by Roberto Bagnara 25 Jul '10

25 Jul '10

Module: ppl/ppl Branch: floating_point Commit: c28d3f92ad09efc6f2aff83a7bb9857ffa38a392 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c28d3f92ad09… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun Jul 25 18:46:58 2010 +0200 Started rewriting the incarnation of concrete expression to be used in PPL tests. --- src/Concrete_Expression.defs.hh | 10 +- src/Makefile.am | 3 - src/Proxy.defs.hh | 54 --------- src/Proxy.inlines.hh | 54 --------- src/Proxy.types.hh | 28 ----- tests/Concrete_Expression/C_Expr.defs.hh | 163 ++++++++++++++------------- tests/Concrete_Expression/C_Expr.inlines.hh | 40 +++++-- 7 files changed, 120 insertions(+), 232 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=c28d3f92…

1 0

[GIT] ppl/ppl(floating_point): Added some documentation.
by Fabio Bossi 24 Jul '10

24 Jul '10

Module: ppl/ppl Branch: floating_point Commit: f6b9896513010c79ce173a2226b833477690f5ab URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6b989651301… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 24 18:45:38 2010 +0200 Added some documentation. --- src/Float.defs.hh | 16 +++++++++++++ src/Linear_Form.defs.hh | 55 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 0 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index e68c3bd..e484458 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -360,6 +360,22 @@ public: }; #endif +/*! \brief + Computes the absolute error of floating point computations. + + \par Template type parameters + + - The class template parameter \p FP_Interval_Type represents the type + of the intervals used in the abstract domain. The interval bounds + should have a floating point type. + + \param analyzed_format The floating point format used by the analyzed + program. + + \return The interval \f$[-\omega; \omega]\f$ where \f$\omega\f$ is the + smallest non-zero positive number in the less precise floating point + format between the analyzer format and the analyzed format. +*/ template <typename FP_Interval_Type> const FP_Interval_Type& compute_absolute_error( Floating_Point_Format analyzed_format); diff --git a/src/Linear_Form.defs.hh b/src/Linear_Form.defs.hh index ccb4e0f..c8c07ae 100644 --- a/src/Linear_Form.defs.hh +++ b/src/Linear_Form.defs.hh @@ -325,11 +325,66 @@ public: // Floating point analysis related methods. + /*! \brief + Verifies if the linear form overflows. + + \return + Returns <CODE>false</CODE> if all coefficients in \p lf are bounded, + <CODE>true</CODE> otherwise. + + \p T must be the type of possibly unbounded quantities. + */ bool overflows() const; + /*! \brief + Computes the relative error associated to floating point computations + that operate on a quantity that is overapproximated by \p *this. + + \param analyzed_format The floating point format used by the analyzed + program. + \param result Becomes the linear form corresponding to the relative + error committed. + + This method makes <CODE>result</CODE> become a linear form + obtained by evaluating the function \f$\varepsilon_{\mathbf{f}}(l)\f$ + on the linear form. This function is defined as: + \f[ + \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 + \f] + where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and + \f$\beta\f$ the base. + + The result is undefined if \p T is not the type of an interval with + floating point boundaries. + */ void relative_error(Floating_Point_Format analyzed_format, Linear_Form& result) const; + /*! \brief + Makes \p result become an interval that overapproximates all the + possible values of \p *this in the interval abstract store \p store. + + \param store The abstract store. + \param result The linear form that will store the result. + + This method makes <CODE>result</CODE> become + \f$\iota(lf)\rho^{\#}\f$, that is an interval defined as: + \f[ + \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) + \f] + + The result is undefined if \p T is not the type of an interval with + floating point boundaries. + */ void intervalize(const Box<C>& store, C& result) const; private:

1 0