diff --git a/spot/misc/Makefile.am b/spot/misc/Makefile.am
index 54d7767b5..d6adcf12f 100644
--- a/spot/misc/Makefile.am
+++ b/spot/misc/Makefile.am
@@ -61,6 +61,7 @@ misc_HEADERS = \
noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
bareword.cc \
+ bitset.cc \
bitvect.cc \
escape.cc \
formater.cc \
diff --git a/spot/misc/bitset.cc b/spot/misc/bitset.cc
new file mode 100644
index 000000000..97bbfef5a
--- /dev/null
+++ b/spot/misc/bitset.cc
@@ -0,0 +1,32 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot 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.
+//
+// Spot 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, see .
+
+#include "config.h"
+#include
+
+namespace spot
+{
+ namespace internal
+ {
+ void report_bit_shift_too_big()
+ {
+ throw std::runtime_error("bit shift by more bits than supported");
+ }
+ }
+}
diff --git a/spot/misc/bitset.hh b/spot/misc/bitset.hh
index d824e00d3..77e3e9684 100644
--- a/spot/misc/bitset.hh
+++ b/spot/misc/bitset.hh
@@ -25,6 +25,13 @@
namespace spot
{
+#ifndef SWIG
+ namespace internal
+ {
+ [[noreturn]] SPOT_API void report_bit_shift_too_big();
+ }
+#endif
+
template
class bitset
{
@@ -37,14 +44,13 @@ namespace spot
/// a special constructor for -1 (cf. mone below)
struct minus_one_tag {};
explicit bitset(minus_one_tag)
- : data{0}
{
for (auto& v : data)
- v -= 1;
+ v = -1U;
}
constexpr explicit bitset(word_t s)
- : data{s}
+ : data{{s}}
{
SPOT_ASSERT(s == 0U || s == 1U);
}
@@ -133,23 +139,36 @@ namespace spot
bitset& operator<<=(unsigned s)
{
- if (SPOT_UNLIKELY(s >= 8*N*sizeof(word_t)))
- throw std::runtime_error("bit shift overflow is undefined behavior");
+#if SPOT_DEBUG || SWIG
+ if (SPOT_UNLIKELY(s >= 8 * N * sizeof(word_t)))
+ internal::report_bit_shift_too_big();
+#else
+ SPOT_ASSUME(s < 8 * N * sizeof(word_t));
+#endif
+
+ // Skip the rest of this function in the most common case of
+ // N==1. g++ 6 can optimize away all the loops if N==1, but
+ // clang++4 cannot and needs help.
+ if (N == 1)
+ {
+ data[0] <<= s;
+ return *this;
+ }
if (s == 0)
return *this;
- const unsigned wshift = s / (8*sizeof(word_t));
- const unsigned offset = s % (8*sizeof(word_t));
+ const unsigned wshift = s / (8 * sizeof(word_t));
+ const unsigned offset = s % (8 * sizeof(word_t));
if (offset == 0)
- {
- for (unsigned i = N-1; i >= wshift; --i)
- data[i] = data[i - wshift];
- }
+ {
+ for (unsigned i = N - 1; i >= wshift; --i)
+ data[i] = data[i - wshift];
+ }
else
{
- const unsigned sub_offset = 8*sizeof(word_t) - offset;
- for (unsigned i = N-1; i > wshift; --i)
+ const unsigned sub_offset = 8 * sizeof(word_t) - offset;
+ for (unsigned i = N - 1; i > wshift; --i)
data[i] = ((data[i - wshift] << offset) |
(data[i - wshift - 1] >> sub_offset));
data[wshift] = data[0] << offset;
@@ -160,25 +179,39 @@ namespace spot
bitset& operator>>=(unsigned s)
{
- if (SPOT_UNLIKELY(s >= 8*N*sizeof(word_t)))
- throw std::runtime_error("bit shift overflow is undefined behavior");
+#if SPOT_DEBUG || SWIG
+ if (SPOT_UNLIKELY(s >= 8 * N * sizeof(word_t)))
+ internal::report_bit_shift_too_big();
+#else
+ SPOT_ASSUME(s < 8 * N * sizeof(word_t));
+#endif
+ // Skip the rest of this function in the most common case of
+ // N==1. g++ 6 can optimize away all the loops if N==1, but
+ // clang++4 cannot and needs help.
+ if (N == 1)
+ {
+ data[0] >>= s;
+ return *this;
+ }
if (s == 0)
return *this;
- const unsigned wshift = s / (8*sizeof(word_t));
- const unsigned offset = s % (8*sizeof(word_t));
+ const unsigned wshift = s / (8 * sizeof(word_t));
+ const unsigned offset = s % (8 * sizeof(word_t));
const unsigned limit = N - wshift - 1;
if (offset == 0)
- for (unsigned i = 0; i <= limit; ++i)
- data[i] = data[i + wshift];
+ {
+ for (unsigned i = 0; i <= limit; ++i)
+ data[i] = data[i + wshift];
+ }
else
{
- const unsigned sub_offset = 8*sizeof(word_t) - offset;
+ const unsigned sub_offset = 8 * sizeof(word_t) - offset;
for (unsigned i = 0; i < limit; ++i)
data[i] = ((data[i + wshift] >> offset) |
(data[i + wshift + 1] << sub_offset));
- data[limit] = data[N-1] >> offset;
+ data[limit] = data[N - 1] >> offset;
}
std::fill(data.begin() + limit + 1, data.end(), word_t(0));
return *this;
diff --git a/spot/misc/common.hh b/spot/misc/common.hh
index 97ad16427..ef090e749 100644
--- a/spot/misc/common.hh
+++ b/spot/misc/common.hh
@@ -125,6 +125,19 @@
#define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented");
+#if SPOT_DEBUG
+#define SPOT_ASSUME(cond) assert(cond)
+#else
+#define SPOT_ASSUME(cond) \
+ do \
+ { \
+ if (!(cond)) \
+ SPOT_UNREACHABLE_BUILTIN(); \
+ } \
+ while (0)
+#endif
+
+
// Useful when forwarding methods such as:
// auto func(int param) SPOT_RETURN(implem_.func(param));
#define SPOT_RETURN(code) -> decltype(code) { return code; }
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 921c06a86..eb93cbc92 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -217,55 +217,39 @@ namespace spot
return id ^ r.id;
}
+#if SPOT_DEBUG || SWIG
+# define SPOT_WRAP_OP(ins) \
+ try \
+ { \
+ ins; \
+ } \
+ catch (const std::runtime_error& e) \
+ { \
+ report_too_many_sets(); \
+ }
+#else
+# define SPOT_WRAP_OP(ins) ins;
+#endif
mark_t operator<<(unsigned i) const
{
- try
- {
- return id << i;
- }
- catch (const std::runtime_error& e)
- {
- report_too_many_sets();
- }
+ SPOT_WRAP_OP(return id << i);
}
mark_t& operator<<=(unsigned i)
{
- try
- {
- id <<= i;
- return *this;
- }
- catch (const std::runtime_error& e)
- {
- report_too_many_sets();
- }
+ SPOT_WRAP_OP(id <<= i; return *this);
}
mark_t operator>>(unsigned i) const
{
- try
- {
- return id >> i;
- }
- catch (const std::runtime_error& e)
- {
- report_too_many_sets();
- }
+ SPOT_WRAP_OP(return id >> i);
}
mark_t& operator>>=(unsigned i)
{
- try
- {
- id >>= i;
- return *this;
- }
- catch (const std::runtime_error& e)
- {
- report_too_many_sets();
- }
+ SPOT_WRAP_OP(id >>= i; return *this);
}
+#undef SPOT_WRAP_OP
mark_t strip(mark_t y) const
{