enable conversion from irep_idt to enum class

Author: kroening

src/util/dstring.h

@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 /// \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,
@@ -29,10 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// `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
@@ -151,7 +148,7 @@ class dstringt final
     return no;
   }
 
-private:
+protected:
   #ifdef __GNUC__
   constexpr
   #endif

src/util/irep.h

@@ -29,8 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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

@@ -43,19 +43,80 @@ 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 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();
+  }
+};
+}
+
 #ifdef __GNUC__
 #define IREP_ID_ONE(the_id)                                         \
-  constexpr dstringt ID_##the_id=dstringt::make_from_table_index(   \
+  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 dstringt ID_##the_id=dstringt::make_from_table_index(   \
+  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(       \
+  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 dstringt ID_##the_id=dstringt::make_from_table_index( \
+  const const irep_idt ID_##the_id=irep_idt::make_from_table_index( \
       static_cast<unsigned>(idt::id_##the_id));
 #endif