- PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Mimic the message given by standard assert.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 2bb170031482313ece6815221552be0253a76deb URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2bb170031482… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 17:15:23 2012 +0200 Mimic the message given by standard assert. --- src/assert.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/assert.cc b/src/assert.cc index 926539c..febd73f 100644 --- a/src/assert.cc +++ b/src/assert.cc @@ -47,6 +47,6 @@ PPL::ppl_assertion_failed(const char* assertion_text, const char* file, unsigned int line, const char* function) { std::cerr << file << ":" << line << ": " << function - << ": Assertion `" << assertion_text << "' failed\n"; + << ": Assertion `" << assertion_text << "' failed.\n"; abort(); }

1 0

[GIT] ppl/ppl(master): Added a comment to clarify definition of PPL_ASSERT.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 81a68dd16a56d4c8d7072081fa10d51a3af78cf0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81a68dd16a56… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 16:48:59 2012 +0200 Added a comment to clarify definition of PPL_ASSERT. --- src/assert.hh | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/src/assert.hh b/src/assert.hh index 3039b77..5b0a65a 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -53,6 +53,7 @@ site: http://bugseng.com/products/ppl/ . */ // Non zero to detect use of PPL_ASSERT instead of PPL_ASSERT_HEAVY +// Note: flag does not affect code built with NDEBUG defined. #define PPL_DEBUG_PPL_ASSERT 1 // The PPL_ASSERT macro states that Boolean condition cond__ should hold. @@ -60,6 +61,9 @@ site: http://bugseng.com/products/ppl/ . */ #if defined(NDEBUG) || (!PPL_DEBUG_PPL_ASSERT) #define PPL_ASSERT(cond__) PPL_ASSERT_IMPL_(cond__) #else +// Note: here we have assertions enabled and PPL_DEBUG_PPL_ASSERT is 1. +// Check if the call to PPL_ASSERT should be replaced by PPL_ASSERT_HEAVY +// (i.e., if the former may interfere with computational weights). #define PPL_ASSERT(cond__) \ do { \ typedef Parma_Polyhedra_Library::Weightwatch_Traits W_Traits; \

1 0

[GIT] ppl/ppl(master): Improved error message reporting for assertion failures.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 488490ab24f427266b6c305a0c48ecc42ddcf4d4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=488490ab24f4… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 16:38:44 2012 +0200 Improved error message reporting for assertion failures. --- src/assert.cc | 8 ++++++++ src/assert.hh | 38 +++++++++++++++++++++++++------------- 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/src/assert.cc b/src/assert.cc index c9d756a..926539c 100644 --- a/src/assert.cc +++ b/src/assert.cc @@ -42,3 +42,11 @@ PPL::ppl_unreachable_msg(const char* msg, abort(); } +void +PPL::ppl_assertion_failed(const char* assertion_text, + const char* file, unsigned int line, + const char* function) { + std::cerr << file << ":" << line << ": " << function + << ": Assertion `" << assertion_text << "' failed\n"; + abort(); +} diff --git a/src/assert.hh b/src/assert.hh index 35c2ef1..3039b77 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -36,6 +36,11 @@ site: http://bugseng.com/products/ppl/ . */ // The PPL_UNREACHABLE macro flags a program point as unreachable. #define PPL_UNREACHABLE PPL_UNREACHABLE_MSG("unreachable") +// 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). +#define PPL_ASSERTION_FAILED(msg__) Parma_Polyhedra_Library:: \ + ppl_assertion_failed(msg__, __FILE__, __LINE__, __func__) // Helper macro PPL_ASSERT_IMPL_: do not use it directly. #if defined(NDEBUG) @@ -43,7 +48,7 @@ site: http://bugseng.com/products/ppl/ . */ #else #define PPL_STRING_(s) #s #define PPL_ASSERT_IMPL_(cond__) \ - ((cond__) ? (void) 0 : PPL_UNREACHABLE_MSG(PPL_STRING_(cond__))) + ((cond__) ? (void) 0 : PPL_ASSERTION_FAILED(PPL_STRING_(cond__))) #endif @@ -90,17 +95,18 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS -//! Helper function causing program termination by calling \c abort. -#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -void ppl_unreachable() #if PPL_CXX_SUPPORTS_ATTRIBUTE_WEAK - __attribute__((weak, noreturn)); +#define PPL_WEAK_NORETURN __attribute__((weak, noreturn)) #else - __attribute__((noreturn)); +#define PPL_WEAK_NORETURN __attribute__((noreturn)) #endif #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Helper function causing program termination by calling \c abort. +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +void ppl_unreachable() PPL_WEAK_NORETURN; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief Helper function printing message on \c std::cerr and causing program termination by calling \c abort. @@ -108,12 +114,18 @@ void ppl_unreachable() #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) void ppl_unreachable_msg(const char* msg, const char* file, unsigned int line, - const char* function) -#if PPL_CXX_SUPPORTS_ATTRIBUTE_WEAK - __attribute__((weak, noreturn)); -#else - __attribute__((noreturn)); -#endif + const char* function) PPL_WEAK_NORETURN; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \brief + Helper function printing an assertion failure message on \c std::cerr + and causing program termination by calling \c abort. +*/ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +void ppl_assertion_failed(const char* assertion_text, + const char* file, unsigned int line, + const char* function) PPL_WEAK_NORETURN; + #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief

1 0

[GIT] ppl/ppl(master): Reordered so as to allow compilability with -DPPL_PROFILE_ADD_WEIGHT=1.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: fb4ff186479c5cd0a16838439b7b9743c9c10292 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fb4ff186479c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:13:14 2012 +0200 Reordered so as to allow compilability with -DPPL_PROFILE_ADD_WEIGHT=1. --- src/globals.defs.hh | 94 ++++++++++++++++++++++++++------------------------- 1 files changed, 48 insertions(+), 46 deletions(-) diff --git a/src/globals.defs.hh b/src/globals.defs.hh index c0b3733..53815ef 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -32,9 +32,6 @@ site: http://bugseng.com/products/ppl/ . */ #include <exception> #include <gmpxx.h> -#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT -#include "Weight_Profiler.defs.hh" -#endif namespace Parma_Polyhedra_Library { @@ -143,49 +140,6 @@ extern unsigned int in_assert; } // namespace Implementation #endif -#ifndef PPL_PROFILE_ADD_WEIGHT -#define PPL_PROFILE_ADD_WEIGHT 0 -#endif - -#if defined(NDEBUG) -#if PPL_PROFILE_ADD_WEIGHT -#define WEIGHT_BEGIN() Weight_Profiler::begin() -#define WEIGHT_ADD(delta) \ - do { \ - static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ - wp__.end(); \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ - wp__.end(factor); \ - } while (false) -#else -#define WEIGHT_BEGIN() \ - do { \ - } while (false) -#define WEIGHT_ADD(delta) \ - do { \ - Weightwatch_Traits::weight += (delta); \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - Weightwatch_Traits::weight += (delta)*(factor); \ - } while (false) -#endif -#else -#define WEIGHT_BEGIN() -#define WEIGHT_ADD(delta) \ - do { \ - if (Implementation::in_assert == 0) \ - Weightwatch_Traits::weight += delta; \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - if (Implementation::in_assert == 0) \ - Weightwatch_Traits::weight += delta * factor; \ - } while (false) -#endif //! User objects the PPL can throw. /*! \ingroup PPL_CXX_interface @@ -515,6 +469,54 @@ least_significant_one_mask(dimension_type i); #define PPL_USE_SPARSE_MATRIX 1 #endif +#ifndef PPL_PROFILE_ADD_WEIGHT +#define PPL_PROFILE_ADD_WEIGHT 0 +#endif + +#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT +#include "Weight_Profiler.defs.hh" +#endif + +#if defined(NDEBUG) +#if PPL_PROFILE_ADD_WEIGHT +#define WEIGHT_BEGIN() Weight_Profiler::begin() +#define WEIGHT_ADD(delta) \ + do { \ + static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ + wp__.end(); \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ + wp__.end(factor); \ + } while (false) +#else +#define WEIGHT_BEGIN() \ + do { \ + } while (false) +#define WEIGHT_ADD(delta) \ + do { \ + Weightwatch_Traits::weight += (delta); \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + Weightwatch_Traits::weight += (delta)*(factor); \ + } while (false) +#endif +#else +#define WEIGHT_BEGIN() +#define WEIGHT_ADD(delta) \ + do { \ + if (Implementation::in_assert == 0) \ + Weightwatch_Traits::weight += delta; \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + if (Implementation::in_assert == 0) \ + Weightwatch_Traits::weight += delta * factor; \ + } while (false) +#endif + #include "globals.inlines.hh" #endif // !defined(PPL_globals_defs_hh)

1 0

[GIT] ppl/ppl(master): Reference to no longer existing namespace removed.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 04e4cfbf6a817a734047d14319aa91f64e2c2183 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04e4cfbf6a81… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:11:56 2012 +0200 Reference to no longer existing namespace removed. (Wonder why we did not have a Doxygen warning.) --- src/Threshold_Watcher.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Threshold_Watcher.defs.hh b/src/Threshold_Watcher.defs.hh index c68ae79..4896adc 100644 --- a/src/Threshold_Watcher.defs.hh +++ b/src/Threshold_Watcher.defs.hh @@ -34,7 +34,7 @@ site: http://bugseng.com/products/ppl/ . */ \tparam Traits A class to set data types and functions for the threshold handling. - See \c Parma_Polyhedra_Library::Watchdog::Weightwatch_Traits for an example. + See \c Parma_Polyhedra_Library::Weightwatch_Traits for an example. */ template <typename Traits> class Parma_Polyhedra_Library::Threshold_Watcher { @@ -80,7 +80,7 @@ private: //! Check threshold reaching. static void check(); -}; // class Parma_Polyhedra_Library::Watchdog::Threshold_Watcher +}; // class Parma_Polyhedra_Library::Threshold_Watcher // Templatic initialization of static data member.

1 0

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

06 Apr '12

Module: ppl/ppl Branch: master Commit: 34fa558e18b00b28060b8da6ae6004c891440050 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=34fa558e18b0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:12:45 2012 +0200 Variable name fixed. --- src/Weight_Profiler.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Weight_Profiler.cc b/src/Weight_Profiler.cc index 064a6d3..75c2795 100644 --- a/src/Weight_Profiler.cc +++ b/src/Weight_Profiler.cc @@ -47,7 +47,7 @@ void Weight_Profiler::output_stats() { << " max( " << stat[VALID].max << ")" << " average(" << average << ")"; std::cout << " variance( " << variance << ")" - << " stddev( " << sqrt(var) << ")"; + << " stddev( " << sqrt(variance) << ")"; } if (stat[DISCARDED].samples > 0) { std::cout << " min_threshold( " << min_threshold << ")"

1 0

[GIT] ppl/ppl(master): Clarified reason of assertion failing by adding a message.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 0e40494f8f379687c9b7d44fbbfb60493e23da1d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e40494f8f37… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 10:41:12 2012 +0200 Clarified reason of assertion failing by adding a message. --- src/Linear_Row.inlines.hh | 12 ++++++++---- 1 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Linear_Row.inlines.hh b/src/Linear_Row.inlines.hh index 9b24a0b..f8d3439 100644 --- a/src/Linear_Row.inlines.hh +++ b/src/Linear_Row.inlines.hh @@ -60,7 +60,8 @@ Linear_Row::Flags::Flags(const Topology t, const Kind k) inline bool Linear_Row::Flags::is_ray_or_point_or_inequality() const { - PPL_ASSERT(test_bits(1U << rpi_validity_bit)); + PPL_ASSERT(test_bits(1U << rpi_validity_bit) + && ("rpi bit tested before being initialized" != 0)); return test_bits(static_cast<unsigned>(RAY_OR_POINT_OR_INEQUALITY) << rpi_bit); } @@ -75,7 +76,8 @@ Linear_Row::Flags::set_is_ray_or_point_or_inequality() { inline bool Linear_Row::Flags::is_line_or_equality() const { - PPL_ASSERT(test_bits(1U << rpi_validity_bit)); + PPL_ASSERT(test_bits(1U << rpi_validity_bit) + && ("rpi bit tested before being initialized" != 0)); return !is_ray_or_point_or_inequality(); } @@ -89,13 +91,15 @@ Linear_Row::Flags::set_is_line_or_equality() { inline bool Linear_Row::Flags::is_not_necessarily_closed() const { - PPL_ASSERT(test_bits(1U << nnc_validity_bit)); + PPL_ASSERT(test_bits(1U << nnc_validity_bit) + && ("nnc bit tested before being initialized" != 0)); return test_bits(static_cast<unsigned>(NOT_NECESSARILY_CLOSED) << nnc_bit); } inline bool Linear_Row::Flags::is_necessarily_closed() const { - PPL_ASSERT(test_bits(1U << nnc_validity_bit)); + PPL_ASSERT(test_bits(1U << nnc_validity_bit) + && ("nnc bit tested before being initialized" != 0)); return !is_not_necessarily_closed(); }

1 0

[GIT] ppl/ppl(master): When dumping Linear_Row:: Flags with assertions turned off,
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: b406ba2b5a15f5b1b8fa011034d9de64af012536 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b406ba2b5a15… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 10:19:18 2012 +0200 When dumping Linear_Row::Flags with assertions turned off, force the (unavailable) rpi/nnc validity bits as "set". --- src/Linear_Row.cc | 24 ++++++++++++++++++------ 1 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/Linear_Row.cc b/src/Linear_Row.cc index 5a5de51..a3646c4 100644 --- a/src/Linear_Row.cc +++ b/src/Linear_Row.cc @@ -152,14 +152,26 @@ const char* bit_names[] = {rpi_valid, is_rpi, nnc_valid, is_nnc}; void PPL::Linear_Row::Flags::ascii_dump(std::ostream& s) const { +#ifndef NDEBUG s << (test_bits(1U << Flags::rpi_validity_bit) ? '+' : '-') - << rpi_valid << ' ' - << (test_bits(1U << Flags::rpi_bit) ? '+' : '-') + << rpi_valid << ' '; +#else + // NOTE: dump the (unavailable) validity bit as set to avoid + // crashes when ascii_loading with assertions turned on. + s << '+' << rpi_valid << ' '; +#endif + s << (test_bits(1U << Flags::rpi_bit) ? '+' : '-') << is_rpi << ' ' - << ' ' - << (test_bits(1U << Flags::nnc_validity_bit) ? '+' : '-') - << nnc_valid << ' ' - << (test_bits(1U << Flags::nnc_bit) ? '+' : '-') + << ' '; +#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; }

1 0

[GIT] ppl/ppl(master): Do not use #define without a value.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 946038b56de1a069614eebe80f1a308b74b8a93e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=946038b56de1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 09:03:47 2012 +0200 Do not use #define without a value. --- src/PIP_Tree.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 8e4f09b..6c5a22c 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -28,9 +28,9 @@ site: http://bugseng.com/products/ppl/ . */ #include <memory> #include <map> -// #define NOISY_PIP_TREE_STRUCTURE -// #define NOISY_PIP -// #define VERY_NOISY_PIP +// #define NOISY_PIP_TREE_STRUCTURE 1 +// #define NOISY_PIP 1 +// #define VERY_NOISY_PIP 1 namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(master): The given problem is not satisfiable ( independently verified with other solvers).
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 3415eb20ae3bd9e1fb42c9208865211575dfe6ca URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3415eb20ae3b… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 09:03:08 2012 +0200 The given problem is not satisfiable (independently verified with other solvers). --- tests/PIP_Problem/bug1.cc | 14 +++----------- 1 files changed, 3 insertions(+), 11 deletions(-) diff --git a/tests/PIP_Problem/bug1.cc b/tests/PIP_Problem/bug1.cc index cc79299..76c7f68 100644 --- a/tests/PIP_Problem/bug1.cc +++ b/tests/PIP_Problem/bug1.cc @@ -25,7 +25,6 @@ site: http://bugseng.com/products/ppl/ . */ #include "files.hh" #include <fstream> -#include <iostream> using namespace IO_Operators; @@ -110,19 +109,12 @@ test01() { cs.insert(O >= 0); cs.insert(H >= 0); -#if 0 - MIP_Problem mip(cs.space_dimension(), cs.begin(), cs.end()); - std::cout << mip.is_satisfiable() << endl; - Variables_Set integer_space_dimensions(A, F1); - mip.add_to_integer_space_dimensions(integer_space_dimensions); - std::cout << mip.is_satisfiable() << endl; -#endif - PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); - bool ok = pip.is_satisfiable(); + if (pip.is_satisfiable()) + return false; - return ok; + return true; } } // namespace

1 0