Do not use dstringt-specific APIs with irep_idt

Always use id2string instead of as_string, and directly refer to the string
container rather than indirectly via dstringt's API.

Author: tautschnig

src/goto-programs/interpreter.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 #include <util/std_types.h>
+#include <util/string_container.h>
 #include <util/symbol_table.h>
 #include <util/ieee_float.h>
 #include <util/fixedbv.h>
@@ -642,7 +643,7 @@ exprt interpretert::get_value(
   {
     // Strings are currently encoded by their irep_idt ID.
     return constant_exprt(
-      irep_idt::make_from_table_index(rhs[integer2size_t(offset)].to_long()),
+      get_string_container().get_string(rhs[integer2size_t(offset)].to_long()),
       type);
   }
 

src/goto-programs/interpreter_evaluate.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/fixedbv.h>
 #include <util/std_expr.h>
+#include <util/string_container.h>
 #include <util/pointer_offset_size.h>
 
 #include <langapi/language_util.h>
@@ -394,7 +395,7 @@ void interpretert::evaluate(
       if(show)
         warning() << "string decoding not fully implemented "
                   << length << eom;
-      mp_integer tmp=value.get_no();
+      mp_integer tmp = get_string_container()[id2string(value)];
       dest.push_back(tmp);
       return;
     }

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -685,7 +685,7 @@ static void find_and_replace_parameter(
 {
   // get the name of the parameter, e.g., `T` from `java::Class::T`
   const std::string &parameter_full_name =
-    as_string(parameter.type_variable_ref().get_identifier());
+    id2string(parameter.type_variable_ref().get_identifier());
   const std::string &parameter_name =
     parameter_full_name.substr(parameter_full_name.rfind("::") + 2);
 
@@ -696,7 +696,7 @@ static void find_and_replace_parameter(
     [&parameter_name](const java_generic_parametert &replacement_param)
     {
       const std::string &replacement_parameter_full_name =
-        as_string(replacement_param.type_variable().get_identifier());
+        id2string(replacement_param.type_variable().get_identifier());
       return parameter_name.compare(
                replacement_parameter_full_name.substr(
                  replacement_parameter_full_name.rfind("::") + 2)) == 0;
@@ -706,7 +706,7 @@ static void find_and_replace_parameter(
   if(replacement_parameter_p != replacement_parameters.end())
   {
     const std::string &replacement_parameter_full_name =
-      as_string(replacement_parameter_p->type_variable().get_identifier());
+      id2string(replacement_parameter_p->type_variable().get_identifier());
 
     // the replacement parameter is a viable one, i.e., it comes from an outer
     // class

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -798,7 +798,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
   // any block-internal edges to target the inner header block.
 
   const irep_idt child_label_name=child_label.get_label();
-  std::string new_label_str=as_string(child_label_name);
+  std::string new_label_str = id2string(child_label_name);
   new_label_str+='$';
   irep_idt new_label_irep(new_label_str);
 
@@ -1281,8 +1281,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
           // constructors.
           if(statement=="invokespecial")
           {
-            if(as_string(arg0.get(ID_identifier))
-               .find("<init>")!=std::string::npos)
+            if(
+              id2string(arg0.get(ID_identifier)).find("<init>") !=
+              std::string::npos)
             {
               if(needed_lazy_methods)
                 needed_lazy_methods->add_needed_class(classname);

src/java_bytecode/java_object_factory.cpp

@@ -1034,7 +1034,7 @@ void java_object_factoryt::gen_nondet_struct_init(
       if(skip_classid)
         continue;
 
-      irep_idt qualified_clsid="java::"+as_string(class_identifier);
+      irep_idt qualified_clsid = "java::" + id2string(class_identifier);
       constant_exprt ci(qualified_clsid, string_typet());
       code_assignt code(me, ci);
       code.add_source_location()=loc;
@@ -1329,13 +1329,13 @@ void java_object_factoryt::gen_nondet_array_init(
   exprt java_zero=from_integer(0, java_int_type());
   assignments.copy_to_operands(code_assignt(counter_expr, java_zero));
 
-  std::string head_name=as_string(counter.base_name)+"_header";
+  std::string head_name = id2string(counter.base_name) + "_header";
   code_labelt init_head_label(head_name, code_skipt());
   code_gotot goto_head(head_name);
 
   assignments.move_to_operands(init_head_label);
 
-  std::string done_name=as_string(counter.base_name)+"_done";
+  std::string done_name = id2string(counter.base_name) + "_done";
   code_labelt init_done_label(done_name, code_skipt());
   code_gotot goto_done(done_name);
 

src/util/symbol_table_base.cpp

@@ -38,10 +38,7 @@ void symbol_table_baset::show(std::ostream &out) const
   std::sort(
     sorted_names.begin(),
     sorted_names.end(),
-    [](const irep_idt &a, const irep_idt &b)
-    {
-      return as_string(a) < as_string(b);
-    });
+    [](const irep_idt &a, const irep_idt &b) { return a.compare(b); });
   out << "\n"
       << "Symbols:"
       << "\n";