October 2010 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): In method Bit_Matrix::OK(), do also check the first Bit_Row.
by Enea Zaffanella 10 Oct '10

10 Oct '10

Module: ppl/ppl Branch: master Commit: 3592af215e8a58aac07e7e76a28c66246f2abc6a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3592af215e8a… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sun Oct 10 16:34:30 2010 +0200 In method Bit_Matrix::OK(), do also check the first Bit_Row. --- src/Bit_Matrix.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Bit_Matrix.cc b/src/Bit_Matrix.cc index 54a5024..7a7a8d0 100644 --- a/src/Bit_Matrix.cc +++ b/src/Bit_Matrix.cc @@ -200,7 +200,7 @@ PPL::Bit_Matrix::OK() const { #endif const Bit_Matrix& x = *this; - for (dimension_type i = num_rows(); i-- > 1; ) { + for (dimension_type i = num_rows(); i-- > 0; ) { const Bit_Row& row = x[i]; if (!row.OK()) return false;

1 0

compiling PPL 0.11 with -flto option to GCC 4.5?
by Basile Starynkevitch 10 Oct '10

10 Oct '10

Hello All & specially Roberto Have anyone been able to compile PPL (e.g. the 0.11 release) with the link time optimization to GCC 4.5.1? I have tried to ./configure CC='gcc-4.5 -flto' CXX='g++-4.5 -flto' --enable-interfaces=c,ocaml but did not succeed. (the gcc-4.5 is from Debian/Experimental, but even with an self built gcc from FSF tarball, it seems to be the same). And -flto is passed thru CC or CXX since it is both a compile & a link time flag. It is probably not a PPL bug, but perhaps a GCC or a binutils (the gold variant) one... Cheers. -- Basile STARYNKEVITCH http://starynkevitch.net/Basile/ email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359 8, rue de la Faiencerie, 92340 Bourg La Reine, France *** opinions {are only mine, sont seulement les miennes} ***

1 0

[GIT] ppl/ppl(floating_point): Added two FIXME notes.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 3f052c1b8df2482f0adeb0c4627c7ede4876bc26 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f052c1b8df2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 19:00:03 2010 +0200 Added two FIXME notes. --- src/linearize.hh | 8 ++++++++ 1 files changed, 8 insertions(+), 0 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 1a06b84..72e759a 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -604,6 +604,10 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, result == FP_Linear_Form(FP_Interval_Type(0)) || result == FP_Linear_Form(FP_Interval_Type(1))) /* + FIXME: find a general way to check if the casted constant + is exactly representable in the less precise format. + */ + /* We are casting to a more precise format or casting a definitely safe value: do not add errors. */ @@ -618,6 +622,10 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, result == FP_Linear_Form(FP_Interval_Type(0)) || result == FP_Linear_Form(FP_Interval_Type(1))) /* + FIXME: find a general way to check if the casted constant + is exactly representable in the less precise format. + */ + /* We are casting to a more precise format or casting a definitely safe value: do not add errors. */

1 0

[GIT] ppl/ppl(floating_point): Never add a rounding error when casting 1.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 8c02f7d8aa8325c3771e4eb66da031d7e05c7b0b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=8c02f7d8aa83… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 15:34:20 2010 +0200 Never add a rounding error when casting 1. --- src/linearize.hh | 14 ++++++++------ 1 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 5374a93..1a06b84 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -601,10 +601,11 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, return false; if (!is_less_precise_than(analyzed_format, cast_arg->type().floating_point_format()) || - result == FP_Linear_Form(FP_Interval_Type(0))) + result == FP_Linear_Form(FP_Interval_Type(0)) || + result == FP_Linear_Form(FP_Interval_Type(1))) /* - We are casting to a more precise format or casting the 0 value. - Do not add errors. + We are casting to a more precise format or casting + a definitely safe value: do not add errors. */ return true; } @@ -614,10 +615,11 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, return false; result = FP_Linear_Form(expr_value); if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format) || - result == FP_Linear_Form(FP_Interval_Type(0))) + result == FP_Linear_Form(FP_Interval_Type(0)) || + result == FP_Linear_Form(FP_Interval_Type(1))) /* - We are casting to a more precise format or casting the 0 value. - Do not add errors. + We are casting to a more precise format or casting + a definitely safe value: do not add errors. */ return true; }

1 0

[GIT] ppl/ppl(floating_point): Never add a rounding error when casting the 0 value.
by Fabio Bossi 05 Oct '10

05 Oct '10

Module: ppl/ppl Branch: floating_point Commit: 500981d998d62c82210b01b5c22994e9c7ef1f4b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=500981d998d6… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Tue Oct 5 10:51:03 2010 +0200 Never add a rounding error when casting the 0 value. --- src/linearize.hh | 16 ++++++++++++---- 1 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/linearize.hh b/src/linearize.hh index 8767f80..5374a93 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -600,8 +600,12 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, if (!linearize(*cast_arg, oracle, lf_store, result)) return false; if (!is_less_precise_than(analyzed_format, - cast_arg->type().floating_point_format())) - // We are casting to a more precise format. Do not add errors. + cast_arg->type().floating_point_format()) || + result == FP_Linear_Form(FP_Interval_Type(0))) + /* + We are casting to a more precise format or casting the 0 value. + Do not add errors. + */ return true; } else { @@ -609,8 +613,12 @@ cast_linearize(const Cast_Operator<Target>& cast_expr, if (!oracle.get_integer_expr_value(*cast_arg, expr_value)) return false; result = FP_Linear_Form(expr_value); - if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format)) - // We are rounding to a less precise format. Do not add errors. + if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format) || + result == FP_Linear_Form(FP_Interval_Type(0))) + /* + We are casting to a more precise format or casting the 0 value. + Do not add errors. + */ return true; }

1 0

[GIT] ppl/ppl(master): Sparse_Row: optimize linear_combine(), avoiding the insertion of too many elements.
by Marco Poletti 03 Oct '10

03 Oct '10

Module: ppl/ppl Branch: master Commit: 27a720c897ec87c9854374630e9846d882e86e7b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=27a720c897ec… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 17:13:33 2010 +0200 Sparse_Row: optimize linear_combine(), avoiding the insertion of too many elements. --- src/Sparse_Row.cc | 164 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 files changed, 163 insertions(+), 1 deletions(-) diff --git a/src/Sparse_Row.cc b/src/Sparse_Row.cc index c3c0f3f..1dec76d 100644 --- a/src/Sparse_Row.cc +++ b/src/Sparse_Row.cc @@ -232,6 +232,107 @@ PPL::Sparse_Row::normalize() { PPL_ASSERT(OK()); } +namespace { + +class sparse_row_linear_combine_helper_iterator { +public: + sparse_row_linear_combine_helper_iterator( + const PPL::Sparse_Row& x, const PPL::Sparse_Row& y, + PPL::Coefficient_traits::const_reference coeff1_1, + PPL::Coefficient_traits::const_reference coeff2_1) + : coeff1(coeff1_1), coeff2(coeff2_1) { + i = x.begin(); + i_end = x.end(); + j = y.begin(); + j_end = y.end(); + update_current_data(); + } + + void operator++() { + if (from_i) + ++i; + if (from_j) + ++j; + update_current_data(); + } + + PPL::Coefficient_traits::const_reference operator*() { + return current_value; + } + + PPL::dimension_type index() { + return current_index; + } + +private: + void update_current_data() { + if (i == i_end) { + if (j == j_end) { + return; + } else { + // i == i_end, j != j_end, so use j. + current_index = j.index(); + current_value = *j; + current_value *= coeff2; + from_i = false; + from_j = true; + } + } else { + if (j == j_end) { + // i != i_end, j == j_end, so use i. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + from_i = true; + from_j = false; + } else { + // i != i_end and j != j_end. + if (i.index() < j.index()) { + // i.index() < j.index(), so use i. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + from_i = true; + from_j = false; + } else { + if (i.index() != j.index()) { + PPL_ASSERT(i.index() > j.index()); + // i.index() > j.index(), so use j. + current_index = j.index(); + current_value = *j; + current_value *= coeff2; + from_i = false; + from_j = true; + } else { + // i.index() == j.index(), so use both i and j. + current_index = i.index(); + current_value = *i; + current_value *= coeff1; + PPL::add_mul_assign(current_value, *j, coeff2); + from_i = true; + from_j = true; + } + } + } + } + PPL_ASSERT(!from_i || i != i_end); + PPL_ASSERT(!from_j || j != j_end); + } + + PPL::Coefficient_traits::const_reference coeff1; + PPL::Coefficient_traits::const_reference coeff2; + PPL::Sparse_Row::const_iterator i; + PPL::Sparse_Row::const_iterator i_end; + PPL::Sparse_Row::const_iterator j; + PPL::Sparse_Row::const_iterator j_end; + PPL::dimension_type current_index; + PPL::Coefficient current_value; + bool from_i; + bool from_j; +}; + +} // namespace + void PPL::Sparse_Row::linear_combine(const Sparse_Row& y, Coefficient_traits::const_reference coeff1, @@ -239,7 +340,9 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, PPL_ASSERT(coeff1 != 0); PPL_ASSERT(coeff2 != 0); PPL_ASSERT(this != &y); + if (coeff1 == 1) { + // Optimize for this special case. iterator i = end(); for (const_iterator j = y.begin(), j_end = y.end(); j != j_end; ++j) { i = insert(i, j.index()); @@ -247,7 +350,45 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, if (*i == 0) i = reset(i); } - } else { + return; + } + + dimension_type counter = 0; + // Count the number of elements that are stored in y but not in *this. + { + iterator i = begin(); + iterator i_end = end(); + const_iterator j = y.begin(); + const_iterator j_end = y.end(); + if (i != i_end) { + while (j != j_end) { + PPL_ASSERT(i != i_end); + if (i.index() == j.index()) { + ++i; + ++j; + if (i == i_end) + break; + } else + if (i.index() < j.index()) { + i = lower_bound(i, j.index()); + if (i == i_end) + break; + } else { + PPL_ASSERT(i.index() > j.index()); + ++counter; + ++j; + } + } + } + PPL_ASSERT(i == i_end || j == j_end); + for ( ; j != j_end; ++j) + ++counter; + } + // This condition is arbitrary. Changing it affects performance but not + // correctness. The values have been tuned using some ppl_lpsol benchmarks + // on 2 October 2010. + if (counter == 0 || counter < 7 * size() / 64) { + // Few insertions needed, do them directly. iterator i = begin(); // This is a const reference to an internal iterator, that is kept valid. // If we just stored a copy, that would be invalidated by the calls to @@ -283,6 +424,27 @@ PPL::Sparse_Row::linear_combine(const Sparse_Row& y, i = insert(i, j.index(), *j); (*i) *= coeff2; } + } else { + // Too many insertions needed, a full copy is probably faster than + // inserting all those new elements into *this. + CO_Tree new_tree(sparse_row_linear_combine_helper_iterator(*this, y, + coeff1, + coeff2), + counter + tree.size()); + std::swap(tree, new_tree); + + // Now remove stored zeroes. + iterator i = begin(); + // Note that end() can not be called only once, because reset() + // invalidates all iterators. + while (i != end()) { + if (*i == 0) { + const dimension_type old_index = i.index(); + i = reset(i); + PPL_ASSERT(find(old_index) == end()); + } else + ++i; + } } }

1 0

[GIT] ppl/ppl(master): Dense_Matrix, Sparse_Matrix: remove useless typedefs for row_type.
by Marco Poletti 03 Oct '10

03 Oct '10

Module: ppl/ppl Branch: master Commit: e9f743717517f834912473cf77d05db585b5e4e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e9f743717517… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Sun Oct 3 09:24:55 2010 +0200 Dense_Matrix, Sparse_Matrix: remove useless typedefs for row_type. --- src/Dense_Matrix.defs.hh | 2 -- src/Sparse_Matrix.defs.hh | 2 -- 2 files changed, 0 insertions(+), 4 deletions(-) diff --git a/src/Dense_Matrix.defs.hh b/src/Dense_Matrix.defs.hh index 2f082b6..1bf916e 100644 --- a/src/Dense_Matrix.defs.hh +++ b/src/Dense_Matrix.defs.hh @@ -44,8 +44,6 @@ site: http://www.cs.unipr.it/ppl/ . */ class Parma_Polyhedra_Library::Dense_Matrix { public: - typedef Dense_Row row_type; - //! Returns the maximum number of rows of a Dense_Matrix. static dimension_type max_num_rows(); diff --git a/src/Sparse_Matrix.defs.hh b/src/Sparse_Matrix.defs.hh index 5331f74..9f6c2d7 100644 --- a/src/Sparse_Matrix.defs.hh +++ b/src/Sparse_Matrix.defs.hh @@ -54,8 +54,6 @@ site: http://www.cs.unipr.it/ppl/ . */ class Parma_Polyhedra_Library::Sparse_Matrix { public: - typedef Sparse_Row row_type; - typedef std::vector<Sparse_Row>::iterator iterator; typedef std::vector<Sparse_Row>::const_iterator const_iterator;

1 0

my problem with using ppl
by saber mirzaei 02 Oct '10

02 Oct '10

Dear PPL Developers, I am currently working on my master thesis that applies abstract model checking of software systems. For implementing an abstract domain, I plan to use PPL for the handling of Polyhedra. Right now my problem is how to inlcude the PPL classes in my C++ project. I am using Ubuntu 10.04 and i'm working with Code Blocks.I installed PPL library by using synaptic and it went well and i have related files in my lib and include directories now. However now I am unsure about how to actually include PPL classes (e.g. "Polyhedron") in a C++ project and also could find no further instructions in the user manual or the README and INSTALL files, provided. Maybe you can help me answering this question: - What is the intended usage of PPL? Should one just include "ppl.hh" and the created libraries? Right now, this yields error messages like:"... undefined reference to `Parma_Polyhedra_Library::Init::Init...." it seems the linker is unable to find the used library functions. Your help will be much appreciated! With best regards, Saber MirzaeiSharif University OF science and technologyComputer department.

2 1

[GIT] ppl/ppl(master): CO_Tree: fix comment.
by Marco Poletti 01 Oct '10

01 Oct '10

Module: ppl/ppl Branch: master Commit: 58d73240616250bff7ab3afa63e102b9bd21d30f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=58d732406162… Author: Marco Poletti <poletti.marco(a)gmail.com> Date: Fri Oct 1 15:34:50 2010 +0200 CO_Tree: fix comment. --- src/CO_Tree.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/CO_Tree.defs.hh b/src/CO_Tree.defs.hh index 7eb4ce0..76ff01c 100644 --- a/src/CO_Tree.defs.hh +++ b/src/CO_Tree.defs.hh @@ -74,8 +74,8 @@ namespace Parma_Polyhedra_Library { available caches. Assuming \p n is the number of elements in the tree and \p B is the number - of <dimension_type,Coefficient> pairs that fit in cache, the time and - cache misses complexities are the following: + of <dimension_type,Coefficient> pairs that fit in a cache line, the + time and cache misses complexities are the following: - Insertions/Queries/Deletions: \f$O(\log^2 n)\f$ time, \f$O(\log \frac{n}{B}))\f$ cache misses.

1 0