enable conversion from irep_idt to enum class

Author: Daniel Kroening

src/util/dstring.h

@@ -21,7 +21,7 @@ Author: Daniel Kroening, [email protected]
 
 /// \ref dstringt has one field, an unsigned integer \ref no which is an index
 /// into a static table of strings. This makes it expensive to create a new
-/// string(because you have to look through the whole table to see if it is
+/// string (because you have to look through the whole table to see if it is
 /// already there, and add it if it isn't) but very cheap to compare strings
 /// (just compare the two integers). It also means that when you have lots of
 /// copies of the same string you only have to store the whole string once,
@@ -30,10 +30,7 @@ Author: Daniel Kroening, [email protected]
 /// `irep_idt` and `irep_namet` are typedef-ed to \ref dstringt in irep.h unless
 /// `USE_STD_STRING` is set.
 ///
-///
-/// Note: Marked final to disable inheritance. No virtual destructor, so
-/// runtime-polymorphic use would be unsafe.
-class dstringt final
+class dstringt
 {
 public:
   // this is safe for static objects
@@ -183,8 +180,8 @@ class dstringt final
     return as_string().end();
   }
 
-private:
-  #ifdef __GNUC__
+protected:
+#ifdef __GNUC__
   constexpr
   #endif
   explicit dstringt(unsigned _no):no(_no)

src/util/irep.h

@@ -27,8 +27,7 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #ifdef USE_DSTRING
-typedef dstringt irep_idt;
-typedef dstringt irep_namet;
+typedef irep_idt irep_namet;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef dstring_hash irep_id_hash;
 #else

src/util/irep_ids.h

@@ -44,20 +44,97 @@ enum class idt : unsigned
 #include "irep_ids.def" // NOLINT(build/include)
 };
 
+class irep_idt final : public dstringt
+{
+public:
+// this is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    irep_idt()
+    : dstringt()
+  {
+  }
+
+// this is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    static irep_idt
+    make_from_table_index(unsigned no)
+  {
+    return irep_idt(no);
+  }
+
+#ifdef __GNUC__
+  // This conversion allows the use of irep_idts
+  // in switch ... case statements.
+  constexpr operator idt() const
+  {
+    return static_cast<idt>(no);
+  }
+#endif
+
+  // this one is safe for static objects
+#ifdef __GNUC__
+  constexpr
+#endif
+    // NOLINTNEXTLINE(runtime/explicit)
+    irep_idt(dstringt s)
+    : dstringt(s)
+  {
+  }
+
+  // this one is not safe for static objects
+  // NOLINTNEXTLINE(runtime/explicit)
+  irep_idt(const char *s) : dstringt(s)
+  {
+  }
+
+  // this one is not safe for static objects
+  // NOLINTNEXTLINE(runtime/explicit)
+  irep_idt(const std::string &s) : dstringt(s)
+  {
+  }
+
+protected:
+#ifdef __GNUC__
+  constexpr
+#endif
+    explicit irep_idt(unsigned _no)
+    : dstringt(_no)
+  {
+  }
+};
+
+// NOLINTNEXTLINE [allow specialisation within 'std']
+namespace std
+{
+/// Default hash function of `dstringt` for use with STL containers.
+template <>
+struct hash<irep_idt> // NOLINT(readability/identifiers)
+{
+  size_t operator()(const irep_idt &irep_id) const
+  {
+    return irep_id.hash();
+  }
+};
+} // namespace std
+
 #ifdef __GNUC__
-#define IREP_ID_ONE(the_id)                                         \
-  constexpr dstringt ID_##the_id=dstringt::make_from_table_index(   \
-      static_cast<unsigned>(idt::id_##the_id));
-#define IREP_ID_TWO(the_id, str)                                    \
-  constexpr dstringt ID_##the_id=dstringt::make_from_table_index(   \
-      static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_ONE(the_id)                                                    \
+  constexpr irep_idt ID_##the_id =                                             \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_TWO(the_id, str)                                               \
+  constexpr irep_idt ID_##the_id =                                             \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
 #else
-#define IREP_ID_ONE(the_id)                                         \
-  const dstringt ID_##the_id=dstringt::make_from_table_index(       \
-      static_cast<unsigned>(idt::id_##the_id));
-#define IREP_ID_TWO(the_id, str)                                    \
-  const const dstringt ID_##the_id=dstringt::make_from_table_index( \
-      static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_ONE(the_id)                                                    \
+  const irep_idt ID_##the_id =                                                 \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
+#define IREP_ID_TWO(the_id, str)                                               \
+  const const irep_idt ID_##the_id =                                           \
+    irep_idt::make_from_table_index(static_cast<unsigned>(idt::id_##the_id));
 #endif
 
 template <>