Merge pull request #1845 from tautschnig/fix-1837

Fix building without USE_DSTRING

Author: Daniel Kroening

.travis.yml

@@ -142,7 +142,7 @@ jobs:
         - CCACHE_CPP2=yes
         - EXTRA_CXXFLAGS="-DNDEBUG"
 
-    # Ubuntu Linux with glibc using clang++-3.7, debug mode
+    # Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -165,7 +165,7 @@ jobs:
       env:
         - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
-        - EXTRA_CXXFLAGS="-DDEBUG"
+        - EXTRA_CXXFLAGS="-DDEBUG -DUSE_STD_STRING"
       script: echo "Not running any tests for a debug build."
 
     # cmake build using g++-5

doc/architectural/cbmc-guide.md

@@ -597,5 +597,5 @@ they are in the code.
 [^2]: Or references, if reference counted data sharing is enabled. It is
     enabled by default; see the `SHARING` macro.
 
-[^3]: When `USE_DSTRING` is enabled (it is by default), this is actually
+[^3]: Unless `USE_STD_STRING` is set, this is actually
 a `dstring` and thus an integer which is a reference into a string table

src/ansi-c/ansi_c_scope.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/irep.h>
 
+#include <unordered_map>
+
 enum class ansi_c_id_classt
 {
   ANSI_C_UNKNOWN,

src/goto-programs/class_hierarchy.h

@@ -16,6 +16,7 @@ Date: April 2016
 
 #include <iosfwd>
 #include <map>
+#include <unordered_map>
 
 #include <util/graph.h>
 #include <util/namespace.h>

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/character_refine_preprocess.h

@@ -24,6 +24,8 @@ Date:   March 2017
 #include <util/std_code.h>
 #include <util/mp_arith.h>
 
+#include <unordered_map>
+
 class character_refine_preprocesst:public messaget
 {
 public:

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -687,7 +687,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);
 
@@ -698,7 +698,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;
@@ -708,7 +708,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/solvers/prop/bdd_expr.h

@@ -23,6 +23,8 @@ Author: Michael Tautschnig, [email protected]
 
 #include <solvers/miniBDD/miniBDD.h>
 
+#include <unordered_map>
+
 class namespacet;
 
 /*! \brief TO_BE_DOCUMENTED

src/util/expr.h

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <functional>
 #include "type.h"
 
+#include <list>
+
 #define forall_operands(it, expr) \
   if((expr).has_operands()) /* NOLINT(readability/braces) */ \
     for(exprt::operandst::const_iterator it=(expr).operands().begin(), \

src/util/irep_ids.h

@@ -12,10 +12,14 @@ 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

src/util/replace_expr.h

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr.h"
 
+#include <unordered_map>
+
 typedef std::unordered_map<exprt, exprt, irep_hash> replace_mapt;
 
 bool replace_expr(const exprt &what, const exprt &by, exprt &dest);

src/util/replace_symbol.h

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr.h"
 
+#include <unordered_map>
+
 class replace_symbolt
 {
 public:

src/util/std_types.h

@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
 #include "invariant.h"
 #include "expr_cast.h"
 
+#include <unordered_map>
+
 class constant_exprt;
 
 /*! \defgroup gr_std_types Conversion to specific types

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";