bitset: optimize the code generated by shifts in common cases
* spot/misc/bitset.hh: Here. * spot/misc/bitset.cc: New file. * spot/misc/Makefile.am: Add it. * spot/twa/acc.hh: Conditionally remove the exception checks around shift operators. * spot/misc/common.hh (SPOT_ASSUME): New macro.
This commit is contained in:
parent
e979791071
commit
cc2c4615d0
5 changed files with 118 additions and 55 deletions
|
|
@ -61,6 +61,7 @@ misc_HEADERS = \
|
||||||
noinst_LTLIBRARIES = libmisc.la
|
noinst_LTLIBRARIES = libmisc.la
|
||||||
libmisc_la_SOURCES = \
|
libmisc_la_SOURCES = \
|
||||||
bareword.cc \
|
bareword.cc \
|
||||||
|
bitset.cc \
|
||||||
bitvect.cc \
|
bitvect.cc \
|
||||||
escape.cc \
|
escape.cc \
|
||||||
formater.cc \
|
formater.cc \
|
||||||
|
|
|
||||||
32
spot/misc/bitset.cc
Normal file
32
spot/misc/bitset.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
|
#include "config.h"
|
||||||
|
#include <spot/misc/bitset.hh>
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
namespace internal
|
||||||
|
{
|
||||||
|
void report_bit_shift_too_big()
|
||||||
|
{
|
||||||
|
throw std::runtime_error("bit shift by more bits than supported");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -25,6 +25,13 @@
|
||||||
|
|
||||||
namespace spot
|
namespace spot
|
||||||
{
|
{
|
||||||
|
#ifndef SWIG
|
||||||
|
namespace internal
|
||||||
|
{
|
||||||
|
[[noreturn]] SPOT_API void report_bit_shift_too_big();
|
||||||
|
}
|
||||||
|
#endif
|
||||||
|
|
||||||
template<size_t N>
|
template<size_t N>
|
||||||
class bitset
|
class bitset
|
||||||
{
|
{
|
||||||
|
|
@ -37,14 +44,13 @@ namespace spot
|
||||||
/// a special constructor for -1 (cf. mone below)
|
/// a special constructor for -1 (cf. mone below)
|
||||||
struct minus_one_tag {};
|
struct minus_one_tag {};
|
||||||
explicit bitset(minus_one_tag)
|
explicit bitset(minus_one_tag)
|
||||||
: data{0}
|
|
||||||
{
|
{
|
||||||
for (auto& v : data)
|
for (auto& v : data)
|
||||||
v -= 1;
|
v = -1U;
|
||||||
}
|
}
|
||||||
|
|
||||||
constexpr explicit bitset(word_t s)
|
constexpr explicit bitset(word_t s)
|
||||||
: data{s}
|
: data{{s}}
|
||||||
{
|
{
|
||||||
SPOT_ASSERT(s == 0U || s == 1U);
|
SPOT_ASSERT(s == 0U || s == 1U);
|
||||||
}
|
}
|
||||||
|
|
@ -133,23 +139,36 @@ namespace spot
|
||||||
|
|
||||||
bitset& operator<<=(unsigned s)
|
bitset& operator<<=(unsigned s)
|
||||||
{
|
{
|
||||||
if (SPOT_UNLIKELY(s >= 8*N*sizeof(word_t)))
|
#if SPOT_DEBUG || SWIG
|
||||||
throw std::runtime_error("bit shift overflow is undefined behavior");
|
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)
|
if (s == 0)
|
||||||
return *this;
|
return *this;
|
||||||
const unsigned wshift = s / (8*sizeof(word_t));
|
const unsigned wshift = s / (8 * sizeof(word_t));
|
||||||
const unsigned offset = s % (8*sizeof(word_t));
|
const unsigned offset = s % (8 * sizeof(word_t));
|
||||||
|
|
||||||
if (offset == 0)
|
if (offset == 0)
|
||||||
{
|
{
|
||||||
for (unsigned i = N-1; i >= wshift; --i)
|
for (unsigned i = N - 1; i >= wshift; --i)
|
||||||
data[i] = data[i - wshift];
|
data[i] = data[i - wshift];
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
const unsigned sub_offset = 8*sizeof(word_t) - offset;
|
const unsigned sub_offset = 8 * sizeof(word_t) - offset;
|
||||||
for (unsigned i = N-1; i > wshift; --i)
|
for (unsigned i = N - 1; i > wshift; --i)
|
||||||
data[i] = ((data[i - wshift] << offset) |
|
data[i] = ((data[i - wshift] << offset) |
|
||||||
(data[i - wshift - 1] >> sub_offset));
|
(data[i - wshift - 1] >> sub_offset));
|
||||||
data[wshift] = data[0] << offset;
|
data[wshift] = data[0] << offset;
|
||||||
|
|
@ -160,25 +179,39 @@ namespace spot
|
||||||
|
|
||||||
bitset& operator>>=(unsigned s)
|
bitset& operator>>=(unsigned s)
|
||||||
{
|
{
|
||||||
if (SPOT_UNLIKELY(s >= 8*N*sizeof(word_t)))
|
#if SPOT_DEBUG || SWIG
|
||||||
throw std::runtime_error("bit shift overflow is undefined behavior");
|
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)
|
if (s == 0)
|
||||||
return *this;
|
return *this;
|
||||||
const unsigned wshift = s / (8*sizeof(word_t));
|
const unsigned wshift = s / (8 * sizeof(word_t));
|
||||||
const unsigned offset = s % (8*sizeof(word_t));
|
const unsigned offset = s % (8 * sizeof(word_t));
|
||||||
const unsigned limit = N - wshift - 1;
|
const unsigned limit = N - wshift - 1;
|
||||||
|
|
||||||
if (offset == 0)
|
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
|
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)
|
for (unsigned i = 0; i < limit; ++i)
|
||||||
data[i] = ((data[i + wshift] >> offset) |
|
data[i] = ((data[i + wshift] >> offset) |
|
||||||
(data[i + wshift + 1] << sub_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));
|
std::fill(data.begin() + limit + 1, data.end(), word_t(0));
|
||||||
return *this;
|
return *this;
|
||||||
|
|
|
||||||
|
|
@ -125,6 +125,19 @@
|
||||||
#define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented");
|
#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:
|
// Useful when forwarding methods such as:
|
||||||
// auto func(int param) SPOT_RETURN(implem_.func(param));
|
// auto func(int param) SPOT_RETURN(implem_.func(param));
|
||||||
#define SPOT_RETURN(code) -> decltype(code) { return code; }
|
#define SPOT_RETURN(code) -> decltype(code) { return code; }
|
||||||
|
|
|
||||||
|
|
@ -217,55 +217,39 @@ namespace spot
|
||||||
return id ^ r.id;
|
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
|
mark_t operator<<(unsigned i) const
|
||||||
{
|
{
|
||||||
try
|
SPOT_WRAP_OP(return id << i);
|
||||||
{
|
|
||||||
return id << i;
|
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
report_too_many_sets();
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
mark_t& operator<<=(unsigned i)
|
mark_t& operator<<=(unsigned i)
|
||||||
{
|
{
|
||||||
try
|
SPOT_WRAP_OP(id <<= i; return *this);
|
||||||
{
|
|
||||||
id <<= i;
|
|
||||||
return *this;
|
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
report_too_many_sets();
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
mark_t operator>>(unsigned i) const
|
mark_t operator>>(unsigned i) const
|
||||||
{
|
{
|
||||||
try
|
SPOT_WRAP_OP(return id >> i);
|
||||||
{
|
|
||||||
return id >> i;
|
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
report_too_many_sets();
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
mark_t& operator>>=(unsigned i)
|
mark_t& operator>>=(unsigned i)
|
||||||
{
|
{
|
||||||
try
|
SPOT_WRAP_OP(id >>= i; return *this);
|
||||||
{
|
|
||||||
id >>= i;
|
|
||||||
return *this;
|
|
||||||
}
|
|
||||||
catch (const std::runtime_error& e)
|
|
||||||
{
|
|
||||||
report_too_many_sets();
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
#undef SPOT_WRAP_OP
|
||||||
|
|
||||||
mark_t strip(mark_t y) const
|
mark_t strip(mark_t y) const
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue