From b12eb0508f1d3c528f6b0746ec8a640a6b744f7f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 25 May 2018 11:29:59 +0200 Subject: [PATCH] fix and check shifting issue The exception raised by << and >> when shifting mark_t by too many bits are only enabled in SPOT_DEBUG, as those operations are quite low-level. However we were always testing them, and although we wanted them to be active in Python, it was not always the case. * spot/twa/acc.hh: introduce max_accsets() as a static constexpr method, so we can see it in Python. * spot/misc/bitset.hh: Fix preprocessing directive so the check is actually enabled when compiling the Python bindings. * bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc: Use max_accsets(). * tests/core/acc.cc: Comment out the shifting exception when SPOT_DEBUG is unset. * tests/python/except.py: Make sure the exception is always raised in Python. --- bin/autcross.cc | 3 ++- bin/autfilt.cc | 9 ++++--- bin/ltlcross.cc | 3 ++- spot/misc/bitset.hh | 4 +-- spot/twa/acc.hh | 26 ++++++++++++++----- tests/core/acc.cc | 58 ++++++++++++++++++++++++------------------ tests/python/except.py | 10 ++++++++ 7 files changed, 75 insertions(+), 38 deletions(-) diff --git a/bin/autcross.cc b/bin/autcross.cc index 95b02b258..e14a1393e 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -509,7 +509,8 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j) { - if (aut_i->num_sets() + aut_j->num_sets() > SPOT_MAX_ACCSETS) + if (aut_i->num_sets() + aut_j->num_sets() > + spot::acc_cond::mark_t::max_accsets()) { std::cerr << "info: building " << autname(i) << '*' << autname(j, true) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e34d59323..20306d037 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -649,7 +649,8 @@ static spot::twa_graph_ptr product(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { if ((type == spot::postprocessor::BA) - && (left->num_sets() + right->num_sets() > SPOT_MAX_ACCSETS)) + && (left->num_sets() + right->num_sets() > + spot::acc_cond::mark_t::max_accsets())) { left = ensure_tba(left); right = ensure_tba(right); @@ -661,7 +662,8 @@ static spot::twa_graph_ptr product_or(spot::twa_graph_ptr left, spot::twa_graph_ptr right) { if ((type == spot::postprocessor::BA) - && (left->num_sets() + right->num_sets() > SPOT_MAX_ACCSETS)) + && (left->num_sets() + right->num_sets() > + spot::acc_cond::mark_t::max_accsets())) { left = ensure_tba(left); right = ensure_tba(right); @@ -965,7 +967,8 @@ parse_opt(int key, char* arg, struct argp_state*) if (res < 0) error(2, 0, "acceptance sets should be non-negative:" " --mask-acc=%ld", res); - if (static_cast(res) > SPOT_MAX_ACCSETS) + if (static_cast(res) >= + spot::acc_cond::mark_t::max_accsets()) error(2, 0, "this implementation does not support that many" " acceptance sets: --mask-acc=%ld", res); opt_mask_acc.set(res); diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 2e226ea97..d119e4e93 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -691,7 +691,8 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { - if (aut_i->num_sets() + aut_j->num_sets() > SPOT_MAX_ACCSETS) + if (aut_i->num_sets() + aut_j->num_sets() > + spot::acc_cond::mark_t::max_accsets()) { // Report the skipped test if both automata are not // complemented, or the --verbose option is used, diff --git a/spot/misc/bitset.hh b/spot/misc/bitset.hh index 5dac1af72..69a6ce3b9 100644 --- a/spot/misc/bitset.hh +++ b/spot/misc/bitset.hh @@ -151,7 +151,7 @@ namespace spot bitset& operator<<=(unsigned s) { -#if SPOT_DEBUG || SWIG +#if SPOT_DEBUG || defined(SWIGPYTHON) if (SPOT_UNLIKELY(s >= 8 * N * sizeof(word_t))) internal::report_bit_shift_too_big(); #else @@ -191,7 +191,7 @@ namespace spot bitset& operator>>=(unsigned s) { -#if SPOT_DEBUG || SWIG +#if SPOT_DEBUG || defined(SWIGPYTHON) if (SPOT_UNLIKELY(s >= 8 * N * sizeof(word_t))) internal::report_bit_shift_too_big(); #else diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index b3e35b75f..1062c2731 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -94,6 +94,16 @@ namespace spot } } + /// \brief The maximum number of acceptance sets supported by + /// this implementation. + /// + /// The value can be changed at compile-time using configure's + /// --enable-max-accsets=N option. + constexpr static unsigned max_accsets() + { + return SPOT_MAX_ACCSETS; + } + static mark_t all() { return mark_t(_value_t::mone()); @@ -220,7 +230,7 @@ namespace spot return id ^ r.id; } -#if SPOT_DEBUG || SWIG +#if SPOT_DEBUG || defined(SWIGPYTHON) # define SPOT_WRAP_OP(ins) \ try \ { \ @@ -567,7 +577,7 @@ namespace spot if (n == 0) return inf({}); acc_cond::mark_t m = mark_t::all(); - m >>= (SPOT_MAX_ACCSETS - n); + m >>= mark_t::max_accsets() - n; return inf(m); } @@ -576,7 +586,7 @@ namespace spot if (n == 0) return fin({}); acc_cond::mark_t m = mark_t::all(); - m >>= (SPOT_MAX_ACCSETS - n); + m >>= mark_t::max_accsets() - n; return fin(m); } @@ -833,6 +843,8 @@ namespace spot acc_code& operator<<=(unsigned sets) { + if (SPOT_UNLIKELY(sets >= mark_t::max_accsets())) + report_too_many_sets(); if (empty()) return *this; unsigned pos = size(); @@ -1247,9 +1259,11 @@ namespace spot if (num == 0) return -1U; unsigned j = num_; - num_ += num; - if (num_ > SPOT_MAX_ACCSETS) + num += j; + if (num > mark_t::max_accsets()) report_too_many_sets(); + // Make sure we do not update if we raised an exception. + num_ = num; all_ = all_sets_(); return j; } @@ -1386,7 +1400,7 @@ namespace spot protected: mark_t all_sets_() const { - return mark_t::all() >> (SPOT_MAX_ACCSETS - num_); + return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_); } unsigned num_; diff --git a/tests/core/acc.cc b/tests/core/acc.cc index 8e5d694da..9ff334a01 100644 --- a/tests/core/acc.cc +++ b/tests/core/acc.cc @@ -64,8 +64,10 @@ int main() auto m1 = spot::acc_cond::mark_t({0, 2}); auto m2 = spot::acc_cond::mark_t({0, 3}); auto m3 = spot::acc_cond::mark_t({2, 1}); - auto m4 = spot::acc_cond::mark_t({0, SPOT_MAX_ACCSETS - 2}); - if (!(m4.min_set() == 1 && m4.max_set() == SPOT_MAX_ACCSETS - 1)) + auto m4 = + spot::acc_cond::mark_t({0, spot::acc_cond::mark_t::max_accsets() - 2}); + if (!((m4.min_set() == 1) && + (m4.max_set() == spot::acc_cond::mark_t::max_accsets() - 1))) return 1; spot::acc_cond::mark_t m0 = {}; @@ -184,33 +186,39 @@ int main() assert(c1 == c2); try - { - spot::acc_cond a{SPOT_MAX_ACCSETS + 1}; - } + { + spot::acc_cond a{spot::acc_cond::mark_t::max_accsets() + 1}; + } catch (const std::runtime_error& e) - { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); - } + { + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + } + +#if SPOT_DEBUG + // Those error message are disabled in non-debugging code as + // shifting mark_t is usually done in the innermost loop of + // algorithms. However, they are still done in Python, and we + // test them in python/except.py + try + { + spot::acc_cond::mark_t m{0}; + m <<= spot::acc_cond::mark_t::max_accsets() + 1; + } + catch (const std::runtime_error& e) + { + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + } try - { - spot::acc_cond::mark_t m{0}; - m <<= SPOT_MAX_ACCSETS + 1; - } + { + spot::acc_cond::mark_t m{0}; + m >>= spot::acc_cond::mark_t::max_accsets() + 1; + } catch (const std::runtime_error& e) - { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); - } - - try - { - spot::acc_cond::mark_t m{0}; - m >>= SPOT_MAX_ACCSETS + 1; - } - catch (const std::runtime_error& e) - { - assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); - } + { + assert(!std::strncmp(e.what(), "Too many acceptance sets used.", 30)); + } +#endif return 0; } diff --git a/tests/python/except.py b/tests/python/except.py index eec7c38aa..a723ad3a8 100644 --- a/tests/python/except.py +++ b/tests/python/except.py @@ -129,3 +129,13 @@ except RuntimeError as e: assert "safety" in str(e) else: report_missing_exception() + +n = spot.mark_t.max_accsets() +m = spot.mark_t([n - 1]) +try: + m = spot.mark_t([0]) << n +except RuntimeError as e: + assert "Too many acceptance sets" in str(e) +else: + print(n, m) + report_missing_exception()