June 2012 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(ppl-1_0-branch): New commits
by Roberto Bagnara 29 Jun '12

29 Jun '12

URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ae7b3951caad… Merge: 734d8127c33feaf13a2125c403dfc229c700cf09 3349ebad2d6197b22f4453e61f40ea5782bdf3e5 Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:45:34 2012 +0200 Merge branch 'master' into ppl-1_0-branch URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3349ebad2d61… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:36:58 2012 +0200 Use std::floor() and std::frexp() instead of floorl() and frexpl(), respectively. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=70012d3f48c6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b53a49d3837… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88b390acbeb6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:20:36 2012 +0200 Spurious blank line removed. URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c8e7c38d59d1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:19:30 2012 +0200 Added AmatoPS12.

1 0

[GIT] ppl/ppl(master): Use std::floor() and std::frexp() instead of floorl( ) and frexpl(), respectively.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 3349ebad2d6197b22f4453e61f40ea5782bdf3e5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3349ebad2d61… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 14:36:58 2012 +0200 Use std::floor() and std::frexp() instead of floorl() and frexpl(), respectively. --- src/checked_float.inlines.hh | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/checked_float.inlines.hh b/src/checked_float.inlines.hh index 42fd370..254e8c4 100644 --- a/src/checked_float.inlines.hh +++ b/src/checked_float.inlines.hh @@ -25,9 +25,7 @@ site: http://bugseng.com/products/ppl/ . */ #define PPL_checked_float_inlines_hh 1 #include "compiler.hh" -#ifndef __alpha #include <cmath> -#endif namespace Parma_Polyhedra_Library { @@ -1009,7 +1007,7 @@ assign_mpq_numeric_float(mpq_class& to, const long double from) { mpz_class& num = to.get_num(); mpz_class& den = to.get_den(); int exp; - long double n = frexpl(from, &exp); + long double n = std::frexp(from, &exp); bool neg = false; if (n < 0) { neg = true; @@ -1020,7 +1018,7 @@ assign_mpq_numeric_float(mpq_class& to, const long double from) { while (true) { n *= mult; exp -= bits; - long double intpart = floorl(n); + long double intpart = std::floor(n); num += (unsigned long)intpart; n -= intpart; if (n == 0)

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 734d8127c33feaf13a2125c403dfc229c700cf09 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=734d8127c33f… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. --- doc/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/Makefile.am b/doc/Makefile.am index 9cde930..2fd6802 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -72,7 +72,7 @@ gpl.dox \ fdl.dox # NOTE: this variable is used to populate Doxygen configuration tag INPUT. -# The file path is that of the build directory, hence we ca not use +# The file path is that of the build directory, hence we cannot use # variable DOX_LICENSE_FILES defined above. DOX_LICENSE_INPUT = \ $(srcdir)/gpl.dox \

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 78dcbda0b861c2280a6598ed04b34be992538062 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=78dcbda0b861… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 712dab4..51b2cff 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2191,7 +2191,7 @@ Summarizing: Title = "Software Model Checking", Journal = "ACM Computing Surveys", Volume = 41, - Nnumber = 4, + Number = 4, Year = 2009, Pages = "1--54", Publisher = "ACM Press",

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Spurious blank line removed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 1f4ca8be811bbc60056b0ddb38129f21587b513a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1f4ca8be811b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:20:36 2012 +0200 Spurious blank line removed. --- doc/ppl_citations.bib | 1 - 1 files changed, 0 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 2e081fb..712dab4 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -304,7 +304,6 @@ Summarizing: programs and show some experimental evaluations." } - @Inproceedings{AmatoS12, Author = "G. Amato and F. Scozzari", Title = "Random: R-Based Analyzer for Numerical Domains",

1 0

[GIT] ppl/ppl(ppl-1_0-branch): Added AmatoPS12.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: ppl-1_0-branch Commit: 4bb66427092501c8c9fd641c0ae58ffd1370c186 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4bb664270925… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Thu Jun 28 14:19:30 2012 +0200 Added AmatoPS12. --- doc/ppl_citations.bib | 20 ++++++++++++++++++++ 1 files changed, 20 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 0e8e854..2e081fb 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -285,6 +285,26 @@ Summarizing: programs." } +@Article{AmatoPS12, + Author = "G. Amato and M. Parton and F. Scozzari", + Title = "Discovering Invariants via Simple Component Analysis", + Journal = "Journal of Symbolic Computation", + Volume = 47, + Number = 12, + Year = 2012, + Pages = "1533--1560", + Abstract = "We propose a new technique combining dynamic and static + analysis of programs to find linear invariants. We use a + statistical tool, called simple component analysis, to + analyze partial execution traces of a given program. We + get a new coordinate system in the vector space of + program variables, which is used to specialize numerical + abstract domains. As an application, we instantiate our + technique to interval analysis of simple imperative + programs and show some experimental evaluations." +} + + @Inproceedings{AmatoS12, Author = "G. Amato and F. Scozzari", Title = "Random: R-Based Analyzer for Numerical Domains",

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 70012d3f48c6aee21fd8e82617f70141461926fe URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=70012d3f48c6… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:02:33 2012 +0200 Typo fixed. --- doc/Makefile.am | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/Makefile.am b/doc/Makefile.am index 9cde930..2fd6802 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -72,7 +72,7 @@ gpl.dox \ fdl.dox # NOTE: this variable is used to populate Doxygen configuration tag INPUT. -# The file path is that of the build directory, hence we ca not use +# The file path is that of the build directory, hence we cannot use # variable DOX_LICENSE_FILES defined above. DOX_LICENSE_INPUT = \ $(srcdir)/gpl.dox \

1 0

[GIT] ppl/ppl(master): Typo fixed.
by Roberto Bagnara 29 Jun '12

29 Jun '12

Module: ppl/ppl Branch: master Commit: 2b53a49d3837c63dedad3ec660305c844b9d1e88 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2b53a49d3837… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Jun 29 10:01:54 2012 +0200 Typo fixed. --- doc/ppl_citations.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 712dab4..51b2cff 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2191,7 +2191,7 @@ Summarizing: Title = "Software Model Checking", Journal = "ACM Computing Surveys", Volume = 41, - Nnumber = 4, + Number = 4, Year = 2009, Pages = "1--54", Publisher = "ACM Press",

1 0

Accessing constraint systems from Java
by Gianluca Amato 29 Jun '12

29 Jun '12

Hi there! I am trying to write a method in Java, which takes a PPL object (let's say a Polyhedron, or an Octagonal_Shape), a sequence of strings as variables names, and generates a string representation of the object similar to the one we obtain with the toString() method, but with the given variable names instead of A, B, etc... My idea was to get a Constraint_System from the object, iterate over Constraints, and access the coefficients of each constraint. However, the Java API is much simpler then the C++ API, and there is no way, for example, to iterate over constraints. For the moment, I am generating a string representation with toString, and apply there the necessary transformations. Do you have any idea how can I circumvent in other ways the limitations of the API? Any plan for a better Java API? Thanks in advance, --gianluca

2 1

Parma Polyhedra Library 1.0
by Roberto Bagnara 28 Jun '12

28 Jun '12

The core development team is very pleased to announce the availability of PPL 1.0, a new release of the Parma Polyhedra Library. This release includes support for the optimized representation of sparse vectors of coefficients, achieving significant performance improvements, e.g., when dealing with constraint systems describing weakly relational abstractions such as boxes and octagonal shapes. The precise list of user-visible changes is below. For more information, please come and visit the new PPL web site at http://bugseng.com/products/ppl On behalf of all the past and present developers listed at http://bugseng.com/products/ppl/credits and in the file CREDITS, Roberto Bagnara Patricia M. Hill Enea Zaffanella Abramo Bagnara BUGSENG srl (http://bugseng.com) -------------------------------------------------------------------------- NEWS for version 1.0 (released on June 28, 2012) -------------------------------------------------------------------------- New and Changed Features ======================== o Significant improvements have been obtained in both time and space resource usage by the definition of data structures and algorithms for the case of "sparse rows", i.e., sequences of coefficients where most of the values are zero. o The library fully supports two different representations for rows: the "dense" representation is an array-like representation tailored to sequences having most of their coefficients different from zero; the "sparse" representation saves memory space (as well as CPU cycles) when most of the coefficients in the sequence are zero. o A generic interface allows for a seamless interaction between the dense and the sparse row representation. Most library entities (linear expressions, constraints, generators, congruences, and their systems) can be built using either representation, specified as a constructor's argument. o As a by-product of this sparse/dense refactoring work, efficiency improvements have been obtained even for those computations that are still based on the dense row representation. o Reasonable default values for the row representation are provided for each library entity, automatically leading to significant memory space savings even in old client/library code, e.g., when dealing with constraint systems describing weakly relational abstractions such as boxes and octagonal shapes. o If desired, these default values can be customized to user's needs by changing just a few lines of library code. For instance, the constraint systems stored inside C_Polyhedron and NNC_Polyhedron objects can be made to use the sparse representation by just changing the following line in Polyhedron.defs.hh: static const Representation default_con_sys_repr = DENSE; to become static const Representation default_con_sys_repr = SPARSE; Bugfixes ======== o Fixed a bug affecting methods bool BD_Shape<T>::contains(const BD_Shape& y) const; bool Octagonal_Shape<T>::contains(const Octagonal_Shape& y) const; whereby the wrong result was obtained when *this is an empty weakly-relational shape and y is not empty. o Fixed a bug affecting the PIP solver whereby a wrong result could have been obtained if the input constraint system contained multiple linear equality constraints. -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com

1 0