From d87d6e4f91db6b76ebe798f3abc943590a355a02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 14 Feb 2018 11:33:24 +0000 Subject: [PATCH 1/5] Include unordered_map where using a std::unordered_map The code fixed here previously relied on unordered_map being included by dstring.h, which is only dragged in when USE_DSTRING is set. --- src/ansi-c/ansi_c_scope.h | 2 ++ src/goto-programs/class_hierarchy.h | 1 + src/java_bytecode/character_refine_preprocess.h | 2 ++ src/solvers/prop/bdd_expr.h | 2 ++ src/util/replace_expr.h | 2 ++ src/util/replace_symbol.h | 2 ++ src/util/std_types.h | 2 ++ 7 files changed, 13 insertions(+) diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h index 0f9bc117729..4095c58ec63 100644 --- a/src/ansi-c/ansi_c_scope.h +++ b/src/ansi-c/ansi_c_scope.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + enum class ansi_c_id_classt { ANSI_C_UNKNOWN, diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index e8b302a0e86..c2fd3ec464f 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -16,6 +16,7 @@ Date: April 2016 #include #include +#include #include #include diff --git a/src/java_bytecode/character_refine_preprocess.h b/src/java_bytecode/character_refine_preprocess.h index a41d59b5226..11cfdd3635f 100644 --- a/src/java_bytecode/character_refine_preprocess.h +++ b/src/java_bytecode/character_refine_preprocess.h @@ -24,6 +24,8 @@ Date: March 2017 #include #include +#include + class character_refine_preprocesst:public messaget { public: diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h index c462a17e669..4b35e1ba7d4 100644 --- a/src/solvers/prop/bdd_expr.h +++ b/src/solvers/prop/bdd_expr.h @@ -23,6 +23,8 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk #include +#include + class namespacet; /*! \brief TO_BE_DOCUMENTED diff --git a/src/util/replace_expr.h b/src/util/replace_expr.h index 058909076dc..fb515e71bfd 100644 --- a/src/util/replace_expr.h +++ b/src/util/replace_expr.h @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr.h" +#include + typedef std::unordered_map replace_mapt; bool replace_expr(const exprt &what, const exprt &by, exprt &dest); diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index 26e246a94cd..5a59096e3a8 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr.h" +#include + class replace_symbolt { public: diff --git a/src/util/std_types.h b/src/util/std_types.h index 8215598fb36..58bbf5d921b 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "expr_cast.h" +#include + class constant_exprt; /*! \defgroup gr_std_types Conversion to specific types From 534f4d28b33a6715a48b113d531002aab18b2e53 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Feb 2018 18:24:20 +0000 Subject: [PATCH 2/5] Include list in expr.h The code fixed here previously relied on list being included by dstring.h, which is only dragged in when USE_DSTRING is set. --- src/util/expr.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/expr.h b/src/util/expr.h index 5b4864920bd..1546d4eed1a 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "type.h" +#include + #define forall_operands(it, expr) \ if((expr).has_operands()) /* NOLINT(readability/braces) */ \ for(exprt::operandst::const_iterator it=(expr).operands().begin(), \ From 25ffad4199414b7e55ac69d1b38d144bf8981213 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Feb 2018 09:40:09 +0000 Subject: [PATCH 3/5] 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. --- src/goto-programs/interpreter.cpp | 3 ++- src/goto-programs/interpreter_evaluate.cpp | 3 ++- src/java_bytecode/java_bytecode_convert_class.cpp | 6 +++--- src/java_bytecode/java_bytecode_convert_method.cpp | 7 ++++--- src/java_bytecode/java_object_factory.cpp | 6 +++--- src/util/symbol_table_base.cpp | 5 +---- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index a2de956dabd..e5b0af2e16f 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -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); } diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 43b291fa983..48fe0b3c649 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -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; } diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 8b45d2692a1..14944e451d2 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/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 ¶meter_full_name = - as_string(parameter.type_variable_ref().get_identifier()); + id2string(parameter.type_variable_ref().get_identifier()); const std::string ¶meter_name = parameter_full_name.substr(parameter_full_name.rfind("::") + 2); @@ -696,7 +696,7 @@ static void find_and_replace_parameter( [¶meter_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 diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 191d2f997db..714fbb94b18 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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("")!=std::string::npos) + if( + id2string(arg0.get(ID_identifier)).find("") != + std::string::npos) { if(needed_lazy_methods) needed_lazy_methods->add_needed_class(classname); diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index a1706cde435..40ee6758222 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/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); diff --git a/src/util/symbol_table_base.cpp b/src/util/symbol_table_base.cpp index fbefd8d1080..dcb436a6fa3 100644 --- a/src/util/symbol_table_base.cpp +++ b/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"; From 52290b0c290c745dbbf62573f59cba8a884e7889 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Feb 2018 09:42:17 +0000 Subject: [PATCH 4/5] Include string when not using dstringt as irep_idt representation Fixes: #1837 together with all previous commits in this series. --- src/util/irep_ids.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h index 2202c95c62b..d63f8f7332f 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -16,6 +16,8 @@ Author: Reuben Thomas, reuben.thomas@me.com #ifdef USE_DSTRING #include "dstring.h" +#else +#include #endif /// \file The irep_ids are generated using a technique called From 590fc2dacce07cfb5ffcefca321a4f4089894cfe Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 15 Feb 2018 11:50:33 +0000 Subject: [PATCH 5/5] Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job This introduces a macro USE_STD_STRING that can be set to disable USE_DSTRING, and thus the use of dstringt as the implementation of irep_idt. The Ubuntu/Clang/DEBUG Travis stage sets this macro to avoid future changes breaking the build when disabling USE_DSTRING. --- .travis.yml | 4 ++-- doc/architectural/cbmc-guide.md | 2 +- src/util/irep_ids.h | 2 ++ 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index ecd05ad492e..48e1152ef9a 100644 --- a/.travis.yml +++ b/.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 diff --git a/doc/architectural/cbmc-guide.md b/doc/architectural/cbmc-guide.md index ccbf0068cea..bd96f4dbba4 100644 --- a/doc/architectural/cbmc-guide.md +++ b/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 diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h index d63f8f7332f..2fec6ff4114 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -12,7 +12,9 @@ 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"