Remove irep_namet

It is impossible for irep_namet to be different from irep_idt as
irep_ids.h creates dstringt/std::string constants, which will then be
used

1) as arguments to irept::get, which requires an irep_namet, hence
irep_namet must be the same type as whichever irep_ids.h generates;
2) in equality tests comparing to irept::id(), hence irep_idt must be
the same type as whichever irep_ids.h generates.

While all of this may be fixable (by providing suitable operators for
whatever type irep_ids.h generates), we do not seem to use irep_namet
anywhere other than irep.{h,cpp}, and will most likely run into many
implicit assumptions that irep_idt and irep_namet are the same type.

Author: tautschnig

src/cpp/cpp_type2name.cpp

@@ -61,7 +61,7 @@ static std::string irep2name(const irept &irep)
       else
         result += ',';
 
-      result += do_prefix(name2string(named_sub.first));
+      result += do_prefix(id2string(named_sub.first));
 
       result += '=';
       result += irep2name(named_sub.second);
@@ -78,7 +78,7 @@ static std::string irep2name(const irept &irep)
         first=false;
       else
         result+=',';
-      result += do_prefix(name2string(named_sub.first));
+      result += do_prefix(id2string(named_sub.first));
       result+='=';
       result += irep2name(named_sub.second);
     }

src/util/README.md

@@ -72,14 +72,12 @@ standard data structures as in irept.
 
 \subsection irep_idt_section Strings: dstringt, the string_container and the ID_*
 
-Within cbmc, strings are represented using \ref irep_idt or \ref irep_namet
-for keys to [named_sub](\ref irept::dt::named_sub). By default these are both
-typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`,
-in which case they are both typedefed to `std::string`. You can also easily
-convert an [irep_idt](\ref irep_idt) or [irep_namet](\ref irep_namet) to a
-`std::string` using the [id2string](\ref id2string) or
-[name2string](\ref name2string) function, respectively, or either of them to a
-`char*` using the [c_str()](\ref dstringt::c_str) member function.
+Within cbmc, strings are represented using \ref irep_idt. By default this is
+typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING`
+to change this typedef to `std::string`. You can also easily convert an
+[irep_idt](\ref irep_idt) to a `std::string` using the
+[id2string](\ref id2string) function, or to a `char*` using the
+[c_str()](\ref dstringt::c_str) member function.
 
 \ref dstringt stores a string as an index into a large
 static table of strings. This makes it easy to compare if two

src/util/dstring.h

@@ -27,8 +27,8 @@ Author: Daniel Kroening, [email protected]
 /// copies of the same string you only have to store the whole string once,
 /// which saves space.
 ///
-/// `irep_idt` and `irep_namet` are typedef-ed to \ref dstringt in irep.h unless
-/// `USE_STD_STRING` is set.
+/// `irep_idt` is typedef-ed to \ref dstringt in irep.h unless `USE_STD_STRING`
+/// is set.
 ///
 ///
 /// Note: Marked final to disable inheritance. No virtual destructor, so

src/util/irep.cpp

@@ -24,7 +24,7 @@ const irept &get_nil_irep()
   return nil_rep_storage;
 }
 
-void irept::move_to_named_sub(const irep_namet &name, irept &irep)
+void irept::move_to_named_sub(const irep_idt &name, irept &irep)
 {
   #ifdef SHARING
   detach();
@@ -42,7 +42,7 @@ void irept::move_to_sub(irept &irep)
   get_sub().back().swap(irep);
 }
 
-const irep_idt &irept::get(const irep_namet &name) const
+const irep_idt &irept::get(const irep_idt &name) const
 {
   const named_subt &s = get_named_sub();
   named_subt::const_iterator it=s.find(name);
@@ -55,27 +55,27 @@ const irep_idt &irept::get(const irep_namet &name) const
   return it->second.id();
 }
 
-bool irept::get_bool(const irep_namet &name) const
+bool irept::get_bool(const irep_idt &name) const
 {
   return get(name)==ID_1;
 }
 
-int irept::get_int(const irep_namet &name) const
+int irept::get_int(const irep_idt &name) const
 {
   return unsafe_string2int(get_string(name));
 }
 
-std::size_t irept::get_size_t(const irep_namet &name) const
+std::size_t irept::get_size_t(const irep_idt &name) const
 {
   return unsafe_string2size_t(get_string(name));
 }
 
-long long irept::get_long_long(const irep_namet &name) const
+long long irept::get_long_long(const irep_idt &name) const
 {
   return unsafe_string2signedlonglong(get_string(name));
 }
 
-void irept::set(const irep_namet &name, const long long value)
+void irept::set(const irep_idt &name, const long long value)
 {
 #ifdef USE_DSTRING
   add(name).id(to_dstring(value));
@@ -84,7 +84,7 @@ void irept::set(const irep_namet &name, const long long value)
 #endif
 }
 
-void irept::set_size_t(const irep_namet &name, const std::size_t value)
+void irept::set_size_t(const irep_idt &name, const std::size_t value)
 {
 #ifdef USE_DSTRING
   add(name).id(to_dstring(value));
@@ -93,7 +93,7 @@ void irept::set_size_t(const irep_namet &name, const std::size_t value)
 #endif
 }
 
-void irept::remove(const irep_namet &name)
+void irept::remove(const irep_idt &name)
 {
 #if NAMED_SUB_IS_FORWARD_LIST
   return get_named_sub().remove(name);
@@ -103,7 +103,7 @@ void irept::remove(const irep_namet &name)
 #endif
 }
 
-const irept &irept::find(const irep_namet &name) const
+const irept &irept::find(const irep_idt &name) const
 {
   const named_subt &s = get_named_sub();
   auto it = s.find(name);
@@ -113,13 +113,13 @@ const irept &irept::find(const irep_namet &name) const
   return it->second;
 }
 
-irept &irept::add(const irep_namet &name)
+irept &irept::add(const irep_idt &name)
 {
   named_subt &s = get_named_sub();
   return s[name];
 }
 
-irept &irept::add(const irep_namet &name, irept irep)
+irept &irept::add(const irep_idt &name, irept irep)
 {
   named_subt &s = get_named_sub();
 

src/util/irep.h

@@ -35,13 +35,11 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef USE_DSTRING
 typedef dstringt irep_idt;
-typedef dstringt irep_namet;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef dstring_hash irep_id_hash;
 #else
 #include "string_hash.h"
 typedef std::string irep_idt;
-typedef std::string irep_namet;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef string_hash irep_id_hash;
 #endif
@@ -55,15 +53,6 @@ inline const std::string &id2string(const irep_idt &d)
   #endif
 }
 
-inline const std::string &name2string(const irep_namet &n)
-{
-  #ifdef USE_DSTRING
-  return as_string(n);
-  #else
-  return n;
-  #endif
-}
-
 #ifdef IREP_DEBUG
 #include <iostream>
 #endif
@@ -91,7 +80,7 @@ struct ref_count_ift<true>
 ///   actually a \ref dstringt and thus an integer which is a reference into a
 ///   string table.)
 ///
-/// * \ref irept::dt::named_sub : A map from `irep_namet` (a string) to \ref
+/// * \ref irept::dt::named_sub : A map from `irep_idt` (a string) to \ref
 ///   irept. This is used for named children, i.e.  subexpressions, parameters,
 ///   etc. Children whose name begins with '#' are ignored by the
 ///   default \ref operator==.
@@ -376,9 +365,9 @@ class irept
       irept,
 #endif
 #if NAMED_SUB_IS_FORWARD_LIST
-      forward_list_as_mapt<irep_namet, irept>>
+      forward_list_as_mapt<irep_idt, irept>>
 #else
-      std::map<irep_namet, irept>>
+      std::map<irep_idt, irept>>
 #endif
 {
 public:
@@ -413,35 +402,35 @@ class irept
   void id(const irep_idt &_data)
   { write().data=_data; }
 
-  const irept &find(const irep_namet &name) const;
-  irept &add(const irep_namet &name);
-  irept &add(const irep_namet &name, irept irep);
+  const irept &find(const irep_idt &name) const;
+  irept &add(const irep_idt &name);
+  irept &add(const irep_idt &name, irept irep);
 
-  const std::string &get_string(const irep_namet &name) const
+  const std::string &get_string(const irep_idt &name) const
   {
     return id2string(get(name));
   }
 
-  const irep_idt &get(const irep_namet &name) const;
-  bool get_bool(const irep_namet &name) const;
-  signed int get_int(const irep_namet &name) const;
-  std::size_t get_size_t(const irep_namet &name) const;
-  long long get_long_long(const irep_namet &name) const;
+  const irep_idt &get(const irep_idt &name) const;
+  bool get_bool(const irep_idt &name) const;
+  signed int get_int(const irep_idt &name) const;
+  std::size_t get_size_t(const irep_idt &name) const;
+  long long get_long_long(const irep_idt &name) const;
 
-  void set(const irep_namet &name, const irep_idt &value)
+  void set(const irep_idt &name, const irep_idt &value)
   {
     add(name, irept(value));
   }
-  void set(const irep_namet &name, irept irep)
+  void set(const irep_idt &name, irept irep)
   {
     add(name, std::move(irep));
   }
-  void set(const irep_namet &name, const long long value);
-  void set_size_t(const irep_namet &name, const std::size_t value);
+  void set(const irep_idt &name, const long long value);
+  void set_size_t(const irep_idt &name, const std::size_t value);
 
-  void remove(const irep_namet &name);
+  void remove(const irep_idt &name);
   void move_to_sub(irept &irep);
-  void move_to_named_sub(const irep_namet &name, irept &irep);
+  void move_to_named_sub(const irep_idt &name, irept &irep);
 
   bool operator==(const irept &other) const;
 
@@ -476,7 +465,7 @@ class irept
 
   std::string pretty(unsigned indent=0, unsigned max_indent=0) const;
 
-  static bool is_comment(const irep_namet &name)
+  static bool is_comment(const irep_idt &name)
   { return !name.empty() && name[0]=='#'; }
 
   /// count the number of named_sub elements that are not comments

src/util/lispirep.cpp

@@ -78,7 +78,7 @@ void irep2lisp(const irept &src, lispexprt &dest)
   {
     lispexprt name;
     name.type=lispexprt::String;
-    name.value = name2string(irep_entry.first);
+    name.value = id2string(irep_entry.first);
     dest.push_back(name);
 
     lispexprt sub;

src/util/type.h

@@ -78,12 +78,12 @@ class typet:public irept
     return static_cast<source_locationt &>(add(ID_C_source_location));
   }
 
-  typet &add_type(const irep_namet &name)
+  typet &add_type(const irep_idt &name)
   {
     return static_cast<typet &>(add(name));
   }
 
-  const typet &find_type(const irep_namet &name) const
+  const typet &find_type(const irep_idt &name) const
   {
     return static_cast<const typet &>(find(name));
   }

src/util/xml_irep.cpp

@@ -34,7 +34,7 @@ void convert(
     if(!irept::is_comment(irep_entry.first))
     {
       xmlt &x_nsub = xml.new_element("named_sub");
-      x_nsub.set_attribute("name", name2string(irep_entry.first));
+      x_nsub.set_attribute("name", id2string(irep_entry.first));
       convert(irep_entry.second, x_nsub);
     }
   }
@@ -44,7 +44,7 @@ void convert(
     if(!irept::is_comment(irep_entry.first))
     {
       xmlt &x_com = xml.new_element("comment");
-      x_com.set_attribute("name", name2string(irep_entry.first));
+      x_com.set_attribute("name", id2string(irep_entry.first));
       convert(irep_entry.second, x_com);
     }
   }