diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-13 12:26:52 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-13 12:26:52 -0800 |
commit | 4e50d35447b5ee07304d2b857af388ea569db98b (patch) | |
tree | 7eb2497463ad1807dd0153b7e60c909f70cabb8d /src/expr | |
parent | 81a2e226251bea677f6a920004e846a08072c851 (diff) |
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`.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.h | 17 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 34 |
2 files changed, 45 insertions, 6 deletions
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 ======================================================= |