May 2012 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Fixed a bug affecting method contains() of weakly-relational shapes.
by Enea Zaffanella 23 May '12

23 May '12

Module: ppl/ppl Branch: master Commit: e27c255a163af8d1ca70494be28ccfb22984b7e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e27c255a163a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed May 23 16:25:11 2012 +0200 Fixed a bug affecting method contains() of weakly-relational shapes. --- src/BD_Shape.templates.hh | 18 +++++++++--------- src/Octagonal_Shape.templates.hh | 17 +++++++++-------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index d655cd6..f14bae4 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -596,15 +596,12 @@ BD_Shape<T>::contains(const BD_Shape& y) const { if (x_space_dim != y.space_dimension()) throw_dimension_incompatible("contains(y)", y); - // The zero-dimensional universe shape contains any other - // dimension-compatible shape. - // The zero-dimensional empty shape only contains another - // zero-dimensional empty shape. if (x_space_dim == 0) { - if (!marked_empty()) - return true; - else - return y.marked_empty(); + // The zero-dimensional empty shape only contains another + // zero-dimensional empty shape. + // The zero-dimensional universe shape contains any other + // zero-dimensional shape. + return marked_empty() ? y.marked_empty() : true; } /* @@ -630,11 +627,14 @@ BD_Shape<T>::contains(const BD_Shape& y) const { that containment does hold. */ y.shortest_path_closure_assign(); - // An empty shape is contained in any other dimension-compatible shapes. if (y.marked_empty()) return true; + // If `x' is empty it can not contain `y' (which is not empty). + if (x.is_empty()) + return false; + // `*this' contains `y' if and only if every cell of `dbm' // is greater than or equal to the correspondent one of `y.dbm'. for (dimension_type i = x_space_dim + 1; i-- > 0; ) { diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 705ef69..817c158 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -1133,15 +1133,12 @@ Octagonal_Shape<T>::contains(const Octagonal_Shape& y) const { if (space_dim != y.space_dim) throw_dimension_incompatible("contains(y)", y); - // The zero-dimensional universe octagon contains any other - // dimension-compatible octagon. - // The zero-dimensional empty octagon only contains another - // zero-dimensional empty octagon. if (space_dim == 0) { - if (!marked_empty()) - return true; - else - return y.marked_empty(); + // The zero-dimensional empty octagon only contains another + // zero-dimensional empty octagon. + // The zero-dimensional universe octagon contains any other + // zero-dimensional octagon. + return marked_empty() ? y.marked_empty() : true; } // `y' needs to be transitively closed. @@ -1150,6 +1147,10 @@ Octagonal_Shape<T>::contains(const Octagonal_Shape& y) const { if (y.marked_empty()) return true; + // If `*this' is empty it can not contain `y' (which is not empty). + if (is_empty()) + return false; + // `*this' contains `y' if and only if every element of `*this' // is greater than or equal to the correspondent one of `y'. for (typename OR_Matrix<N>::const_element_iterator

1 0

[GIT] ppl/ppl(master): Added tests showing a bug in method contains() of weakly-relational shapes.
by Enea Zaffanella 23 May '12

23 May '12

Module: ppl/ppl Branch: master Commit: 5e45d91a1e7eec00093fb90902f3394c9b183935 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5e45d91a1e7e… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Wed May 23 16:23:01 2012 +0200 Added tests showing a bug in method contains() of weakly-relational shapes. Method returns a wrong result when the shape is empty and the other argument is not empty. Tests are based on a bug report from Gianluca Amato. --- tests/BD_Shape/contains1.cc | 19 +++++++++++++++++++ tests/Octagonal_Shape/contains1.cc | 29 ++++++++++++++++++++++++++--- 2 files changed, 45 insertions(+), 3 deletions(-) diff --git a/tests/BD_Shape/contains1.cc b/tests/BD_Shape/contains1.cc index 36e2c4f..e434d97 100644 --- a/tests/BD_Shape/contains1.cc +++ b/tests/BD_Shape/contains1.cc @@ -172,6 +172,24 @@ test06() { return !contained; } +bool +test07() { + TBD_Shape bds1(3, EMPTY); + + print_constraints(bds1, "*** bds1 ***"); + + TBD_Shape bds2(3, UNIVERSE); + + print_constraints(bds2, "*** bds2 ***"); + + bool contained = bds1.contains(bds2); + + nout << "*** bds1.contains(bds2) ***" << endl; + nout << (contained ? "true" : "false") << endl; + + return !contained; +} + } // namespace BEGIN_MAIN @@ -181,4 +199,5 @@ BEGIN_MAIN DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); + DO_TEST(test07); END_MAIN diff --git a/tests/Octagonal_Shape/contains1.cc b/tests/Octagonal_Shape/contains1.cc index 21b7c5a..649f3ea 100644 --- a/tests/Octagonal_Shape/contains1.cc +++ b/tests/Octagonal_Shape/contains1.cc @@ -245,20 +245,24 @@ test07() { bool test08() { - TOctagonal_Shape oc1(0); + TOctagonal_Shape oc1(3, UNIVERSE); print_constraints(oc1, "*** oc1 ***"); - TOctagonal_Shape oc2(0, EMPTY); + TOctagonal_Shape oc2(3, EMPTY); print_constraints(oc2, "*** oc2 ***"); bool contained = oc1.contains(oc2); + bool strictly_contained = oc1.strictly_contains(oc2); nout << "*** oc1.contains(oc2) ***" << endl; nout << (contained ? "true" : "false") << endl; - return contained; + nout << "*** oc1.strictly_contains(oc2) ***" << endl; + nout << (strictly_contained ? "true" : "false") << endl; + + return contained && strictly_contained; } bool @@ -333,6 +337,24 @@ test11() { return !contained; } +bool +test12() { + TOctagonal_Shape oc1(3, EMPTY); + + print_constraints(oc1, "*** oc1 ***"); + + TOctagonal_Shape oc2(3, UNIVERSE); + + print_constraints(oc2, "*** oc2 ***"); + + bool contained = oc1.contains(oc2); + + nout << "*** oc1.contains(oc2) ***" << endl; + nout << (contained ? "true" : "false") << endl; + + return !contained; +} + } // namespace BEGIN_MAIN @@ -347,4 +369,5 @@ BEGIN_MAIN DO_TEST(test09); DO_TEST(test10); DO_TEST(test11); + DO_TEST(test12); END_MAIN

1 0

A bug for the Octagonal_Shape class
by Gianluca Amato 23 May '12

23 May '12

Hi all, I have discovered a bug in the "striclty_contains" method for the Octagonal_Shape class. The following piece of code Octagonal_Shape<double> o1(3,UNIVERSE); Octagonal_Shape<double> o2(3,EMPTY); bool result = o1.strictly_contains(o2); ends with result==false instead of result==true. Note that method "contains" works. The bug is both in the released versions and in the git. --gianluca

2 1

[GIT] ppl/ppl(master): Links fixed.
by Roberto Bagnara 18 May '12

18 May '12

Module: ppl/ppl Branch: master Commit: 794459a3b6a2cb42f9a8a8817be449700805b2b8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=794459a3b6a2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri May 18 13:41:02 2012 +0200 Links fixed. --- CREDITS | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CREDITS b/CREDITS index 12fe199..1e735b2 100644 --- a/CREDITS +++ b/CREDITS @@ -388,8 +388,8 @@ projects and organizations: [19] http://www.haible.de/bruno/ [20] http://www.irisa.fr/prive/Bertrand.Jeannet/ [21] http://www.irisa.fr/prive/Bertrand.Jeannet/newpolka.html -[22] http://bugseng.com/products/ppl/Documentation/chernikova.c -[23] http://bugseng.com/products/ppl/Documentation/bibliography#LeVerge92 +[22] http://bugseng.com/products/ppl/documentation/chernikova.c +[23] http://bugseng.com/products/ppl/documentation/bibliography#LeVerge92 [24] http://research.microsoft.com/~logozzo/ [25] http://homepages.inf.ed.ac.uk/kwxm/ [26] http://www.math.unipr.it/~medori/

1 0

[GIT] ppl/ppl(master): Mention a recently fixed bug in the PIP solver.
by Enea Zaffanella 18 May '12

18 May '12

Module: ppl/ppl Branch: master Commit: 597ea89c8c669695cf02ecabb842721b2febff53 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=597ea89c8c66… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 18 09:08:02 2012 +0200 Mention a recently fixed bug in the PIP solver. --- NEWS | 23 +++++++++++++++++++++++ 1 files changed, 23 insertions(+), 0 deletions(-) diff --git a/NEWS b/NEWS index ff1c636..8c2be8d 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,29 @@ in any medium, provided this notice is preserved. Parma Polyhedra Library NEWS -- history of user-visible changes =============================================================== +-------------------------------------------------------------------------- +NEWS for version 0.13 (release date TBD) +-------------------------------------------------------------------------- + +New and Changed Features +======================== + +o Added a generic interface for sequences of coefficients enabling a + seamless switch between the dense or the sparse row representation. + The implementation of many library entities (linear expressions, + constraints, generators, congruences, and their systems) can now be + tailored to the specific usage context, sometimes leading to significant + memory space savings (e.g., for constraint systems describing weakly + relational abstractions such as boxes and octagonal shapes). + + +Bugfixes +======== + +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. + -------------------------------------------------------------------------- NEWS for version 0.12.1 (released on April 16, 2012)

1 0

[GIT] ppl/ppl(master): Properly match #endif's directives using comments.
by Enea Zaffanella 18 May '12

18 May '12

Module: ppl/ppl Branch: master Commit: 300c3a4bea8c72fdd218dba212553ae74779c116 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=300c3a4bea8c… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri May 18 09:03:50 2012 +0200 Properly match #endif's directives using comments. --- tests/ppl_test.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/ppl_test.hh b/tests/ppl_test.hh index b91361c..1eacfa6 100644 --- a/tests/ppl_test.hh +++ b/tests/ppl_test.hh @@ -371,7 +371,7 @@ check_noisy(const char* return true; #endif return false; -#endif +#endif // !PPL_HAVE_DECL_GETENV } template<typename CharT, typename Traits = std::char_traits<CharT> > @@ -493,8 +493,8 @@ typedef BD_Shape<ANALYZER_FP_FORMAT> FP_BD_Shape; floating point computations. */ typedef Octagonal_Shape<ANALYZER_FP_FORMAT> FP_Octagonal_Shape; -#endif -#endif +#endif // ANALYZED_FP_FORMAT +#endif // ANALYZER_FP_FORMAT template <typename Shape> inline bool

1 0

PPL make check fails (OS X)
by Sergey Oboguev 12 May '12

12 May '12

When building ppl-0.12.1 on OS X, tests failed: test04 test05 FAIL: polyhedron1 tests failed: test04 test05 FAIL: polyhedron2 ====================================== 2 of 10 tests failed Please report to ppl-devel(a)cs.unipr.it ====================================== make[5]: *** [check-TESTS] Error 1 make[4]: *** [check-am] Error 2 make[3]: *** [run_tests.stamp] Error 1 make[2]: *** [check-am] Error 2 make[1]: *** [check-recursive] Error 1 make: *** [check-recursive] Error 1

3 4

Fwd: Re: Need your help on building ppl~
by Roberto Bagnara 06 May '12

06 May '12

-------- Original Message -------- Subject: Re: [PPL-devel] Need your help on building ppl~ Date: Sun, 6 May 2012 14:09:49 +0800 From: Xikui Wang <idleft(a)gmail.com> To: Roberto Bagnara <bagnara(a)cs.unipr.it> Hi Roberto: The newer version did solved my problem~ Thank you very much! Xikui 2012/5/5 Roberto Bagnara <bagnara(a)cs.unipr.it <mailto:bagnara@cs.unipr.it>> On 05/05/12 05:03, Xikui Wang wrote: Hi guys: I met a problem when building ppl, and I can't figure out why this happened. After a rough search on google and review on documentation, I still can't find a solution. So, could someone help me with this? Thanks a lot~ Hi Xikui, can you please try the PPL 0.12.2 snapshot available at http://bugseng.com/products/__ppl/download/ftp/snapshots/ <http://bugseng.com/products/ppl/download/ftp/snapshots/> Please let us know if that solves the problem you discovered. Thanks, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~__bagnara/ <http://www.cs.unipr.it/~bagnara/> mailto:bagnara@cs.unipr.it <mailto:bagnara@cs.unipr.it>

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Version number bumped.
by Roberto Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: 6c885858519880d09b1649c17bd6024d642cc05d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=6c8858585198… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat May 5 16:02:16 2012 +0200 Version number bumped. --- configure.ac | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/configure.ac b/configure.ac index a19ca2f..3d150eb 100644 --- a/configure.ac +++ b/configure.ac @@ -24,7 +24,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.12.2pre1], [ppl-devel(a)cs.unipr.it], [ppl]) +AC_INIT([the Parma Polyhedra Library], [0.12.2pre2], [ppl-devel(a)cs.unipr.it], [ppl]) # Minimum Autoconf version required. AC_PREREQ(2.61)

1 0

[GIT] ppl/ppl(ppl-0_12-branch): Avoid use C++ library for exact conversion from floating point numbers to string : the library is free to ignore requested precision.
by Abramo Bagnara 05 May '12

05 May '12

Module: ppl/ppl Branch: ppl-0_12-branch Commit: a3bd8dd6849b1ccb6a2a3a7e7eac51fb49381810 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a3bd8dd6849b… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Thu May 3 17:26:43 2012 +0200 Avoid use C++ library for exact conversion from floating point numbers to string: the library is free to ignore requested precision. --- README | 3 - m4/Makefile.am | 3 - m4/ac_cxx_double_binary_format.m4 | 4 +- m4/ac_cxx_double_exact_output.m4 | 141 ------------------ m4/ac_cxx_float_binary_format.m4 | 4 +- m4/ac_cxx_float_exact_output.m4 | 137 ----------------- m4/ac_cxx_long_double_binary_format.m4 | 4 +- m4/ac_cxx_long_double_exact_output.m4 | 254 -------------------------------- src/checked.cc | 33 ++++ src/checked.defs.hh | 2 + src/checked_float.inlines.hh | 54 ++++++- src/checked_mpq.inlines.hh | 20 +--- 12 files changed, 86 insertions(+), 573 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=a3bd8dd6…

1 0