From: Tim King <taking@cs.nyu.edu>
Date: Wed, 29 Aug 2018 17:27:57 +0000 (-0700)
Subject: Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
X-Git-Tag: cvc5-1.0.0~4699
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ae13e7e30aaaa088de057496c649649067867dc;p=cvc5.git

Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)
---

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index e474c3dfb..c6dc66eb2 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -23,6 +23,7 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 
+#include <cstdint>
 #include <unordered_map>
 
 namespace CVC4 {
@@ -107,6 +108,14 @@ struct KindValueToTableValueMapping {
 
 namespace attr {
 
+// Returns a 64 bit integer with a single `bit` set when `bit` < 64.
+// Avoids problems in (1 << x) when sizeof(x) <= sizeof(uint64_t).
+inline uint64_t GetBitSet(uint64_t bit)
+{
+  constexpr uint64_t kOne = 1;
+  return kOne << bit;
+}
+
 /**
  * An "AttrHash<value_type>"---the hash table underlying
  * attributes---is simply a mapping of pair<unique-attribute-id, Node>
@@ -141,30 +150,24 @@ class AttrHash<bool> :
 
     uint64_t& d_word;
 
-    unsigned d_bit;
-
-  public:
+    uint64_t d_bit;
 
-    BitAccessor(uint64_t& word, unsigned bit) :
-      d_word(word),
-      d_bit(bit) {
-    }
+   public:
+    BitAccessor(uint64_t& word, uint64_t bit) : d_word(word), d_bit(bit) {}
 
     BitAccessor& operator=(bool b) {
       if(b) {
         // set the bit
-        d_word |= (1 << d_bit);
+        d_word |= GetBitSet(d_bit);
       } else {
         // clear the bit
-        d_word &= ~(1 << d_bit);
+        d_word &= ~GetBitSet(d_bit);
       }
 
       return *this;
     }
 
-    operator bool() const {
-      return (d_word & (1 << d_bit)) ? true : false;
-    }
+    operator bool() const { return (d_word & GetBitSet(d_bit)) ? true : false; }
   };/* class AttrHash<bool>::BitAccessor */
 
   /**
@@ -177,18 +180,18 @@ class AttrHash<bool> :
 
     std::pair<NodeValue* const, uint64_t>* d_entry;
 
-    unsigned d_bit;
+    uint64_t d_bit;
 
-  public:
+   public:
 
     BitIterator() :
       d_entry(NULL),
       d_bit(0) {
     }
 
-    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
-      d_entry(&entry),
-      d_bit(bit) {
+    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, uint64_t bit)
+        : d_entry(&entry), d_bit(bit)
+    {
     }
 
     std::pair<NodeValue* const, BitAccessor> operator*() {
@@ -211,9 +214,9 @@ class AttrHash<bool> :
 
     const std::pair<NodeValue* const, uint64_t>* d_entry;
 
-    unsigned d_bit;
+    uint64_t d_bit;
 
-  public:
+   public:
 
     ConstBitIterator() :
       d_entry(NULL),
@@ -221,14 +224,15 @@ class AttrHash<bool> :
     }
 
     ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
-                     unsigned bit) :
-      d_entry(&entry),
-      d_bit(bit) {
+                     uint64_t bit)
+        : d_entry(&entry), d_bit(bit)
+    {
     }
 
-    std::pair<NodeValue* const, bool> operator*() {
-      return std::make_pair(d_entry->first,
-                            (d_entry->second & (1 << d_bit)) ? true : false);
+    std::pair<NodeValue* const, bool> operator*()
+    {
+      return std::make_pair(
+          d_entry->first, (d_entry->second & GetBitSet(d_bit)) ? true : false);
     }
 
     bool operator==(const ConstBitIterator& b) {
@@ -260,8 +264,8 @@ public:
     Debug.printf("boolattr",
                  "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                  &(*i).second,
-                 (unsigned long long)((*i).second),
-                 unsigned(k.first));
+                 (uint64_t)((*i).second),
+                 uint64_t(k.first));
     */
     return BitIterator(*i, k.first);
   }
@@ -284,8 +288,8 @@ public:
     Debug.printf("boolattr",
                  "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                  &(*i).second,
-                 (unsigned long long)((*i).second),
-                 unsigned(k.first));
+                 (uint64_t)((*i).second),
+                 uint64_t(k.first));
     */
     return ConstBitIterator(*i, k.first);
   }