diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index cec99a3c1..11a6a78db 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -33,6 +33,7 @@ misc_HEADERS = \ bareword.hh \ bddlt.hh \ bddop.hh \ + bitvect.hh \ casts.hh \ common.hh \ escape.hh \ @@ -59,6 +60,7 @@ noinst_LTLIBRARIES = libmisc.la libmisc_la_SOURCES = \ bareword.cc \ bddop.cc \ + bitvect.cc \ escape.cc \ formater.cc \ intvcomp.cc \ diff --git a/src/misc/bitvect.cc b/src/misc/bitvect.cc new file mode 100644 index 000000000..e84928bb1 --- /dev/null +++ b/src/misc/bitvect.cc @@ -0,0 +1,176 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 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 . + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif +#include "bitvect.hh" +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + + // How many block_t do we need to store BITCOUNT bits? + size_t block_needed(size_t bitcount) + { + const size_t bpb = 8 * sizeof(bitvect::block_t); + size_t n = (bitcount + bpb - 1) / bpb; + if (n < 1) + return 1; + return n; + } + + // Fowler–Noll–Vo hash parameters for 64bits + template + struct fnv + { + static unsigned long init() + { + return 14695981039346656037UL; + } + + static unsigned long prime() + { + return 1099511628211UL; + } + }; + + // Fowler–Noll–Vo hash parameters for 32bits + template<> + struct fnv<4> + { + static unsigned int init() + { + return 2166136261U; + } + + static unsigned int prime() + { + return 16777619U; + } + }; + + } + + bitvect::bitvect(size_t size, size_t block_count): + size_(size), + block_count_(block_count), + storage_(&local_storage_) + { + clear_all(); + } + + bitvect::bitvect(size_t size, size_t block_count, bool): + size_(size), + block_count_(block_count), + storage_(&local_storage_) + { + } + + bitvect* bitvect::clone() const + { + size_t n = block_needed(size_); + // Allocate some memory for the bitvect. The instance + // already contains one int of local_storage_, but + // we allocate n-1 more so that we store the table. + void* mem = operator new(sizeof(bitvect) + + (n - 1) * sizeof(bitvect::block_t)); + bitvect* res = new(mem) bitvect(size_, n, true); + memcpy(res->storage_, storage_, res->block_count_ * sizeof(block_t)); + return res; + } + + size_t bitvect::hash() const + { + + block_t res = fnv::init(); + size_t i; + for (i = 0; i < block_count_ - 1; ++i) + { + res ^= storage_[i]; + res *= fnv::prime(); + } + // Deal with the last block, that might not be fully used. + // Compute the number n of bits used in the last block. + const size_t bpb = 8 * sizeof(bitvect::block_t); + size_t n = size() % bpb; + // Use only the least n bits from storage_[i]. + res ^= storage_[i] & ((1UL << n) - 1); + return res; + } + + bitvect* make_bitvect(size_t bitcount) + { + size_t n = block_needed(bitcount); + // Allocate some memory for the bitvect. The instance + // already contains one int of local_storage_, but + // we allocate n-1 more so that we store the table. + void* mem = operator new(sizeof(bitvect) + + (n - 1) * sizeof(bitvect::block_t)); + return new(mem) bitvect(bitcount, n); + } + + + bitvect_array* make_bitvect_array(size_t bitcount, size_t vectcount) + { + size_t n = block_needed(bitcount); + // Size of one bitvect. + size_t bvsize = sizeof(bitvect) + (n - 1) * sizeof(bitvect::block_t); + // Allocate the bitvect_array with enough space at the end + // to store all bitvect instances. + void* mem = operator new(sizeof(bitvect_array) + bvsize * vectcount); + bitvect_array* bva = new(mem) bitvect_array(vectcount, bvsize); + // Initialize all the bitvect instances. + for (size_t i = 0; i < vectcount; ++i) + new(bva->storage_ + i * bvsize) bitvect(bitcount, n); + return bva; + } + + std::ostream& operator<<(std::ostream& os , const bitvect& v) + { + for (size_t i = 0, end = v.size(); i != end; ++i) + os << (v.get(i) ? '1' : '0'); + return os; + } + + std::ostream& operator<<(std::ostream& os , const bitvect_array& a) + { + size_t end = a.size(); + if (end == 0) + { + os << "empty\n"; + return os; + } + int w = floor(log10(end - 1)) + 1; + for (size_t i = 0; i != end; ++i) + { + os.width(w); + os << i; + os.width(1); + os << ": " << a.at(i) << "\n"; + } + return os; + } +} diff --git a/src/misc/bitvect.hh b/src/misc/bitvect.hh new file mode 100644 index 000000000..361f9897f --- /dev/null +++ b/src/misc/bitvect.hh @@ -0,0 +1,473 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 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 . + +#ifndef SPOT_MISC_BITVECT_HH +# define SPOT_MISC_BITVECT_HH + +# include "common.hh" +# include +# include +# include +# include +# include +namespace spot +{ + /// \addtogroup misc_tools + /// @{ + + class SPOT_API bitvect; + class SPOT_API bitvect_array; + + ///\brief Allocate a bit-vector of \a bitcount bits. + /// + /// The resulting object should be released with delete. + SPOT_API bitvect* make_bitvect(size_t bitcount); + + /// \brief Allocate \a vectcount bit-vectors of \a bitcount bits. + /// + /// The resulting bitvect_array should be released with delete. + SPOT_API bitvect_array* make_bitvect_array(size_t bitcount, + size_t vectcount); + + /// \brief A bit vector + class SPOT_API bitvect + { + private: + // Used by make_bitvect to construct a large bitvect in place. + bitvect(size_t size, size_t block_count); + bitvect(size_t size, size_t block_count, bool); + + public: + typedef unsigned long block_t; + + bitvect(): + size_(0), + block_count_(1), + storage_(&local_storage_), + local_storage_(0) + { + } + + bitvect(const bitvect& other): + size_(other.size_), + block_count_(1), + storage_(&local_storage_) + { + *this = other; + } + + bitvect* clone() const; + + void make_empty() + { + size_ = 0; + } + + bitvect& operator=(const bitvect& other) + { + reserve_blocks(other.block_count_); + size_ = other.size(); + for (size_t i = 0; i < block_count_; ++i) + storage_[i] = other.storage_[i]; + return *this; + } + + ~bitvect() + { + if (storage_ != &local_storage_) + free(storage_); + } + + /// Grow the bitvector to \a new_block_count blocks. + /// + /// This only changes the capacity of the bitvector, not its size. + void reserve_blocks(size_t new_block_count) + { + if (new_block_count < block_count_) + return; + if (storage_ == &local_storage_) + { + block_t* new_storage_ = static_cast + (malloc(new_block_count * sizeof(block_t))); + for (size_t i = 0; i < block_count_; ++i) + new_storage_[i] = storage_[i]; + storage_ = new_storage_; + } + else + { + storage_ = static_cast + (realloc(storage_, new_block_count * sizeof(block_t))); + } + block_count_ = new_block_count; + } + + private: + void grow() + { + size_t new_block_count_ = (block_count_ + 1) * 7 / 5; + reserve_blocks(new_block_count_); + } + + public: + /// Append one bit. + void push_back(bool val) + { + if (size() == capacity()) + grow(); + size_t pos = size_++; + if (val) + set(pos); + else + clear(pos); + } + + /// \brief Append the lowest \a count bits of \a data. + void push_back(block_t data, unsigned count) + { + if (size() + count > capacity()) + grow(); + const size_t bpb = 8 * sizeof(block_t); + + // Clear the higher bits. + if (count != bpb) + data &= (1UL << count) - 1; + + size_t n = size() % bpb; + size_t i = size_ / bpb; + size_ += count; + if (n == 0) // Aligned on block_t boundary + { + storage_[i] = data; + } + else // Only (bpb-n) bits free in this block. + { + // Take the lower bpb-n bits of data... + block_t mask = (1UL << (bpb - n)) - 1; + block_t data1 = (data & mask) << n; + mask <<= n; + // ... write them on the higher bpb-n bits of last block. + storage_[i] = (storage_[i] & ~mask) | data1; + // Write the remaining bits in the next block. + if (bpb - n < count) + storage_[i + 1] = data >> (bpb - n); + } + } + + size_t size() const + { + return size_; + } + + size_t capacity() const + { + return 8 * block_count_ * sizeof(block_t); + } + + size_t hash() const; + + bool get(size_t pos) const + { + assert(pos < size_); + const size_t bpb = 8 * sizeof(block_t); + return storage_[pos / bpb] & (1UL << (pos % bpb)); + } + + void clear_all() + { + for (size_t i = 0; i < block_count_; ++i) + storage_[i] = 0; + } + + bool is_fully_clear() const + { + size_t i; + for (i = 0; i < block_count_ - 1; ++i) + if (storage_[i] != 0) + return false; + // The last block might not be fully used, compare only the + // relevant portion. + const size_t bpb = 8 * sizeof(bitvect::block_t); + block_t mask = (1UL << (size() % bpb)) - 1; + return (storage_[i] & mask) == 0; + } + + bool is_fully_set() const + { + size_t i; + for (i = 0; i < block_count_ - 1; ++i) + if (storage_[i] != -1UL) + return false; + // The last block might not be fully used, compare only the + // relevant portion. + const size_t bpb = 8 * sizeof(bitvect::block_t); + block_t mask = (1UL << (size() % bpb)) - 1; + return ((~storage_[i]) & mask) == 0; + } + + void set_all() + { + for (size_t i = 0; i < block_count_; ++i) + storage_[i] = -1UL; + } + + void flip_all() + { + for (size_t i = 0; i < block_count_; ++i) + storage_[i] = ~storage_[i]; + } + + void set(size_t pos) + { + assert(pos < size_); + const size_t bpb = 8 * sizeof(block_t); + storage_[pos / bpb] |= 1UL << (pos % bpb); + } + + void clear(size_t pos) + { + assert(pos < size_); + const size_t bpb = 8 * sizeof(block_t); + storage_[pos / bpb] &= ~(1UL << (pos % bpb)); + } + + void flip(size_t pos) + { + assert(pos < size_); + const size_t bpb = 8 * sizeof(block_t); + storage_[pos / bpb] ^= (1UL << (pos % bpb)); + } + + + bitvect& operator|=(const bitvect& other) + { + assert(other.block_count_ <= block_count_); + for (size_t i = 0; i < other.block_count_; ++i) + storage_[i] |= other.storage_[i]; + return *this; + } + + bitvect& operator&=(const bitvect& other) + { + assert(other.block_count_ <= block_count_); + for (size_t i = 0; i < other.block_count_; ++i) + storage_[i] &= other.storage_[i]; + return *this; + } + + bitvect& operator^=(const bitvect& other) + { + assert(other.block_count_ <= block_count_); + for (size_t i = 0; i < other.block_count_; ++i) + storage_[i] ^= other.storage_[i]; + return *this; + } + + bitvect& operator-=(const bitvect& other) + { + assert(other.block_count_ <= block_count_); + for (size_t i = 0; i < other.block_count_; ++i) + storage_[i] &= ~other.storage_[i]; + return *this; + } + + bool operator==(const bitvect& other) const + { + if (other.block_count_ != block_count_) + return false; + size_t i; + for (i = 0; i < other.block_count_ - 1; ++i) + if (storage_[i] != other.storage_[i]) + return false; + // The last block might not be fully used, compare only the + // relevant portion. + const size_t bpb = 8 * sizeof(bitvect::block_t); + block_t mask = (1UL << (size() % bpb)) - 1; + return (storage_[i] & mask) == (other.storage_[i] & mask); + } + + bool operator!=(const bitvect& other) const + { + return !(*this == other); + } + + bool operator<(const bitvect& other) const + { + if (block_count_ != other.block_count_) + return block_count_ < other.block_count_; + size_t i; + for (i = 0; i < other.block_count_ - 1; ++i) + if (storage_[i] > other.storage_[i]) + return false; + // The last block might not be fully used, compare only the + // relevant portion. + const size_t bpb = 8 * sizeof(bitvect::block_t); + block_t mask = (1UL << (size() % bpb)) - 1; + return (storage_[i] & mask) < (other.storage_[i] & mask); + } + + bool operator>=(const bitvect& other) const + { + return !(*this < other); + } + + bool operator>(const bitvect& other) const + { + return other < *this; + } + + bool operator<=(const bitvect& other) const + { + return !(other < *this); + } + + // \brief Extract a range of bits. + // + // Build a new bit-vector using the bits from \a begin (included) + // to \a end (excluded). + bitvect* extract_range(size_t begin, size_t end) + { + assert(begin <= end); + assert(end <= size()); + size_t count = end - begin; + bitvect* res = make_bitvect(count); + res->make_empty(); + + if (end == begin) + return res; + + const size_t bpb = 8 * sizeof(bitvect::block_t); + + size_t indexb = begin / bpb; + unsigned bitb = begin % bpb; + size_t indexe = (end - 1) / bpb; + + if (indexb == indexe) + { + block_t data = storage_[indexb]; + data >>= bitb; + res->push_back(data, count); + } + else + { + block_t data = storage_[indexb]; + data >>= bitb; + res->push_back(data, bpb - bitb); + count -= bpb - bitb; + while (count >= bpb) + { + ++indexb; + res->push_back(storage_[indexb], bpb); + count -= bpb; + assert(indexb != indexe || bpb == 0); + } + if (count > 0) + { + ++indexb; + assert(indexb == indexe); + assert(count == end % bpb); + res->push_back(storage_[indexb], count); + } + } + return res; + } + + friend SPOT_API bitvect* + ::spot::make_bitvect(size_t bitcount); + + /// Print a bitvect. + friend SPOT_API std::ostream& operator<<(std::ostream&, + const bitvect&); + + private: + friend SPOT_API bitvect_array* + ::spot::make_bitvect_array(size_t bitcount, + size_t vectcount); + + size_t size_; + size_t block_count_; + // storage_ points to local_storage_ as long as size_ <= block_count_ * 8. + block_t* storage_; + // Keep this at the end of the structure: when make_bitvect is used, + // it may allocate more block_t at the end of this structure. + block_t local_storage_; + }; + + class SPOT_API bitvect_array + { + private: + /// Private constructor used by make_bitvect_array(). + bitvect_array(size_t size, size_t bvsize): + size_(size), + bvsize_(bvsize) + { + } + + /// Not implemented. + SPOT_LOCAL bitvect_array(const bitvect_array&); + /// Not implemented. + SPOT_LOCAL void operator=(const bitvect_array&); + + + public: + ~bitvect_array() + { + for (size_t i = 0; i < size_; ++i) + at(i).~bitvect(); + } + + /// The number of bitvect in the array. + size_t size() const + { + return size_; + } + + /// Return the bit-vector at \a index. + bitvect& at(const size_t index) + { + assert(index < size_); + return *reinterpret_cast(storage_ + index * bvsize_); + } + + /// Return the bit-vector at \a index. + const bitvect& at(const size_t index) const + { + assert(index < size_); + return *reinterpret_cast(storage_ + index * bvsize_); + } + + friend SPOT_API bitvect_array* + ::spot::make_bitvect_array(size_t bitcount, + size_t vectcount); + + + /// Print a bitvect_array. + friend SPOT_API std::ostream& operator<<(std::ostream&, + const bitvect_array&); + + private: + size_t size_; + size_t bvsize_; + char storage_[0]; + }; + + /// @} +} + + +#endif // SPOT_MISC_BITVECT_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 073467851..b6ab29824 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -31,6 +31,7 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ bddprod \ + bitvect \ complement \ explicit \ explicit2 \ @@ -48,6 +49,7 @@ check_PROGRAMS = \ # Keep this sorted alphabetically. bddprod_SOURCES = ltlprod.cc bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT +bitvect_SOURCES = bitvect.cc complement_SOURCES = complementation.cc explicit_SOURCES = explicit.cc explicit2_SOURCES = explicit2.cc @@ -69,6 +71,7 @@ tripprod_SOURCES = tripprod.cc # because such failures will be easier to diagnose and fix. TESTS = \ intvcomp.test \ + bitvect.test \ eltl2tgba.test \ explicit.test \ explicit2.test \ diff --git a/src/tgbatest/bitvect.cc b/src/tgbatest/bitvect.cc new file mode 100644 index 000000000..4cd758a27 --- /dev/null +++ b/src/tgbatest/bitvect.cc @@ -0,0 +1,133 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013 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 +#include "misc/bitvect.hh" + +void ruler() +{ + std::cout << "\n "; + for (size_t x = 0; x < 76; ++x) + if (x % 10 == 0) + std::cout << x / 10; + else + std::cout << "_"; + std::cout << "\n "; + for (size_t x = 0; x < 76; ++x) + std::cout << x % 10; + std::cout << "\n\n"; +} + +#define ECHO(name) std::cout << #name": " << *name << "\n" + +int main() +{ + ruler(); + spot::bitvect* v = spot::make_bitvect(15); + ECHO(v); + v->set(10); + v->set(7); + v->set(12); + ECHO(v); + + ruler(); + spot::bitvect* w = spot::make_bitvect(42); + w->set(30); + w->set(41); + w->set(13); + w->set(7); + ECHO(w); + *w ^= *v; + ECHO(w); + + ruler(); + spot::bitvect* x = spot::make_bitvect(75); + x->set(70); + x->set(60); + ECHO(x); + *x |= *w; + ECHO(x); + + for (size_t i = 0; i < 30; ++i) + w->push_back((i & 3) == 0); + ECHO(w); + *x &= *w; + ECHO(x); + x->set_all(); + ECHO(x); + + ruler(); + + w->push_back(0x09, 4); + ECHO(w); + spot::bitvect* y = w->extract_range(0, 71); + ECHO(y); + delete y; + y = w->extract_range(0, 64); + ECHO(y); + delete y; + y = w->extract_range(64, 75); + ECHO(y); + delete y; + y = w->extract_range(0, 75); + ECHO(y); + delete y; + y = w->extract_range(7, 64); + ECHO(y); + delete y; + y = w->extract_range(7, 72); + ECHO(y); + delete y; + + delete v; + delete w; + delete x; + + ruler(); + + spot::bitvect_array* a = spot::make_bitvect_array(60, 10); + for (size_t y = 0; y < a->size(); ++y) + for (size_t x = 0; x < 60; ++x) + { + if (((x ^ y) & 3) < 2) + a->at(y).set(x); + } + std::cout << *a; + + ruler(); + + for (size_t i = 0; i < 12; ++i) + a->at(4).push_back((i & 2) == 0); + a->at(6) = a->at(4); + a->at(8) = a->at(7); + a->at(6) ^= a->at(8); + + std::cout << *a; + + std::cout << "Comp: " + << (a->at(0) == a->at(1)) + << (a->at(0) == a->at(2)) + << (a->at(1) != a->at(2)) + << (a->at(0) < a->at(2)) + << (a->at(0) > a->at(2)) + << (a->at(3) < a->at(4)) + << (a->at(5) > a->at(6)) << std::endl; + + delete a; +} diff --git a/src/tgbatest/bitvect.test b/src/tgbatest/bitvect.test new file mode 100755 index 000000000..5407f5929 --- /dev/null +++ b/src/tgbatest/bitvect.test @@ -0,0 +1,90 @@ +#!/bin/sh +# Copyright (C) 2013 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 . + + +. ./defs + +set -e + +run 0 ../bitvect | tee stderr +cat >expected <