- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Ignore always unhandled bits.
by Abramo Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: e4dbb6e73d34028361b3ae69cd7324318a0ff720 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4dbb6e73d34… Author: Abramo Bagnara <abramo.bagnara(a)gmail.com> Date: Sat Apr 7 15:54:20 2012 +0200 Ignore always unhandled bits. --- src/Linear_Row.cc | 62 +++++++++++++++++++++++++++++------------------------ 1 files changed, 34 insertions(+), 28 deletions(-) diff --git a/src/Linear_Row.cc b/src/Linear_Row.cc index a3646c4..86204ac 100644 --- a/src/Linear_Row.cc +++ b/src/Linear_Row.cc @@ -142,37 +142,35 @@ PPL::Linear_Row::all_homogeneous_terms_are_zero() const { namespace { // These are the keywords that indicate the individual assertions. -const char* rpi_valid = "RPI_V"; -const char* is_rpi = "RPI"; -const char* nnc_valid = "NNC_V"; -const char* is_nnc = "NNC"; -const char* bit_names[] = {rpi_valid, is_rpi, nnc_valid, is_nnc}; +const char* rpi_valid_text = "RPI_V"; +const char* is_rpi_text = "RPI"; +const char* nnc_valid_text = "NNC_V"; +const char* is_nnc_text = "NNC"; +const char* bit_texts[] = {rpi_valid_text, is_rpi_text, + nnc_valid_text, is_nnc_text}; } // namespace void PPL::Linear_Row::Flags::ascii_dump(std::ostream& s) const { -#ifndef NDEBUG - s << (test_bits(1U << Flags::rpi_validity_bit) ? '+' : '-') - << rpi_valid << ' '; + bool is_rpi = test_bits(1U << Flags::rpi_bit); + bool is_nnc = test_bits(1U << Flags::nnc_bit); + bool rpi_valid; + bool nnc_valid; +#ifdef NDEBUG + // Dump unhandled bits always as true so to permit loading from a + // debug enabled executable without failing assertions. + rpi_valid = true; + nnc_valid = true; #else - // NOTE: dump the (unavailable) validity bit as set to avoid - // crashes when ascii_loading with assertions turned on. - s << '+' << rpi_valid << ' '; + rpi_valid = test_bits(1U << Flags::rpi_validity_bit); + nnc_valid = test_bits(1U << Flags::nnc_validity_bit); #endif - s << (test_bits(1U << Flags::rpi_bit) ? '+' : '-') - << is_rpi << ' ' - << ' '; -#ifndef NDEBUG - s << (test_bits(1U << Flags::nnc_validity_bit) ? '+' : '-') - << nnc_valid << ' '; -#else - // NOTE: dump the (unavailable) validity bit as set to avoid - // crashes when ascii_loading with assertions turned on. - s << '+' << nnc_valid << ' '; -#endif - s << (test_bits(1U << Flags::nnc_bit) ? '+' : '-') - << is_nnc; + s << (rpi_valid ? '+' : '-') << rpi_valid_text << ' ' + << (is_rpi ? '+' : '-') << is_rpi_text << ' ' + << ' ' + << (nnc_valid ? '+' : '-') << nnc_valid_text << ' ' + << (is_nnc ? '+' : '-') << is_nnc_text; } PPL_OUTPUT_DEFINITIONS_ASCII_ONLY(Linear_Row::Flags) @@ -183,15 +181,23 @@ PPL::Linear_Row::Flags::ascii_load(std::istream& s) { // Assume that the bits are used in sequence. reset_bits(std::numeric_limits<base_type>::max()); for (unsigned int bit = 0; - bit < (sizeof(bit_names) / sizeof(char*)); + bit < (sizeof(bit_texts) / sizeof(char*)); ++bit) { if (!(s >> str)) return false; - if (str[0] == '+') - set_bits(1U << (Dense_Row::Flags::first_free_bit + bit)); + if (str[0] == '+') { + bool load = true; +#ifdef NDEBUG + // Do not load unhandled bits. + if (bit == rpi_validity_bit || bit == nnc_validity_bit) + load = false; +#endif + if (load) + set_bits(1U << (Dense_Row::Flags::first_free_bit + bit)); + } else if (str[0] != '-') return false; - if (str.compare(1, strlen(bit_names[bit]), bit_names[bit]) != 0) + if (str.compare(1, strlen(bit_texts[bit]), bit_texts[bit]) != 0) return false; } return true;

1 0

[GIT] ppl/ppl(master): Cleaned.
by Roberto Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: a772590b835729ca6a4a9b971dfbb207c92fd451 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a772590b8357… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 7 15:25:34 2012 +0200 Cleaned. --- tests/PIP_Problem/Makefile.am | 4 +--- 1 files changed, 1 insertions(+), 3 deletions(-) diff --git a/tests/PIP_Problem/Makefile.am b/tests/PIP_Problem/Makefile.am index 0a5041c..1d7bc47 100644 --- a/tests/PIP_Problem/Makefile.am +++ b/tests/PIP_Problem/Makefile.am @@ -58,7 +58,7 @@ pipproblem1 pipproblem2 pipproblem3 XFAIL_TESTS = -BUGS = bug1 bug2 +BUGS = # # Sources for the tests @@ -72,8 +72,6 @@ pipproblem1_SOURCES = pipproblem1.cc pipproblem2_SOURCES = pipproblem2.cc pipproblem3_SOURCES = pipproblem3.cc -bug1_SOURCES = bug1.cc - check_PROGRAMS = \ $(TESTS) \ $(BUGS)

1 0

[GIT] ppl/ppl(master): Avoid using @ outside BibTex entries.
by Roberto Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: 7dfc47517c842761f050c228ca845bfab2dbbfb5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7dfc47517c84… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 7 14:11:39 2012 +0200 Avoid using @ outside BibTex entries. --- 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 f38d43b..2a72a68 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -1,6 +1,6 @@ A bibliography of papers that cite the Parma Polyhedra Library and/or the works that defined the theory upon which it is based. -Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> +Copyright (C) 2001-2010 Roberto Bagnara <bagnara AT cs.unipr.it> Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com) This BibTeX database is made available under the Open Data Commons

1 0

[GIT] ppl/ppl(master): Avoid using @ outside BibTex entries.
by Roberto Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: 1fe7c0066396293c2f836a5324e173aaafd1c60e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1fe7c0066396… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 7 14:09:41 2012 +0200 Avoid using @ outside BibTex entries. --- doc/ppl.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index 81ee363..9810fa3 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -1,6 +1,6 @@ A bibliography of papers that were consulted and/or written for the design and implementation of the Parma Polyhedra Library. -Copyright (C) 2001-2010 Roberto Bagnara <bagnara(a)cs.unipr.it> +Copyright (C) 2001-2010 Roberto Bagnara <bagnara AT cs.unipr.it> Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com) This BibTeX database is made available under the Open Data Commons

1 0

[GIT] ppl/ppl(master): Missing comma added.
by Roberto Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: f6936a75a6bf5cbfaacf908f21961f9d6c8f8572 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f6936a75a6bf… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 7 14:04:23 2012 +0200 Missing comma added. --- doc/ppl.bib | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/doc/ppl.bib b/doc/ppl.bib index 6fdb496..81ee363 100644 --- a/doc/ppl.bib +++ b/doc/ppl.bib @@ -461,7 +461,7 @@ Summarizing: Journal = "Information and Computation", Publisher = "Elsevier Science B.V.", Year = 2012, - Note = "To appear." + Note = "To appear.", Abstract = "The classical technique for proving termination of a generic sequential computer program involves the synthesis of a \emph{ranking function} for each loop of

1 0

[GIT] ppl/ppl(master): Avoid non-ASCII characters.
by Roberto Bagnara 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: 88234071d1135d533010e15182990f89656937fc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=88234071d113… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Sat Apr 7 14:00:05 2012 +0200 Avoid non-ASCII characters. --- doc/ppl.bib | 34 +++++++++++++++++----------------- doc/ppl_citations.bib | 40 ++++++++++++++++++++-------------------- 2 files changed, 37 insertions(+), 37 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=88234071…

1 0

[GIT] ppl/ppl(master): Added calls to WEIGHT macros.
by Enea Zaffanella 07 Apr '12

07 Apr '12

Module: ppl/ppl Branch: master Commit: 5234d75213a363d1123261ba2a7ed420e655552e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5234d75213a3… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Sat Apr 7 11:35:41 2012 +0200 Added calls to WEIGHT macros. --- src/PIP_Tree.cc | 131 ++++++++++++++++++++++++++++++++++++++++++++++++------- 1 files changed, 115 insertions(+), 16 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=5234d752…

1 0

[GIT] ppl/ppl(master): Weight computation fixed and adjusted.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 339439dc72b06d5e29c20cfbef6cac871d330ec4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=339439dc72b0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 19:21:23 2012 +0200 Weight computation fixed and adjusted. --- src/MIP_Problem.cc | 15 ++++++++------- 1 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/MIP_Problem.cc b/src/MIP_Problem.cc index a7cd706..ac47a84 100644 --- a/src/MIP_Problem.cc +++ b/src/MIP_Problem.cc @@ -1028,15 +1028,16 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { break; if (k->first > column) { j = tableau_i.lower_bound(j, k->first); - } else { + } + else { PPL_ASSERT(k->first == column); - WEIGHT_BEGIN(); PPL_ASSERT(tableau_i.get(base[i]) != 0); + WEIGHT_BEGIN(); assign(float_tableau_value, *j); float_tableau_value /= float_tableau_denom; float_tableau_value *= float_tableau_value; k->second += float_tableau_value; - WEIGHT_ADD_MUL(338, tableau_num_rows); + WEIGHT_ADD(22); ++j; ++k; } @@ -1086,7 +1087,7 @@ PPL::MIP_Problem::steepest_edge_float_entering_index() const { current_value = challenger_value; entering_index = j; } - WEIGHT_ADD_MUL(338, tableau_num_rows); + WEIGHT_ADD_MUL(10, tableau_num_rows); } } @@ -1337,7 +1338,7 @@ PPL::MIP_Problem::linear_combine(Row& x, const Row& y, #endif x.normalize(); - WEIGHT_ADD_MUL(83, x_size); + WEIGHT_ADD_MUL(31, x_size); } // TODO: Remove this when the sparse working cost has been tested enough. @@ -1461,7 +1462,7 @@ PPL::MIP_Problem t_e0 = t_i0; t_ee = t_ie; } - WEIGHT_ADD(1044); + WEIGHT_ADD(642); } } return exiting_base_index; @@ -1555,7 +1556,7 @@ PPL::MIP_Problem::compute_simplex_using_steepest_edge_float() { if (cost_sgn_coeff < 0) neg_assign(current_numer); abs_assign(current_denom, cost_sgn_coeff); - WEIGHT_ADD(566); + WEIGHT_ADD(433); } }

1 0

[GIT] ppl/ppl(master): Let ppl_unreachable_msg() print a more sensible message.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 0cab1cdf4cf2578661e4461104dcd8c26e50cbf5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0cab1cdf4cf2… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 17:34:28 2012 +0200 Let ppl_unreachable_msg() print a more sensible message. --- src/assert.cc | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/assert.cc b/src/assert.cc index febd73f..284d296 100644 --- a/src/assert.cc +++ b/src/assert.cc @@ -37,8 +37,8 @@ void PPL::ppl_unreachable_msg(const char* msg, const char* file, unsigned int line, const char* function) { - std::cerr << "Aborting PPL computation!\n"; - std::cerr << file << ":" << line << ": " << function << ": " << msg << "\n"; + std::cerr << file << ":" << line << ": " << function + << ": Latent fault detected: " << msg << ".\n"; abort(); }

1 0

[GIT] ppl/ppl(master): Punctuation fixed.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: a4ddaf31d0887e566e87b15fa2e5412ceca1f8f6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a4ddaf31d088… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 17:16:50 2012 +0200 Punctuation fixed. --- src/assert.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/assert.hh b/src/assert.hh index 5b0a65a..7751da2 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -38,7 +38,7 @@ site: http://bugseng.com/products/ppl/ . */ // The PPL_ASSERTION_FAILED macro is used to output a message after // an assertion failure and then cause program termination. -// (It is meant to be used only when assertions are turned on). +// (It is meant to be used only when assertions are turned on.) #define PPL_ASSERTION_FAILED(msg__) Parma_Polyhedra_Library:: \ ppl_assertion_failed(msg__, __FILE__, __LINE__, __func__)

1 0