August 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Merge branch 'ppl-0_11-branch'
by Roberto Bagnara 05 Aug '10

05 Aug '10

Module: ppl/ppl Branch: master Commit: be8e13942cefd8f33451f8e66934c6d2847f980d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=be8e13942cef… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Aug 5 09:11:32 2010 +0200 Merge branch 'ppl-0_11-branch' ---

1 0

[GIT] ppl/ppl(master): Avoid using overlapping regular expressions.
by Roberto Bagnara 05 Aug '10

05 Aug '10

Module: ppl/ppl Branch: master Commit: b68f8ff2bde57db64ec4439d8a2592da351742e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b68f8ff2bde5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Aug 5 09:08:44 2010 +0200 Avoid using overlapping regular expressions. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 779209e..6dd13ad 100644 --- a/configure.ac +++ b/configure.ac @@ -1274,7 +1274,7 @@ xno | xnone) enableval=${available_instantiations} fi # Avoid extra blanks. - required_instantiations=`echo "${enableval}" | sed -e 's/[[ ]][[ ]]*/ /g' -e 's/[[ ]]*$[[@<>,]]$[[ ]]*/\1/g' -e 's/>>/> >/g' -e 's/^[[ ]]//g' -e 's/[[ ]]$//g'` + required_instantiations=`echo "${enableval}" | sed -e 's/[[ ]][[ ]]*/ /g' -e 's/[[ ]]*$[[@<>,]]$/\1/g' -e 's/$[[@<>,]]$[[ ]]*/\1/g' -e 's/>>/> >/g' -e 's/^[[ ]]//g' -e 's/[[ ]]$//g'` # Check the specified instantiations for validity. ac_save_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS -I${srcdir}"

1 0

[GIT] ppl/ppl(master): Version number bumped.
by Roberto Bagnara 05 Aug '10

05 Aug '10

Module: ppl/ppl Branch: master Commit: efcba16903e4a2a00111c894763a06053457be67 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=efcba16903e4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Aug 5 09:02:09 2010 +0200 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 1bedb40..779209e 100644 --- a/configure.ac +++ b/configure.ac @@ -23,7 +23,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [0.11pre25], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11.1pre1], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Avoid using overlapping regular expressions .
by Roberto Bagnara 05 Aug '10

05 Aug '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: b68f8ff2bde57db64ec4439d8a2592da351742e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b68f8ff2bde5… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Aug 5 09:08:44 2010 +0200 Avoid using overlapping regular expressions. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 779209e..6dd13ad 100644 --- a/configure.ac +++ b/configure.ac @@ -1274,7 +1274,7 @@ xno | xnone) enableval=${available_instantiations} fi # Avoid extra blanks. - required_instantiations=`echo "${enableval}" | sed -e 's/[[ ]][[ ]]*/ /g' -e 's/[[ ]]*$[[@<>,]]$[[ ]]*/\1/g' -e 's/>>/> >/g' -e 's/^[[ ]]//g' -e 's/[[ ]]$//g'` + required_instantiations=`echo "${enableval}" | sed -e 's/[[ ]][[ ]]*/ /g' -e 's/[[ ]]*$[[@<>,]]$/\1/g' -e 's/$[[@<>,]]$[[ ]]*/\1/g' -e 's/>>/> >/g' -e 's/^[[ ]]//g' -e 's/[[ ]]$//g'` # Check the specified instantiations for validity. ac_save_CPPFLAGS="$CPPFLAGS" CPPFLAGS="$CPPFLAGS -I${srcdir}"

1 0

[GIT] ppl/ppl(ppl-0_11-branch): Version number bumped.
by Roberto Bagnara 05 Aug '10

05 Aug '10

Module: ppl/ppl Branch: ppl-0_11-branch Commit: efcba16903e4a2a00111c894763a06053457be67 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=efcba16903e4… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Aug 5 09:02:09 2010 +0200 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index 1bedb40..779209e 100644 --- a/configure.ac +++ b/configure.ac @@ -23,7 +23,7 @@ # Process this file with Autoconf to produce a configure script. # Every other copy of the package version number gets its value from here. -AC_INIT([the Parma Polyhedra Library], [0.11pre25], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.11.1pre1], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

Re: [PPL-devel] Parma Polyhedra Library 0.11
by Roberto Bagnara 05 Aug '10

05 Aug '10

On 08/04/10 20:58, Jack Howarth wrote: > On Wed, Aug 04, 2010 at 05:43:33PM +0200, Roberto Bagnara wrote: >> The core development team is very pleased to announce the availability >> of PPL 0.11, a new release of the Parma Polyhedra Library. >> >> This release has many new features, some of which developed in strict >> coordination with the people behind GCC/Graphite. The main novelties >> are: >> >> - a class PIP_Problem that provides a Parametric Integer Programming >> problem solver; >> >> - "deterministic" timeout computation facilities; >> >> - support for termination analysis via the automatic synthesis of >> linear ranking functions; >> >> - support for approximating computations involving (bounded) >> machine integers. > > Roberto, > I noticed that this release bumps the actual soversion numbers so > that we have libppl.9.dylib, libpwl.5.dylib and libppl_c.4.dylib rather > than libppl.7.dylib, libpwl.4.dylib and libppl_c.2.dylib from the > 0.10.x releases. Hi Jack, yes, the soversion numbers have been updated as needed (this should not come as a surprise though). > So I assume we now need legacy ppl packages for > the older cloog library builds and will have to bump the soversion > on any newer cloog that builds against ppl 0.11, right? I am not familiar enough with cloog to answer that. What I can do is to recommend the use of PPL 0.11 instead of PPL 0.10.* for the reasons explained in the NEWS file. Cheers, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

Parma Polyhedra Library 0.11
by Roberto Bagnara 04 Aug '10

04 Aug '10

The core development team is very pleased to announce the availability of PPL 0.11, a new release of the Parma Polyhedra Library. This release has many new features, among which: - a class PIP_Problem that provides a Parametric Integer Programming problem solver; - "deterministic" timeout computation facilities; - support for termination analysis via the automatic synthesis of linear ranking functions; - support for approximating computations involving (bounded) machine integers. This release includes several other enhancements, speed improvements and some bug fixes. The precise list of user-visible changes is below. For more information, please come and visit the PPL web site at http://www.cs.unipr.it/ppl/ On behalf of all the past and present developers listed at http://www.cs.unipr.it/ppl/Credits/ and in the file CREDITS, Roberto Bagnara Patricia M. Hill Enea Zaffanella Applied Formal Methods Laboratory Department of Mathematics University of Parma, Italy -------------------------------------------------------------------------- NEWS for version 0.11 (released on August 2, 2010) -------------------------------------------------------------------------- New and Changed Features ======================== o New class PIP_Problem provides a Parametric Integer Programming (PIP) problem solver (mainly based on P. Feautrier's specification). The implementation combines a parametric dual simplex algorithm using exact arithmetic with Gomory's cut generation. o New "deterministic" timeout computation facilities: it is now possible to set computational bounds (on the library calls taking exponential time) that do not depend on the actual elapsed time and hence are independent from the actual computation environment (CPU, operating system, etc.). o New support for termination analysis via the automatic synthesis of linear ranking functions. Given a sound approximation of a loop, the PPL provides methods to decide whether that approximation admits a linear ranking function (possibly obtaining one as a witness for termination) and to compute the space of all such functions. In addition, methods are provided to obtain the space of all linear quasi-ranking functions, for use in conditional termination analysis. o New support for approximating computations involving (bounded) machine integers. A general wrapping operator is provided that is parametric with respect to the set of space dimensions (variables) to be wrapped, the width, representation and overflow behavior of all these variables. An optional constraint system can, when given, improve the precision. o All the PPL semantic objects provide new methods void drop_some_non_integer_points(Complexity_Class) void drop_some_non_integer_points(const Variables_Set&, Complexity_Class) which possibly tighten the object by dropping some points with non-integer coordinates (for the space dimensions corresponding to `vars'), within a certain computational complexity bound. o New Linear_Expression methods bool is_zero() const bool all_homogeneous_terms_are_zero() const return true if and only if `*this' is 0, and if and only if all the homogeneous terms of `*this' are 0, respectively. o New Linear_Expression methods void add_mul_assign(Coefficient_traits::const_reference c, Variable v) void sub_mul_assign(Coefficient_traits::const_reference c, Variable v) assign linear expression *this + c * v (resp., *this - c * v) to *this, while avoiding the allocation of a temporary Linear_Expression. o For the PPL semantic objects, other than the Pointset_Powerset and Partially_Reduced Product, there is a new method: bool frequency(const Linear_Expression& expr, Coefficient& freq_n, Coefficient& freq_d, Coefficient& val_n, Coefficient& val_d) This operator computes both the "frequency" (f = freq_n/freq_d) and a value (v = val_n/val_d) closest to zero so that every point in the object satisfies the congruence (expr %= v) / f. o New reduction operator "Shape_Preserving_Reduction" has been added to the Partially_Reduced_Product abstraction. This operator is aimed at the product of a grid and a shape domain, allowing the bounds of the shape to shrink to touch the points of the grid, such that the new bounds are parallel to the old bounds. o The Java interface has to be explicitly initialized before use by calling static method Parma_Polyhedra_Library.initialize_library(). Initialization makes more explicit the exact point where PPL floating point rounding mode is set; it also allows for the caching of Java classes and field/method IDs, thereby reducing the overhead of native method callbacks. o The C and Java interfaces now support timeout computation facilities. o Implementation of general (C and NNC) polyhedra speeded up. o Implementation of the MIP solver speeded up. o When the PPL has been configured with CPPFLAGS="-DPPL_ARM_CAN_CONTROL_FPU=1", the library initialization procedure checks that the FPU can indeed be controlled and fails if that is not the case. o New configure option --with-gmp-prefix supersedes the (now removed) options --with-libgmp-prefix and --with-libgmpxx-prefix. o New configuration option `--with-gmp-build=DIR' allows to use a non-installed build of GMP in DIR. Deprecated and Removed Methods ============================== o All methods having a name ending in `_and_minimize' (e.g., add_constraints_and_minimize, poly_hull_assign_and_minimize, ...) have been removed (they were deprecated in version 0.10). Bugfixes ======== o Corrected a bug in maximize and mininimize optimization methods of class template Pointset_Powerset, whereby the Boolean value true (indicating successful optimization) was returned for empty powersets. o Corrected a bug in method bool NNC_Polyhedron::poly_hull_assign_if_exact(const NNC_Polyhedron&); whereby some inexact NNC hulls were incorrectly flagged as exact. -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[GIT] ppl/w3ppl(master): Little improvements: Mazzi and Trabucchi are former students.
by Enea Zaffanella 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: c898ecc1e5d35a95ca79936ee12b459e2f81746e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=c898ecc1e5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed Aug 4 14:01:15 2010 +0200 Little improvements: Mazzi and Trabucchi are former students. --- htdocs/Credits/Credits.raw | 12 +++++++----- 1 files changed, 7 insertions(+), 5 deletions(-) diff --git a/htdocs/Credits/Credits.raw b/htdocs/Credits/Credits.raw index 0ee838f..2c84d69 100644 --- a/htdocs/Credits/Credits.raw +++ b/htdocs/Credits/Credits.raw @@ -142,9 +142,9 @@ maintained and improved by the following people: </LI> <LI> Giordano Fracasso - (University of Parma) wrote the initial version - of the support for native and checked integer - coefficients. + (student of the University of Parma) + wrote the initial version of the support for + native and checked integer coefficients. </LI> <LI> Maximiliano Marchesi @@ -154,7 +154,8 @@ maintained and improved by the following people: </LI> <LI> Elena Mazzi - (University of Parma) worked on our implementation + (former student of the University of Parma) + worked on our implementation of bounded differences and octagons. She also participated in the theoretical and practical work concerning widening operators for weakly @@ -192,7 +193,8 @@ maintained and improved by the following people: </LI> <LI> Fabio Trabucchi - (University of Parma) worked on a development + (former student of the University of Parma) + worked on a development branch where he added serializers for all the objects of the PPL. Support for serialization based on Fabio's work, will be available in a

1 0

[GIT] ppl/w3ppl(master): Added a section on exact join detection.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: cd96ace3f3f109fd8da4b1b02a32b2062184950c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=cd96ace3f3… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:59:53 2010 +0200 Added a section on exact join detection. --- htdocs/Documentation/papers.raw | 25 +++++++++++++++++++++++++ 1 files changed, 25 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index 24efded..25418c1 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -198,6 +198,31 @@ and software systems (including the analysis of imperative programs). </TR> </TABLE> +<H3>On Exact Join Detection</H3> + +<TABLE> +<TR valign="top"> +<TD align="right"> +[<A HREF="bibliography#BagnaraHZ10CGTA">BHZ10</A>] +</TD> +<TD> +R. Bagnara, P. M. Hill, and E. Zaffanella. + Exact join detection for convex polyhedra and other numerical + abstractions. + <em>Computational Geometry: Theory and Applications</em>, + 43(5):453-473, 2010. +<BLOCKQUOTE> +Read this paper if you are interested in the theory we developed +for computing the <EM>exact join</EM> predicates provided by +the PPL (exact join detection is the problem of deciding whether +the least upper bound of two or more numerical abstractions is equal +to their set-theoretic union). +</BLOCKQUOTE> +</TD> +</TR> +</TABLE> + + <H3>On the Synthesis of Linear Ranking Functions</H3> <TABLE>

1 0

[GIT] ppl/w3ppl(master): Missing label added.
by Roberto Bagnara 04 Aug '10

04 Aug '10

Module: ppl/w3ppl Branch: master Commit: cadd225c086b58ed038ff25ba0c4d10f55bea374 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=cadd225c08… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Wed Aug 4 14:51:47 2010 +0200 Missing label added. --- htdocs/Documentation/papers.raw | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/htdocs/Documentation/papers.raw b/htdocs/Documentation/papers.raw index bf72d12..24efded 100644 --- a/htdocs/Documentation/papers.raw +++ b/htdocs/Documentation/papers.raw @@ -203,7 +203,7 @@ and software systems (including the analysis of imperative programs). <TR valign="top"> <TD align="right"> -[<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR"></A>] +[<A HREF="http://www.cs.unipr.it/ppl/Documentation/BagnaraMPZ10TR">BMPZ10</A>] </TD> <TD> R. Bagnara, F. Mesnard, A. Pescetti, and E. Zaffanella.

1 0