From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 13 Jan 2020 20:26:52 +0000 (-0800)
Subject: Support arbitrary unsigned integer attributes (#3591)
X-Git-Tag: cvc5-1.0.0~3737
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e50d35447b5ee07304d2b857af388ea569db98b;p=cvc5.git

Support arbitrary unsigned integer attributes (#3591)

Fixes #3586. On macOS, `size_t` resolves to `unsigned long` whereas `uint64_t`
resolves to `unsigned long long`. Even though the types have the same bit-width
and signedness, they are not considered the same type. This caused issues with
`Attribute`s that store `size_t` values because we only specialized the
`getTable()` struct for `uint64_t`. This commit changes the specialization to
work for arbitrary unsigned integer types of at most 64-bit. It does that by
generalizing the specialization of `getTable()` and by implementing a
`KindValueToTableValueMapping` for unsigned integer attributes of up to 64-bit
that casts integers between the attributes bit-width and `uint64_t`.
---

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 46302fc9f..44bf7aae5 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -61,7 +61,7 @@ class AttributeManager {
    * getTable<> is a helper template that gets the right table from an
    * AttributeManager given its type.
    */
-  template <class T, bool context_dep>
+  template <class T, bool context_dep, class Enable>
   friend struct getTable;
 
   bool d_inGarbageCollection;
@@ -190,8 +190,13 @@ namespace attr {
 /**
  * The getTable<> template provides (static) access to the
  * AttributeManager field holding the table.
+ *
+ * The `Enable` template parameter is used to instantiate the template
+ * conditionally: If the template substitution of Enable fails (e.g. when using
+ * `std::enable_if` in the template parameter and the condition is false), the
+ * instantiation is ignored due to the SFINAE rule.
  */
-template <class T, bool context_dep>
+template <class T, bool context_dep, class Enable = void>
 struct getTable;
 
 /** Access the "d_bools" member of AttributeManager. */
@@ -208,8 +213,12 @@ struct getTable<bool, false> {
 };
 
 /** Access the "d_ints" member of AttributeManager. */
-template <>
-struct getTable<uint64_t, false> {
+template <class T>
+struct getTable<T,
+                false,
+                // Use this specialization only for unsigned integers
+                typename std::enable_if<std::is_unsigned<T>::value>::type>
+{
   static const AttrTableId id = AttrTableUInt64;
   typedef AttrHash<uint64_t> table_type;
   static inline table_type& get(AttributeManager& am) {
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index bc34324b0..94d51b188 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -91,9 +91,15 @@ namespace attr {
  *
  * This general (non-specialized) implementation of the template does
  * nothing.
+ *
+ * The `Enable` template parameter is used to instantiate the template
+ * conditionally: If the template substitution of Enable fails (e.g. when using
+ * `std::enable_if` in the template parameter and the condition is false), the
+ * instantiation is ignored due to the SFINAE rule.
  */
-template <class T>
-struct KindValueToTableValueMapping {
+template <class T, class Enable = void>
+struct KindValueToTableValueMapping
+{
   /** Simple case: T == table_value_type */
   typedef T table_value_type;
   /** No conversion necessary */
@@ -102,6 +108,30 @@ struct KindValueToTableValueMapping {
   inline static T convertBack(const T& t) { return t; }
 };
 
+/**
+ * This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit
+ * integers s.t. they can be stored in the hash table for integral-valued
+ * attributes.
+ */
+template <class T>
+struct KindValueToTableValueMapping<
+    T,
+    // Use this specialization only for unsigned integers
+    typename std::enable_if<std::is_unsigned<T>::value>::type>
+{
+  typedef uint64_t table_value_type;
+  /** Convert from unsigned integer to uint64_t */
+  static uint64_t convert(const T& t)
+  {
+    static_assert(sizeof(T) <= sizeof(uint64_t),
+                  "Cannot store integer attributes of a bit-width that is "
+                  "greater than 64-bits");
+    return static_cast<uint64_t>(t);
+  }
+  /** Convert from uint64_t to unsigned integer */
+  static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
+};
+
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE HASH TABLES =======================================================