Merge pull request #8040 from tautschnig/cleanup/dstring

tautschnig · web-flow · commit 7601bb1a1a9e · 2023-12-18T09:40:16.000+01:00
Cleanup USE_STD_STRING/USE_DSTRING configuration option
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.h b/jbmc/src/java_bytecode/character_refine_preprocess.h
@@ -23,6 +23,7 @@ Date:   March 2017
 #include <util/mp_arith.h>
 #include <util/std_code_base.h>
 
+#include <list>
 #include <unordered_map>
 
 class code_function_callt;
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -10,14 +10,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
 
-#include <set>
-#include <map>
-
 #include <util/std_types.h>
 
 #include "bytecode_info.h"
 #include "java_types.h"
 
+#include <list>
+#include <map>
+#include <set>
+
 struct java_bytecode_parse_treet
 {
   // Disallow copy construction and copy assignment, but allow move construction
diff --git a/jbmc/src/java_bytecode/java_class_loader_base.h b/jbmc/src/java_bytecode/java_class_loader_base.h
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "jar_pool.h"
 
+#include <list>
+
 class message_handlert;
 struct java_bytecode_parse_treet;
 
diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp
@@ -23,6 +23,7 @@ Author: Daniel Kroening, dkr@amazon.com
 
 #include <fstream> // IWYU pragma: keep
 #include <iostream>
+#include <list>
 #include <map>
 #include <regex>
 #include <sstream>
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
@@ -18,6 +18,7 @@ Date: June 2006
 #include <util/std_types.h>
 #include <util/symbol.h>
 
+#include <list>
 #include <map>
 
 class cmdlinet;
diff --git a/src/goto-cc/ld_mode.h b/src/goto-cc/ld_mode.h
@@ -17,6 +17,8 @@ Date: June 2006
 #include "gcc_message_handler.h"
 #include "goto_cc_mode.h"
 
+#include <list>
+
 class ld_modet : public goto_cc_modet
 {
 public:
diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h
@@ -5,11 +5,12 @@
 #ifndef CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
 #define CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
 
+#include <util/message.h>
+
 #include <functional>
+#include <list>
 #include <map>
 
-#include <util/message.h>
-
 class cmdlinet;
 class exprt; // IWYU pragma: keep
 class goto_modelt;
diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h
@@ -9,15 +9,16 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
 #define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
 
-#include <map>
-#include <set>
-#include <unordered_set>
-
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
+#include <list>
+#include <map>
+#include <set>
+#include <unordered_set>
+
 class code_blockt;
 class goto_modelt;
 
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -12,16 +12,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
 
+#include <util/invariant.h>
+#include <util/source_location.h>
+
 #include "goto_instruction_code.h"
 
 #include <iosfwd>
-#include <set>
 #include <limits>
+#include <list>
+#include <set>
 #include <string>
 
-#include <util/invariant.h>
-#include <util/source_location.h>
-
 class code_gotot;
 class namespacet;
 enum class validation_modet;
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
@@ -20,6 +20,9 @@ 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>
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -9,24 +9,24 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Symbolic Execution
 
-#include "goto_symex.h"
-
-#include <memory>
-
-#include <pointer-analysis/value_set_dereference.h>
-
 #include <util/exception_utils.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format.h>
 #include <util/format_expr.h>
 #include <util/invariant.h>
+#include <util/magic.h>
 #include <util/mathematical_expr.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
 
+#include <pointer-analysis/value_set_dereference.h>
+
+#include "goto_symex.h"
 #include "path_storage.h"
 
+#include <memory>
+
 symex_configt::symex_configt(const optionst &options)
   : max_depth(options.get_unsigned_int_option("depth")),
     doing_path_exploration(options.is_set("paths")),
diff --git a/src/goto-synthesizer/expr_enumerator.h b/src/goto-synthesizer/expr_enumerator.h
@@ -11,6 +11,7 @@ Author: Qinheping Hu
 
 #include <util/expr.h>
 
+#include <list>
 #include <map>
 #include <set>
 
diff --git a/src/libcprover-cpp/verification_result.cpp b/src/libcprover-cpp/verification_result.cpp
@@ -114,7 +114,7 @@ std::vector<std::string> verification_resultt::get_property_ids() const
   std::vector<std::string> result;
   for(const auto &props : _impl->get_properties())
   {
-    result.push_back(as_string(props.first));
+    result.push_back(id2string(props.first));
   }
   return result;
 }
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_utils.h"
 
+#include <list>
 #include <utility>
 
 bvt bv_utilst::build_constant(const mp_integer &n, std::size_t width)
diff --git a/src/solvers/smt2_incremental/response_or_error.h b/src/solvers/smt2_incremental/response_or_error.h
@@ -20,11 +20,6 @@ class response_or_errort final
   {
   }
 
-  explicit response_or_errort(std::string message)
-    : smt_or_messages{std::vector<std::string>{std::move(message)}}
-  {
-  }
-
   explicit response_or_errort(std::vector<std::string> messages)
     : smt_or_messages{std::move(messages)}
   {
diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp
@@ -139,14 +139,14 @@ valid_smt_error_response(const irept &parse_tree)
   // unexpected in the parse tree is now considered to be an invalid response.
   if(parse_tree.get_sub().size() == 1)
   {
-    return {response_or_errort<smt_responset>{
-      "Error response is missing the error message."}};
+    return {response_or_errort<smt_responset>{std::vector<std::string>{
+      {"Error response is missing the error message."}}}};
   }
   if(parse_tree.get_sub().size() > 2)
   {
-    return {response_or_errort<smt_responset>{
-      "Error response has multiple error messages - \"" +
-      print_parse_tree(parse_tree) + "\"."}};
+    return {response_or_errort<smt_responset>{std::vector<std::string>{
+      {"Error response has multiple error messages - \"" +
+       print_parse_tree(parse_tree) + "\"."}}}};
   }
   return validation_propagating<smt_error_responset, smt_responset>(
     validate_string_literal(parse_tree.get_sub()[1]));
@@ -250,10 +250,10 @@ static std::optional<response_or_errort<smt_termt>> try_select_validation(
     return {};
   if(parse_tree.get_sub().size() != 3)
   {
-    return response_or_errort<smt_termt>{
-      "\"select\" is expected to have 2 arguments, but " +
-      std::to_string(parse_tree.get_sub().size()) +
-      " arguments were found - \"" + print_parse_tree(parse_tree) + "\"."};
+    return response_or_errort<smt_termt>{std::vector<std::string>{
+      {"\"select\" is expected to have 2 arguments, but " +
+       std::to_string(parse_tree.get_sub().size()) +
+       " arguments were found - \"" + print_parse_tree(parse_tree) + "\"."}}};
   }
   const auto array = validate_term(parse_tree.get_sub()[1], identifier_table);
   const auto index = validate_term(parse_tree.get_sub()[2], identifier_table);
@@ -281,8 +281,8 @@ static response_or_errort<smt_termt> validate_term(
   {
     return *select_validation;
   }
-  return response_or_errort<smt_termt>{"Unrecognised SMT term - \"" +
-                                       print_parse_tree(parse_tree) + "\"."};
+  return response_or_errort<smt_termt>{std::vector<std::string>{
+    {"Unrecognised SMT term - \"" + print_parse_tree(parse_tree) + "\"."}}};
 }
 
 static response_or_errort<smt_get_value_responset::valuation_pairt>
@@ -305,10 +305,10 @@ validate_valuation_pair(
   if(valid_descriptor.get_sort() != valid_value.get_sort())
   {
     return resultt{
-      "Mismatched descriptor and value sorts in - " +
-      print_parse_tree(pair_parse_tree) + "\nDescriptor has sort " +
-      smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +
-      smt_to_smt2_string(valid_value.get_sort())};
+      {"Mismatched descriptor and value sorts in - " +
+       print_parse_tree(pair_parse_tree) + "\nDescriptor has sort " +
+       smt_to_smt2_string(valid_descriptor.get_sort()) + "\nValue has sort " +
+       smt_to_smt2_string(valid_value.get_sort())}};
   }
   // see https://github.com/diffblue/cbmc/issues/7464 for why we explicitly name
   // the valuation_pairt type here:
@@ -378,6 +378,6 @@ response_or_errort<smt_responset> validate_smt_response(
   {
     return *get_value_response;
   }
-  return response_or_errort<smt_responset>{"Invalid SMT response \"" +
-                                           id2string(parse_tree.id()) + "\""};
+  return response_or_errort<smt_responset>{std::vector<std::string>{
+    {"Invalid SMT response \"" + id2string(parse_tree.id()) + "\""}}};
 }
diff --git a/src/solvers/strings/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp
@@ -10,15 +10,17 @@ Author: Jesse Sigal, jesse.sigal@diffblue.com
 /// Defines related function for string constraints.
 
 #include "string_constraint_instantiation.h"
-#include <algorithm>
-#include <unordered_set>
 
 #include <util/arith_tools.h>
 #include <util/expr_iterator.h>
 #include <util/format_expr.h>
 
 #include "string_constraint.h"
 
+#include <algorithm>
+#include <list>
+#include <unordered_set>
+
 /// Look for symbol \p qvar in the expression \p index and return true if found
 /// \return True, iff \p qvar appears in \p index.
 static bool contains(const exprt &index, const symbol_exprt &qvar)
diff --git a/src/statement-list/statement_list_parse_tree.h b/src/statement-list/statement_list_parse_tree.h
@@ -15,6 +15,8 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 #include <util/std_code_base.h>
 #include <util/std_expr.h>
 
+#include <list>
+
 /// Intermediate representation of a parsed Statement List file before
 /// converting it into a goto program. Contains all data structures that are
 /// necessary for describing Statement List functions and function blocks.
diff --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp
@@ -45,7 +45,7 @@ enum class idt:unsigned
 #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(#the_id);
+#  define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(#  str);
 
 #endif
 
diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp
@@ -13,11 +13,12 @@ Date: May 2007
 
 #include "irep_serialization.h"
 
+#include "exception_utils.h"
+#include "string_container.h"
+
 #include <climits>
 #include <iostream>
 
-#include "exception_utils.h"
-
 void irep_serializationt::write_irep(
   std::ostream &out,
   const irept &irep)
@@ -211,7 +212,11 @@ void irep_serializationt::write_string_ref(
   std::ostream &out,
   const irep_idt &s)
 {
-  size_t id=irep_id_hash()(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
@@ -274,7 +274,7 @@ class json_stringt:public jsont
   {
   }
 
-#ifndef USE_STD_STRING
+#ifdef USE_DSTRING
   explicit json_stringt(const irep_idt &_value)
     : jsont(kindt::J_STRING, id2string(_value))
   {
diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h
@@ -8,6 +8,7 @@
 
 #include "symbol.h" // IWYU pragma: keep
 
+#include <list>
 #include <map>
 #include <unordered_map>
 
diff --git a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp
@@ -52,7 +52,7 @@ SCENARIO(
 
       auto type = signedbv_typet(32);
       auto val2 = make_constant(from_integer(2, type), env, ns);
-      auto x_name = symbol_exprt(dstringt("x"), type);
+      auto x_name = symbol_exprt("x", type);
 
       env.assign(x_name, val2, ns);
 
@@ -65,10 +65,10 @@ SCENARIO(
 
       auto type = signedbv_typet(32);
       auto val2 = make_constant(from_integer(2, type), env, ns);
-      auto x_name = symbol_exprt(dstringt("x"), type);
+      auto x_name = symbol_exprt("x", type);
 
       auto val3 = make_constant(from_integer(3, type), env, ns);
-      auto y_name = symbol_exprt(dstringt("y"), type);
+      auto y_name = symbol_exprt("y", type);
 
       env.assign(x_name, val2, ns);
       env.assign(y_name, val3, ns);
diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp
@@ -25,7 +25,7 @@ SCENARIO(
   const typet type = signedbv_typet(32);
   const exprt val2 = from_integer(2, type);
 
-  const exprt x_name = symbol_exprt(dstringt("x"), type);
+  const exprt x_name = symbol_exprt("x", type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;
diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp
@@ -24,9 +24,9 @@ SCENARIO(
 {
   const auto int_type = signedbv_typet(32);
   const auto ptr_type = pointer_typet(int_type, 32);
-  const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type);
+  const auto val2_symbol = symbol_exprt("val2", int_type);
 
-  const auto x_name = symbol_exprt(dstringt("x"), int_type);
+  const auto x_name = symbol_exprt("x", int_type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;
diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp
diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp
diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp
diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp
diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp
diff --git a/unit/compound_block_locations.h b/unit/compound_block_locations.h
diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp
diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp
diff --git a/unit/solvers/smt2_incremental/smt_response_validation.cpp b/unit/solvers/smt2_incremental/smt_response_validation.cpp
diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp

Original file line number	Diff line number	Diff line change
`@@ -17,6 +17,8 @@ Date: June 2006`
`17`	`17`	`#include "gcc_message_handler.h"`
`18`	`18`	`#include "goto_cc_mode.h"`
`19`	`19`
	`20`	`+#include <list>`
	`21`	`+`
`20`	`22`	`class ld_modet : public goto_cc_modet`
`21`	`23`	`{`
`22`	`24`	`public:`