Remove support for irep_idt-as-std::string

While #8040 ensured we were still able to compile the code base with
`irep_idt` typedef'd to `std::string` (via `USE_STD_STRING`),
experiments at that time also demonstrated that performance is
substantially worse, and not all tests would pass.

This commit now removes this untested feature to pave the way for
changes that may break `dstringt` to `std::string` compatibility.

Author: tautschnig

Diff for: src/analyses/goto_rw.h

@@ -203,12 +203,7 @@ class shift_exprt;
 class rw_range_sett
 {
 public:
-  #ifdef USE_DSTRING
   typedef std::map<irep_idt, std::unique_ptr<range_domain_baset>> objectst;
-  #else
-  typedef std::unordered_map<
-    irep_idt, std::unique_ptr<range_domain_baset>, string_hash> objectst;
-  #endif
 
   virtual ~rw_range_sett();
 

Diff for: src/analyses/reaching_definitions.h

@@ -274,23 +274,15 @@ class rd_range_domaint:public ai_domain_baset
   sparse_bitvector_analysist<reaching_definitiont> *const bv_container;
 
   typedef std::set<std::size_t> values_innert;
-  #ifdef USE_DSTRING
   typedef std::map<irep_idt, values_innert> valuest;
-  #else
-  typedef std::unordered_map<irep_idt, values_innert> valuest;
-  #endif
   /// It is an ordered map from program variable names to `ID`s of
   /// `reaching_definitiont` instances stored in map pointed to by
   /// `bv_container`. The map is not empty only if `has_value` is `UNKNOWN`.
   /// Variables in the map are all those which are live at the associated
   /// instruction.
   valuest values;
 
-  #ifdef USE_DSTRING
   typedef std::map<irep_idt, ranges_at_loct> export_cachet;
-  #else
-  typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
-  #endif
   /// It is a helper data structure. It consists of data already stored in
   /// `values` and `bv_container`. It is basically (an ordered) map from (a
   /// subset of) variables in `values` to iterators to GOTO instructions where

Diff for: src/goto-programs/graphml_witness.cpp

@@ -20,9 +20,6 @@ Author: Daniel Kroening
 #include <util/prefix.h>
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
-#ifndef USE_DSTRING
-#  include <util/string_container.h>
-#endif
 #include <util/symbol.h>
 
 #include <ansi-c/expr2c.h>
@@ -78,12 +75,7 @@ std::string graphml_witnesst::convert_assign_rec(
   const irep_idt &identifier,
   const code_assignt &assign)
 {
-#ifdef USE_DSTRING
   const auto cit = cache.find({identifier.get_no(), &assign.read()});
-#else
-  const auto cit =
-    cache.find({get_string_container()[id2string(identifier)], &assign.read()});
-#endif
   if(cit != cache.end())
     return cit->second;
 
@@ -219,12 +211,7 @@ std::string graphml_witnesst::convert_assign_rec(
     result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
   }
 
-#ifdef USE_DSTRING
   cache.insert({{identifier.get_no(), &assign.read()}, result});
-#else
-  cache.insert(
-    {{get_string_container()[id2string(identifier)], &assign.read()}, result});
-#endif
   return result;
 }
 

Diff for: src/libcprover-cpp/verification_result.h

@@ -12,16 +12,8 @@
 #include <string>
 #include <vector>
 
-#ifndef USE_STD_STRING
-#  define USE_DSTRING
-#endif
-
-#ifdef USE_DSTRING
 class dstringt;
 typedef dstringt irep_idt;
-#else
-typedef std::string irep_idt;
-#endif
 
 struct property_infot;
 using propertiest = std::map<irep_idt, property_infot>;

Diff for: src/pointer-analysis/value_set_fi.h

@@ -191,19 +191,11 @@ class value_set_fit
 
   typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
 
-  #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;
   typedef std::set<idt> flatten_seent;
   typedef std::unordered_set<idt> gvs_recursion_sett;
   typedef std::unordered_set<idt> recfind_recursion_sett;
   typedef std::unordered_set<idt> assign_recursion_sett;
-  #else
-  typedef std::unordered_map<idt, entryt, string_hash> valuest;
-  typedef std::unordered_set<idt, string_hash> flatten_seent;
-  typedef std::unordered_set<idt, string_hash> gvs_recursion_sett;
-  typedef std::unordered_set<idt, string_hash> recfind_recursion_sett;
-  typedef std::unordered_set<idt, string_hash> assign_recursion_sett;
-  #endif
 
   std::vector<exprt>
   get_value_set(const exprt &expr, const namespacet &ns) const;

Diff for: src/util/README.md

@@ -72,9 +72,9 @@ 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. 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
+Within cbmc, strings are represented using \ref irep_idt, which is
+typedefed to \ref dstringt.
+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.

Diff for: src/util/dstring.h

@@ -29,8 +29,7 @@ struct diagnostics_helpert;
 /// copies of the same string you only have to store the whole string once,
 /// which saves space.
 ///
-/// `irep_idt` is 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.
 ///
 ///
 /// Note: Marked final to disable inheritance. No virtual destructor, so

Diff for: src/util/irep.cpp

@@ -76,20 +76,12 @@ long long irept::get_long_long(const irep_idt &name) const
 
 void irept::set(const irep_idt &name, const long long value)
 {
-#ifdef USE_DSTRING
   add(name).id(to_dstring(value));
-#else
-  add(name).id(std::to_string(value));
-#endif
 }
 
 void irept::set_size_t(const irep_idt &name, const std::size_t value)
 {
-#ifdef USE_DSTRING
   add(name).id(to_dstring(value));
-#else
-  add(name).id(std::to_string(value));
-#endif
 }
 
 void irept::remove(const irep_idt &name)

Diff for: src/util/irep.h

@@ -33,24 +33,13 @@ Author: Daniel Kroening, [email protected]
 #include <map>
 #endif
 
-#ifdef USE_DSTRING
 typedef dstringt irep_idt;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef dstring_hash irep_id_hash;
-#else
-#include "string_hash.h"
-typedef std::string irep_idt;
-// NOLINTNEXTLINE(readability/identifiers)
-typedef string_hash irep_id_hash;
-#endif
 
 inline const std::string &id2string(const irep_idt &d)
 {
-  #ifdef USE_DSTRING
   return as_string(d);
-  #else
-  return d;
-  #endif
 }
 
 #ifdef IREP_DEBUG
@@ -76,9 +65,8 @@ struct ref_count_ift<true>
 
 /// A node with data in a tree, it contains:
 ///
-/// * \ref irept::dt::data : A string (Unless `USE_STD_STRING` is set, this is
-///   actually a \ref dstringt and thus an integer which is a reference into a
-///   string table.)
+/// * \ref irept::dt::data : A \ref dstringt and thus an integer which is a
+///   reference into a string table.)
 ///
 /// * \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,

Diff for: src/util/irep_ids.cpp

@@ -25,8 +25,6 @@ const char *irep_ids_table[]=
   nullptr,
 };
 
-#ifdef USE_DSTRING
-
 enum class idt:unsigned
 {
 #define IREP_ID_ONE(the_id) id_##the_id,
@@ -42,13 +40,6 @@ enum class idt:unsigned
   const dstringt ID_##the_id=dstringt::make_from_table_index(                  \
       static_cast<unsigned>(idt::id_##the_id));
 
-#else
-
-#define IREP_ID_ONE(the_id) const std::string ID_##the_id(#the_id);
-#  define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(#  str);
-
-#endif
-
 #include "irep_ids.def" // NOLINT(build/include)
 
 string_containert::string_containert()

Diff for: src/util/irep_ids.h

@@ -12,15 +12,7 @@ Author: Reuben Thomas, [email protected]
 #ifndef CPROVER_UTIL_IREP_IDS_H
 #define CPROVER_UTIL_IREP_IDS_H
 
-#ifndef USE_STD_STRING
-#define USE_DSTRING
-#endif
-
-#ifdef USE_DSTRING
 #include "dstring.h"
-#else
-#include <string>
-#endif
 
 /// \file
 /// The irep_ids are generated using a technique called
@@ -34,18 +26,9 @@ Author: Reuben Thomas, [email protected]
 /// into a const extern irep_idt with the variable name `ID_param` and the
 /// string value `"contents"`.
 
-#ifdef USE_DSTRING
-
 #define IREP_ID_ONE(the_id) extern const dstringt ID_##the_id;
 #define IREP_ID_TWO(the_id, str) extern const dstringt ID_##the_id;
 
-#else
-
-#define IREP_ID_ONE(the_id) extern const std::string ID_##the_id;
-#define IREP_ID_TWO(the_id, str) extern const std::string ID_##the_id;
-
-#endif
-
 #include "irep_ids.def"
 
 #endif

Diff for: src/util/irep_serialization.cpp

@@ -212,11 +212,7 @@ void irep_serializationt::write_string_ref(
   std::ostream &out,
   const irep_idt &s)
 {
-#ifdef USE_DSTRING
   size_t id = s.get_no();
-#else
-  size_t id = get_string_container()[s];
-#endif
   if(id>=ireps_container.string_map.size())
     ireps_container.string_map.resize(id+1, false);
 

Diff for: src/util/json.h

@@ -274,12 +274,10 @@ class json_stringt:public jsont
   {
   }
 
-#ifdef USE_DSTRING
   explicit json_stringt(const irep_idt &_value)
     : jsont(kindt::J_STRING, id2string(_value))
   {
   }
-#endif
 
   /// Constructon from string literal.
   explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value)

Diff for: unit/util/irep.cpp

@@ -22,13 +22,8 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       const std::size_t ref_count_size = 0;
 #endif
 
-#ifdef USE_DSTRING
       const std::size_t data_size = sizeof(dstringt);
       REQUIRE(sizeof(dstringt) == sizeof(unsigned));
-#else
-      const std::size_t data_size = sizeof(std::string);
-      REQUIRE(sizeof(std::string) == sizeof(void *));
-#endif
 
       const std::size_t sub_size = sizeof(std::vector<int>);
 #ifndef _GLIBCXX_DEBUG