From 7daea8d3cb7a7104285b30bfebfa3c14438b4789 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 13 Feb 2015 18:44:46 +0100
Subject: [PATCH] bitvect: Fix routines for 64-width vectors

* src/misc/bitvect.hh: Here.
* src/tgbatest/det.test, src/ltltest/ltlfilt.test: Add test cases.
---
 src/ltltest/ltlfilt.test |  6 ++++++
 src/misc/bitvect.hh      | 45 ++++++++++++++++++++++++++--------------
 src/tgbatest/det.test    | 17 +++++++++++++++
 3 files changed, 53 insertions(+), 15 deletions(-)

diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test
index 5a057ba2f..6af667b97 100755
--- a/src/ltltest/ltlfilt.test
+++ b/src/ltltest/ltlfilt.test
@@ -179,3 +179,9 @@ grep 'invalid' stderr
 
 SPOT_STUTTER_CHECK=5 \
 ../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}'
+
+# This one was incorrectly diagnosed as stutter invariant because of a
+# bug in the bitvectors.
+../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
+
+true
diff --git a/src/misc/bitvect.hh b/src/misc/bitvect.hh
index 48310b160..43612d056 100644
--- a/src/misc/bitvect.hh
+++ b/src/misc/bitvect.hh
@@ -206,26 +206,32 @@ namespace spot
     bool is_fully_clear() const
     {
       size_t i;
-      for (i = 0; i < block_count_ - 1; ++i)
+      const size_t bpb = 8 * sizeof(bitvect::block_t);
+      size_t rest = size() % bpb;
+      for (i = 0; i < block_count_ - !!rest; ++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;
+      if (!rest)
+	return true;
+      block_t mask = (1UL << rest) - 1;
       return (storage_[i] & mask) == 0;
     }
 
     bool is_fully_set() const
     {
       size_t i;
-      for (i = 0; i < block_count_ - 1; ++i)
+      const size_t bpb = 8 * sizeof(bitvect::block_t);
+      size_t rest = size() % bpb;
+      for (i = 0; i < block_count_ - !!rest; ++i)
 	if (storage_[i] != -1UL)
 	  return false;
+      if (!rest)
+	return true;
       // 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;
+      block_t mask = (1UL << rest) - 1;
       return ((~storage_[i]) & mask) == 0;
     }
 
@@ -303,14 +309,17 @@ namespace spot
       assert(other.block_count_ >= block_count_);
 
       size_t i;
-      for (i = 0; i < block_count_ - 1; ++i)
+      const size_t bpb = 8 * sizeof(bitvect::block_t);
+      size_t rest = size() % bpb;
+      for (i = 0; i < block_count_ - !!rest; ++i)
 	if ((storage_[i] & other.storage_[i]) != other.storage_[i])
 	  return false;
+      if (!rest)
+	return true;
 
       // 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;
+      block_t mask = (1UL << rest) - 1;
       return ((storage_[i] & mask & other.storage_[i])
 	      == (other.storage_[i] & mask));
     }
@@ -323,13 +332,16 @@ namespace spot
 	return true;
       size_t i;
       size_t m = other.used_blocks();
-      for (i = 0; i < m - 1; ++i)
+      const size_t bpb = 8 * sizeof(bitvect::block_t);
+      size_t rest = size() % bpb;
+      for (i = 0; i < m - !!rest; ++i)
 	if (storage_[i] != other.storage_[i])
 	  return false;
+      if (!rest)
+	return true;
       // 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;
+      block_t mask = (1UL << rest) - 1;
       return (storage_[i] & mask) == (other.storage_[i] & mask);
     }
 
@@ -346,13 +358,16 @@ namespace spot
 	return false;
       size_t i;
       size_t m = other.used_blocks();
-      for (i = 0; i < m - 1; ++i)
+      const size_t bpb = 8 * sizeof(bitvect::block_t);
+      size_t rest = size() % bpb;
+      for (i = 0; i < m - !!rest; ++i)
 	if (storage_[i] > other.storage_[i])
 	  return false;
+      if (!rest)
+	return true;
       // 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;
+      block_t mask = (1UL << rest) - 1;
       return (storage_[i] & mask) < (other.storage_[i] & mask);
     }
 
diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test
index 641eaa345..5d98c5b9d 100755
--- a/src/tgbatest/det.test
+++ b/src/tgbatest/det.test
@@ -151,4 +151,21 @@ diff out.tgba ex.tgba
 run 0 ../../bin/ltl2tgba -H '(0 R Xa) R (a xor Fa)' > out.hoa
 grep deterministic out.hoa && exit 1
 
+
+# These highlighted a bug in the bitvector routines because their
+# state count is a multiple of 64.
+cat >input <<EOF
+G(!a | Xa),2
+G(!a | XXa),4
+G(!a | XXXa),8
+G(!a | XXXXa),16
+G(!a | XXXXXa),32
+G(!a | XXXXXXa),64
+G(!a | XXXXXXXa),128
+G(!a | XXXXXXXXa),256
+EOF
+run 0 ../../bin/ltl2tgba -D -F input/1 --stats='%f,%s' > output
+cat output
+diff input output
+
 true