From 4d935bf14f30ea8908fffdec64f85534e3f955f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Jan 2024 12:09:48 +0000 Subject: [PATCH] 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. --- src/analyses/goto_rw.h | 5 ----- src/analyses/reaching_definitions.h | 8 -------- src/goto-programs/graphml_witness.cpp | 13 ------------- src/libcprover-cpp/verification_result.h | 8 -------- src/pointer-analysis/value_set_fi.h | 8 -------- src/util/README.md | 6 +++--- src/util/dstring.h | 3 +-- src/util/irep.cpp | 8 -------- src/util/irep.h | 16 ++-------------- src/util/irep_ids.cpp | 9 --------- src/util/irep_ids.h | 17 ----------------- src/util/irep_serialization.cpp | 4 ---- src/util/json.h | 2 -- unit/util/irep.cpp | 5 ----- 14 files changed, 6 insertions(+), 106 deletions(-) diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index a6c1bf227fb..0ea8126e6a4 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -203,12 +203,7 @@ class shift_exprt; class rw_range_sett { public: - #ifdef USE_DSTRING typedef std::map> objectst; - #else - typedef std::unordered_map< - irep_idt, std::unique_ptr, string_hash> objectst; - #endif virtual ~rw_range_sett(); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index fb8e0a78374..faa8c46224a 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -274,11 +274,7 @@ class rd_range_domaint:public ai_domain_baset sparse_bitvector_analysist *const bv_container; typedef std::set values_innert; - #ifdef USE_DSTRING typedef std::map valuest; - #else - typedef std::unordered_map 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`. @@ -286,11 +282,7 @@ class rd_range_domaint:public ai_domain_baset /// instruction. valuest values; - #ifdef USE_DSTRING typedef std::map export_cachet; - #else - typedef std::unordered_map 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 --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index d15753b8fa1..60495c65374 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -20,9 +20,6 @@ Author: Daniel Kroening #include #include #include -#ifndef USE_DSTRING -# include -#endif #include #include @@ -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 --git a/src/libcprover-cpp/verification_result.h b/src/libcprover-cpp/verification_result.h index 77829931516..6176ef8486d 100644 --- a/src/libcprover-cpp/verification_result.h +++ b/src/libcprover-cpp/verification_result.h @@ -12,16 +12,8 @@ #include #include -#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; diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 8b3ad907dde..d07e01ead43 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -191,19 +191,11 @@ class value_set_fit typedef std::unordered_set dynamic_object_id_sett; - #ifdef USE_DSTRING typedef std::map valuest; typedef std::set flatten_seent; typedef std::unordered_set gvs_recursion_sett; typedef std::unordered_set recfind_recursion_sett; typedef std::unordered_set assign_recursion_sett; - #else - typedef std::unordered_map valuest; - typedef std::unordered_set flatten_seent; - typedef std::unordered_set gvs_recursion_sett; - typedef std::unordered_set recfind_recursion_sett; - typedef std::unordered_set assign_recursion_sett; - #endif std::vector get_value_set(const exprt &expr, const namespacet &ns) const; diff --git a/src/util/README.md b/src/util/README.md index 1c01fa7d725..4da10511149 100644 --- a/src/util/README.md +++ b/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 --git a/src/util/dstring.h b/src/util/dstring.h index 973711699e9..38926cb754e 100644 --- a/src/util/dstring.h +++ b/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 --git a/src/util/irep.cpp b/src/util/irep.cpp index 650e8bc768f..36e103ea8ff 100644 --- a/src/util/irep.cpp +++ b/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 --git a/src/util/irep.h b/src/util/irep.h index eb91b9f73ef..97fea5e9c4a 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -33,24 +33,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #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 /// 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 --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp index bb933862ed7..26fcd44d7df 100644 --- a/src/util/irep_ids.cpp +++ b/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(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 --git a/src/util/irep_ids.h b/src/util/irep_ids.h index b96ff929f25..b8ee3957006 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -12,15 +12,7 @@ Author: Reuben Thomas, reuben.thomas@me.com #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 -#endif /// \file /// The irep_ids are generated using a technique called @@ -34,18 +26,9 @@ Author: Reuben Thomas, reuben.thomas@me.com /// 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 --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index e959e8d99f1..20f37d8a194 100644 --- a/src/util/irep_serialization.cpp +++ b/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 --git a/src/util/json.h b/src/util/json.h index dbb0b706f68..2ef36d85f07 100644 --- a/src/util/json.h +++ b/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 --git a/unit/util/irep.cpp b/unit/util/irep.cpp index da50c0b85ad..66f92ffd63c 100644 --- a/unit/util/irep.cpp +++ b/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); #ifndef _GLIBCXX_DEBUG