April 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(bounded_arithmetic): New file wrap1. cc will contain tests for method Polyhedron::wrap_assign().
by Roberto Bagnara 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: bounded_arithmetic Commit: 636f1db00bb3ae68ffbcdfbe22bc56c03f9cfdbd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=636f1db00bb3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Apr 21 11:36:33 2009 +0200 New file wrap1.cc will contain tests for method Polyhedron::wrap_assign(). --- tests/Polyhedron/Makefile.am | 7 ++++++ tests/Polyhedron/wrap1.cc | 48 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 55 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index b7994d4..b4162e1 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -132,6 +132,7 @@ topclosure1 \ unconstrain1 \ universe1 universe2 \ variablesset1 \ +wrap1 \ writeconsys1 \ writegensys1 \ writepolyhedron1 writepolyhedron2 \ @@ -203,6 +204,7 @@ nnc_smm1 \ nnc_timeelapse1 \ nnc_unconstrain1 \ nnc_universe1 \ +nnc_wrap1 \ nnc_writepolyhedron1 # @@ -403,6 +405,8 @@ universe2_SOURCES = universe2.cc variablesset1_SOURCES = variablesset1.cc +wrap1_SOURCES = wrap1.cc + writeconsys1_SOURCES = writeconsys1.cc writegensys1_SOURCES = writegensys1.cc @@ -623,6 +627,9 @@ nnc_unconstrain1_CXXFLAGS = $(DERIVED_CXXFLAGS) nnc_universe1_SOURCES = universe1.cc nnc_universe1_CXXFLAGS = $(DERIVED_CXXFLAGS) +nnc_wrap1_SOURCES = wrap1.cc +nnc_wrap1_CXXFLAGS = $(DERIVED_CXXFLAGS) + nnc_writepolyhedron1_SOURCES = writepolyhedron1.cc nnc_writepolyhedron1_CXXFLAGS = $(DERIVED_CXXFLAGS) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc new file mode 100644 index 0000000..dfcb77e --- /dev/null +++ b/tests/Polyhedron/wrap1.cc @@ -0,0 +1,48 @@ +/* Test Polyhedron::wrap_assign(). + Copyright (C) 2001-2009 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 { + +bool +test01() { + // FIXME: to be written. + bool ok = true; + + return ok; +} + +bool +test02() { + // FIXME: to be written. + bool ok = true; + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); +END_MAIN

1 0

[GIT] ppl/ppl(bounded_arithmetic): Added the declaration and a stub implementation of new method
by Roberto Bagnara 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: bounded_arithmetic Commit: 3879ecb87976c3fec4e498b45f75d2424ee98c2e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3879ecb87976… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Apr 21 11:34:24 2009 +0200 Added the declaration and a stub implementation of new method Polyhedron::wrap_assign(). --- src/Polyhedron.defs.hh | 40 ++++++++++++++++++++++++++++++++++++++++ src/Polyhedron_public.cc | 10 ++++++++++ 2 files changed, 50 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 6e4ba7f..0c8f1e9 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -1423,6 +1423,46 @@ public: */ void time_elapse_assign(const Polyhedron& y); + /*! \brief + \ref Wrapping_Operator "Wraps" the specified dimensions of the + vector space. + + \param vars + The set of Variable objects corresponding to the space dimensions + to be wrapped. + + \param w + The width of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param s + The signedness of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param w + The overflow behavior of the bounded integer type corresponding to + all the dimensions to be wrapped. + + \param wrap_individually + <CODE>true</CODE> if the dimensions should be wrapped individually + (something that results in greater efficiency to the detriment of + precision). + + \param k_threshold + A precision parameter of the \ref Wrap_Operator "wrapping operator": + higher values result in possibly improved precision. + + \exception std::invalid_argument + Thrown if \p *this is dimension-incompatible with one of the + Variable objects contained in \p vars. + */ + void wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + bool wrap_individually = true, + unsigned k_threshold = 16); + //! Assigns to \p *this its topological closure. void topological_closure_assign(); diff --git a/src/Polyhedron_public.cc b/src/Polyhedron_public.cc index 5f95530..ea0b69e 100644 --- a/src/Polyhedron_public.cc +++ b/src/Polyhedron_public.cc @@ -3460,6 +3460,16 @@ PPL::Polyhedron::time_elapse_assign(const Polyhedron& y) { } void +PPL::Polyhedron::wrap_assign(const Variables_Set& vars, + Bounded_Integer_Type_Width w, + Bounded_Integer_Type_Signedness s, + Bounded_Integer_Type_Overflow o, + bool wrap_individually, + unsigned k_threshold) { + // FIXME: to be written. +} + +void PPL::Polyhedron::topological_closure_assign() { // Necessarily closed polyhedra are trivially closed. if (is_necessarily_closed())

1 0

[GIT] ppl/ppl(bounded_arithmetic): New enumerations Bounded_Integer_Type_Width, Bounded_Integer_Type_Signedness
by Roberto Bagnara 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: bounded_arithmetic Commit: 3f568dac0119fa57aea5fa923f43f80b7d0f04f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f568dac0119… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Apr 21 11:33:15 2009 +0200 New enumerations Bounded_Integer_Type_Width, Bounded_Integer_Type_Signedness and Bounded_Integer_Type_Overflow to encode the width, signedness and overflow behavior of bounded integer types, respectively. --- src/globals.types.hh | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 65 insertions(+), 0 deletions(-) diff --git a/src/globals.types.hh b/src/globals.types.hh index fe3545a..03a70bc 100644 --- a/src/globals.types.hh +++ b/src/globals.types.hh @@ -70,6 +70,71 @@ enum Optimization_Mode { MAXIMIZATION }; +//! Widths of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Width { + //! \hideinitializer 8 bits. + BITS_8 = 8, + + //! \hideinitializer 16 bits. + BITS_16 = 16, + + //! \hideinitializer 32 bits. + BITS_32 = 32, + + //! \hideinitializer 64 bits. + BITS_64 = 64, + + //! \hideinitializer 128 bits. + BITS_128 = 128, +}; + +//! Signedness of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Signedness { + //! Unsigned integer. + UNSIGNED, + + //! Signed integer represented by the two's complement of the absolute value. + SIGNED_2_COMPLEMENT +}; + +//! Overflow behavior of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Overflow { + /*! \brief + On overflow, wrapping takes place. + + FIXME: formally specify what "wrapping takes place" means. + */ + OVERFLOW_WRAPS, + + /*! \brief + On overflow, the result is undefined. + + This simply means that the result of the operation resulting in an + overflow can take any value. + + \note + Even though something more serious can happen in the system + being analyzed ---due to, e.g., C's undefined behavior---, here we + are only concerned with the results of arithmetic operations. + It is the responsibility of the analyzer to ensure that other + manifestations of undefined behavior are conservatively approximated. + */ + OVERFLOW_UNDEFINED, + + /*! \brief + Overflow is impossible. + + This is for the analysis of languages where overflow is trapped + before it affects the state, for which, thus, any indication that + an overflow may have affected the state is necessarily due to + the imprecision of the analysis. + */ + OVERFLOW_IMPOSSIBLE +}; + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_globals_types_hh)

1 0

[GIT] ppl/ppl(bounded_arithmetic): Corrected silly typo in compile-time check.
by Enea Zaffanella 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: bounded_arithmetic Commit: cd10d9cbc12869eb3f2c1538cf466a9dd0f715af URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cd10d9cbc128… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 21 09:08:45 2009 +0200 Corrected silly typo in compile-time check. --- src/BD_Shape.templates.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index e6cda70..042eb59 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -2077,8 +2077,8 @@ template <typename T> template <bool integer_upper_bound> bool BD_Shape<T>::BHZ09_upper_bound_assign_if_exact(const BD_Shape& y) { - PPL_COMPILE_TIME_CHECK(not (integer_upper_bound - && std::numeric_limits<T>::is_integer), + PPL_COMPILE_TIME_CHECK(!integer_upper_bound + || std::numeric_limits<T>::is_integer, "BD_Shape<T>::BHZ09_upper_bound_assign_if_exact(y):" " instantiating for integer upper bound," " but T in not an integer datatype.");

1 0

Re: [PPL-devel] GMP 4.3.0 released
by Roberto Bagnara 21 Apr '09

21 Apr '09

Torbjorn Granlund wrote: > It is my great pleasure to announce the availability a new major release of > the GNU Multiple Precision Arithmetic Library (GMP). The new release is > identified as 4.3.0. Hi Torbjorn, congratulations and thank you for the new release. > Speedups: > * Vastly improved assembly code for x86-64 processors from AMD and Intel. I have run a couple of application programs based on the Parma Polyhedra Library (PPL), which heavily depends on GMP. On an AMD Opteron 2384 "Shanghai" I got the following running times (best run out of 10): Application A Application B GMP 4.2.4 GMP 4.3.0 GMP 4.2.4 GMP 4.3.0 238 s 187 s 34.2 s 34.8 s On an Intel Core2 Q9400, instead, I got: Application A Application B GMP 4.2.4 GMP 4.3.0 GMP 4.2.4 GMP 4.3.0 339 s 213 s 29.8 s 28.9 s > Misc: > * The gmp_version variable now always contains three parts. For this > release, it is "4.3.0". Aaargh! This broke our GMP detection procedure. Moreover, PPL 0.10.1 was released only a few hours before the release of GMP 4.3.0. I guess now we have no choice but release PPL 0.10.2 with a revised GMP detection procedure. Was a release candidate made available and announced somewhere? If so, I would like to subscribe the list for this kind of announcements. Thanks again, Roberto -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

2 2

[GIT] ppl/ppl(master): Corrected silly typo in compile-time check.
by Enea Zaffanella 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: master Commit: cd10d9cbc12869eb3f2c1538cf466a9dd0f715af URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cd10d9cbc128… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Tue Apr 21 09:08:45 2009 +0200 Corrected silly typo in compile-time check. --- src/BD_Shape.templates.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index e6cda70..042eb59 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -2077,8 +2077,8 @@ template <typename T> template <bool integer_upper_bound> bool BD_Shape<T>::BHZ09_upper_bound_assign_if_exact(const BD_Shape& y) { - PPL_COMPILE_TIME_CHECK(not (integer_upper_bound - && std::numeric_limits<T>::is_integer), + PPL_COMPILE_TIME_CHECK(!integer_upper_bound + || std::numeric_limits<T>::is_integer, "BD_Shape<T>::BHZ09_upper_bound_assign_if_exact(y):" " instantiating for integer upper bound," " but T in not an integer datatype.");

1 0

[GIT] ppl/ppl(master): Typos fixed.
by Roberto Bagnara 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: master Commit: 8b5167c49d1ea70388b3340cd16d3b6a1d895c29 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8b5167c49d1e… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Apr 21 08:21:15 2009 +0200 Typos fixed. --- src/Bit_Row.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Bit_Row.cc b/src/Bit_Row.cc index 1983f21..c784d0a 100644 --- a/src/Bit_Row.cc +++ b/src/Bit_Row.cc @@ -310,8 +310,8 @@ void PPL::Bit_Row::union_helper(const Bit_Row& y, const Bit_Row& z) { mp_size_t y_size = y.vec->_mp_size; mp_size_t z_size = z.vec->_mp_size; - assert(y_size <= z.size); - assert(vec->_mp_alloc >= z.size); + assert(y_size <= z_size); + assert(vec->_mp_alloc >= z_size); vec->_mp_size = z_size; mp_srcptr yp = y.vec->_mp_d; mp_srcptr zp = z.vec->_mp_d;

1 0

[GIT] ppl/ppl(master): Typos fixed.
by Roberto Bagnara 21 Apr '09

21 Apr '09

Module: ppl/ppl Branch: master Commit: ac1770aa59f14266f2c6e712d529b09cd583e11f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ac1770aa59f1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Apr 21 08:07:47 2009 +0200 Typos fixed. --- src/Bit_Row.inlines.hh | 8 ++++---- 1 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Bit_Row.inlines.hh b/src/Bit_Row.inlines.hh index 2ad8a19..e262777 100644 --- a/src/Bit_Row.inlines.hh +++ b/src/Bit_Row.inlines.hh @@ -52,12 +52,12 @@ Bit_Row::Bit_Row(const Bit_Row& y, const Bit_Row& z) { const mp_size_t y_size = y.vec->_mp_size; const mp_size_t z_size = z.vec->_mp_size; if (y_size < z_size) { - assert(z_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIB); + assert(z_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIMB); mpz_init2(vec, z_size * PPL_BITS_PER_GMP_LIMB); union_helper(y, z); } else { - assert(y_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIB); + assert(y_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIMB); mpz_init2(vec, y_size * PPL_BITS_PER_GMP_LIMB); union_helper(z, y); } @@ -127,12 +127,12 @@ set_union(const Bit_Row& x, const Bit_Row& y, Bit_Row& z) { const mp_size_t x_size = x.vec->_mp_size; const mp_size_t y_size = y.vec->_mp_size; if (x_size < y_size) { - assert(y_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIB); + assert(y_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIMB); mpz_realloc2(z.vec, y_size * PPL_BITS_PER_GMP_LIMB); z.union_helper(x, y); } else { - assert(x_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIB); + assert(x_size <= ULONG_MAX / PPL_BITS_PER_GMP_LIMB); mpz_realloc2(z.vec, x_size * PPL_BITS_PER_GMP_LIMB); z.union_helper(y, x); }

1 0

[GIT] ppl/ppl(master): Mentioned the speed improvements committed today.
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: c817701410d0653fa368359c9ad9ed54f0536005 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c817701410d0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 22:35:51 2009 +0200 Mentioned the speed improvements committed today. --- NEWS | 6 ++++++ 1 files changed, 6 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index 4c21daa..9b35ac5 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,12 @@ NEWS for version 0.11 (released date to be decided) New and Changed Features ======================== +o Implementation of general (NNC) polyhedra speeded up. + + +New and Changed Features +======================== + Deprecated and removed methods ------------------------------

1 0

[GIT] ppl/ppl(master): Version number bumped.
by Roberto Bagnara 20 Apr '09

20 Apr '09

Module: ppl/ppl Branch: master Commit: e21f9ce03b4f36e9d367fb346ddaf3c68c8fc498 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e21f9ce03b4f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon Apr 20 22:25:50 2009 +0200 Version number bumped. --- README | 38 +++++++++++++++++++------------------- Watchdog/src/Makefile.am | 1 + configure.ac | 2 +- demos/ppl_lcdd/ppl_lcdd.1 | 2 +- demos/ppl_lpsol/ppl_lpsol.1 | 2 +- doc/libppl.3 | 8 ++++---- doc/libppl_c.3 | 16 ++++++++-------- doc/ppl-config.1 | 12 ++++++------ doc/ppl-config_extra_man_text | 10 +++++----- interfaces/C/Makefile.am | 5 +++-- src/Makefile.am | 5 +++-- 11 files changed, 52 insertions(+), 49 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=e21f9ce0…

1 0