May 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): New tests for Polyhedron::wrap_assign().
by Roberto Bagnara 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: e8ea60a5e953796c5b04660e652467f0f6f09f0d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e8ea60a5e953… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 11:18:40 2009 +0200 New tests for Polyhedron::wrap_assign(). --- tests/Polyhedron/Makefile.am | 7 ++- tests/Polyhedron/wrap1.cc | 10 ++-- tests/Polyhedron/wrap2.cc | 98 ++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 108 insertions(+), 7 deletions(-) diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index b4162e1..9a2acb0 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -132,7 +132,7 @@ topclosure1 \ unconstrain1 \ universe1 universe2 \ variablesset1 \ -wrap1 \ +wrap1 wrap2 \ writeconsys1 \ writegensys1 \ writepolyhedron1 writepolyhedron2 \ @@ -204,7 +204,7 @@ nnc_smm1 \ nnc_timeelapse1 \ nnc_unconstrain1 \ nnc_universe1 \ -nnc_wrap1 \ +nnc_wrap1 nnc_wrap2 \ nnc_writepolyhedron1 # @@ -406,6 +406,7 @@ universe2_SOURCES = universe2.cc variablesset1_SOURCES = variablesset1.cc wrap1_SOURCES = wrap1.cc +wrap2_SOURCES = wrap2.cc writeconsys1_SOURCES = writeconsys1.cc @@ -629,6 +630,8 @@ nnc_universe1_CXXFLAGS = $(DERIVED_CXXFLAGS) nnc_wrap1_SOURCES = wrap1.cc nnc_wrap1_CXXFLAGS = $(DERIVED_CXXFLAGS) +nnc_wrap2_SOURCES = wrap2.cc +nnc_wrap2_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 index bc65191..e8077a7 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -572,8 +572,8 @@ test20() { Variable y(1); C_Polyhedron ph(2); - ph.add_constraint(x >= 255); - ph.add_constraint(x <= 257); + ph.add_constraint(2*x >= 1); + ph.add_constraint(3*x <= 2); ph.add_constraint(y >= 255); ph.add_constraint(y <= 257); @@ -587,8 +587,8 @@ test20() { ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs, 16, false); C_Polyhedron known_result(2); - known_result.add_constraint(x >= 0); - known_result.add_constraint(x <= 1); + known_result.add_constraint(2*x >= 0); + known_result.add_constraint(3*x <= 2); known_result.add_constraint(y >= 0); known_result.add_constraint(y <= 1); @@ -621,5 +621,5 @@ BEGIN_MAIN DO_TEST(test17); DO_TEST(test18); DO_TEST_F8(test19); - DO_TEST(test20); + DO_TEST_F8(test20); END_MAIN diff --git a/tests/Polyhedron/wrap2.cc b/tests/Polyhedron/wrap2.cc new file mode 100644 index 0000000..363c28f --- /dev/null +++ b/tests/Polyhedron/wrap2.cc @@ -0,0 +1,98 @@ +/* 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() { + Variable x(0); + Variable y(1); + + C_Polyhedron ph(2); + ph.add_constraint(x >= 255); + ph.add_constraint(x <= 257); + ph.add_constraint(y >= 255); + ph.add_constraint(y <= 257); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x + y <= 100); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs, 16, false); + + C_Polyhedron known_result(2); + known_result.add_constraint(x >= 0); + known_result.add_constraint(x <= 1); + known_result.add_constraint(y >= 0); + known_result.add_constraint(y <= 1); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + +bool +test02() { + Variable x(0); + Variable y(1); + + C_Polyhedron ph(2); + ph.add_constraint(x >= 255); + ph.add_constraint(x <= 257); + ph.add_constraint(y >= 255); + ph.add_constraint(y <= 257); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x + y <= 100); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs, 16, true); + + C_Polyhedron known_result(2); + known_result.add_constraint(x >= 0); + known_result.add_constraint(y >= 0); + known_result.add_constraint(y <= 1); + known_result.add_constraint(x+y <= 100); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + +} // namespace + +BEGIN_MAIN + DO_TEST_F8(test01); + DO_TEST_F8(test02); +END_MAIN

1 0

[GIT] ppl/ppl(master): Known result for test03() corrected; test now marked to succeed.
by Enea Zaffanella 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 79c0986359562c47bc4f88b03dfc7b796a0b978b URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=79c098635956… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 10:22:09 2009 +0200 Known result for test03() corrected; test now marked to succeed. --- tests/Box/wrap1.cc | 6 ++---- 1 files changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index 6a0d1f9..43dacd5 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -109,10 +109,8 @@ test03() { box.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs); - // FIXME. TBox known_result(2); - known_result.refine_with_constraint(6 <= x); - // known_result.refine_with_constraint(0 <= x); + known_result.refine_with_constraint(0 <= x); known_result.refine_with_constraint(x <= 255); known_result.refine_with_constraint(0 <= y); known_result.refine_with_constraint(y <= 50); @@ -197,7 +195,7 @@ test05() { BEGIN_MAIN DO_TEST_F8(test01); DO_TEST_F8(test02); - DO_TEST_F(test03); + DO_TEST_F8(test03); DO_TEST_F8(test04); DO_TEST_F8(test05); END_MAIN

1 0

[GIT] ppl/ppl(master): First draft of Box::wrap_assign() is now operational . Added a few tests.
by Enea Zaffanella 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 656fbd60bb14e3304468e8016937a188ead46418 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=656fbd60bb14… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 10:17:59 2009 +0200 First draft of Box::wrap_assign() is now operational. Added a few tests. --- src/Box.templates.hh | 82 +++++++++++++++++++++++++++++++++---------------- tests/Box/wrap1.cc | 70 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 125 insertions(+), 27 deletions(-) diff --git a/src/Box.templates.hh b/src/Box.templates.hh index 0561430..3f311fa 100644 --- a/src/Box.templates.hh +++ b/src/Box.templates.hh @@ -1420,7 +1420,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, const Constraint_System* pcs, unsigned complexity_threshold, bool wrap_individually) { -#if 1 // Generic implementation commented out. +#if 0 // Generic implementation commented out. Implementation::wrap_assign(*this, vars, w, r, o, pcs, complexity_threshold, wrap_individually, @@ -1429,66 +1429,94 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, used(wrap_individually); used(complexity_threshold); Box& x = *this; - const dimension_type space_dim = x.space_dimension(); - // Dimension-compatibility check of `*pcs', if any. - if (pcs != 0 && pcs->space_dimension() > space_dim) - throw_dimension_incompatible("wrap_assign(vars, w, s, o, pcs, ...)", *pcs); + + // Dimension-compatibility check for `*pcs', if any. + const dimension_type vars_space_dim = vars.space_dimension(); + if (pcs != 0 && pcs->space_dimension() > vars_space_dim) { + std::ostringstream s; + s << "PPL::Box<ITV>::wrap_assign(vars, w, r, o, pcs, ...):" + << std::endl + << "vars.space_dimension() == " << vars_space_dim + << ", pcs->space_dimension() == " << pcs->space_dimension() << "."; + throw std::invalid_argument(s.str()); + } // Wrapping no variable only requires refining with *pcs, if any. if (vars.empty()) { if (pcs != 0) - pointset.refine_with_constraints(*pcs); + refine_with_constraints(*pcs); return; } - // Dimension-compatibility check. - const dimension_type vars_space_dim = vars.space_dimension(); - if (space_dim < vars_space_dim) - throw_dimension_incompatible("wrap_assign(vs, w, s, o, ...)", - vars_space_dim); + // Dimension-compatibility check for `vars'. + const dimension_type space_dim = x.space_dimension(); + if (space_dim < vars_space_dim) { + std::ostringstream s; + s << "PPL::Box<ITV>::wrap_assign(vars, ...):" + << std::endl + << "this->space_dimension() == " << space_dim + << ", required space dimension == " << vars_space_dim << "."; + throw std::invalid_argument(s.str()); + } + // Wrapping an empty polyhedron is a no-op. if (x.is_empty()) return; - const Variables_Set::const_iterator vs_end = vars.end(); - // FIXME: temporarily (ab-) using Coefficient. // Set `min_value' and `max_value' to the minimum and maximum values // a variable of width `w' and signedness `s' can take. PPL_DIRTY_TEMP_COEFFICIENT(min_value); PPL_DIRTY_TEMP_COEFFICIENT(max_value); - if (s == UNSIGNED) { + if (r == UNSIGNED) { min_value = 0; mul_2exp_assign(max_value, Coefficient_one(), w); + --max_value; } else { - assert(s == SIGNED_2_COMPLEMENT); + assert(r == SIGNED_2_COMPLEMENT); mul_2exp_assign(max_value, Coefficient_one(), w-1); neg_assign(min_value, max_value); + --max_value; } - // FIXME: Build the quadrant interval. - I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); - I_Constraint<Coefficient> upper = i_constraint(LESS_THAN, max_value); - PPL_DIRTY_TEMP(ITV, quadrant_itv); - quadrant_itv.build(lower, upper); + + // FIXME: Build the (integer) quadrant interval. + PPL_DIRTY_TEMP(ITV, integer_quadrant_itv); + PPL_DIRTY_TEMP(ITV, rational_quadrant_itv); + { + I_Constraint<Coefficient> lower = i_constraint(GREATER_OR_EQUAL, min_value); + I_Constraint<Coefficient> upper = i_constraint(LESS_OR_EQUAL, max_value); + integer_quadrant_itv.build(lower, upper); + // The rational quadrant is only needed if overflow is undefined. + if (o == OVERFLOW_UNDEFINED) { + ++max_value; + upper = i_constraint(LESS_THAN, max_value); + rational_quadrant_itv.build(lower, upper); + } + } + + const Variables_Set::const_iterator vs_end = vars.end(); if (pcs == 0) { // No constraint refinement is needed here. switch (o) { case OVERFLOW_WRAPS: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) - x.seq[*i].wrap_assign(w, s, quadrant_itv); + x.seq[*i].wrap_assign(w, r, integer_quadrant_itv); + reset_empty_up_to_date(); break; case OVERFLOW_UNDEFINED: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { ITV& x_seq_v = x.seq[*i]; - if (!quadrant_itv.contains(x_seq_v)) - x_seq_v.assign(UNIVERSE); + if (!rational_quadrant_itv.contains(x_seq_v)) { + x_seq_v.assign(integer_quadrant_itv); + } } break; case OVERFLOW_IMPOSSIBLE: for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) - x.seq[*i].intersect_assign(quadrant_itv); + x.seq[*i].intersect_assign(integer_quadrant_itv); + reset_empty_up_to_date(); break; } assert(x.OK()); @@ -1530,7 +1558,7 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, // Loop through the variable indexes in `vars'. for (Variables_Set::const_iterator i = vars.begin(); i != vs_end; ++i) { const dimension_type v = *i; - refinement_itv = quadrant_itv; + refinement_itv = integer_quadrant_itv; // Look for the refinement constraints for space dimension index `v'. map_type::const_iterator var_cs_map_iter = var_cs_map.find(v); if (var_cs_map_iter != var_cs_map_end) { @@ -1548,10 +1576,10 @@ Box<ITV>::wrap_assign(const Variables_Set& vars, ITV& x_seq_v = x.seq[v]; switch (o) { case OVERFLOW_WRAPS: - x_seq_v.wrap_assign(w, s, refinement_itv); + x_seq_v.wrap_assign(w, r, refinement_itv); break; case OVERFLOW_UNDEFINED: - if (!quadrant_itv.contains(x_seq_v)) + if (!rational_quadrant_itv.contains(x_seq_v)) x_seq_v.assign(UNIVERSE); break; case OVERFLOW_IMPOSSIBLE: diff --git a/tests/Box/wrap1.cc b/tests/Box/wrap1.cc index 0045246..6a0d1f9 100644 --- a/tests/Box/wrap1.cc +++ b/tests/Box/wrap1.cc @@ -124,10 +124,80 @@ test03() { return ok; } +bool +test04() { + Variable x(0); + TBox box1(1); + box1.add_constraint(2*x == 511); + + print_constraints(box1, "*** box ***"); + + Variables_Set vars(x); + + // Making copies before affecting box1. + TBox box2(box1); + TBox box3(box1); + + TBox good_enough_result(box1); + TBox precise_result(1, EMPTY); + + box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE); + + // FIXME: Implementation can be more precise than expected. + bool ok = box1.contains(precise_result) && good_enough_result.contains(box1) + && box2.contains(precise_result) && good_enough_result.contains(box2) + && box3.contains(precise_result) && good_enough_result.contains(box3); + + print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***"); + print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***"); + print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***"); + + return ok; +} + +bool +test05() { + Variable x(0); + TBox box1(1); + box1.add_constraint(2*x == 18*256 + 511); + + print_constraints(box1, "*** box ***"); + + Variables_Set vars(x); + + // Making copies before affecting box1. + TBox box2(box1); + TBox box3(box1); + + box1.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS); + box2.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_UNDEFINED); + box3.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_IMPOSSIBLE); + + TBox known_result1(1, EMPTY); + TBox known_result2(1); + known_result2.add_constraint(x >= 0); + known_result2.add_constraint(x <= 255); + TBox known_result3(1, EMPTY); + + bool ok = (box1 == known_result1) + && (box2 == known_result2) + && (box3 == known_result3); + + print_constraints(box1, "*** box.wrap_assign(..., OVERFLOW_WRAPS) ***"); + print_constraints(box2, "*** box.wrap_assign(..., OVERFLOW_UNDEFINED) ***"); + print_constraints(box3, "*** box.wrap_assign(..., OVERFLOW_IMPOSSIBLE) ***"); + + return ok; +} + } // namespace BEGIN_MAIN DO_TEST_F8(test01); DO_TEST_F8(test02); DO_TEST_F(test03); + DO_TEST_F8(test04); + DO_TEST_F8(test05); END_MAIN

1 0

[GIT] ppl/ppl(master): Fixed a bug in wrap_assign_col().
by Roberto Bagnara 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: a1c80c743c7c0561a584a3f12d4bf3245aab2985 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a1c80c743c7c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 10:13:53 2009 +0200 Fixed a bug in wrap_assign_col(). --- src/wrap_assign.hh | 13 ++++++------- tests/Polyhedron/wrap1.cc | 2 +- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 55f8ac4..74382f2 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -117,8 +117,7 @@ wrap_assign_col(PSET& dest, Coefficient_traits::const_reference min_value, Coefficient_traits::const_reference max_value, const Constraint_System* pcs, - Coefficient& tmp1, - Coefficient& tmp2) { + Coefficient& tmp) { if (first == end) { PSET p(src); if (pcs != 0) @@ -136,19 +135,19 @@ wrap_assign_col(PSET& dest, const Variable& x = wrap_dim_translations.var; const Coefficient& first_quadrant = wrap_dim_translations.first_quadrant; const Coefficient& last_quadrant = wrap_dim_translations.last_quadrant; - Coefficient& quadrant = tmp1; - Coefficient& shift = tmp2; + Coefficient& shift = tmp; + PPL_DIRTY_TEMP_COEFFICIENT(quadrant); for (quadrant = first_quadrant; quadrant <= last_quadrant; ++quadrant) { if (quadrant != 0) { mul_2exp_assign(shift, quadrant, w); PSET p(src); p.affine_image(x, x - shift, 1); wrap_assign_col(dest, p, vars, first+1, end, w, min_value, max_value, - pcs, tmp1, tmp2); + pcs, tmp); } else wrap_assign_col(dest, src, vars, first+1, end, w, min_value, max_value, - pcs, tmp1, tmp2); + pcs, tmp); } } } @@ -372,7 +371,7 @@ wrap_assign(PSET& pointset, PSET hull(space_dim, EMPTY); wrap_assign_col(hull, pointset, dimensions_to_be_translated, translations.begin(), translations.end(), - w, min_value, max_value, pcs, ln, ld); + w, min_value, max_value, pcs, ln); pointset.swap(hull); } } diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index edec4ba..bc65191 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -621,5 +621,5 @@ BEGIN_MAIN DO_TEST(test17); DO_TEST(test18); DO_TEST_F8(test19); - DO_TEST_F(test20); + DO_TEST(test20); END_MAIN

1 0

[GIT] ppl/ppl(master): Added a test showing a bug in wrap_assign when wrap_individually == false.
by Enea Zaffanella 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: 21df1e86b0b5605512dabf6021fdf277ab8dc9c8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=21df1e86b0b5… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Mon May 18 08:59:11 2009 +0200 Added a test showing a bug in wrap_assign when wrap_individually == false. Test is test20(), temporarily marked as an expected failure. --- tests/Polyhedron/wrap1.cc | 34 ++++++++++++++++++++++++++++++++++ 1 files changed, 34 insertions(+), 0 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index a36b931..edec4ba 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -566,6 +566,39 @@ test19() { return ok; } +bool +test20() { + Variable x(0); + Variable y(1); + + C_Polyhedron ph(2); + ph.add_constraint(x >= 255); + ph.add_constraint(x <= 257); + ph.add_constraint(y >= 255); + ph.add_constraint(y <= 257); + + print_constraints(ph, "*** ph ***"); + + Variables_Set vars(x, y); + + Constraint_System cs; + cs.insert(x + y <= 100); + + ph.wrap_assign(vars, BITS_8, UNSIGNED, OVERFLOW_WRAPS, &cs, 16, false); + + C_Polyhedron known_result(2); + known_result.add_constraint(x >= 0); + known_result.add_constraint(x <= 1); + known_result.add_constraint(y >= 0); + known_result.add_constraint(y <= 1); + + bool ok = (ph == known_result); + + print_constraints(ph, "*** ph.wrap_assign(...) ***"); + + return ok; +} + } // namespace BEGIN_MAIN @@ -588,4 +621,5 @@ BEGIN_MAIN DO_TEST(test17); DO_TEST(test18); DO_TEST_F8(test19); + DO_TEST_F(test20); END_MAIN

1 0

[GIT] ppl/ppl(master): 8-bit coefficients are now enough for test07().
by Roberto Bagnara 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: beee742bea103893f505d0bba069597c2cb3ae8e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=beee742bea10… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 08:20:34 2009 +0200 8-bit coefficients are now enough for test07(). --- tests/Polyhedron/wrap1.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/tests/Polyhedron/wrap1.cc b/tests/Polyhedron/wrap1.cc index 3695a97..a36b931 100644 --- a/tests/Polyhedron/wrap1.cc +++ b/tests/Polyhedron/wrap1.cc @@ -575,7 +575,7 @@ BEGIN_MAIN DO_TEST_F8(test04); DO_TEST_F16(test05); DO_TEST_F16(test06); - DO_TEST_F16A(test07); + DO_TEST_F8(test07); DO_TEST_F8(test08); DO_TEST_F16(test09); DO_TEST_F16(test10);

1 0

[GIT] ppl/ppl(master): Added declarations and stub implementations for drop_some_non_integer_points ().
by Roberto Bagnara 18 May '09

18 May '09

Module: ppl/ppl Branch: master Commit: b8bd2d5df01c50ebf74723388bef3c988b410289 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b8bd2d5df01c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Mon May 18 08:16:34 2009 +0200 Added declarations and stub implementations for drop_some_non_integer_points(). --- src/BD_Shape.defs.hh | 29 +++++++++++++++++++++++++++++ src/BD_Shape.inlines.hh | 16 ++++++++++++++++ src/BD_Shape.templates.hh | 33 +++++++++++++++++++++------------ src/Box.defs.hh | 29 +++++++++++++++++++++++++++++ src/Box.templates.hh | 27 +++++++++++++++++++++++++++ src/Grid.defs.hh | 29 +++++++++++++++++++++++++++++ src/Octagonal_Shape.defs.hh | 29 +++++++++++++++++++++++++++++ src/Octagonal_Shape.inlines.hh | 16 ++++++++++++++++ src/Octagonal_Shape.templates.hh | 38 ++++++++++++++++++++++++-------------- src/Polyhedron.defs.hh | 29 +++++++++++++++++++++++++++++ 10 files changed, 249 insertions(+), 26 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=b8bd2d5d…

1 0

[Fwd: GNU Automake 1.11 released]
by Roberto Bagnara 18 May '09

18 May '09

-------- Original Message -------- Subject: GNU Automake 1.11 released Date: Sun, 17 May 2009 19:52:38 +0200 From: Ralf Wildenhues <Ralf.Wildenhues(a)gmx.de> Reply-To: bug-automake(a)gnu.org To: automake(a)gnu.org, autotools-announce(a)gnu.org, info-gnu(a)gnu.org We're pleased to announce the release of Automake 1.11. Automake is a tool for automatically generating `Makefile.in's suitable for use with Autoconf, compliant with the GNU Makefile standards, and portable to various make implementations. This release contains a bunch of new features and a bunch of bug fixes over previous versions. Highlights over 1.10, in no particular order: Optional Linux kernel style less verbose compile rules, faster rules for (un)install, support for parallel tests, colored tests output, improved Fortran and initial Vala support, threaded automake execution, lzma/xz compressed tarballs, man pages which are not transformed, non-".c" default sources, better AM_MAINTAINER_MODE, man pages for aclocal and automake. See the NEWS excerpt below for more details, and a couple of things to note when upgrading. The important changes of 1.11 over the last test release, 1.10b, are documented here: <http://git.savannah.gnu.org/cgit/automake.git/tree/NEWS?id=7fa2890c4ec91ae2…> Further, the test release was released using GPLv3+, but the 1.11 release uses GPLv2+. Automake will again move to GPLv3+ once the Exception has been rewritten to use the new GPL Exception language. A big thanks to all people who have been testing pre-release, reporting bugs, contributing code, suggesting enhancements, and answering user questions on the mailing lists! You can find the new release here: ftp://ftp.gnu.org/gnu/automake/automake-1.11.tar.gz ftp://ftp.gnu.org/gnu/automake/automake-1.11.tar.gz.sig ftp://ftp.gnu.org/gnu/automake/automake-1.11.tar.bz2 ftp://ftp.gnu.org/gnu/automake/automake-1.11.tar.bz2.sig Soon it will also appear on the GNU mirrors which are listed here: http://www.gnu.org/order/ftp.html Finally, here are the MD5 checksums: 4db4efe027e26b33930a7e151de19d0f automake-1.11.tar.bz2 fab0bd2c3990a6679adaf9eeac0c6d2a automake-1.11.tar.gz Please report bugs by mail to <bug-automake(a)gnu.org>. New in 1.11: * Version requirements: - Autoconf 2.62 or greater is required. * Changes to aclocal: - The autoconf version check implemented by aclocal in aclocal.m4 (and new in Automake 1.10) is degraded to a warning. This helps in the common case where the Autoconf versions used are compatible. * Changes to automake: - The automake program can run multiple threads for creating most Makefile.in files concurrently, if at least Perl 5.7.2 is available with interpreter-based threads enabled. Set the environment variable AUTOMAKE_JOBS to the maximum number of threads to use, in order to enable this experimental feature. * Changes to Libtool support: - Libtool generic flags are now passed to the install and uninstall modes as well. - distcheck works with Libtool 2.x even when LT_OUTPUT is used, as config.lt is removed correctly now. * Languages changes: - subdir-object mode works now with Fortran (F77, FC, preprocessed Fortran, and Ratfor). - For files with extension .f90, .f95, .f03, or .f08, the flag $(FCFLAGS_f[09]x) computed by AC_FC_SRCEXT is now used in compile rules. - Files with extension .sx are also treated as preprocessed assembler. - The default source file extension (.c) can be overridden with AM_DEFAULT_SOURCE_EXT now. - Python 3.0 is supported now, Python releases prior to 2.0 are no longer supported. - AM_PATH_PYTHON honors python's idea about the site directory. - There is initial support for the Vala programming language, when using Vala 0.7.0 or later. * Miscellaneous changes: - Automake development is done in a git repository on Savannah now, see http://git.sv.gnu.org/gitweb/?p=automake.git A read-only CVS mirror is provided at cvs -d :pserver:anonymous@pserver.git.sv.gnu.org:/automake.git \ checkout -d automake HEAD - "make dist" can now create xz-compressed tarballs, as well as (deprecated?) lzma-compressed tarballs. - `automake --add-missing' will by default install the GPLv3 file as COPYING if it is missing. It will also warn that the license file should be added to source control. Note that Automake will never overwrite an existing COPYING file, even when the `--force-missing' option is used. - The manual is now distributed under the terms of the GNU FDL 1.3. - Automake ships and installs man pages for automake and aclocal now. - New shorthand `$(pkglibexecdir)' for `$(libexecdir)/@PACKAGE@'. - install-sh supports -C, which does not update the installed file (and its time stamps) if the contents did not change. - The `gnupload' script has been revamped. - The `depcomp' and `compile' scripts now work with MSVC under MSYS. - The targets `install' and `uninstall' are more efficient now, in that for example multiple files from one Automake variable such as `bin_SCRIPTS' are copied in one `install' (or `libtool --mode=install') invocation if they do not have to be renamed. Both install and uninstall may sometimes enter (`cd' into) the target installation directory now, when no build-local scripts are used. Both install and uninstall do not fail anymore but do nothing if an installation directory variable like `bindir' is set to the empty string. For built-in rules, `make install' now fails reliably if installation of a file failed. Conversely, `make uninstall' even succeeds when issued multiple times. These changes may need some adjustments from users: For example, some `install' programs refuse to install multiple copies of the same file in one invocation, so you may need to remove duplicate entries from file lists. Also, within one set of files, say, nobase_data_DATA, the order of installation may be changed, or even unstable among different hosts, due to the use of associative arrays in awk. The increased use of awk matches a similar move in Autoconf to provide for better scaling. Further, most undocumented per-rule install command variables such as binSCRIPT_INSTALL have been removed because they are not needed any more. Packages which use them should be using the appropriate one of INSTALL_{DATA,PROGRAM,SCRIPT} or their install_sh_{DATA,PROGRAM,SCRIPT} counterpart, depending on the type of files and the need for automatic target directory creation. - The "deleted header file problem" for *.m4 files is avoided by stub rules. This allows `make' to trigger a rerun of `aclocal' also if some previously needed macro file has been removed. - Rebuild rules now also work for a removed `subdir/Makefile.in' in an otherwise up to date tree. - The `color-tests' option causes colored test result output on terminals. - The `parallel-tests' option enables a new test driver that allows for parallel test execution, inter-test dependencies, lazy test execution for unit-testing, re-testing only failed tests, and formatted result output as RST (reStructuredText) and HTML. Enabling this option may require some changes to your test suite setup; see the manual for details. - The `silent-rules' option enables Linux kernel-style silent build output. This option requires the widely supported but non-POSIX `make' feature of recursive variable expansion, so do not use it if your package needs to build with `make' implementations that do not support it. To enable less verbose build output, the developer has to use the Automake option `silent-rules' in `AM_INIT_AUTOMAKE', or call the `AM_SILENT_RULES' macro. The user may then set the default verbosity by passing the `--enable-silent-rules' option to `configure'. At `make' run time, this default may be overridden using `make V=0' for less verbose, and `make V=1' for backward-compatible verbose output. - New prefix `notrans_' for manpages which should not be transformed by --program-transform. - New macro AM_COND_IF for conditional evaluation and conditional config files. - For AC_CONFIG_LINKS, if source and destination are equal, do not remove the file in a non-VPATH build. Such setups work with Autoconf 2.62 or newer. - AM_MAINTAINER_MODE now allows for an optional argument specifying the default setting. - AM_SUBST_NOTMAKE may prevent substitution of AC_SUBSTed variables, useful especially for multi-line values. - Automake's early configure-time sanity check now diagnoses an unsafe absolute source directory name and makes configure fail. - The Automake macros and rules cope better with whitespace in the current directory name, as long as the relative path to `configure' does not contain whitespace. To this end, the values of `$(MISSING)' and `$(install_sh)' may contain suitable quoting, and their expansion might need `eval'uation if used outside of a makefile. These undocumented variables may be used in several documented macros such as $(AUTOCONF) or $(MAKEINFO). Bugs fixed in 1.11: * Long standing bugs: - Fix aix dependency tracking for libtool objects. - Work around AIX sh quoting issue in AC_PROG_CC_C_O, leading to unnecessary use of the `compile' script. - For nobase_*_LTLIBRARIES with nonempty directory components, the correct `-rpath' argument is used now. - `config.status --file=Makefile depfiles' now also works with the extra quoting used internally by Autoconf 2.62 and newer (it used to work only without the `--file=' bit). - The `missing' script works better with versioned tool names. - Semantics for `missing help2man' have been revamped: Previously, if `help2man' was not present, `missing help2man' would have the following semantics: if some man page was out of date but present, then a warning would be printed, but the exit status was 0. If the man page was not present at all, then `missing' would create a replacement man page containing an error message, and exit with a status of 2. This does not play well with `make': the next run will see this particular man page as being up to date, and will only error out on the next generated man page, if any; repeat until all pages are done. This was not desirable. These are the new semantics: if some man page is not present, and help2man is not either, then `missing' will warn and generate the replacement page containing the error message, but exit successfully. However, `make dist' will ensure that no such bogus man pages are packaged into a tarball. - Targets provided by automake behave better with `make -n', in that they take care not to create files. - `config.status Makefile... depfiles' works fine again in the presence of disabled dependency tracking. - The default no-op recursive rules for these targets also work with BSD make now: html, install-html, install-dvi, install-pdf, install-pdf, install-info. - `make distcheck' works also when both a directory and some file below it have been added to a distribution variable, such as EXTRA_DIST or *_SOURCES. - Texinfo dvi, ps, pdf, and html output files are not removed upon `make mostlyclean' any more; only the LaTeX by-products are. - Renamed objects also work with the `subdir-objects' option and source file languages which Automake does not know itself. - `automake' now correctly complains about variable assignments which are preceded by a comment, extend over multiple lines with backslash-escaped newlines, and end in a comment sign. Previous versions would silently and wrongly ignore such assignments completely. * Bugs introduced by 1.10: - Fix output of dummy dependency files in presence of post-processed Makefile.in's again, but also cope with long lines. - $(EXEEXT) is automatically appended to filenames of XFAIL_TESTS that have been declared as programs in the same Makefile. This is for consistency with the analogous change to TESTS in 1.10. - Fix order of standard includes to again be `-I. -I$(srcdir)', followed by directories containing config headers. -- Prof. Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it

1 0

[GIT] ppl/ppl(master): Finished the documentation about the wrapping operator.
by Roberto Bagnara 17 May '09

17 May '09

Module: ppl/ppl Branch: master Commit: 5a29f32dbb8b1543d8738da6eae2eb318162c22d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5a29f32dbb8b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sun May 17 17:42:14 2009 +0200 Finished the documentation about the wrapping operator. --- doc/definitions.dox | 49 ++++++++++++++++++++++++++++++++++++++++++++----- src/globals.types.hh | 6 +++--- 2 files changed, 47 insertions(+), 8 deletions(-) diff --git a/doc/definitions.dox b/doc/definitions.dox index c651cdf..ff19299 100644 --- a/doc/definitions.dox +++ b/doc/definitions.dox @@ -437,7 +437,17 @@ library user to provide the PPL's method with approximations of reality that are consistent with respect to the desired results. -\section Approximating_Bounded_Arithmetic Approximating Bounded Arithmetic +\section Approximating_Integers Approximating Integers + +FIXME(0.11): to be written. + + +\subsection Dropping_Non_Integer_Points Dropping Non-Integer Points + +FIXME(0.11): to be written. + + +\subsection Approximating_Bounded_Integers Approximating Bounded Integers The Parma Polyhedra Library provides services that allow to compute correct approximations of bounded arithmetic as available in widespread @@ -494,7 +504,7 @@ Supported overflow behaviors are: FIXME(0.11): to be continued. -\subsection Wrapping_Operator Wrapping Operator +\subsubsection Wrapping_Operator Wrapping Operator One possibility to precisely approximate the semantics of programs that operate on bounded integer variables is to follow the approach described @@ -522,9 +532,38 @@ combinations. The PPL provides a general wrapping operator 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, - -FIXME(0.11): to be continued. +the width, representation and overflow behavior of all these variables. +An optional constraint system allows, when given, to increase the +precision. This constraint system, which must only depend on variables +with respect to which wrapping is performed, is assumed to represent +the conditional or looping construct guard with respect to which +wrapping is performed. Since wrapping requires the computation of +upper bounds and due to non-distributivity of constraint refinement +over upper bounds, passing a constraint system in this way can be more +precise than refining the result of the wrapping operation afterwards. +The general wrapping operator offered by the PPL also allows to control +the complexity/precision ratio by means of two additional parameters: +an unsigned integer encoding a complexity threshold, with higher values +resulting in possibly improved precision; and a Boolean controlling +whether space dimensions should be wrapped individually, something that +results in much greater efficiency to the detriment of precision, +or collectively. + +Note that the PPL assumes that any space dimension subject to wrapping +is being used to capture the value of bounded integer values. As a +consequence the library is free to drop, from the involved numerical +abstraction, any point having a non-integer coordinate in correspondence +of a space dimension subject to wrapping. It must be stressed that +freedom to drop such points does not constitute an obligation to remove +all of them (especially because this would be extraordinarily expensive +on some numerical abstractions). +The PPL provides operators for the more systematic +\ref Dropping_Non_Integer_Points +"removal of points with non-integral coordinates". + +The wrapping operator will only remove some of these points +as a byproduct of its main task and only when this comes at a negligible +extra cost. \section convex_polys Convex Polyhedra diff --git a/src/globals.types.hh b/src/globals.types.hh index 5ed9e76..546445d 100644 --- a/src/globals.types.hh +++ b/src/globals.types.hh @@ -75,7 +75,7 @@ enum Optimization_Mode { Widths of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Width { //! \hideinitializer 8 bits. @@ -98,7 +98,7 @@ enum Bounded_Integer_Type_Width { Representation of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Representation { //! Unsigned binary. @@ -115,7 +115,7 @@ enum Bounded_Integer_Type_Representation { Overflow behavior of bounded integer types. See the section on - \ref Approximating_Bounded_Arithmetic "approximating bounded arithmetic". + \ref Approximating_Bounded_Integers "approximating bounded integers". */ enum Bounded_Integer_Type_Overflow { /*! \brief

1 0

[GIT] ppl/ppl(master): Rounding direction is not relevant here.
by Abramo Bagnara 17 May '09

17 May '09

Module: ppl/ppl Branch: master Commit: 4335c8f28a366f43954ca56c08e890dfe68445fc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4335c8f28a36… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sun May 17 16:42:56 2009 +0200 Rounding direction is not relevant here. --- src/wrap_assign.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/wrap_assign.hh b/src/wrap_assign.hh index 5b1498e..55f8ac4 100644 --- a/src/wrap_assign.hh +++ b/src/wrap_assign.hh @@ -313,13 +313,13 @@ wrap_assign(PSET& pointset, quadrants = last_quadrant - first_quadrant + 1; unsigned extension; - Result r = assign_r(extension, quadrants, ROUND_DIRECT); + Result r = assign_r(extension, quadrants, ROUND_IGNORE); if (result_overflow(r) || extension > complexity_threshold) goto set_full_range; if (!wrap_individually && !collective_wrap_too_complex) { r = mul_assign_r(collective_wrap_complexity, - collective_wrap_complexity, extension, ROUND_DIRECT); + collective_wrap_complexity, extension, ROUND_IGNORE); if (result_overflow(r) || collective_wrap_complexity > complexity_threshold) collective_wrap_too_complex = true;

1 0