- PPL-devel - BUGSENG Mailman

[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

[GIT] ppl/ppl(floating_point): Fixed operator names.
by Fabio Bossi 24 Jul '10

24 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 74620fd8c5d3cf65eb8503a5825bb196fe0d9cb1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=74620fd8c5d3… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 24 17:44:00 2010 +0200 Fixed operator names. --- tests/Concrete_Expression/C_Expr.defs.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index 05c2311..93c5dac 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -61,9 +61,9 @@ public: //! Returns the right-hand side of \p *this. const C_Expr* right_hand_side() const; - static const Concrete_Expression_BOP PLUS = 0; - static const Concrete_Expression_BOP MINUS = 1; - static const Concrete_Expression_BOP TIMES = 2; + static const Concrete_Expression_BOP ADD = 0; + static const Concrete_Expression_BOP SUB = 1; + static const Concrete_Expression_BOP MUL = 2; static const Concrete_Expression_BOP DIV = 3; static const Concrete_Expression_BOP REM = 4; static const Concrete_Expression_BOP BAND = 5;

1 0

[GIT] ppl/ppl(floating_point): Small improvement in bnot_linearize.
by Fabio Bossi 24 Jul '10

24 Jul '10

Module: ppl/ppl Branch: floating_point Commit: f4d76853831054292145b3d7f4c327e925f6af51 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f4d768538310… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 24 16:37:28 2010 +0200 Small improvement in bnot_linearize. --- src/linearize.hh | 4 +++- 1 files changed, 3 insertions(+), 1 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index ca40451..681e846 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -65,7 +65,9 @@ bnot_linearize(const Unary_Operator<Target>& uop_expr, } else // Here int_r strictly contains 0. - return false; + result = FP_Interval_Type(0); + result.join_assign(1); + return true; } template <typename Target, typename FP_Interval_Type>

1 0

[GIT] ppl/ppl(floating_point): Some progress with the linearization algorithm.
by Fabio Bossi 24 Jul '10

24 Jul '10

Module: ppl/ppl Branch: floating_point Commit: eee4fc2395d61a069a73f388ab68b3c6cf9173dd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=eee4fc2395d6… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 24 16:09:40 2010 +0200 Some progress with the linearization algorithm. --- src/linearize.hh | 246 ++++++++++++++++++++++++++++++++++++++++++++++++----- 1 files changed, 222 insertions(+), 24 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=eee4fc23…

1 0

[GIT] ppl/ppl(floating_point): Added a skeleton for the new linearization function.
by Fabio Bossi 24 Jul '10

24 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 1c4c91c248d74dc5abb8c5b45507dfe9665ff6b5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1c4c91c248d7… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Jul 24 12:39:51 2010 +0200 Added a skeleton for the new linearization function. Also added an idea for the linearization of the unary negation expression. --- src/linearize.hh | 160 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 160 insertions(+), 0 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh new file mode 100644 index 0000000..6a39f03 --- /dev/null +++ b/src/linearize.hh @@ -0,0 +1,160 @@ +1/* Linearization function implementation. + Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#ifndef PPL_linearize_hh +#define PPL_linearize_hh 1 + +#include "Concrete_Expression.defs.hh" +#include "Float.defs.hh" +#include "Linear_Form.defs.hh" +#include "Box.defs.hh" +#include <map> + +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) { + 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. + return false; +} + +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, + Linear_Form<FP_Interval_Type>& result) { + 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; + + // Check that analyzer_format is a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<analyzer_format>::is_exact, + "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()); + + /* + Floating_Point_Format analyzed_format = expr.floating_point_format(); + FP_Interval_Type absolute_error = + compute_absolute_error<FP_Interval_Type>(analyzed_format); + */ + switch(expr.kind()) { + case INT_CON: + // TODO. + break; + case FP_CON: + Floating_Point_Constant<Target> fpc_expr = + static_cast<Floating_Point_Constant<Target>>(expr); + result = FP_Linear_Form(FP_Interval(fpc_expr.get_value_as_string())); + return true; + break; + case UOP: + Unary_Operator<Target> uop_expr = + static_cast<Unary_Operator<Target>>(expr); + switch (uop_expr.get_uop()) { + case PLUS: + return linearize(uop_expr.get_arg(), int_store, lf_store, result); + break; + case MINUS: + if (!linearize(uop_expr.get_arg(), int_store, lf_store, result)) + return false; + + result.negate(); + return true; + break; + case BNOT: + return bnot_linearize(uop_expr, int_store, lf_store, result); + break; + default: + throw std::runtime_error("PPL internal error"); + } + break; + case BOP: + Binary_Operator<Target> bop_expr = + static_cast<Binary_Operator<Target>>(expr); + switch (bop_expr.get_bop()) { + case ADD: + return add_linearize(bop_expr, int_store, lf_store, result); + break; + case SUB: + return sub_linearize(bop_expr, int_store, lf_store, result); + break; + case MUL: + return mul_linearize(bop_expr, int_store, lf_store, result); + break; + case DIV: + return div_linearize(bop_expr, int_store, lf_store, result); + break; + case REM: + case BAND: + case BOR: + case BXOR: + case LSHIFT: + case RSHIFT: + default: + throw std::runtime_error("PPL internal error"); + } + break; + case CAST: + // TODO. + break; + default: + throw std::runtime_error("PPL internal error"); + } +} + +} // namespace Parma_Polyhedra_Library + +#endif // !defined(PPL_linearize_hh)

2 1

[GIT] ppl/ppl(floating_point): Added a few trivial tests.
by Fabio Bossi 23 Jul '10

23 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 2af7d3f9cb5283ce313f38d9d217d881ea53a3dd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2af7d3f9cb52… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 23 13:50:13 2010 +0200 Added a few trivial tests. --- tests/Concrete_Expression/Makefile.am | 7 +++- tests/Concrete_Expression/float.cc | 44 ++++++++++++++++++++++++++++++ tests/Concrete_Expression/linearform1.cc | 34 +++++++++++++++++++++++ 3 files changed, 83 insertions(+), 2 deletions(-) diff --git a/tests/Concrete_Expression/Makefile.am b/tests/Concrete_Expression/Makefile.am index c433cad..015f0f8 100644 --- a/tests/Concrete_Expression/Makefile.am +++ b/tests/Concrete_Expression/Makefile.am @@ -51,12 +51,13 @@ $(top_builddir)/src/libppl.la \ @extra_libraries@ ORIGINAL_TESTS = \ -C_Expr +C_Expr \ +float \ +linearform1 #bdshape1 \ #bdshape2 \ #digitalfilters1 \ #floatingpointexpr1 \ -#linearform1 \ #octagonalshape1 \ #octagonalshape2 \ #polyhedron1 \ @@ -138,6 +139,8 @@ bdshape2_SOURCES = bdshape2.cc digitalfilters1_SOURCES = digitalfilters1.cc +float_SOURCES = float.cc + floatingpointexpr1_SOURCES = floatingpointexpr1.cc linearform1_SOURCES = linearform1.cc diff --git a/tests/Concrete_Expression/float.cc b/tests/Concrete_Expression/float.cc new file mode 100644 index 0000000..28f8d78 --- /dev/null +++ b/tests/Concrete_Expression/float.cc @@ -0,0 +1,44 @@ +/* Test function compute_absolute_error. + Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" + +namespace { + +using namespace Parma_Polyhedra_Library::IO_Operators; + +bool +test01() { + std::cout << compute_absolute_error<FP_Interval>(IEEE754_HALF) << + std::endl; + + std::cout << compute_absolute_error<FP_Interval>(IEEE754_HALF) << + std::endl; + + return 1; +} + +} + +BEGIN_MAIN + DO_TEST(test01); +END_MAIN diff --git a/tests/Concrete_Expression/linearform1.cc b/tests/Concrete_Expression/linearform1.cc index 63b828c..5f532dd 100644 --- a/tests/Concrete_Expression/linearform1.cc +++ b/tests/Concrete_Expression/linearform1.cc @@ -21,6 +21,7 @@ For the most up-to-date information see the Parma Polyhedra Library site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" +#include <limits> namespace { @@ -291,6 +292,37 @@ test08() { return ok1 && ok2 && ok3 && ok4 && ok5 && ok6; } +bool +test09() { + Variable A(0); + FP_Linear_Form f; + bool ok1 = !f.overflows(); + f += A; + bool ok2 = !f.overflows(); + FP_Interval max(std::numeric_limits<ANALYZER_FP_FORMAT>::max()); + f *= max; + f *= max; + bool ok3 = f.overflows(); + return ok1 && ok2 && ok3; +} + +bool +test10() { + Variable A(0); + FP_Linear_Form f; + FP_Interval_Abstract_Store s(2); + FP_Interval i(2.0); + f += i; + f += A; + s.set_interval(A, i); + FP_Interval result; + f.intervalize(s, result); + FP_Interval known_result = i+i; + nout << "Result: " << result << std::endl; + nout << "Known result: " << known_result << std::endl; + return result == known_result; +} + } // namespace BEGIN_MAIN @@ -302,4 +334,6 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); + DO_TEST(test10); END_MAIN

1 0