July 2010 - PPL-devel - BUGSENG Mailman

[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

[GIT] ppl/ppl(floating_point): Added missing inline specifier.
by Fabio Bossi 23 Jul '10

23 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 9c9c1ff2fef76d9dd8fbf669cf96c349794f9df5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9c9c1ff2fef7… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 23 11:30:13 2010 +0200 Added missing inline specifier. Make check now works. --- src/Concrete_Expression.inlines.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Concrete_Expression.inlines.hh b/src/Concrete_Expression.inlines.hh index 3c9cd1e..c812919 100644 --- a/src/Concrete_Expression.inlines.hh +++ b/src/Concrete_Expression.inlines.hh @@ -73,7 +73,7 @@ Concrete_Expression_Type::bounded_integer_type_width() const { return impl.bounded_integer_type_width; } -Bounded_Integer_Type_Representation +inline Bounded_Integer_Type_Representation Concrete_Expression_Type::bounded_integer_type_representation() const { return impl.bounded_integer_type_representation; }

1 0

[GIT] ppl/ppl(floating_point): Avoid a cyclic dependency problem ( make check still doesn't work).
by Fabio Bossi 23 Jul '10

23 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 0db84c97d57aa3eb8324d5b9113ca8393efa65f3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0db84c97d57a… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Jul 23 11:15:56 2010 +0200 Avoid a cyclic dependency problem (make check still doesn't work). --- src/Linear_Form.defs.hh | 2 +- src/Linear_Form.templates.hh | 1 + 2 files changed, 2 insertions(+), 1 deletions(-) diff --git a/src/Linear_Form.defs.hh b/src/Linear_Form.defs.hh index f7ed492..ccb4e0f 100644 --- a/src/Linear_Form.defs.hh +++ b/src/Linear_Form.defs.hh @@ -428,6 +428,6 @@ private: }; #include "Linear_Form.inlines.hh" -#include "Linear_Form.templates.hh" +// Linear_Form.templates.hh is not included here on purpose. #endif // !defined(PPL_Linear_Form_defs_hh) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index f676626..e508759 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -23,6 +23,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #ifndef PPL_Linear_Form_templates_hh #define PPL_Linear_Form_templates_hh 1 +#include "Linear_Form.defs.hh" #include "Linear_Expression.defs.hh" #include "Box.defs.hh" #include <stdexcept>

1 0

[GIT] ppl/ppl(floating_point): Restored inclusion of Polyhedron.defs. hh to allow
by Fabio Bossi 22 Jul '10

22 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 608cd868519a4b228aea86441b5bb25d0ee4fcf5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=608cd868519a… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Jul 22 15:31:36 2010 +0200 Restored inclusion of Polyhedron.defs.hh to allow compilation of Grid_public.cc. --- src/Grid.defs.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Grid.defs.hh b/src/Grid.defs.hh index bf4e617..4ee26be 100644 --- a/src/Grid.defs.hh +++ b/src/Grid.defs.hh @@ -40,7 +40,7 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Poly_Gen_Relation.defs.hh" #include "Grid_Certificate.types.hh" #include "Box.types.hh" -#include "Polyhedron.types.hh" +#include "Polyhedron.defs.hh" #include "BD_Shape.types.hh" #include "Octagonal_Shape.types.hh" #include <vector>

1 0

[GIT] ppl/ppl(floating_point): Added a FIXME note.
by Fabio Bossi 22 Jul '10

22 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 1e5b8d148576252e05021bfaf76a14e14416f8c0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1e5b8d148576… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Jul 22 12:18:02 2010 +0200 Added a FIXME note. --- src/Float.templates.hh | 1 + 1 files changed, 1 insertions(+), 0 deletions(-) diff --git a/src/Float.templates.hh b/src/Float.templates.hh index ab93c35..e5bf852 100644 --- a/src/Float.templates.hh +++ b/src/Float.templates.hh @@ -33,6 +33,7 @@ const FP_Interval_Type& compute_absolute_error( const Floating_Point_Format analyzed_format) { typedef typename FP_Interval_Type::boundary_type analyzer_format; + // FIXME: check if initializing caches with EMPTY is better. static const FP_Interval_Type ZERO_INTERVAL = FP_Interval_Type(0); // Cached results for each different analyzed format. static FP_Interval_Type ieee754_half_result = ZERO_INTERVAL;

1 0

[GIT] ppl/ppl(floating_point): Fixed a typo.
by Fabio Bossi 22 Jul '10

22 Jul '10

Module: ppl/ppl Branch: floating_point Commit: 36c398be7c32598e44f067236ad2aa040a927265 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=36c398be7c32… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Thu Jul 22 11:52:09 2010 +0200 Fixed a typo. --- src/Float.templates.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Float.templates.hh b/src/Float.templates.hh index 139a153..ab93c35 100644 --- a/src/Float.templates.hh +++ b/src/Float.templates.hh @@ -21,8 +21,8 @@ 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_Float_Templates_hh -#define PPL_Float_Templates_hh 1 +#ifndef PPL_Float_templates_hh +#define PPL_Float_templates_hh 1 #include <cmath> @@ -121,4 +121,4 @@ const FP_Interval_Type& compute_absolute_error( } // namespace Parma_Polyhedra_Library -#endif // !defined(PPL_Float_Templates_hh) +#endif // !defined(PPL_Float_templates_hh)

1 0