Module: ppl/ppl Branch: master Commit: 5d56513b2dc23fae0bc40c822299f2cfc18dad35 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5d56513b2dc23...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Sat Dec 10 12:50:48 2011 +0100

Added functions ppl_unreachable() and ppl_unreachable_msg(), causing program termination using abort(). Let PPL_UNREACHABLE and PPL_ASSERT be based on these functions. Avoid a cycle in header inclusion dependencies.

---

doc/devref.doxyconf-html.in | 2 + doc/devref.doxyconf-latex.in | 2 + src/Makefile.am | 1 + src/Partial_Function.inlines.hh | 2 +- src/assert.cc | 44 +++++++++++++++++++ src/assert.hh | 91 +++++++++++++++++++++++++++------------ src/checked.defs.hh | 1 + src/globals.inlines.hh | 2 +- 8 files changed, 115 insertions(+), 30 deletions(-)

diff --git a/doc/devref.doxyconf-html.in b/doc/devref.doxyconf-html.in index ea929aa..33619fd 100644 --- a/doc/devref.doxyconf-html.in +++ b/doc/devref.doxyconf-html.in @@ -92,6 +92,8 @@ INPUT = @srcdir@/definitions.dox \ ../src/version.hh \ @srcdir@/../src/version.cc \ @srcdir@/../src/meta_programming.hh \ + @srcdir@/../src/assert.hh \ + @srcdir@/../src/assert.cc \ @srcdir@/../src/Float.defs.hh \ @srcdir@/../src/Float.inlines.hh \ @srcdir@/../src/Float.cc \ diff --git a/doc/devref.doxyconf-latex.in b/doc/devref.doxyconf-latex.in index 1c75de1..7521241 100644 --- a/doc/devref.doxyconf-latex.in +++ b/doc/devref.doxyconf-latex.in @@ -92,6 +92,8 @@ INPUT = @srcdir@/definitions.dox \ ../src/version.hh \ @srcdir@/../src/version.cc \ @srcdir@/../src/meta_programming.hh \ + @srcdir@/../src/assert.hh \ + @srcdir@/../src/assert.cc \ @srcdir@/../src/Float.defs.hh \ @srcdir@/../src/Float.inlines.hh \ @srcdir@/../src/Float.cc \ diff --git a/src/Makefile.am b/src/Makefile.am index be1d931..1e488e7 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -431,6 +431,7 @@ BDS_Status.idefs.hh \ Og_Status.idefs.hh

libppl_la_SOURCES = \ +assert.cc \ Box.cc \ checked.cc \ Checked_Number.cc \ diff --git a/src/Partial_Function.inlines.hh b/src/Partial_Function.inlines.hh index 1ca05fb..212088b 100644 --- a/src/Partial_Function.inlines.hh +++ b/src/Partial_Function.inlines.hh @@ -25,7 +25,7 @@ site: http://bugseng.com/products/ppl/ . */ #define PPL_Partial_Function_inlines_hh 1

#include <stdexcept> -#include <cassert> +#include "assert.hh"

namespace Parma_Polyhedra_Library {

diff --git a/src/assert.cc b/src/assert.cc new file mode 100644 index 0000000..2a951a4 --- /dev/null +++ b/src/assert.cc @@ -0,0 +1,44 @@ +/* Definitions of assert-like functions. + Copyright (C) 2001-2010 Roberto Bagnara bagnara@cs.unipr.it + Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com) + +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://bugseng.com/products/ppl/ . */ + +#include "ppl-config.h" +#include "assert.hh" +#include <cstdlib> +#include <iostream> + +namespace PPL = Parma_Polyhedra_Library; + +void +PPL::ppl_unreachable() { + abort(); +} + +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"; + abort(); +} + diff --git a/src/assert.hh b/src/assert.hh index f480f10..277fd07 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -1,4 +1,4 @@ -/* Implementation of PPL_ASSERT macro. +/* Implementation of PPL assert-like macros. Copyright (C) 2001-2010 Roberto Bagnara bagnara@cs.unipr.it Copyright (C) 2010-2011 BUGSENG srl (http://bugseng.com)

@@ -24,55 +24,90 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_assert_hh #define PPL_assert_hh 1

-#include <cassert> #include "globals.defs.hh"

+// The PPL_UNREACHABLE_MSG macro flags a program point as unreachable. +// Argument `msg__' is added to output when assertions are turned on. #if defined(NDEBUG) +#define PPL_UNREACHABLE_MSG(msg__) Parma_Polyhedra_Library::ppl_unreachable() +#else +#define PPL_UNREACHABLE_MSG(msg__) Parma_Polyhedra_Library:: \ + ppl_unreachable_msg(msg__, __FILE__, __LINE__, __func__) +#endif + +// The PPL_UNREACHABLE macro flags a program point as unreachable. +#define PPL_UNREACHABLE PPL_UNREACHABLE_MSG("unreachable")

-#define PPL_ASSERT(cond__) -#define PPL_ASSERT_HEAVY(cond__) -// Try to force a segmentation fault (volatile null pointer deref). -#define PPL_UNREACHABLE (*(volatile int*)0)

+// Helper macro PPL_ASSERT_IMPL_: do not use it directly. +#if defined(NDEBUG) +#define PPL_ASSERT_IMPL_(cond__) ((void) 0) #else +#define PPL_STRING_(s) #s +#define PPL_ASSERT_IMPL_(cond__) \ + ((cond__) ? (void) 0 : PPL_UNREACHABLE_MSG(PPL_STRING_(cond__))) +#endif +

// Non zero to detect use of PPL_ASSERT instead of PPL_ASSERT_HEAVY #define PPL_DEBUG_PPL_ASSERT 1 -#if !PPL_DEBUG_PPL_ASSERT -#define PPL_ASSERT(cond__) assert(cond__) + +// The PPL_ASSERT macro states that Boolean condition cond__ should hold. +// This is meant to replace uses of C assert(). +#if defined(NDEBUG) || (!PPL_DEBUG_PPL_ASSERT) +#define PPL_ASSERT(cond__) PPL_ASSERT_IMPL_(cond__) #else -#define PPL_ASSERT(cond__) \ - do { \ - Parma_Polyhedra_Library::Weightwatch_Traits::Threshold \ - old_weight__ \ - = Parma_Polyhedra_Library::Weightwatch_Traits::weight; \ - assert(cond__); \ - assert(old_weight__ == Parma_Polyhedra_Library::Weightwatch_Traits::weight && \ - "PPL_ASSERT_HEAVY have to be used here"); \ +#define PPL_ASSERT(cond__) \ + do { \ + typedef Parma_Polyhedra_Library::Weightwatch_Traits W_Traits; \ + W_Traits::Threshold old_weight__ = W_Traits::weight; \ + PPL_ASSERT_IMPL_(cond__); \ + PPL_ASSERT_IMPL_(old_weight__ == W_Traits::weight \ + && "PPL_ASSERT_HEAVY have to be used here"); \ } while(0) -#endif +#endif // !defined(NDEBUG) && PPL_DEBUG_PPL_ASSERT

-// The evaluation of asserted conditions could have a non zero -// computational weight (i.e., the execution path could contain an -// invocation of WEIGHT_ADD). -#define PPL_ASSERT_HEAVY(cond__) \ - do { \ - ++Parma_Polyhedra_Library::Implementation::in_assert; \ - assert(cond__); \ - --Parma_Polyhedra_Library::Implementation::in_assert; \ - } while (0) - -#define PPL_UNREACHABLE PPL_ASSERT(false)

+// Macro PPL_ASSERT_HEAVY is meant to be used when the evaluation of +// the assertion may change computational weights (via WEIGHT_ADD). +#if defined(NDEBUG) +#define PPL_ASSERT_HEAVY(cond__) PPL_ASSERT_IMPL_(cond__) +#else +#define PPL_ASSERT_HEAVY(cond__) \ + do { \ + ++Parma_Polyhedra_Library::Implementation::in_assert; \ + PPL_ASSERT_IMPL_(cond__); \ + --Parma_Polyhedra_Library::Implementation::in_assert; \ + } while (0) #endif // !defined(NDEBUG)

+// Macro PPL_EXPECT (resp., PPL_EXPECT_HEAVY) should be used rather than +// PPL_ASSERT (resp., PPL_ASSERT_HEAVY) when the condition is assumed to +// hold but it is not under library control (typically, it depends on +// user provided input). +#define PPL_EXPECT(cond__) PPL_ASSERT(cond__) #define PPL_EXPECT_HEAVY(cond__) PPL_ASSERT_HEAVY(cond__)

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() __attribute__((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. +*/ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +void ppl_unreachable_msg(const char* msg, + const char* file, unsigned int line, + const char* function) __attribute__((weak, noreturn)); + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief Returns \c true if and only if \p x_copy contains \p y_copy.

diff --git a/src/checked.defs.hh b/src/checked.defs.hh index 642d763..7434544 100644 --- a/src/checked.defs.hh +++ b/src/checked.defs.hh @@ -24,6 +24,7 @@ site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_checked_defs_hh #define PPL_checked_defs_hh 1

+#include <cassert> #include <iostream> #include <gmpxx.h> #include "mp_std_bits.defs.hh" diff --git a/src/globals.inlines.hh b/src/globals.inlines.hh index 6a72759..7098542 100644 --- a/src/globals.inlines.hh +++ b/src/globals.inlines.hh @@ -25,7 +25,7 @@ site: http://bugseng.com/products/ppl/ . */ #define PPL_globals_inlines_hh 1

#include <limits> -#include "assert.hh" +#include <cassert>

namespace Parma_Polyhedra_Library {