Merge pull request #8154 from tautschnig/cleanup/remove_use_std_string

Remove support for irep_idt-as-std::string

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