September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added Latex macro for abstract division.
by Fabio Biselli 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 26d546f62d36497e70ab0118e67302d46b2072cd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=26d546f62d36… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 8 16:09:33 2009 +0200 Added Latex macro for abstract division. --- doc/ppl.sty | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl.sty b/doc/ppl.sty index 1406cf3..0015104 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -189,6 +189,6 @@ \newcommand*{\aslf}{\boxplus^{\#}_{\mathbf{f}}} \newcommand*{\adlf}{\boxminus^{\#}_{\mathbf{f}}} -%\newcommand*{\adivlf}{\oslash^{\#}_{\mathbf{f}}} +\newcommand*{\adivlf}{\boxslash^{\#}_{\mathbf{f}}} \newcommand*{\amlf}{\boxtimes^{\#}_{\mathbf{f}}}

1 0

[GIT] ppl/ppl(floating_point): Removed useless comments.
by Roberto Amadini 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d6956e262f595f39d49a0050843268547b15d78f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d6956e262f59… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 8 14:08:04 2009 +0200 Removed useless comments. --- .../floatingpointexpr1.cc | 3 --- 1 files changed, 0 insertions(+), 3 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index d2ac873..4575fdc 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -239,9 +239,6 @@ test06() { float exp = pow(2, -22); fl_r_oc coeff = fl_r_oc(2 - exp); coeff.join_assign(2 + exp); - //fl_r_oc coeff = fl_r_oc(-exp); - //coeff.join_assign(exp); - //coeff += fl_r_oc(2); Float_Interval_Linear_Form known_result = Float_Interval_Linear_Form(Variable(0)); known_result *= coeff;

1 0

[GIT] ppl/ppl(floating_point): Added test for unary minus and multiplication by constant.
by Roberto Amadini 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c508c610981bd3590bb5dec574481e28b24ae865 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c508c610981b… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Tue Sep 8 14:00:38 2009 +0200 Added test for unary minus and multiplication by constant. --- .../floatingpointexpr1.cc | 34 ++++++++++++++++++- 1 files changed, 32 insertions(+), 2 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index a5014b0..d2ac873 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -224,7 +224,7 @@ test05() { bool test06() { sstr store; - fl_r_oc tmp = fl_r_oc(0); + fl_r_oc tmp(0); tmp.join_assign(1); store[0] = tmp; store[1] = fl_r_oc(2); @@ -256,7 +256,7 @@ test06() { bool test07() { ddtr store; - db_r_oc tmp = db_r_oc(0); + db_r_oc tmp(0); tmp.join_assign(1); store[0] = tmp; store[1] = db_r_oc(2); @@ -281,6 +281,35 @@ test07() { return result == known_result; } +// Tests the linearization of [1/4, 1/2] * (-A) where A = [1, 10]. +bool +test08() { + sdtr store; + fl_r_oc tmp(1); + tmp.join_assign(10); + store[0] = tmp; + con_fpesd* con = new con_fpesd(1 / 4.0, 1 / 2.0); + var_fpesd* var0 = new var_fpesd(0); + opp_fpesd* opp = new opp_fpesd(var0); + mul_fpesd mul(con, opp); + Float_Interval_Linear_Form result; + mul.linearize(store, lsdtr(), result); + + Variable A(0); + Float_Interval_Linear_Form known_result = Float_Interval_Linear_Form(A); + float exp = pow(2, -53); + tmp = fl_r_oc(-1 / 2.0 - exp); + tmp.join_assign(-1 / 4.0 + exp); + known_result *= tmp; + tmp = fl_r_oc(-std::numeric_limits<float>::denorm_min()); + tmp.join_assign(std::numeric_limits<float>::denorm_min()); + known_result += tmp; + + nout << "*** known_result ***" << endl + << known_result << endl; + return result == known_result; +} + } // namespace BEGIN_MAIN @@ -291,4 +320,5 @@ BEGIN_MAIN DO_TEST(test05); DO_TEST(test06); DO_TEST(test07); + DO_TEST(test08); END_MAIN

1 0

[GIT] ppl/ppl(pip): Moved the simplex tableau from PIP_Problem to PIP_Solution_Node.
by François Galea 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: pip Commit: bc85f3ea87bfbafa73d4dee424b33086c7e76ca6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=bc85f3ea87bf… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Sep 8 12:56:49 2009 +0200 Moved the simplex tableau from PIP_Problem to PIP_Solution_Node. --- src/PIP_Problem.cc | 114 +++--------------------------- src/PIP_Problem.defs.hh | 69 +----------------- src/PIP_Problem.inlines.hh | 30 -------- src/PIP_Problem.templates.hh | 3 +- src/PIP_Tree.cc | 140 ++++++++++++++++++++++++++++++++++++ src/PIP_Tree.defs.hh | 161 ++++++++++++++++++++++++++++++++++++++++-- src/PIP_Tree.inlines.hh | 30 ++++++++ 7 files changed, 339 insertions(+), 208 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=bc85f3ea…

1 0

[GIT] ppl/ppl(floating_point): Updated linearization documentation;
by Fabio Biselli 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 58e9e3af70bd3cfeb8e5709c1eeafd5b691b84a2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=58e9e3af70bd… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 8 14:20:01 2009 +0200 Updated linearization documentation; Added formulas to class descriptions; --- doc/ppl.sty | 11 +++++ src/Difference_Floating_Point_Expression.defs.hh | 32 +++++++++++--- src/Division_Floating_Point_Expression.defs.hh | 31 ++++++++++++-- src/Floating_Point_Expression.defs.hh | 44 +++++++++++--------- ...ultiplication_Floating_Point_Expression.defs.hh | 28 +++++++++++-- src/Sum_Floating_Point_Expression.defs.hh | 25 ++++++++--- 6 files changed, 129 insertions(+), 42 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=58e9e3af…

1 0

[GIT] ppl/ppl(floating_point): Fixed documentation
by Fabio Biselli 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1e570d889993548394bae0a46b74d99477961748 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1e570d889993… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 8 12:33:45 2009 +0200 Fixed documentation --- doc/ppl.sty | 5 +++++ src/Floating_Point_Expression.defs.hh | 2 ++ src/Sum_Floating_Point_Expression.defs.hh | 12 +++++++++++- 3 files changed, 18 insertions(+), 1 deletions(-) diff --git a/doc/ppl.sty b/doc/ppl.sty index 7282dc7..b35a373 100644 --- a/doc/ppl.sty +++ b/doc/ppl.sty @@ -176,3 +176,8 @@ \newcommand*{\entailsP}{\entailss{\smallP}} \newcommand*{\NentailsP}{\Nentailss{\smallP}} \newcommand*{\sentailsP}{\sentailss{\smallP}} + + +% Interval floating point arithmetics + +\newcommand*{\asifp}{\oplus^{\#}_{\mathbf{f}}} diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index a3e7b59..079995d 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -103,6 +103,7 @@ public: //! Destructor. virtual ~Floating_Point_Expression(); + //! Linearizes a floating point expression. /*! \brief Makes \p result become a Linear Form that correctly approximates the value of the floating point expression in the given composite @@ -140,6 +141,7 @@ public: */ static bool overflows(const FP_Linear_Form& lf); + //! Computes the relative error of a given linear form. /*! \brief Static helper method that is used by <CODE>linearize</CODE> to account for the relative errors on \p lf. diff --git a/src/Sum_Floating_Point_Expression.defs.hh b/src/Sum_Floating_Point_Expression.defs.hh index fcf1523..0df171c 100644 --- a/src/Sum_Floating_Point_Expression.defs.hh +++ b/src/Sum_Floating_Point_Expression.defs.hh @@ -52,6 +52,16 @@ namespace Parma_Polyhedra_Library { of the intervals used in the abstract domain. - The class template type parameter \p FP_Format represents the format of the floating point variable used in the concrete domain. + + \par Linearizations of floating-point sum expressions + + Let \f$i + \sum_{v \in V}i_{v}v \f$ be a linear form we define an abstract + operator \f$\boxplus^{\#}\f$: + \f[ + $i + \sum_{v \in V}i_{v}v$\boxplus^{\#}$i' + \sum_{v \in V}i'_{v}v$ + = + $i \asifp i'$ + \sum_{v \in V}$i_{v} \asifp i'_{v}$v + \f] */ template <typename FP_Interval_Type, typename FP_Format> class Sum_Floating_Point_Expression @@ -61,7 +71,7 @@ public: /*! \brief Alias for the Linear_Form<FP_Interval_Type> from - Floating_Point_Expression + Floating_Point_Expression. */ typedef typename Floating_Point_Expression<FP_Interval_Type, FP_Format>

1 0

about install PPL under SGI IRIX 6.5
by 陈功 08 Sep '09

08 Sep '09

Hi It always said"checking for the GMP library version 4.1.3 or above... no configure: error: Cannot find GMP version 4.1.3 or higher." and I am sure I have already installed GMP 4.2.4 the attachement is the full log can you help me? thanks

2 3

[GIT] ppl/ppl(floating_point): Notify that open intervals should not be allowed.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f25dd63720cd0b6520bf7f5cfcffa1970928a641 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f25dd63720cd… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 11:49:17 2009 +0200 Notify that open intervals should not be allowed. --- src/Floating_Point_Expression.defs.hh | 3 ++- 1 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index ade7fe8..a3e7b59 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -59,7 +59,8 @@ struct IEEE754_Double { - The class template type 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. + should have a floating point type and open intervals should not be + allowed, otherwise the analysis will not be sound. - The class template type parameter \p FP_Format represents the floating point format used in the concrete domain. This parameter must be a struct which contains \f$3\f$ fields:

1 0

[GIT] ppl/ppl(floating_point): Documentation improved.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f5c91db1d219bb2dff6770b4561e3ee0d1eac985 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f5c91db1d219… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 10:12:24 2009 +0200 Documentation improved. --- src/Floating_Point_Expression.defs.hh | 57 ++++++++++++++++++++++---------- 1 files changed, 39 insertions(+), 18 deletions(-) diff --git a/src/Floating_Point_Expression.defs.hh b/src/Floating_Point_Expression.defs.hh index 68618a6..ade7fe8 100644 --- a/src/Floating_Point_Expression.defs.hh +++ b/src/Floating_Point_Expression.defs.hh @@ -48,9 +48,9 @@ struct IEEE754_Double { static const unsigned short exponent_bias = 1023; }; -//! A floating point expression on a given format +//! A floating point expression on a given format. /*! \ingroup PPL_CXX_Interface - This class offers a generic implemenation of a + This class represents a concrete <EM>floating point expression</EM> of format \f$$\mathbf{f}$\f$, this includes constants, variables of format \f$$\mathbf{f}$\f$, binary and unary arithmetic operators. @@ -58,10 +58,10 @@ struct IEEE754_Double { \par Template type parameters - The class template type parameter \p FP_Interval_Type represents the type - of the intervals used in the abstract domain. Here we assume that the - value has floating point type. - - The class template type parameter \p FP_Format represents the format - of the floating point expression used in the concrete domain. + of the intervals used in the abstract domain. The interval bounds + should have a floating point type. + - The class template type parameter \p FP_Format represents the floating + point format used in the concrete domain. This parameter must be a struct which contains \f$3\f$ fields: -# <CODE>static const unsigned short fraction_bits</CODE> that represents the number of bits of the fraction. @@ -79,25 +79,43 @@ public: typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; //! Alias for a map that associates a variable index to an interval. + /*! + The type a linear form abstract store associating each variable with an + interval that correctly approximates its value. + */ typedef std::map<dimension_type, FP_Interval_Type> FP_Interval_Abstract_Store; //! Alias for a map that associates a variable index to a linear form. + /*! + The type a linear form abstract store associating each variable with a + linear form that correctly approximates its value. + */ typedef std::map<dimension_type, FP_Linear_Form> FP_Linear_Form_Abstract_Store; + //! The floating point format used by the analyzer. typedef typename FP_Interval_Type::boundary_type boundary_type; + //! The interval policy used by \p FP_Interval_Type. typedef typename FP_Interval_Type::info_type info_type; //! Destructor. virtual ~Floating_Point_Expression(); /*! \brief - Modifies a linear form \p result that correctly approximates the - floating point expression in the given abstract store. - \param store The abstract store. + Makes \p result become a Linear Form that correctly approximates the + value of the floating point expression in the given composite + abstract store. + \param int_store The interval abstract store. + \param lf_store The linear form abstract store. \param result The modified linear form. */ + /*! + All variables occuring in the floating point expression MUST have + an associated interval in \p int_store. + If this precondition is not met, calling the method causes an + undefined behavior. + */ virtual void linearize(const FP_Interval_Abstract_Store& int_store, const FP_Linear_Form_Abstract_Store& lf_store, FP_Linear_Form& result) const = 0; @@ -105,32 +123,35 @@ public: //! Absolute error. /*! \brief Initialized by computing the smallest non-zero positive - number in the less precise format between the analyzer and the analyzed - format. + number in the less precise floating point format between the + analyzer format and the analyzed format. */ static boundary_type absolute_error; + + // FIXME: this may not be the best place for them. /*! \brief Verifies if a given linear form overflows. \param lf The linear form to verify. \return - Return <CODE>true</CODE> if is bounded, <CODE>false</CODE> otherwise. - */ // FIXME: this may not be the best place for them. + Returns <CODE>true</CODE> if all coefficients in \p lf are bounded, + <CODE>false</CODE> otherwise. + */ static bool overflows(const FP_Linear_Form& lf); /*! \brief - Modifies the linear form \p result that is used by <CODE>linearize</CODE> + Static helper method that is used by <CODE>linearize</CODE> to account for the relative errors on \p lf. \param lf The linear form used to compute the relative error. - \param result The linear form corresponding to the relative error of - \p lf. + \param result Becomes the linear form corresponding to a relative + error committed on \p lf. */ static void relative_error(const FP_Linear_Form& lf, FP_Linear_Form& result); /*! \brief - Modifies an interval \p result that over approximates the range of - \p lf in the abstract store \p store. + Makes \p result become an interval that overapproximates all the + possible values of \p lf in the interval abstract store \p store. \param lf The linear form to aproximate. \param store The abstract store. \param result The linear form that will be modified.

1 0

[GIT] ppl/ppl(floating_point): Deleted FIXME note.
by Fabio Bossi 08 Sep '09

08 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 90c1a7723fdeb7cda0219d5972b987912f67c042 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=90c1a7723fde… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Sep 8 09:27:12 2009 +0200 Deleted FIXME note. --- .../floatingpointexpr1.cc | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index d4c8fce..a5014b0 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -65,7 +65,6 @@ typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store lsstr; typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr; -//FIXME: Why the analyzed format can't be IEEE754_Double? typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store sdtr; typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr;

1 0