From b14a49536c5353601d9599914927ddf2a196424e Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 17 May 2017 17:52:14 +0100 Subject: [PATCH 01/11] Tidy up symbol_tablet::move Added comment Move rather than copy empty symbol into table --- src/util/symbol_table.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index c9e42ff5517..f6f3eaabf43 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -44,23 +44,23 @@ bool symbol_tablet::add(const symbolt &symbol) /// location in the symbol table bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) { - symbolt tmp; - + // Add an empty symbol to the table or retrieve existing symbol with same name std::pair result= - symbols.insert(std::pair(symbol.name, tmp)); + symbols.emplace(symbol.name, symbolt()); if(!result.second) { + // Return the address of the symbol that already existed in the table new_symbol=&result.first->second; return true; } - symbol_base_map.insert( - std::pair(symbol.base_name, symbol.name)); - symbol_module_map.insert( - std::pair(symbol.module, symbol.name)); + symbol_base_map.emplace(symbol.base_name, symbol.name); + symbol_module_map.emplace(symbol.module, symbol.name); + // Move the provided symbol into the symbol table result.first->second.swap(symbol); + // Return the address of the new symbol in the table new_symbol=&result.first->second; return false; From 7798daad628a3b14acbc044f499e8ee574df163b Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 21 Sep 2017 12:58:18 +0100 Subject: [PATCH 02/11] Add move insert to symbol_table Make insertions strong exception-safe Use emplace instead of insert --- src/java_bytecode/java_utils.cpp | 6 ++-- src/util/fresh_symbol.cpp | 19 ++++------- src/util/symbol_table.cpp | 58 ++++++++++++++++++++++++++------ src/util/symbol_table.h | 7 +++- 4 files changed, 64 insertions(+), 26 deletions(-) diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index bf41076d84c..8307d39568d 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -86,9 +86,9 @@ void generate_class_stub( new_symbol.mode=ID_java; new_symbol.is_type=true; - symbolt *class_symbol; + auto res=symbol_table.insert(std::move(new_symbol)); - if(symbol_table.move(new_symbol, class_symbol)) + if(!res) { messaget message(message_handler); message.warning() << @@ -99,7 +99,7 @@ void generate_class_stub( else { // create the class identifier etc - java_root_class(*class_symbol); + java_root_class(*res); } } diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 71bb64b3ce9..3acd78f97f4 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -39,27 +39,22 @@ symbolt &get_fresh_aux_symbol( symbol_tablet &symbol_table) { auxiliary_symbolt new_symbol; - symbolt *symbol_ptr; - do + optionalt> res; + // Loop until find a name that doesn't clash with a non-auxilliary symbol + while(!res) { // Distinguish local variables with the same name new_symbol.base_name= - basename_prefix+ - "$"+ - std::to_string(++temporary_counter); + basename_prefix+"$"+std::to_string(++temporary_counter); if(name_prefix.empty()) new_symbol.name=new_symbol.base_name; else - new_symbol.name= - name_prefix+ - "::"+ - id2string(new_symbol.base_name); + new_symbol.name=name_prefix+"::"+id2string(new_symbol.base_name); new_symbol.type=type; new_symbol.location=source_location; new_symbol.mode=symbol_mode; + res=symbol_table.insert(std::move(new_symbol)); } - while(symbol_table.move(new_symbol, symbol_ptr)); - - return *symbol_ptr; + return *res; } diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index f6f3eaabf43..14caabbfe4d 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -16,17 +16,31 @@ Author: Daniel Kroening, kroening@kroening.com /// there is a symbol with the same name already in the symbol table. bool symbol_tablet::add(const symbolt &symbol) { - if(!symbols.insert(std::pair(symbol.name, symbol)).second) + std::pair result= + symbols.emplace(symbol.name, symbol); + if(!result.second) return true; - - symbol_base_map.insert( - std::pair(symbol.base_name, symbol.name)); - symbol_module_map.insert( - std::pair(symbol.module, symbol.name)); - + add_base_and_module(result.first); return false; } +/// Move a new symbol to the symbol table +/// \remark: This is a nicer interface than move but achieves the same result +/// \param symbol: The symbol to be added to the symbol table +/// \return Returns an optional reference to the newly inserted symbol, without +/// a value if a symbol with the same name already exists in the symbol table +optionalt> symbol_tablet::insert( + symbolt &&symbol) +{ + // Add the symbol to the table or retrieve existing symbol with the same name + std::pair result= + symbols.emplace(symbol.name, std::move(symbol)); + if(!result.second) + return optionalt>(); + add_base_and_module(result.first); + return std::ref(result.first->second); +} + /// Move a symbol into the symbol table. If there is already a symbol with the /// same name then symbol is unchanged, new_symbol points to the symbol with the /// same name and true is returned. Otherwise, the symbol is moved into the @@ -55,17 +69,41 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) return true; } - symbol_base_map.emplace(symbol.base_name, symbol.name); - symbol_module_map.emplace(symbol.module, symbol.name); - // Move the provided symbol into the symbol table result.first->second.swap(symbol); + + add_base_and_module(result.first); + // Return the address of the new symbol in the table new_symbol=&result.first->second; return false; } +void symbol_tablet::add_base_and_module(symbolst::iterator added_symbol) +{ + symbolt &symbol=added_symbol->second; + try + { + symbol_base_mapt::iterator base_result= + symbol_base_map.emplace(symbol.base_name, symbol.name); + try + { + symbol_module_map.emplace(symbol.module, symbol.name); + } + catch(...) + { + symbol_base_map.erase(base_result); + throw; + } + } + catch(...) + { + symbols.erase(added_symbol); + throw; + } +} + /// Remove a symbol from the symbol table /// \param name: The name of the symbol to remove /// \return Returns a boolean indicating whether the process failed diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 9a1b0b7f95c..40943412cd4 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "symbol.h" #define forall_symbols(it, expr) \ @@ -60,12 +62,15 @@ class symbol_tablet bool add(const symbolt &symbol); + optionalt> insert(symbolt &&symbol); bool move(symbolt &symbol, symbolt *&new_symbol); - // this will go away, use add instead bool move(symbolt &symbol) { symbolt *new_symbol; return move(symbol, new_symbol); } +private: + void add_base_and_module(symbolst::iterator added_symbol); +public: void clear() { symbols.clear(); From 1def64c6416e63e3a54074bc907ea266a43d3772 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 21 Sep 2017 16:24:05 +0100 Subject: [PATCH 03/11] Added INVARIANT to symbol_tablet::remove --- src/util/symbol_table.cpp | 53 +++++++++++++++++++++------------------ 1 file changed, 29 insertions(+), 24 deletions(-) diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 14caabbfe4d..317ad49d7ff 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symbol_table.h" #include +#include /// Add a new symbol to the symbol table /// \param symbol: The symbol to be added to the symbol table @@ -109,35 +110,39 @@ void symbol_tablet::add_base_and_module(symbolst::iterator added_symbol) /// \return Returns a boolean indicating whether the process failed bool symbol_tablet::remove(const irep_idt &name) { - symbolst::iterator entry=symbols.find(name); - + symbolst::const_iterator entry=symbols.find(name); if(entry==symbols.end()) return true; - for(symbol_base_mapt::iterator - it=symbol_base_map.lower_bound(entry->second.base_name), - it_end=symbol_base_map.upper_bound(entry->second.base_name); - it!=it_end; - ++it) - if(it->second==name) - { - symbol_base_map.erase(it); - break; - } - - for(symbol_module_mapt::iterator - it=symbol_module_map.lower_bound(entry->second.module), - it_end=symbol_module_map.upper_bound(entry->second.module); - it!=it_end; - ++it) - if(it->second==name) - { - symbol_module_map.erase(it); - break; - } + const symbolt &symbol=entry->second; + + symbol_base_mapt::const_iterator + base_it=symbol_base_map.lower_bound(entry->second.base_name), + base_it_end=symbol_base_map.upper_bound(entry->second.base_name); + while(base_it!=base_it_end && base_it->second!=name) + ++base_it; + INVARIANT( + base_it!=base_it_end, + "symbolt::base_name should not be changed " + "after it is added to the symbol_table " + "(name: "+id2string(symbol.name)+", " + "current base_name: "+id2string(symbol.base_name)+")"); + symbol_base_map.erase(base_it); + + symbol_module_mapt::const_iterator + module_it=symbol_module_map.lower_bound(entry->second.module), + module_it_end=symbol_module_map.upper_bound(entry->second.module); + while(module_it!=module_it_end && module_it->second!=name) + ++module_it; + INVARIANT( + module_it!=module_it_end, + "symbolt::module should not be changed " + "after it is added to the symbol_table " + "(name: "+id2string(symbol.name)+", " + "current module: "+id2string(symbol.module)+")"); + symbol_module_map.erase(module_it); symbols.erase(entry); - return false; } From e8657297ac6ba73bdb21768f97bdd43f64577ec3 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 25 Sep 2017 11:46:20 +0100 Subject: [PATCH 04/11] Updated comment --- src/util/symbol_table.cpp | 8 +------- src/util/symbol_table.h | 26 ++++++++------------------ 2 files changed, 9 insertions(+), 25 deletions(-) diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 317ad49d7ff..cfd35eaf8db 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -1,10 +1,4 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. #include "symbol_table.h" diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 40943412cd4..a7ffdf5afe8 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -1,24 +1,13 @@ -/*******************************************************************\ +// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved. -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ +/// \file +/// Symbol table +/// \defgroup gr_symbol_table Symbol Table #ifndef CPROVER_UTIL_SYMBOL_TABLE_H #define CPROVER_UTIL_SYMBOL_TABLE_H -/*! \file util/symbol_table.h - * \brief Symbol table - * - * \author Daniel Kroening -*/ - -/*! \defgroup gr_symbol_table Symbol Table -*/ - #include #include #include @@ -27,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symbol.h" + #define forall_symbols(it, expr) \ for(symbol_tablet::symbolst::const_iterator it=(expr).begin(); \ it!=(expr).end(); ++it) @@ -48,9 +38,9 @@ typedef std::multimap symbol_module_mapt; it_end=(expr).upper_bound(module); \ it!=it_end; ++it) -/*! \brief The symbol table - \ingroup gr_symbol_table -*/ + +/// \brief The symbol table +/// \ingroup gr_symbol_table class symbol_tablet { public: From d1d502f8d0c6a128cadfa35a9e0ae8dff3af4d8f Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 22 Sep 2017 16:02:24 +0100 Subject: [PATCH 05/11] Restricted interface of current symbol_tablet --- src/ansi-c/ansi_c_entry_point.cpp | 6 +- src/ansi-c/c_typecheck_base.cpp | 16 ++-- src/ansi-c/c_typecheck_code.cpp | 4 +- src/ansi-c/c_typecheck_expr.cpp | 6 +- src/ansi-c/c_typecheck_type.cpp | 17 ++-- src/cpp/cpp_declarator_converter.cpp | 20 ++--- src/cpp/cpp_instantiate_template.cpp | 9 +-- src/cpp/cpp_typecheck.cpp | 30 +++---- src/cpp/cpp_typecheck_compound_type.cpp | 32 +++----- src/cpp/cpp_typecheck_declaration.cpp | 5 +- src/cpp/cpp_typecheck_enum_type.cpp | 4 +- src/cpp/cpp_typecheck_expr.cpp | 25 +++--- src/cpp/cpp_typecheck_namespace.cpp | 2 +- src/cpp/cpp_typecheck_template.cpp | 22 +++--- src/cpp/cpp_typecheck_virtual_table.cpp | 2 +- src/goto-cc/compile.cpp | 9 ++- src/goto-cc/linker_script_merge.cpp | 16 ++-- src/goto-instrument/dump_c.cpp | 13 +-- src/goto-instrument/function.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 17 ++-- src/goto-instrument/remove_function.cpp | 2 +- src/goto-instrument/stack_depth.cpp | 2 +- src/goto-instrument/uninitialized.cpp | 2 +- src/goto-programs/goto_convert_exceptions.cpp | 2 +- src/goto-programs/remove_complex.cpp | 4 +- src/goto-programs/remove_exceptions.cpp | 2 +- src/goto-programs/remove_returns.cpp | 16 +--- src/goto-programs/remove_vector.cpp | 4 +- src/goto-programs/string_abstraction.cpp | 14 ++-- src/goto-programs/string_instrumentation.cpp | 6 +- src/goto-symex/symex_function_call.cpp | 2 +- .../java_bytecode_convert_class.cpp | 2 +- .../java_bytecode_convert_method.cpp | 2 +- .../java_bytecode_instrument.cpp | 2 +- src/java_bytecode/java_bytecode_language.cpp | 2 +- src/java_bytecode/java_bytecode_typecheck.cpp | 8 +- .../java_bytecode_typecheck_expr.cpp | 2 +- src/java_bytecode/java_entry_point.cpp | 8 +- .../java_string_library_preprocess.cpp | 2 +- src/jsil/jsil_convert.cpp | 2 +- src/jsil/jsil_entry_point.cpp | 4 +- src/jsil/jsil_typecheck.cpp | 12 ++- src/linking/linking.cpp | 66 ++++++++-------- src/linking/linking_class.h | 2 +- src/linking/remove_internal_symbols.cpp | 18 ++--- src/linking/static_lifetime_init.cpp | 16 ++-- src/pointer-analysis/add_failed_symbols.cpp | 36 ++++----- .../value_set_dereference.cpp | 2 +- src/util/language.cpp | 3 +- src/util/symbol_table.cpp | 44 ++++++----- src/util/symbol_table.h | 79 ++++++++++++++----- 51 files changed, 303 insertions(+), 322 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index fc25290079a..70beee5c57c 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -212,7 +212,7 @@ bool generate_ansi_c_start_function( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(INITIALIZE_FUNCTION); if(init_it==symbol_table.symbols.end()) @@ -478,11 +478,11 @@ bool generate_ansi_c_start_function( new_symbol.value.swap(init_code); new_symbol.mode=symbol.mode; - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol))) { messaget message; message.set_message_handler(message_handler); - message.error() << "failed to move main symbol" << messaget::eom; + message.error() << "failed to insert main symbol" << messaget::eom; return true; } diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index b0a8f1734c3..46a4f4a1baa 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -100,7 +100,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) } // see if we have it already - symbol_tablet::symbolst::iterator old_it= + symbol_tablet::symbolst::const_iterator old_it= symbol_table.symbols.find(symbol.name); if(old_it==symbol_table.symbols.end()) @@ -121,10 +121,11 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) throw 0; } + symbolt & existing_symbol=symbol_table.get_writeable(symbol.name); if(symbol.is_type) - typecheck_redefinition_type(old_it->second, symbol); + typecheck_redefinition_type(existing_symbol, symbol); else - typecheck_redefinition_non_type(old_it->second, symbol); + typecheck_redefinition_non_type(existing_symbol, symbol); } } @@ -350,10 +351,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type( { const irep_idt &identifier=p_it->get_identifier(); - symbol_tablet::symbolst::iterator p_s_it= + symbol_tablet::symbolst::const_iterator p_s_it= symbol_table.symbols.find(identifier); if(p_s_it!=symbol_table.symbols.end()) - symbol_table.symbols.erase(p_s_it); + symbol_table.erase(p_s_it); } } else @@ -732,10 +733,7 @@ void c_typecheck_baset::typecheck_declaration( // add code contract (if any); we typecheck this after the // function body done above, so as to have parameter symbols // available - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(identifier); - assert(s_it!=symbol_table.symbols.end()); - symbolt &new_symbol=s_it->second; + symbolt &new_symbol=symbol_table.get_writeable(identifier); typecheck_spec_expr(contract, ID_C_spec_requires); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a45420839a4..5529ab6213b 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -287,7 +287,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) irep_idt identifier=d_it->get_name(); // look it up - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -298,7 +298,7 @@ void c_typecheck_baset::typecheck_decl(codet &code) throw 0; } - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; // This must not be an incomplete type, unless it's 'extern' // or a typedef. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index c41a2240309..00d68f46c35 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -485,7 +485,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) symbol.name=ID_gcc_builtin_va_arg; symbol.type=symbol_type; - symbol_table.move(symbol); + symbol_table.insert(std::move(symbol)); } void c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(exprt &expr) @@ -704,7 +704,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) declaration.declarators().front().get_name(); // look it up - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -715,7 +715,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr) throw 0; } - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime || !is_complete_type(symbol.type) || symbol.type.id()==ID_code) diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index a047108d1b0..85e44a317d3 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -208,12 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type) { const irep_idt &tag_name= to_c_enum_tag_type(type.subtype()).get_identifier(); - - symbol_tablet::symbolst::iterator entry= - symbol_table.symbols.find(tag_name); - assert(entry!=symbol_table.symbols.end()); - - entry->second.type.subtype()=result; + symbol_table.get_writeable(tag_name).type.subtype()=result; } type=result; @@ -736,7 +731,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) identifier=type.find(ID_tag).get(ID_identifier); // does it exist already? - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it==symbol_table.symbols.end()) @@ -787,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) type.set(ID_tag, base_name); typecheck_compound_body(type); - s_it->second.type.swap(type); + symbol_table.get_writeable(s_it->first).type.swap(type); } } else if(have_body) @@ -1213,19 +1208,19 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) enum_tag_symbol.type.subtype()=underlying_type; // is it in the symbol table already? - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(identifier); if(s_it!=symbol_table.symbols.end()) { // Yes. - symbolt &symbol=s_it->second; + const symbolt &symbol=s_it->second; if(symbol.type.id()==ID_incomplete_c_enum) { // Ok, overwrite the type in the symbol table. // This gives us the members and the subtype. - symbol.type=enum_tag_symbol.type; + symbol_table.get_writeable(symbol.name).type=enum_tag_symbol.type; } else if(symbol.type.id()==ID_c_enum) { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 2ea5732f436..14fce68930c 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -98,10 +98,7 @@ symbolt &cpp_declarator_convertert::convert( } // try static first - symbol_tablet::symbolst::iterator c_it= - cpp_typecheck.symbol_table.symbols.find(final_identifier); - - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) { // adjust type if it's a non-static member function if(final_type.id()==ID_code) @@ -111,9 +108,7 @@ symbolt &cpp_declarator_convertert::convert( get_final_identifier(); // try again - c_it=cpp_typecheck.symbol_table.symbols.find(final_identifier); - - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) { cpp_typecheck.error().source_location= declarator.name().source_location(); @@ -125,9 +120,7 @@ symbolt &cpp_declarator_convertert::convert( } } - assert(c_it!=cpp_typecheck.symbol_table.symbols.end()); - - symbolt &symbol=c_it->second; + symbolt &symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); combine_types(declarator.name().source_location(), final_type, symbol); enforce_rules(symbol); @@ -194,13 +187,10 @@ symbolt &cpp_declarator_convertert::convert( } // already there? - symbol_tablet::symbolst::iterator c_it= - cpp_typecheck.symbol_table.symbols.find(final_identifier); - - if(c_it==cpp_typecheck.symbol_table.symbols.end()) + if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) return convert_new_symbol(storage_spec, member_spec, declarator); - symbolt &symbol=c_it->second; + symbolt &symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); if(!storage_spec.is_extern()) symbol.is_extern = false; diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index c80c757298e..f8d2328f913 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -372,7 +372,7 @@ const symbolt &cpp_typecheckt::instantiate_template( // been instantiated using these arguments { // need non-const handle on template symbol - symbolt &s=symbol_table.symbols.find(template_symbol.name)->second; + symbolt &s=symbol_table.get_writeable(template_symbol.name); irept &instantiated_with=s.value.add("instantiated_with"); instantiated_with.get_sub().push_back(specialization_template_args); } @@ -451,12 +451,7 @@ const symbolt &cpp_typecheckt::instantiate_template( if(is_template_method) { - symbol_tablet::symbolst::iterator it = - symbol_table.symbols.find(class_name); - - assert(it!=symbol_table.symbols.end()); - - symbolt &symb = it->second; + symbolt &symb=symbol_table.get_writeable(class_name); assert(new_decl.declarators().size() == 1); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index b1be4281d3b..b851de89087 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -151,9 +151,9 @@ void cpp_typecheckt::static_and_dynamic_initialization() disable_access_control = true; - for(const auto &d_it : dynamic_initializations) + for(const irep_idt &d_it : dynamic_initializations) { - symbolt &symbol=symbol_table.symbols.find(d_it)->second; + const symbolt &symbol=symbol_table.lookup(d_it); if(symbol.is_extern) continue; @@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() // Make it nil to get zero initialization by // __CPROVER_initialize - symbol.value.make_nil(); + symbol_table.get_writeable(d_it).value.make_nil(); } else { @@ -210,7 +210,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() init_symbol.is_type=false; init_symbol.is_macro=false; - symbol_table.move(init_symbol); + symbol_table.insert(std::move(init_symbol)); disable_access_control=false; } @@ -223,14 +223,15 @@ void cpp_typecheckt::do_not_typechecked() { cont = false; - Forall_symbols(s_it, symbol_table.symbols) + for(const auto &named_symbol : symbol_table.symbols) { - symbolt &symbol=s_it->second; + const symbolt &symbol=named_symbol.second; if(symbol.value.id()=="cpp_not_typechecked" && symbol.value.get_bool("is_used")) { assert(symbol.type.id()==ID_code); + symbolt &symbol=symbol_table.get_writeable(named_symbol.first); if(symbol.base_name=="operator=") { @@ -256,29 +257,28 @@ void cpp_typecheckt::do_not_typechecked() } while(cont); - Forall_symbols(s_it, symbol_table.symbols) + for(const auto &named_symbol : symbol_table.symbols) { - symbolt &symbol=s_it->second; - if(symbol.value.id()=="cpp_not_typechecked") - symbol.value.make_nil(); + if(named_symbol.second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(named_symbol.first).value.make_nil(); } } void cpp_typecheckt::clean_up() { - symbol_tablet::symbolst::iterator it=symbol_table.symbols.begin(); + symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); while(it!=symbol_table.symbols.end()) { - symbol_tablet::symbolst::iterator cur_it = it; + symbol_tablet::symbolst::const_iterator cur_it = it; it++; - symbolt &symbol = cur_it->second; + const symbolt &symbol=cur_it->second; // erase templates if(symbol.type.get_bool(ID_is_template)) { - symbol_table.symbols.erase(cur_it); + symbol_table.erase(cur_it); continue; } else if(symbol.type.id()==ID_struct || @@ -286,7 +286,7 @@ void cpp_typecheckt::clean_up() { // remove methods from 'components' struct_union_typet &struct_union_type= - to_struct_union_type(symbol.type); + to_struct_union_type(symbol_table.get_writeable(cur_it->first).type); const struct_union_typet::componentst &components= struct_union_type.components(); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 6b5c7c1625b..14bf62b0d68 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -159,20 +159,17 @@ void cpp_typecheckt::typecheck_compound_type( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= - symbol_table.symbols.find(symbol_name); - - if(previous_symbol!=symbol_table.symbols.end()) + if(symbol_table.has_symbol(symbol_name)) { // we do! - - symbolt &symbol=previous_symbol->second; + const symbolt &symbol=symbol_table.lookup(symbol_name); if(has_body) { if(symbol.type.id()=="incomplete_"+type.id_string()) { // a previously incomplete struct/union becomes complete + symbolt &symbol=symbol_table.get_writeable(symbol_name); symbol.type.swap(type); typecheck_compound_body(symbol); } @@ -523,10 +520,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // get the virtual-table symbol type irep_idt vt_name="virtual_table::"+id2string(symbol.name); - symbol_tablet::symbolst::iterator vtit = - symbol_table.symbols.find(vt_name); - - if(vtit==symbol_table.symbols.end()) + if(!symbol_table.has_symbol(vt_name)) { // first time: create a virtual-table symbol type symbolt vt_symb_type; @@ -540,9 +534,8 @@ void cpp_typecheckt::typecheck_compound_declarator( vt_symb_type.type.set(ID_name, vt_symb_type.name); vt_symb_type.is_type=true; - bool failed=symbol_table.move(vt_symb_type); + bool failed=!symbol_table.insert(std::move(vt_symb_type)); assert(!failed); - vtit=symbol_table.symbols.find(vt_name); // add a virtual-table pointer struct_typet::componentt compo; @@ -558,10 +551,9 @@ void cpp_typecheckt::typecheck_compound_declarator( put_compound_into_scope(compo); } - assert(vtit->second.type.id()==ID_struct); - - struct_typet &virtual_table= - to_struct_type(vtit->second.type); + typet &vt=symbol_table.get_writeable(vt_name).type; + INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct"); + struct_typet &virtual_table=to_struct_type(vt); component.set("virtual_name", virtual_name); component.set("is_virtual", is_virtual); @@ -569,7 +561,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // add an entry to the virtual table struct_typet::componentt vt_entry; vt_entry.type()=pointer_type(component.type()); - vt_entry.set_name(id2string(vtit->first)+"::"+virtual_name); + vt_entry.set_name(id2string(vt_name)+"::"+virtual_name); vt_entry.set(ID_base_name, virtual_name); vt_entry.set(ID_pretty_name, virtual_name); vt_entry.set(ID_access, ID_public); @@ -618,7 +610,7 @@ void cpp_typecheckt::typecheck_compound_declarator( arg.set(ID_C_identifier, arg_symb.name); // add the parameter to the symbol table - bool failed=symbol_table.move(arg_symb); + bool failed=!symbol_table.insert(std::move(arg_symb)); assert(!failed); } @@ -676,7 +668,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // add the function to the symbol table { - bool failed=symbol_table.move(func_symb); + const bool failed=!symbol_table.insert(std::move(func_symb)); assert(!failed); } @@ -1416,7 +1408,7 @@ void cpp_typecheckt::convert_anon_struct_union_member( struct_typet::componentst &components) { symbolt &struct_union_symbol= - symbol_table.symbols[follow(declaration.type()).get(ID_name)]; + symbol_table.get_writeable(follow(declaration.type()).get(ID_name)); if(declaration.storage_spec().is_static() || declaration.storage_spec().is_mutable()) diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index c91c8d979cf..87d2b5626b1 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -74,7 +74,8 @@ void cpp_typecheckt::convert_anonymous_union( new_code.move_to_operands(decl_statement); // do scoping - symbolt union_symbol=symbol_table.symbols[follow(symbol.type).get(ID_name)]; + symbolt union_symbol= + symbol_table.get_writeable(follow(symbol.type).get(ID_name)); const irept::subt &components=union_symbol.type.add(ID_components).get_sub(); forall_irep(it, components) @@ -104,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union( id.is_member=true; } - symbol_table.symbols[union_symbol.name].type.set( + symbol_table.get_writeable(union_symbol.name).type.set( "#unnamed_object", symbol.base_name); code.swap(new_code); diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 74a18107622..c7893c3c06a 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -121,14 +121,14 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) // check if we have it - symbol_tablet::symbolst::iterator previous_symbol= + symbol_tablet::symbolst::const_iterator previous_symbol= symbol_table.symbols.find(symbol_name); if(previous_symbol!=symbol_table.symbols.end()) { // we do! - symbolt &symbol=previous_symbol->second; + const symbolt &symbol=previous_symbol->second; if(has_body) { diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index dec8510eb7b..e1fda7f9f14 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1238,15 +1238,13 @@ void cpp_typecheckt::typecheck_expr_member( if(expr.type().id()==ID_code) { // Check if the function body has to be typechecked - symbol_tablet::symbolst::iterator it= + symbol_tablet::symbolst::const_iterator it= symbol_table.symbols.find(component_name); assert(it!=symbol_table.symbols.end()); - symbolt &func_symb=it->second; - - if(func_symb.value.id()=="cpp_not_typechecked") - func_symb.value.set("is_used", true); + if(it->second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(component_name).value.set("is_used", true); } } @@ -2204,10 +2202,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( type.id()==ID_code && type.find(ID_return_type).id()==ID_destructor) { - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(it->get(ID_name)); - assert(s_it!=symbol_table.symbols.end()); - add_method_body(&(s_it->second)); + add_method_body(&symbol_table.get_writeable(it->get(ID_name))); break; } } @@ -2376,7 +2371,7 @@ void cpp_typecheckt::typecheck_method_application( member_expr.swap(expr.function()); const symbolt &symbol=lookup(member_expr.get(ID_component_name)); - add_method_body(&(symbol_table.symbols.find(symbol.name)->second)); + add_method_body(&symbol_table.get_writeable(symbol.name)); // build new function expression exprt new_function(cpp_symbol_expr(symbol)); @@ -2418,7 +2413,7 @@ void cpp_typecheckt::typecheck_method_application( if(symbol.value.id()=="cpp_not_typechecked" && !symbol.value.get_bool("is_used")) { - symbol_table.symbols[symbol.name].value.set("is_used", true); + symbol_table.get_writeable(symbol.name).value.set("is_used", true); } } @@ -2681,15 +2676,13 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr) if(expr.id()==ID_symbol) { // Check if the function body has to be typechecked - symbol_tablet::symbolst::iterator it= + symbol_tablet::symbolst::const_iterator it= symbol_table.symbols.find(expr.get(ID_identifier)); assert(it != symbol_table.symbols.end()); - symbolt &func_symb=it->second; - - if(func_symb.value.id()=="cpp_not_typechecked") - func_symb.value.set("is_used", true); + if(it->second.value.id()=="cpp_not_typechecked") + symbol_table.get_writeable(it->first).value.set("is_used", true); } c_typecheck_baset::typecheck_expr_function_identifier(expr); diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index c3ae770ad90..f41ebe2b196 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -73,7 +73,7 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) symbol.module=module; symbol.type=typet(ID_namespace); - if(symbol_table.move(symbol)) + if(!symbol_table.insert(std::move(symbol))) { error().source_location=symbol.location; error() << "cpp_typecheckt::convert_namespace: symbol_table.move() failed" diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 4fb722f011e..06f16f6010c 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -107,14 +107,12 @@ void cpp_typecheckt::typecheck_class_template( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= - symbol_table.symbols.find(symbol_name); - - if(previous_symbol!=symbol_table.symbols.end()) + if(symbol_table.has_symbol(symbol_name)) { // there already + auto &previous_symbol=symbol_table.get_writeable(symbol_name); cpp_declarationt &previous_declaration= - to_cpp_declaration(previous_symbol->second.type); + to_cpp_declaration(previous_symbol.type); bool previous_has_body= previous_declaration.type().find(ID_body).is_not_nil(); @@ -126,7 +124,7 @@ void cpp_typecheckt::typecheck_class_template( error() << "template struct `" << base_name << "' defined previously\n" << "location of previous definition: " - << previous_symbol->second.location << eom; + << previous_symbol.location << eom; throw 0; } @@ -138,7 +136,7 @@ void cpp_typecheckt::typecheck_class_template( previous_declaration.template_type(), declaration.template_type()); - previous_symbol->second.type.swap(declaration); + previous_symbol.type.swap(declaration); #if 0 std::cout << "*****\n"; @@ -244,7 +242,7 @@ void cpp_typecheckt::typecheck_function_template( // check if we have it already - symbol_tablet::symbolst::iterator previous_symbol= + symbol_tablet::symbolst::const_iterator previous_symbol= symbol_table.symbols.find(symbol_name); if(previous_symbol!=symbol_table.symbols.end()) @@ -265,7 +263,7 @@ void cpp_typecheckt::typecheck_function_template( if(has_value) { - previous_symbol->second.type.swap(declaration); + symbol_table.get_writeable(symbol_name).type.swap(declaration); cpp_scopes.id_map[symbol_name]=&template_scope; } @@ -384,7 +382,7 @@ void cpp_typecheckt::typecheck_class_template_member( const cpp_idt &cpp_id=**(id_set.begin()); symbolt &template_symbol= - symbol_table.symbols.find(cpp_id.identifier)->second; + symbol_table.get_writeable(cpp_id.identifier); exprt &template_methods=static_cast( template_symbol.value.add("template_methods")); @@ -576,12 +574,12 @@ void cpp_typecheckt::convert_class_template_specialization( throw 0; } - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find((*id_set.begin())->identifier); assert(s_it!=symbol_table.symbols.end()); - symbolt &template_symbol=s_it->second; + const symbolt &template_symbol=s_it->second; if(!template_symbol.type.get_bool(ID_is_template)) { diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index ade9c5c1568..2b65c0ca7d3 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -95,7 +95,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) } vt_symb_var.value=values; - bool failed=symbol_table.move(vt_symb_var); + bool failed=!symbol_table.insert(std::move(vt_symb_var)); assert(!failed); } } diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 03cdd8544f6..ff4a560d094 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -704,8 +704,8 @@ void compilet::convert_symbols(goto_functionst &dest) typedef std::set symbols_sett; symbols_sett symbols; - Forall_symbols(it, symbol_table.symbols) - symbols.insert(it->first); + for(const auto &named_symbol : symbol_table.symbols) + symbols.insert(named_symbol.first); // the symbol table iterators aren't stable for(symbols_sett::const_iterator @@ -713,7 +713,8 @@ void compilet::convert_symbols(goto_functionst &dest) it!=symbols.end(); ++it) { - symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(*it); + symbol_tablet::symbolst::const_iterator s_it= + symbol_table.symbols.find(*it); assert(s_it!=symbol_table.symbols.end()); if(s_it->second.type.id()==ID_code && @@ -724,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest) { debug() << "Compiling " << s_it->first << eom; converter.convert_function(s_it->first); - s_it->second.value=exprt("compiled"); + symbol_table.get_writeable(*it).value=exprt("compiled"); } } } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index f7ee9e0b057..947afcf518c 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -168,17 +168,17 @@ int linker_script_merget::pointerize_linker_defined_symbols( // First, pointerize the actual linker-defined symbols for(const auto &pair : linker_values) { - const auto &entry=symbol_table.symbols.find(pair.first); - if(entry==symbol_table.symbols.end()) + if(!symbol_table.has_symbol(pair.first)) continue; - entry->second.type=pointer_type(char_type()); - entry->second.is_extern=false; - entry->second.value=pair.second.second; + symbolt &entry=symbol_table.get_writeable(pair.first); + entry.type=pointer_type(char_type()); + entry.is_extern=false; + entry.value=pair.second.second; } // Next, find all occurrences of linker-defined symbols that are _values_ // of some symbol in the symbol table, and pointerize them too - for(auto &pair : symbol_table.symbols) + for(const auto &pair : symbol_table.symbols) { std::list to_pointerize; symbols_to_pointerize(linker_values, pair.second.value, to_pointerize); @@ -188,7 +188,9 @@ int linker_script_merget::pointerize_linker_defined_symbols( debug() << "Pointerizing the symbol-table value of symbol " << pair.first << eom; int fail=pointerize_subexprs_of( - pair.second.value, to_pointerize, linker_values); + symbol_table.get_writeable(pair.first).value, + to_pointerize, + linker_values); if(to_pointerize.empty() && fail==0) continue; ret=1; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 0b210d966d1..8e485d62ea6 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -47,14 +47,15 @@ void dump_ct::operator()(std::ostream &os) // add copies of struct types when ID_C_transparent_union is only // annotated to parameter symbol_tablet symbols_transparent; - Forall_symbols(it, copied_symbol_table.symbols) + for(const auto &named_symbol : copied_symbol_table.symbols) { - symbolt &symbol=it->second; + const symbolt &symbol=named_symbol.second; if(symbol.type.id()!=ID_code) continue; - code_typet &code_type=to_code_type(symbol.type); + code_typet &code_type= + to_code_type(copied_symbol_table.get_writeable(named_symbol.first).type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -90,9 +91,9 @@ void dump_ct::operator()(std::ostream &os) // add tags to anonymous union/struct/enum, // and prepare lexicographic order std::set symbols_sorted; - Forall_symbols(it, copied_symbol_table.symbols) + for(const auto &named_symbol : copied_symbol_table.symbols) { - symbolt &symbol=it->second; + symbolt &symbol=copied_symbol_table.get_writeable(named_symbol.first); bool tag_added=false; // TODO we could get rid of some of the ID_anonymous by looking up @@ -113,7 +114,7 @@ void dump_ct::operator()(std::ostream &os) tag_added=true; } - const std::string name_str=id2string(it->first); + const std::string name_str=id2string(named_symbol.first); if(symbol.is_type && (symbol.type.id()==ID_union || symbol.type.id()==ID_struct || diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index 5cf1883fb8f..938f0e83db1 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -45,7 +45,7 @@ code_function_callt function_to_call( new_symbol.base_name=id; new_symbol.type=function_type; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); s_it=symbol_table.symbols.find(id); assert(s_it!=symbol_table.symbols.end()); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index e773b91cd02..0338042d417 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -133,11 +133,8 @@ void goto_program2codet::scan_for_varargs() { system_headers.insert("stdarg.h"); - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(func_name); - assert(it!=symbol_table.symbols.end()); - - code_typet &code_type=to_code_type(it->second.type); + code_typet &code_type= + to_code_type(symbol_table.get_writeable(func_name).type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -1671,12 +1668,10 @@ void goto_program2codet::remove_const(typet &type) if(!const_removed.insert(identifier).second) return; - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(identifier); - assert(it!=symbol_table.symbols.end()); - assert(it->second.is_type); + symbolt &symbol=symbol_table.get_writeable(identifier); + assert(symbol.is_type); - remove_const(it->second.type); + remove_const(symbol.type); } else if(type.id()==ID_array) remove_const(type.subtype()); @@ -1959,7 +1954,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) symbol.type=code_type; id=symbol.name; - symbol_table.move(symbol); + symbol_table.insert(std::move(symbol)); } const symbolt &symbol=ns.lookup(id); diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index 2ec053ccac4..d175d7ca3b0 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -51,7 +51,7 @@ void remove_function( message.status() << "Removing body of " << identifier << messaget::eom; entry->second.clear(); - goto_model.symbol_table.lookup(identifier).value.make_nil(); + goto_model.symbol_table.get_writeable(identifier).value.make_nil(); } } diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 2dc96cdf8bd..606a25f40bb 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -38,7 +38,7 @@ symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table) new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return symbol_exprt(identifier, type); } diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 5c416946213..188e750b2c9 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -93,7 +93,7 @@ void uninitializedt::add_assertions(goto_programt &goto_program) new_symbol.is_file_local=true; new_symbol.is_lvalue=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } Forall_goto_program_instructions(i_it, goto_program) diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index d51a16c13ad..14e0ff6208f 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -264,7 +264,7 @@ symbol_exprt goto_convertt::exception_flag() new_symbol.is_thread_local=true; new_symbol.is_file_local=false; new_symbol.type=bool_typet(); - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } return symbol_exprt(id, bool_typet()); diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index 78b655e4108..ea60d6a6ff1 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -282,8 +282,8 @@ static void remove_complex(symbolt &symbol) /// removes complex data type void remove_complex(symbol_tablet &symbol_table) { - Forall_symbols(it, symbol_table.symbols) - remove_complex(it->second); + for(const auto &named_symbol : symbol_table.symbols) + remove_complex(symbol_table.get_writeable(named_symbol.first)); } /// removes complex data type diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index d437ddf622b..48fa1589eb2 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -200,7 +200,7 @@ void remove_exceptionst::add_exceptional_returns( || has_uncaught_exceptions) { // look up the function symbol - symbol_tablet::symbolst::iterator s_it= + symbol_tablet::symbolst::const_iterator s_it= symbol_table.symbols.find(function_id); INVARIANT( diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index cc3a68440c3..62052b6e0c5 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -62,11 +62,7 @@ void remove_returnst::replace_returns( if(has_return_value) { // look up the function symbol - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(function_id); - - assert(s_it!=symbol_table.symbols.end()); - symbolt &function_symbol=s_it->second; + symbolt &function_symbol=symbol_table.get_writeable(function_id); // make the return type 'void' f_it->second.type.return_type()=empty_typet(); @@ -251,18 +247,14 @@ bool remove_returnst::restore_returns( // do we have X#return_value? std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX; - symbol_tablet::symbolst::iterator rv_it= + symbol_tablet::symbolst::const_iterator rv_it= symbol_table.symbols.find(rv_name); if(rv_it==symbol_table.symbols.end()) return true; // look up the function symbol - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(function_id); - - assert(s_it!=symbol_table.symbols.end()); - symbolt &function_symbol=s_it->second; + symbolt &function_symbol=symbol_table.get_writeable(function_id); // restore the return type f_it->second.type=original_return_type(symbol_table, function_id); @@ -270,7 +262,7 @@ bool remove_returnst::restore_returns( // remove the return_value symbol from the symbol_table irep_idt rv_name_id=rv_it->second.name; - symbol_table.symbols.erase(rv_it); + symbol_table.erase(rv_it); goto_programt &goto_program=f_it->second.body; diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index a5874999b78..93e1a45907e 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -190,8 +190,8 @@ static void remove_vector(symbolt &symbol) /// removes vector data type static void remove_vector(symbol_tablet &symbol_table) { - Forall_symbols(it, symbol_table.symbols) - remove_vector(it->second); + for(const auto &named_symbol : symbol_table.symbols) + remove_vector(symbol_table.get_writeable(named_symbol.first)); } /// removes vector data type diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index f7599e16578..8cf7d931642 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -174,9 +174,7 @@ void string_abstractiont::add_str_arguments( const irep_idt &name, goto_functionst::goto_functiont &fct) { - symbol_tablet::symbolst::iterator sym_entry=symbol_table.symbols.find(name); - assert(sym_entry!=symbol_table.symbols.end()); - symbolt &fct_symbol=sym_entry->second; + symbolt &fct_symbol=symbol_table.get_writeable(name); code_typet::parameterst ¶meters= to_code_type(fct.type).parameters(); @@ -234,7 +232,7 @@ void string_abstractiont::add_argument( new_symbol.mode=fct_symbol.mode; new_symbol.pretty_name=str_args.back().get_base_name(); - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } void string_abstractiont::abstract(goto_programt &dest) @@ -453,7 +451,7 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( assignment1->code.add_source_location()=ref_instr->source_location; } - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return sym_expr; } @@ -937,7 +935,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write) new_symbol.mode=ID_C; new_symbol.pretty_name=identifier; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); return ns.lookup(identifier).symbol_expr(); } @@ -989,7 +987,7 @@ void string_abstractiont::build_new_symbol(const symbolt &symbol, new_symbol.is_static_lifetime=symbol.is_static_lifetime; new_symbol.is_thread_local=symbol.is_thread_local; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); if(symbol.is_static_lifetime) { @@ -1037,7 +1035,7 @@ bool string_abstractiont::build_symbol_constant( assignment1->code=code_assignt(new_symbol.symbol_expr(), value); } - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } dest=address_of_exprt(symbol_exprt(identifier, string_struct)); diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 6e696c30042..a0741d6a7d7 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -809,8 +809,8 @@ void string_instrumentationt::do_strerror( new_symbol_buf.pretty_name=new_symbol_buf.base_name; new_symbol_buf.name=new_symbol_buf.base_name; - symbol_table.move(new_symbol_buf); - symbol_table.move(new_symbol_size); + symbol_table.insert(std::move(new_symbol_buf)); + symbol_table.insert(std::move(new_symbol_size)); } const symbolt &symbol_size=ns.lookup(identifier_size); @@ -885,7 +885,7 @@ void string_instrumentationt::invalidate_buffer( new_symbol.is_lvalue=true; new_symbol.is_static_lifetime=true; - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } const symbolt &cntr_sym=ns.lookup(cntr_id); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 6dc9a944010..0243f1487c2 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -156,7 +156,7 @@ void goto_symext::parameter_assignments( symbol.base_name="va_arg"+std::to_string(va_count); symbol.type=it1->type(); - new_symbol_table.move(symbol); + new_symbol_table.insert(std::move(symbol)); symbol_exprt lhs=symbol_exprt(id, it1->type()); diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 0942b52fbf7..d27ff99b41b 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -216,7 +216,7 @@ void java_bytecode_convert_classt::convert( // Do we have the static field symbol already? const auto s_it=symbol_table.symbols.find(new_symbol.name); if(s_it!=symbol_table.symbols.end()) - symbol_table.symbols.erase(s_it); // erase, we stubbed it + symbol_table.erase(s_it); // erase, we stubbed it if(symbol_table.add(new_symbol)) assert(false && "failed to add static field symbol"); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 840b214049a..b3b497806f4 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -488,7 +488,7 @@ void java_bytecode_convert_methodt::convert( INVARIANT( s_it!=symbol_table.symbols.end(), "the symbol was there earlier on this function; it must be there now"); - symbol_table.symbols.erase(s_it); + symbol_table.erase(s_it); // Insert the method symbol in the symbol table symbol_table.add(method_symbol); diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index dd29b0b5ec5..eb26390d1ad 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -617,5 +617,5 @@ void java_bytecode_instrument( // instrument(...) can add symbols to the table, so it's // not safe to hold a reference to a symbol across a call. for(const auto &symbol : symbols_to_instrument) - instrument(symbol_table.lookup(symbol).value); + instrument(symbol_table.get_writeable(symbol).value); } diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index afda2091079..553d1903382 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -374,7 +374,7 @@ void java_bytecode_languaget::replace_string_methods( if(generated_code.is_not_nil()) { // Replace body of the function by code generated by string preprocess - symbolt &symbol=context.lookup(id); + symbolt &symbol=context.get_writeable(id); symbol.value=generated_code; // Specifically instrument the new code, since this comes after the // blanket instrumentation pass called before typechecking. diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index 5b09fcdaf23..7833cd2d44e 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/src/java_bytecode/java_bytecode_typecheck.cpp @@ -48,22 +48,18 @@ void java_bytecode_typecheckt::typecheck() // recursively doing base classes first. for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.symbols[id]; - + symbolt &symbol=symbol_table.get_writeable(id); if(!symbol.is_type) continue; - typecheck_type_symbol(symbol); } // We now check all non-type symbols for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.symbols[id]; - + symbolt &symbol=symbol_table.get_writeable(id); if(symbol.is_type) continue; - typecheck_non_type_symbol(symbol); } } diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index f25e988e850..4cf3568d410 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -291,7 +291,7 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr) // member doesn't exist. In this case struct_type should be an opaque // stub, and we'll add the member to it. symbolt &symbol_table_type= - symbol_table.lookup("java::"+id2string(struct_type.get_tag())); + symbol_table.get_writeable("java::"+id2string(struct_type.get_tag())); auto &add_to_components= to_struct_type(symbol_table_type.type).components(); add_to_components diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 08c1f44564b..342a22035af 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -40,7 +40,7 @@ static void create_initialize(symbol_tablet &symbol_table) { // If __CPROVER_initialize already exists, replace it. It may already exist // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend. - symbol_table.symbols.erase(INITIALIZE_FUNCTION); + symbol_table.remove(INITIALIZE_FUNCTION); symbolt initialize; initialize.name=INITIALIZE_FUNCTION; @@ -96,7 +96,7 @@ void java_static_lifetime_init( const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { - symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE_FUNCTION); + symbolt &initialize_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION); code_blockt &code_block=to_code_block(to_code(initialize_symbol.value)); // We need to zero out all static variables, or nondet-initialize if they're @@ -541,7 +541,7 @@ bool generate_java_start_function( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(INITIALIZE_FUNCTION); if(init_it==symbol_table.symbols.end()) @@ -668,7 +668,7 @@ bool generate_java_start_function( new_symbol.value.swap(init_code); new_symbol.mode=ID_java; - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol))) { message.error() << "failed to move main symbol" << messaget::eom; return true; diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index c4176fd741a..fdf03006318 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -166,7 +166,7 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( /// \param symbol_table: a symbol_table containing an entry for java Strings /// \return the type of data fields in java Strings. -typet string_data_type(symbol_tablet symbol_table) +typet string_data_type(const symbol_tablet &symbol_table) { symbolt sym=symbol_table.lookup("java::java.lang.String"); typet concrete_type=sym.type; diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index 328a1c76223..1b0bf9c02c2 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -50,7 +50,7 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree) if(symbol_table.has_symbol(new_symbol.name)) { - symbolt &s=symbol_table.lookup(new_symbol.name); + const symbolt &s=symbol_table.lookup(new_symbol.name); if(s.value.id()=="no-body-just-yet") { symbol_table.remove(s.name); diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 2f4d88e1bb3..50b3e5e54aa 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -129,7 +129,7 @@ bool jsil_entry_point( // build call to initialization function { - symbol_tablet::symbolst::iterator init_it= + symbol_tablet::symbolst::const_iterator init_it= symbol_table.symbols.find(CPROVER_PREFIX "initialize"); if(init_it==symbol_table.symbols.end()) @@ -162,7 +162,7 @@ bool jsil_entry_point( new_symbol.type.swap(main_type); new_symbol.value.swap(init_code); - if(symbol_table.move(new_symbol)) + if(!symbol_table.insert(std::move(new_symbol))) { messaget message; message.set_message_handler(message_handler); diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index 81ebf82f87b..e82a6967dc0 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -48,7 +48,7 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) throw 0; } - symbolt &s=symbol_table.lookup(id); + symbolt &s=symbol_table.get_writeable(id); if(s.type.id().empty() || s.type.is_nil()) s.type=type; else @@ -749,11 +749,11 @@ void jsil_typecheckt::typecheck_function_call( if(symbol_table.has_symbol(id)) { - symbolt &s=symbol_table.lookup(id); + const symbolt &s=symbol_table.lookup(id); if(s.type.id()==ID_code) { - code_typet &codet=to_code_type(s.type); + const code_typet &codet=to_code_type(s.type); for(std::size_t i=0; i src_symbols; // First apply the renaming - Forall_symbols(s_it, src_symbol_table.symbols) + for(const auto &named_symbol : src_symbol_table.symbols) { + symbolt symbol=named_symbol.second; // apply the renaming - rename_symbol(s_it->second.type); - rename_symbol(s_it->second.value); + rename_symbol(symbol.type); + rename_symbol(symbol.value); + // Add to vector + src_symbols.emplace(named_symbol.first, std::move(symbol)); } // Move over all the non-colliding ones id_sett collisions; - Forall_symbols(s_it, src_symbol_table.symbols) + for(const auto &named_symbol : src_symbols) { // renamed? - if(s_it->first!=s_it->second.name) + if(named_symbol.first!=named_symbol.second.name) { // new - main_symbol_table.add(s_it->second); + main_symbol_table.add(named_symbol.second); } else { - symbol_tablet::symbolst::iterator - m_it=main_symbol_table.symbols.find(s_it->first); - - if(m_it==main_symbol_table.symbols.end()) + if(!main_symbol_table.has_symbol(named_symbol.first)) { // new - main_symbol_table.add(s_it->second); + main_symbol_table.add(named_symbol.second); } else - collisions.insert(s_it->first); + collisions.insert(named_symbol.first); } } // Now do the collisions - for(id_sett::const_iterator - i_it=collisions.begin(); - i_it!=collisions.end(); - i_it++) + for(const irep_idt &collision : collisions) { - symbolt &old_symbol=main_symbol_table.symbols[*i_it]; - symbolt &new_symbol=src_symbol_table.symbols[*i_it]; + symbolt &old_symbol=main_symbol_table.get_writeable(collision); + symbolt &new_symbol=src_symbols.at(collision); if(new_symbol.is_type) duplicate_type_symbol(old_symbol, new_symbol); @@ -1288,12 +1283,15 @@ void linkingt::copy_symbols() } // Apply type updates to initializers - Forall_symbols(s_it, main_symbol_table.symbols) + for(const auto &named_symbol : main_symbol_table.symbols) { - if(!s_it->second.is_type && - !s_it->second.is_macro && - s_it->second.value.is_not_nil()) - object_type_updates(s_it->second.value); + if(!named_symbol.second.is_type && + !named_symbol.second.is_macro && + named_symbol.second.value.is_not_nil()) + { + object_type_updates( + main_symbol_table.get_writeable(named_symbol.first).value); + } } } diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index d3fa633af2f..70b59f59bc1 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -105,7 +105,7 @@ class linkingt:public typecheckt void duplicate_type_symbol( symbolt &old_symbol, - symbolt &new_symbol); + const symbolt &new_symbol); std::string expr_to_string( const namespacet &ns, diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 4755515200e..11037431b66 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -61,15 +61,16 @@ void get_symbols_rec( } } -/// A symbol is EXPORTED if it is a * non-static function with body that is not -/// extern inline * symbol used in an EXPORTED symbol * type used in an EXPORTED -/// symbol +/// Removes internal symbols from a symbol table +/// A symbol is EXPORTED if it is a +/// * non-static function with body that is not extern inline +/// * symbol used in an EXPORTED symbol +/// * type used in an EXPORTED symbol /// /// Read /// http://gcc.gnu.org/ml/gcc/2006-11/msg00006.html /// on "extern inline" -/// \par parameters: symbol table -/// \return symbol table, with internal symbols removed +/// \param symbol_table: symbol table to clean up void remove_internal_symbols( symbol_tablet &symbol_table) { @@ -148,16 +149,15 @@ void remove_internal_symbols( } // remove all that are _not_ exported! - for(symbol_tablet::symbolst::iterator + for(symbol_tablet::symbolst::const_iterator it=symbol_table.symbols.begin(); it!=symbol_table.symbols.end(); ) // no it++ { if(exported.find(it->first)==exported.end()) { - symbol_tablet::symbolst::iterator next=it; - ++next; - symbol_table.symbols.erase(it); + symbol_tablet::symbolst::const_iterator next=std::next(it); + symbol_table.erase(it); it=next; } else diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 2cacc49b032..8fe0d160739 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -31,13 +31,10 @@ bool static_lifetime_init( { namespacet ns(symbol_table); - symbol_tablet::symbolst::iterator s_it= - symbol_table.symbols.find(INITIALIZE_FUNCTION); - - if(s_it==symbol_table.symbols.end()) + if(!symbol_table.has_symbol(INITIALIZE_FUNCTION)) return false; - symbolt &init_symbol=s_it->second; + symbolt &init_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION); init_symbol.value=code_blockt(); init_symbol.value.add_source_location()=source_location; @@ -104,12 +101,9 @@ bool static_lifetime_init( { // C standard 6.9.2, paragraph 5 // adjust the type to an array of size 1 - symbol_tablet::symbolst::iterator it= - symbol_table.symbols.find(identifier); - assert(it!=symbol_table.symbols.end()); - - it->second.type=type; - it->second.type.set(ID_size, from_integer(1, size_type())); + symbolt &symbol=symbol_table.get_writeable(identifier); + symbol.type=type; + symbol.type.set(ID_size, from_integer(1, size_type())); } if(type.id()==ID_incomplete_struct || diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index e8da3c0d773..f066427a13e 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -22,12 +22,6 @@ irep_idt failed_symbol_id(const irep_idt &id) void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table) { - if(!symbol.is_lvalue) - return; - - if(symbol.type.get(ID_C_failed_symbol)!="") - return; - if(symbol.type.id()==ID_pointer) { symbolt new_symbol; @@ -45,28 +39,32 @@ void add_failed_symbol(symbolt &symbol, symbol_tablet &symbol_table) if(new_symbol.type.id()==ID_pointer) add_failed_symbol(new_symbol, symbol_table); // recursive call - symbol_table.move(new_symbol); + symbol_table.insert(std::move(new_symbol)); } } +void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table) +{ + if(!symbol.is_lvalue) + return; + + if(symbol.type.get(ID_C_failed_symbol)!="") + return; + + add_failed_symbol(symbol_table.get_writeable(symbol.name), symbol_table); +} + void add_failed_symbols(symbol_tablet &symbol_table) { // the symbol table iterators are not stable, and // we are adding new symbols, this // is why we need a list of pointers - typedef std::list< ::symbolt *> symbol_listt; - symbol_listt symbol_list; - - Forall_symbols(it, symbol_table.symbols) - symbol_list.push_back(&(it->second)); + std::list symbol_list; + for(auto &named_symbol : symbol_table.symbols) + symbol_list.push_back(&(named_symbol.second)); - for(symbol_listt::const_iterator - it=symbol_list.begin(); - it!=symbol_list.end(); - it++) - { - add_failed_symbol(**it, symbol_table); - } + for(const symbolt *symbol : symbol_list) + add_failed_symbol(*symbol, symbol_table); } exprt get_failed_symbol( diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 87712e13bee..1323ee31b59 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -178,7 +178,7 @@ exprt value_set_dereferencet::dereference( failure_value=symbol.symbol_expr(); failure_value.set(ID_C_invalid_object, true); - new_symbol_table.move(symbol); + new_symbol_table.insert(std::move(symbol)); } valuet value; diff --git a/src/util/language.cpp b/src/util/language.cpp index 6bd0211d4a4..7f89a0b92c3 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -86,7 +86,8 @@ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) { if(is_symbol_opaque_function(symbol_entry.second)) { - symbolt &symbol=symbol_entry.second; + symbolt &symbol= + symbol_table.get_writeable(symbol_entry.second.name); generate_opaque_parameter_symbols(symbol, symbol_table); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index cfd35eaf8db..cf26879d324 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -12,7 +12,7 @@ bool symbol_tablet::add(const symbolt &symbol) { std::pair result= - symbols.emplace(symbol.name, symbol); + internal_symbols.emplace(symbol.name, symbol); if(!result.second) return true; add_base_and_module(result.first); @@ -29,7 +29,7 @@ optionalt> symbol_tablet::insert( { // Add the symbol to the table or retrieve existing symbol with the same name std::pair result= - symbols.emplace(symbol.name, std::move(symbol)); + internal_symbols.emplace(symbol.name, std::move(symbol)); if(!result.second) return optionalt>(); add_base_and_module(result.first); @@ -55,7 +55,7 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) { // Add an empty symbol to the table or retrieve existing symbol with same name std::pair result= - symbols.emplace(symbol.name, symbolt()); + internal_symbols.emplace(symbol.name, symbolt()); if(!result.second) { @@ -81,20 +81,20 @@ void symbol_tablet::add_base_and_module(symbolst::iterator added_symbol) try { symbol_base_mapt::iterator base_result= - symbol_base_map.emplace(symbol.base_name, symbol.name); + internal_symbol_base_map.emplace(symbol.base_name, symbol.name); try { - symbol_module_map.emplace(symbol.module, symbol.name); + internal_symbol_module_map.emplace(symbol.module, symbol.name); } catch(...) { - symbol_base_map.erase(base_result); + internal_symbol_base_map.erase(base_result); throw; } } catch(...) { - symbols.erase(added_symbol); + internal_symbols.erase(added_symbol); throw; } } @@ -107,13 +107,18 @@ bool symbol_tablet::remove(const irep_idt &name) symbolst::const_iterator entry=symbols.find(name); if(entry==symbols.end()) return true; + erase(entry); + return false; +} +void symbol_tablet::erase(const symbolst::const_iterator &entry) +{ const symbolt &symbol=entry->second; symbol_base_mapt::const_iterator base_it=symbol_base_map.lower_bound(entry->second.base_name), base_it_end=symbol_base_map.upper_bound(entry->second.base_name); - while(base_it!=base_it_end && base_it->second!=name) + while(base_it!=base_it_end && base_it->second!=symbol.name) ++base_it; INVARIANT( base_it!=base_it_end, @@ -121,12 +126,12 @@ bool symbol_tablet::remove(const irep_idt &name) "after it is added to the symbol_table " "(name: "+id2string(symbol.name)+", " "current base_name: "+id2string(symbol.base_name)+")"); - symbol_base_map.erase(base_it); + internal_symbol_base_map.erase(base_it); symbol_module_mapt::const_iterator module_it=symbol_module_map.lower_bound(entry->second.module), module_it_end=symbol_module_map.upper_bound(entry->second.module); - while(module_it!=module_it_end && module_it->second!=name) + while(module_it!=module_it_end && module_it->second!=symbol.name) ++module_it; INVARIANT( module_it!=module_it_end, @@ -134,10 +139,9 @@ bool symbol_tablet::remove(const irep_idt &name) "after it is added to the symbol_table " "(name: "+id2string(symbol.name)+", " "current module: "+id2string(symbol.module)+")"); - symbol_module_map.erase(module_it); + internal_symbol_module_map.erase(module_it); - symbols.erase(entry); - return false; + internal_symbols.erase(entry); } /// Print the contents of the symbol table @@ -164,17 +168,15 @@ const symbolt &symbol_tablet::lookup(const irep_idt &identifier) const return it->second; } -/// Find a symbol in the symbol table. Throws a string if no such symbol is -/// found. +/// Find a symbol in the symbol table. /// \param identifier: The name of the symbol to look for /// \return The symbol in the symbol table with the correct name -symbolt &symbol_tablet::lookup(const irep_idt &identifier) +symbolt &symbol_tablet::get_writeable(const irep_idt &identifier) { - symbolst::iterator it=symbols.find(identifier); - - if(it==symbols.end()) - throw "symbol "+id2string(identifier)+" not found"; - + symbolst::iterator it=internal_symbols.find(identifier); + INVARIANT( + it!=symbols.end(), + "symbol "+id2string(identifier)+" should be in the symbol map"); return it->second; } diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index a7ffdf5afe8..6729f28f2f5 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -21,10 +21,6 @@ for(symbol_tablet::symbolst::const_iterator it=(expr).begin(); \ it!=(expr).end(); ++it) -#define Forall_symbols(it, expr) \ - for(symbol_tablet::symbolst::iterator it=(expr).begin(); \ - it!=(expr).end(); ++it) - typedef std::multimap symbol_base_mapt; typedef std::multimap symbol_module_mapt; @@ -46,37 +42,84 @@ class symbol_tablet public: typedef std::unordered_map symbolst; - symbolst symbols; - symbol_base_mapt symbol_base_map; - symbol_module_mapt symbol_module_map; +private: + symbolst internal_symbols; + symbol_base_mapt internal_symbol_base_map; + symbol_module_mapt internal_symbol_module_map; - bool add(const symbolt &symbol); +public: + const symbolst &symbols; + const symbol_base_mapt &symbol_base_map; + const symbol_module_mapt &symbol_module_map; + + symbol_tablet() + : symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + symbol_tablet(const symbol_tablet &other) + : internal_symbols(other.internal_symbols), + internal_symbol_base_map(other.internal_symbol_base_map), + internal_symbol_module_map(other.symbol_module_map), + symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + + symbol_tablet &operator=(const symbol_tablet &other) + { + internal_symbols=other.internal_symbols; + internal_symbol_base_map=other.internal_symbol_base_map; + internal_symbol_module_map=other.symbol_module_map; + return *this; + } + + symbol_tablet(symbol_tablet &&other) + : internal_symbols(std::move(other.internal_symbols)), + internal_symbol_base_map(std::move(other.internal_symbol_base_map)), + internal_symbol_module_map(std::move(other.symbol_module_map)), + symbols(internal_symbols), + symbol_base_map(internal_symbol_base_map), + symbol_module_map(internal_symbol_module_map) + { + } + + symbol_tablet &operator=(symbol_tablet &&other) + { + internal_symbols=std::move(other.internal_symbols); + internal_symbol_base_map=std::move(other.internal_symbol_base_map); + internal_symbol_module_map=std::move(other.symbol_module_map); + return *this; + } + + bool add(const symbolt &symbol); optionalt> insert(symbolt &&symbol); bool move(symbolt &symbol, symbolt *&new_symbol); - // this will go away, use add instead - bool move(symbolt &symbol) - { symbolt *new_symbol; return move(symbol, new_symbol); } private: void add_base_and_module(symbolst::iterator added_symbol); public: void clear() { - symbols.clear(); - symbol_base_map.clear(); - symbol_module_map.clear(); + internal_symbols.clear(); + internal_symbol_base_map.clear(); + internal_symbol_module_map.clear(); } bool remove(const irep_idt &name); + void erase(const symbolst::const_iterator &entry); + void show(std::ostream &out) const; void swap(symbol_tablet &other) { - symbols.swap(other.symbols); - symbol_base_map.swap(other.symbol_base_map); - symbol_module_map.swap(other.symbol_module_map); + internal_symbols.swap(other.internal_symbols); + internal_symbol_base_map.swap(other.internal_symbol_base_map); + internal_symbol_module_map.swap(other.internal_symbol_module_map); } bool has_symbol(const irep_idt &name) const @@ -84,8 +127,8 @@ class symbol_tablet return symbols.find(name)!=symbols.end(); } - symbolt &lookup(const irep_idt &identifier); const symbolt &lookup(const irep_idt &identifier) const; + symbolt &get_writeable(const irep_idt &identifier); }; std::ostream &operator << ( From a9d802b38a931b79b0402666a59facad7dd721ae Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 25 Sep 2017 20:02:02 +0100 Subject: [PATCH 06/11] Made lookup return optional This was requested in review and removes a lot of double map lookups (has_symbol followed by lookup) --- src/ansi-c/ansi_c_entry_point.cpp | 2 +- src/ansi-c/c_typecheck_base.cpp | 4 +- src/ansi-c/c_typecheck_type.cpp | 6 +-- src/cpp/cpp_declarator_converter.cpp | 17 ++++++--- src/cpp/cpp_instantiate_template.cpp | 4 +- src/cpp/cpp_typecheck.cpp | 12 +++--- src/cpp/cpp_typecheck_compound_type.cpp | 12 +++--- src/cpp/cpp_typecheck_declaration.cpp | 4 +- src/cpp/cpp_typecheck_expr.cpp | 11 +++--- src/cpp/cpp_typecheck_template.cpp | 10 +++-- src/goto-cc/compile.cpp | 2 +- src/goto-cc/linker_script_merge.cpp | 8 ++-- src/goto-instrument/accelerate/accelerate.cpp | 2 +- .../accelerate/acceleration_utils.cpp | 2 +- .../accelerate/polynomial_accelerator.cpp | 2 +- src/goto-instrument/dump_c.cpp | 6 +-- src/goto-instrument/goto_program2code.cpp | 4 +- src/goto-instrument/remove_function.cpp | 2 +- src/goto-instrument/wmm/shared_buffers.h | 9 +++-- src/goto-programs/interpreter.cpp | 4 +- src/goto-programs/mm_io.cpp | 10 +++-- .../rebuild_goto_start_function.cpp | 2 +- src/goto-programs/remove_complex.cpp | 2 +- .../remove_const_function_pointers.cpp | 4 +- src/goto-programs/remove_exceptions.cpp | 38 ++++++++++--------- src/goto-programs/remove_returns.cpp | 4 +- .../remove_static_init_loops.cpp | 8 ++-- src/goto-programs/remove_vector.cpp | 2 +- .../remove_virtual_functions.cpp | 2 +- src/goto-programs/string_abstraction.cpp | 2 +- src/java_bytecode/ci_lazy_methods.cpp | 2 +- .../java_bytecode_convert_method.cpp | 13 ++++--- .../java_bytecode_instrument.cpp | 2 +- src/java_bytecode/java_bytecode_language.cpp | 2 +- src/java_bytecode/java_bytecode_typecheck.cpp | 4 +- .../java_bytecode_typecheck_expr.cpp | 2 +- src/java_bytecode/java_entry_point.cpp | 10 ++--- .../java_string_library_preprocess.cpp | 23 +++++------ src/jsil/jsil_convert.cpp | 6 ++- src/jsil/jsil_typecheck.cpp | 15 +++++--- src/linking/linking.cpp | 6 +-- src/linking/static_lifetime_init.cpp | 9 +++-- src/pointer-analysis/add_failed_symbols.cpp | 2 +- src/util/config.cpp | 7 ++-- src/util/language.cpp | 2 +- src/util/symbol_table.cpp | 24 ++++++------ src/util/symbol_table.h | 20 +++++----- .../convert_abstract_class.cpp | 10 ++--- unit/src/java_bytecode/load_java_class.cpp | 2 +- 49 files changed, 194 insertions(+), 164 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 70beee5c57c..dece5734526 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -72,7 +72,7 @@ void record_function_outputs( codet output(ID_output); output.operands().resize(2); - const symbolt &return_symbol=symbol_table.lookup("return'"); + const symbolt &return_symbol=*symbol_table.lookup("return'"); output.op0()= address_of_exprt( diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 46a4f4a1baa..1d213aa8f0a 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -121,7 +121,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol) throw 0; } - symbolt & existing_symbol=symbol_table.get_writeable(symbol.name); + symbolt & existing_symbol=*symbol_table.get_writeable(symbol.name); if(symbol.is_type) typecheck_redefinition_type(existing_symbol, symbol); else @@ -733,7 +733,7 @@ void c_typecheck_baset::typecheck_declaration( // add code contract (if any); we typecheck this after the // function body done above, so as to have parameter symbols // available - symbolt &new_symbol=symbol_table.get_writeable(identifier); + symbolt &new_symbol=*symbol_table.get_writeable(identifier); typecheck_spec_expr(contract, ID_C_spec_requires); diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 85e44a317d3..1cc2ac95cc0 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -208,7 +208,7 @@ void c_typecheck_baset::typecheck_type(typet &type) { const irep_idt &tag_name= to_c_enum_tag_type(type.subtype()).get_identifier(); - symbol_table.get_writeable(tag_name).type.subtype()=result; + symbol_table.get_writeable(tag_name)->get().type.subtype()=result; } type=result; @@ -782,7 +782,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) type.set(ID_tag, base_name); typecheck_compound_body(type); - symbol_table.get_writeable(s_it->first).type.swap(type); + symbol_table.get_writeable(s_it->first)->get().type.swap(type); } } else if(have_body) @@ -1220,7 +1220,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) { // Ok, overwrite the type in the symbol table. // This gives us the members and the subtype. - symbol_table.get_writeable(symbol.name).type=enum_tag_symbol.type; + symbol_table.get_writeable(symbol.name)->get().type=enum_tag_symbol.type; } else if(symbol.type.id()==ID_c_enum) { diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 14fce68930c..bdc977eff6f 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -98,7 +98,10 @@ symbolt &cpp_declarator_convertert::convert( } // try static first - if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) + symbol_tablet::opt_symbol_reft maybe_symbol= + cpp_typecheck.symbol_table.get_writeable(final_identifier); + + if(!maybe_symbol) { // adjust type if it's a non-static member function if(final_type.id()==ID_code) @@ -108,7 +111,8 @@ symbolt &cpp_declarator_convertert::convert( get_final_identifier(); // try again - if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) + maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); + if(!maybe_symbol) { cpp_typecheck.error().source_location= declarator.name().source_location(); @@ -120,7 +124,7 @@ symbolt &cpp_declarator_convertert::convert( } } - symbolt &symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); + symbolt &symbol=*maybe_symbol; combine_types(declarator.name().source_location(), final_type, symbol); enforce_rules(symbol); @@ -187,10 +191,11 @@ symbolt &cpp_declarator_convertert::convert( } // already there? - if(!cpp_typecheck.symbol_table.has_symbol(final_identifier)) + symbol_tablet::opt_symbol_reft maybe_symbol= + cpp_typecheck.symbol_table.get_writeable(final_identifier); + if(!maybe_symbol) return convert_new_symbol(storage_spec, member_spec, declarator); - - symbolt &symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier); + symbolt &symbol=*maybe_symbol; if(!storage_spec.is_extern()) symbol.is_extern = false; diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index f8d2328f913..50da8557d3b 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -372,7 +372,7 @@ const symbolt &cpp_typecheckt::instantiate_template( // been instantiated using these arguments { // need non-const handle on template symbol - symbolt &s=symbol_table.get_writeable(template_symbol.name); + symbolt &s=*symbol_table.get_writeable(template_symbol.name); irept &instantiated_with=s.value.add("instantiated_with"); instantiated_with.get_sub().push_back(specialization_template_args); } @@ -451,7 +451,7 @@ const symbolt &cpp_typecheckt::instantiate_template( if(is_template_method) { - symbolt &symb=symbol_table.get_writeable(class_name); + symbolt &symb=*symbol_table.get_writeable(class_name); assert(new_decl.declarators().size() == 1); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index b851de89087..570acc0aa1a 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -153,7 +153,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() for(const irep_idt &d_it : dynamic_initializations) { - const symbolt &symbol=symbol_table.lookup(d_it); + const symbolt &symbol=*symbol_table.lookup(d_it); if(symbol.is_extern) continue; @@ -178,7 +178,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() // Make it nil to get zero initialization by // __CPROVER_initialize - symbol_table.get_writeable(d_it).value.make_nil(); + symbol_table.get_writeable(d_it)->get().value.make_nil(); } else { @@ -231,7 +231,7 @@ void cpp_typecheckt::do_not_typechecked() symbol.value.get_bool("is_used")) { assert(symbol.type.id()==ID_code); - symbolt &symbol=symbol_table.get_writeable(named_symbol.first); + symbolt &symbol=*symbol_table.get_writeable(named_symbol.first); if(symbol.base_name=="operator=") { @@ -260,7 +260,7 @@ void cpp_typecheckt::do_not_typechecked() for(const auto &named_symbol : symbol_table.symbols) { if(named_symbol.second.value.id()=="cpp_not_typechecked") - symbol_table.get_writeable(named_symbol.first).value.make_nil(); + symbol_table.get_writeable(named_symbol.first)->get().value.make_nil(); } } @@ -285,8 +285,8 @@ void cpp_typecheckt::clean_up() symbol.type.id()==ID_union) { // remove methods from 'components' - struct_union_typet &struct_union_type= - to_struct_union_type(symbol_table.get_writeable(cur_it->first).type); + struct_union_typet &struct_union_type=to_struct_union_type( + symbol_table.get_writeable(cur_it->first)->get().type); const struct_union_typet::componentst &components= struct_union_type.components(); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 14bf62b0d68..6887d3163ce 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -159,17 +159,19 @@ void cpp_typecheckt::typecheck_compound_type( // check if we have it already - if(symbol_table.has_symbol(symbol_name)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(symbol_name); + if(maybe_symbol) { // we do! - const symbolt &symbol=symbol_table.lookup(symbol_name); + const symbolt &symbol=*maybe_symbol; if(has_body) { if(symbol.type.id()=="incomplete_"+type.id_string()) { // a previously incomplete struct/union becomes complete - symbolt &symbol=symbol_table.get_writeable(symbol_name); + symbolt &symbol=*symbol_table.get_writeable(symbol_name); symbol.type.swap(type); typecheck_compound_body(symbol); } @@ -551,7 +553,7 @@ void cpp_typecheckt::typecheck_compound_declarator( put_compound_into_scope(compo); } - typet &vt=symbol_table.get_writeable(vt_name).type; + typet &vt=symbol_table.get_writeable(vt_name)->get().type; INVARIANT(vt.id()==ID_struct, "Virtual tables must be stored as struct"); struct_typet &virtual_table=to_struct_type(vt); @@ -1408,7 +1410,7 @@ void cpp_typecheckt::convert_anon_struct_union_member( struct_typet::componentst &components) { symbolt &struct_union_symbol= - symbol_table.get_writeable(follow(declaration.type()).get(ID_name)); + *symbol_table.get_writeable(follow(declaration.type()).get(ID_name)); if(declaration.storage_spec().is_static() || declaration.storage_spec().is_mutable()) diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 87d2b5626b1..988b4de3568 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -75,7 +75,7 @@ void cpp_typecheckt::convert_anonymous_union( // do scoping symbolt union_symbol= - symbol_table.get_writeable(follow(symbol.type).get(ID_name)); + *symbol_table.get_writeable(follow(symbol.type).get(ID_name)); const irept::subt &components=union_symbol.type.add(ID_components).get_sub(); forall_irep(it, components) @@ -105,7 +105,7 @@ void cpp_typecheckt::convert_anonymous_union( id.is_member=true; } - symbol_table.get_writeable(union_symbol.name).type.set( + symbol_table.get_writeable(union_symbol.name)->get().type.set( "#unnamed_object", symbol.base_name); code.swap(new_code); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index e1fda7f9f14..b0a4a450395 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1244,7 +1244,8 @@ void cpp_typecheckt::typecheck_expr_member( assert(it!=symbol_table.symbols.end()); if(it->second.value.id()=="cpp_not_typechecked") - symbol_table.get_writeable(component_name).value.set("is_used", true); + symbol_table.get_writeable(component_name)->get() + .value.set("is_used", true); } } @@ -2202,7 +2203,7 @@ void cpp_typecheckt::typecheck_side_effect_function_call( type.id()==ID_code && type.find(ID_return_type).id()==ID_destructor) { - add_method_body(&symbol_table.get_writeable(it->get(ID_name))); + add_method_body(&symbol_table.get_writeable(it->get(ID_name))->get()); break; } } @@ -2371,7 +2372,7 @@ void cpp_typecheckt::typecheck_method_application( member_expr.swap(expr.function()); const symbolt &symbol=lookup(member_expr.get(ID_component_name)); - add_method_body(&symbol_table.get_writeable(symbol.name)); + add_method_body(&symbol_table.get_writeable(symbol.name)->get()); // build new function expression exprt new_function(cpp_symbol_expr(symbol)); @@ -2413,7 +2414,7 @@ void cpp_typecheckt::typecheck_method_application( if(symbol.value.id()=="cpp_not_typechecked" && !symbol.value.get_bool("is_used")) { - symbol_table.get_writeable(symbol.name).value.set("is_used", true); + symbol_table.get_writeable(symbol.name)->get().value.set("is_used", true); } } @@ -2682,7 +2683,7 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr) assert(it != symbol_table.symbols.end()); if(it->second.value.id()=="cpp_not_typechecked") - symbol_table.get_writeable(it->first).value.set("is_used", true); + symbol_table.get_writeable(it->first)->get().value.set("is_used", true); } c_typecheck_baset::typecheck_expr_function_identifier(expr); diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 06f16f6010c..feecc6ea169 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -107,10 +107,12 @@ void cpp_typecheckt::typecheck_class_template( // check if we have it already - if(symbol_table.has_symbol(symbol_name)) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(symbol_name); + if(maybe_symbol) { // there already - auto &previous_symbol=symbol_table.get_writeable(symbol_name); + symbolt &previous_symbol=*maybe_symbol; cpp_declarationt &previous_declaration= to_cpp_declaration(previous_symbol.type); @@ -263,7 +265,7 @@ void cpp_typecheckt::typecheck_function_template( if(has_value) { - symbol_table.get_writeable(symbol_name).type.swap(declaration); + symbol_table.get_writeable(symbol_name)->get().type.swap(declaration); cpp_scopes.id_map[symbol_name]=&template_scope; } @@ -382,7 +384,7 @@ void cpp_typecheckt::typecheck_class_template_member( const cpp_idt &cpp_id=**(id_set.begin()); symbolt &template_symbol= - symbol_table.get_writeable(cpp_id.identifier); + *symbol_table.get_writeable(cpp_id.identifier); exprt &template_methods=static_cast( template_symbol.value.add("template_methods")); diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index ff4a560d094..530e074bd88 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -725,7 +725,7 @@ void compilet::convert_symbols(goto_functionst &dest) { debug() << "Compiling " << s_it->first << eom; converter.convert_function(s_it->first); - symbol_table.get_writeable(*it).value=exprt("compiled"); + symbol_table.get_writeable(*it)->get().value=exprt("compiled"); } } } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 947afcf518c..8d683aa4418 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -168,9 +168,11 @@ int linker_script_merget::pointerize_linker_defined_symbols( // First, pointerize the actual linker-defined symbols for(const auto &pair : linker_values) { - if(!symbol_table.has_symbol(pair.first)) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(pair.first); + if(!maybe_symbol) continue; - symbolt &entry=symbol_table.get_writeable(pair.first); + symbolt &entry=*maybe_symbol; entry.type=pointer_type(char_type()); entry.is_extern=false; entry.value=pair.second.second; @@ -188,7 +190,7 @@ int linker_script_merget::pointerize_linker_defined_symbols( debug() << "Pointerizing the symbol-table value of symbol " << pair.first << eom; int fail=pointerize_subexprs_of( - symbol_table.get_writeable(pair.first).value, + symbol_table.get_writeable(pair.first)->get().value, to_pointerize, linker_values); if(to_pointerize.empty() && fail==0) diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 199ea59de21..518765e11ab 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -428,7 +428,7 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator) if(it->id()==ID_symbol && it->type() == bool_typet()) { const irep_idt &id=to_symbol_expr(*it).get_identifier(); - const symbolt &sym=symbol_table.lookup(id); + const symbolt &sym=*symbol_table.lookup(id); if(sym.module=="scratch") { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index b275be15bab..9a3ac8651f5 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -233,7 +233,7 @@ void acceleration_utilst::stash_variables( it!=vars.end(); ++it) { - symbolt orig=symbol_table.lookup(*it); + symbolt orig=*symbol_table.lookup(*it); symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type); substitution[orig.symbol_expr()]=stashed_sym.symbol_expr(); program.assign(stashed_sym.symbol_expr(), orig.symbol_expr()); diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index ccd3691560f..7ff1a9e5679 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -773,7 +773,7 @@ void polynomial_acceleratort::stash_variables( it!=vars.end(); ++it) { - symbolt orig=symbol_table.lookup(*it); + symbolt orig=*symbol_table.lookup(*it); symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type); substitution[orig.symbol_expr()]=stashed_sym.symbol_expr(); program.assign(stashed_sym.symbol_expr(), orig.symbol_expr()); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 8e485d62ea6..2384f225513 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -54,8 +54,8 @@ void dump_ct::operator()(std::ostream &os) if(symbol.type.id()!=ID_code) continue; - code_typet &code_type= - to_code_type(copied_symbol_table.get_writeable(named_symbol.first).type); + code_typet &code_type=to_code_type( + copied_symbol_table.get_writeable(named_symbol.first)->get().type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -93,7 +93,7 @@ void dump_ct::operator()(std::ostream &os) std::set symbols_sorted; for(const auto &named_symbol : copied_symbol_table.symbols) { - symbolt &symbol=copied_symbol_table.get_writeable(named_symbol.first); + symbolt &symbol=*copied_symbol_table.get_writeable(named_symbol.first); bool tag_added=false; // TODO we could get rid of some of the ID_anonymous by looking up diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 0338042d417..a299159d8dc 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -134,7 +134,7 @@ void goto_program2codet::scan_for_varargs() system_headers.insert("stdarg.h"); code_typet &code_type= - to_code_type(symbol_table.get_writeable(func_name).type); + to_code_type(symbol_table.get_writeable(func_name)->get().type); code_typet::parameterst ¶meters=code_type.parameters(); for(code_typet::parameterst::iterator @@ -1668,7 +1668,7 @@ void goto_program2codet::remove_const(typet &type) if(!const_removed.insert(identifier).second) return; - symbolt &symbol=symbol_table.get_writeable(identifier); + symbolt &symbol=*symbol_table.get_writeable(identifier); assert(symbol.is_type); remove_const(symbol.type); diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp index d175d7ca3b0..f9344f68238 100644 --- a/src/goto-instrument/remove_function.cpp +++ b/src/goto-instrument/remove_function.cpp @@ -51,7 +51,7 @@ void remove_function( message.status() << "Removing body of " << identifier << messaget::eom; entry->second.clear(); - goto_model.symbol_table.get_writeable(identifier).value.make_nil(); + goto_model.symbol_table.get_writeable(identifier)->get().value.make_nil(); } } diff --git a/src/goto-instrument/wmm/shared_buffers.h b/src/goto-instrument/wmm/shared_buffers.h index 0550291637e..a3b87a26d86 100644 --- a/src/goto-instrument/wmm/shared_buffers.h +++ b/src/goto-instrument/wmm/shared_buffers.h @@ -158,9 +158,12 @@ class shared_bufferst irep_idt choice(const irep_idt &function, const std::string &suffix) { - const std::string function_base_name = (symbol_table.has_symbol(function)? - id2string(symbol_table.lookup(function).base_name): - "main"); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(function); + const std::string function_base_name = + maybe_symbol + ? id2string(maybe_symbol->get().base_name) + : "main"; return add(function_base_name+"_weak_choice", function_base_name+"_weak_choice", suffix, bool_typet()); } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index c65bc472a46..b3ba928bcca 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -444,7 +444,7 @@ typet interpretert::get_type(const irep_idt &id) const { dynamic_typest::const_iterator it=dynamic_types.find(id); if(it==dynamic_types.end()) - return symbol_table.lookup(id).type; + return symbol_table.lookup(id)->get().type; return it->second; } @@ -1041,7 +1041,7 @@ exprt interpretert::get_value(const irep_idt &id) if(findit!=dynamic_types.end()) get_type=findit->second; else - get_type=symbol_table.lookup(id).type; + get_type=symbol_table.lookup(id)->get().type; symbol_exprt symbol_expr(id, get_type); mp_integer whole_lhs_object_address=evaluate_address(symbol_expr); diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 16ffc1063d0..56313c42201 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -118,11 +118,13 @@ void mm_io( irep_idt id_r=CPROVER_PREFIX "mm_io_r"; irep_idt id_w=CPROVER_PREFIX "mm_io_w"; - if(symbol_table.has_symbol(id_r)) - mm_io_r=symbol_table.lookup(id_r).symbol_expr(); + symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id_r); + if(maybe_symbol) + mm_io_r=maybe_symbol->get().symbol_expr(); - if(symbol_table.has_symbol(id_w)) - mm_io_w=symbol_table.lookup(id_w).symbol_expr(); + maybe_symbol=symbol_table.lookup(id_w); + if(maybe_symbol) + mm_io_w=maybe_symbol->get().symbol_expr(); for(auto & f : goto_functions.function_map) mm_io(mm_io_r, mm_io_w, f.second, ns); diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 76f0deacc2e..230490318dc 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -81,7 +81,7 @@ bool rebuild_goto_start_functiont::operator()() irep_idt rebuild_goto_start_functiont::get_entry_point_mode() const { const symbolt ¤t_entry_point= - symbol_table.lookup(goto_functionst::entry_point()); + *symbol_table.lookup(goto_functionst::entry_point()); return current_entry_point.mode; } diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index ea60d6a6ff1..141fc4709fc 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -283,7 +283,7 @@ static void remove_complex(symbolt &symbol) void remove_complex(symbol_tablet &symbol_table) { for(const auto &named_symbol : symbol_table.symbols) - remove_complex(symbol_table.get_writeable(named_symbol.first)); + remove_complex(*symbol_table.get_writeable(named_symbol.first)); } /// removes complex data type diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index de5649892f2..9b8e67c8b68 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -68,7 +68,7 @@ exprt remove_const_function_pointerst::replace_const_symbols( if(is_const_expression(expression)) { const symbolt &symbol= - symbol_table.lookup(expression.get(ID_identifier)); + *symbol_table.lookup(expression.get(ID_identifier)); if(symbol.type.id()!=ID_code) { const exprt &symbol_value=symbol.value; @@ -105,7 +105,7 @@ exprt remove_const_function_pointerst::resolve_symbol( const symbol_exprt &symbol_expr) const { const symbolt &symbol= - symbol_table.lookup(symbol_expr.get_identifier()); + *symbol_table.lookup(symbol_expr.get_identifier()); return symbol.value; } diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 48fa1589eb2..a2cfcc10947 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -134,10 +134,10 @@ void remove_exceptionst::add_exceptional_returns( const irep_idt &function_id=func_it->first; goto_programt &goto_program=func_it->second.body; - INVARIANT( - symbol_table.has_symbol(function_id), - "functions should be recorded in the symbol table"); - const symbolt &function_symbol=symbol_table.lookup(function_id); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(function_id); + INVARIANT(maybe_symbol, "functions should be recorded in the symbol table"); + const symbolt &function_symbol=*maybe_symbol; // for now only add exceptional returns for Java if(function_symbol.mode!=ID_java) @@ -148,10 +148,10 @@ void remove_exceptionst::add_exceptional_returns( // some methods (e.g. the entry method) have already been added to // the symbol table; if you find it, initialise it - if(symbol_table.has_symbol(id2string(function_id)+EXC_SUFFIX)) + maybe_symbol=symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + if(maybe_symbol) { - const symbolt &symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + const symbolt &symbol=*maybe_symbol; symbol_exprt lhs_expr_null=symbol.symbol_expr(); null_pointer_exprt rhs_expr_null((pointer_type(empty_typet()))); goto_programt::targett t_null= @@ -255,10 +255,11 @@ void remove_exceptionst::instrument_exception_handler( to_code_landingpad(instr_it->code).catch_expr(); irep_idt thrown_exception_global=id2string(function_id)+EXC_SUFFIX; - if(symbol_table.has_symbol(thrown_exception_global)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(thrown_exception_global); + if(maybe_symbol) { - const symbol_exprt thrown_global_symbol= - symbol_table.lookup(thrown_exception_global).symbol_expr(); + const symbol_exprt thrown_global_symbol=maybe_symbol->get().symbol_expr(); // next we reset the exceptional return to NULL null_pointer_exprt null_voidptr((pointer_type(empty_typet()))); @@ -314,7 +315,7 @@ void remove_exceptionst::add_exception_dispatch_sequence( // find the symbol corresponding to the caught exceptions const symbolt &exc_symbol= - symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); + *symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add GOTOs implementing the dynamic dispatch of the @@ -389,7 +390,7 @@ void remove_exceptionst::instrument_throw( // find the symbol where the thrown exception should be stored: const symbolt &exc_symbol= - symbol_table.lookup(id2string(func_it->first)+EXC_SUFFIX); + *symbol_table.lookup(id2string(func_it->first)+EXC_SUFFIX); symbol_exprt exc_thrown=exc_symbol.symbol_expr(); // add the assignment with the appropriate cast @@ -424,19 +425,20 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - const irep_idt &callee_inflight_exception=id2string(callee_id)+EXC_SUFFIX; - const irep_idt &local_inflight_exception=id2string(function_id)+EXC_SUFFIX; + symbol_tablet::opt_const_symbol_reft callee_inflight_exception= + symbol_table.lookup(id2string(callee_id)+EXC_SUFFIX); + symbol_tablet::opt_const_symbol_reft local_inflight_exception= + symbol_table.lookup(id2string(function_id)+EXC_SUFFIX); - if(symbol_table.has_symbol(callee_inflight_exception) && - symbol_table.has_symbol(local_inflight_exception)) + if(callee_inflight_exception && local_inflight_exception) { add_exception_dispatch_sequence( func_it, instr_it, stack_catch, locals); const symbol_exprt callee_inflight_exception_expr= - symbol_table.lookup(callee_inflight_exception).symbol_expr(); + callee_inflight_exception->get().symbol_expr(); const symbol_exprt local_inflight_exception_expr= - symbol_table.lookup(local_inflight_exception).symbol_expr(); + local_inflight_exception->get().symbol_expr(); // add a null check (so that instanceof can be applied) equal_exprt eq_null( diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 62052b6e0c5..1a22bd72359 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -62,7 +62,7 @@ void remove_returnst::replace_returns( if(has_return_value) { // look up the function symbol - symbolt &function_symbol=symbol_table.get_writeable(function_id); + symbolt &function_symbol=*symbol_table.get_writeable(function_id); // make the return type 'void' f_it->second.type.return_type()=empty_typet(); @@ -254,7 +254,7 @@ bool remove_returnst::restore_returns( return true; // look up the function symbol - symbolt &function_symbol=symbol_table.get_writeable(function_id); + symbolt &function_symbol=*symbol_table.get_writeable(function_id); // restore the return type f_it->second.type=original_return_type(symbol_table, function_id); diff --git a/src/goto-programs/remove_static_init_loops.cpp b/src/goto-programs/remove_static_init_loops.cpp index c0f3c05150f..794ec547fc4 100644 --- a/src/goto-programs/remove_static_init_loops.cpp +++ b/src/goto-programs/remove_static_init_loops.cpp @@ -58,21 +58,23 @@ void remove_static_init_loopst::unwind_enum_static( const std::string &fname=id2string(ins.function); size_t class_prefix_length=fname.find_last_of('.'); // is the function symbol in the symbol table? - if(!symbol_table.has_symbol(ins.function)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(ins.function); + if(!maybe_symbol) { message.warning() << "function `" << id2string(ins.function) << "` is not in symbol table" << messaget::eom; continue; } // is Java function and static init? - const symbolt &function_name=symbol_table.lookup(ins.function); + const symbolt &function_name=*maybe_symbol; if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit))) continue; assert( class_prefix_length!=std::string::npos && "could not identify class name"); const std::string &classname=fname.substr(0, class_prefix_length); - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*symbol_table.lookup(classname); const class_typet &class_type=to_class_type(class_symbol.type); size_t unwinds=class_type.get_size_t(ID_java_enum_static_unwind); diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 93e1a45907e..f2e7f5b9fe4 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -191,7 +191,7 @@ static void remove_vector(symbolt &symbol) static void remove_vector(symbol_tablet &symbol_table) { for(const auto &named_symbol : symbol_table.symbols) - remove_vector(symbol_table.get_writeable(named_symbol.first)); + remove_vector(*symbol_table.get_writeable(named_symbol.first)); } /// removes vector data type diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 26671e18527..e1f8c79444c 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -273,7 +273,7 @@ void remove_virtual_functionst::get_functions( root_function.class_id=resolved_call.get_class_identifier(); const symbolt &called_symbol= - symbol_table.lookup(resolved_call.get_virtual_method_name()); + *symbol_table.lookup(resolved_call.get_virtual_method_name()); root_function.symbol_expr=called_symbol.symbol_expr(); root_function.symbol_expr.set( diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 8cf7d931642..05f9371e492 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -174,7 +174,7 @@ void string_abstractiont::add_str_arguments( const irep_idt &name, goto_functionst::goto_functiont &fct) { - symbolt &fct_symbol=symbol_table.get_writeable(name); + symbolt &fct_symbol=*symbol_table.get_writeable(name); code_typet::parameterst ¶meters= to_code_type(fct.type).parameters(); diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 41eab823e42..c9ddec10d81 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -144,7 +144,7 @@ bool ci_lazy_methodst::operator()( method_converter( *parsed_method.first, *parsed_method.second, new_lazy_methods); gather_virtual_callsites( - symbol_table.lookup(mname).value, + symbol_table.lookup(mname)->get().value, virtual_callsites); any_new_methods=true; } diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index b3b497806f4..00652d34618 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -320,7 +320,7 @@ void java_bytecode_convert_methodt::convert( id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature; method_id=method_identifier; - const auto &old_sym=symbol_table.lookup(method_identifier); + const symbolt &old_sym=*symbol_table.lookup(method_identifier); // Obtain a std::vector of code_typet::parametert objects from the // (function) type of the symbol @@ -883,14 +883,15 @@ bool java_bytecode_convert_methodt::class_needs_clinit( findit_any.first->second=true; return true; } - auto findit_symbol=symbol_table.symbols.find(classname); + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(classname); // Stub class? - if(findit_symbol==symbol_table.symbols.end()) + if(!maybe_symbol) { warning() << "SKIPPED: " << classname << eom; return false; } - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*maybe_symbol; for(const auto &base : to_class_type(class_symbol.type).bases()) { if(class_needs_clinit(to_symbol_type(base.type()).get_identifier())) @@ -948,7 +949,7 @@ exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper( code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt()); init_body.move_to_operands(set_already_run); const irep_idt &real_clinit_name=id2string(classname)+".:()V"; - const symbolt &class_symbol=symbol_table.lookup(classname); + const symbolt &class_symbol=*symbol_table.lookup(classname); auto findsymit=symbol_table.symbols.find(real_clinit_name); if(findsymit!=symbol_table.symbols.end()) @@ -2831,7 +2832,7 @@ bool java_bytecode_convert_methodt::is_method_inherited( if(resolved_call.is_valid()) { const symbolt &function_symbol= - symbol_table.lookup(resolved_call.get_virtual_method_name()); + *symbol_table.lookup(resolved_call.get_virtual_method_name()); INVARIANT(function_symbol.type.id()==ID_code, "Function must be code"); diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index eb26390d1ad..1b30f02d037 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -617,5 +617,5 @@ void java_bytecode_instrument( // instrument(...) can add symbols to the table, so it's // not safe to hold a reference to a symbol across a call. for(const auto &symbol : symbols_to_instrument) - instrument(symbol_table.get_writeable(symbol).value); + instrument(symbol_table.get_writeable(symbol)->get().value); } diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 553d1903382..cd6210bdb8f 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -374,7 +374,7 @@ void java_bytecode_languaget::replace_string_methods( if(generated_code.is_not_nil()) { // Replace body of the function by code generated by string preprocess - symbolt &symbol=context.get_writeable(id); + symbolt &symbol=*context.get_writeable(id); symbol.value=generated_code; // Specifically instrument the new code, since this comes after the // blanket instrumentation pass called before typechecking. diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index 7833cd2d44e..e7f096c8333 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/src/java_bytecode/java_bytecode_typecheck.cpp @@ -48,7 +48,7 @@ void java_bytecode_typecheckt::typecheck() // recursively doing base classes first. for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.get_writeable(id); + symbolt &symbol=*symbol_table.get_writeable(id); if(!symbol.is_type) continue; typecheck_type_symbol(symbol); @@ -57,7 +57,7 @@ void java_bytecode_typecheckt::typecheck() // We now check all non-type symbols for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.get_writeable(id); + symbolt &symbol=*symbol_table.get_writeable(id); if(symbol.is_type) continue; typecheck_non_type_symbol(symbol); diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 4cf3568d410..d73525ccc60 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -291,7 +291,7 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr) // member doesn't exist. In this case struct_type should be an opaque // stub, and we'll add the member to it. symbolt &symbol_table_type= - symbol_table.get_writeable("java::"+id2string(struct_type.get_tag())); + *symbol_table.get_writeable("java::"+id2string(struct_type.get_tag())); auto &add_to_components= to_struct_type(symbol_table_type.type).components(); add_to_components diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 342a22035af..fa77deeb671 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -96,7 +96,7 @@ void java_static_lifetime_init( const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { - symbolt &initialize_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION); + symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION); code_blockt &code_block=to_code_block(to_code(initialize_symbol.value)); // We need to zero out all static variables, or nondet-initialize if they're @@ -109,7 +109,7 @@ void java_static_lifetime_init( for(const auto &symname : symbol_names) { - const symbolt &sym=symbol_table.lookup(symname); + const symbolt &sym=*symbol_table.lookup(symname); if(should_init_symbol(sym)) { if(sym.value.is_nil() && sym.type!=empty_typet()) @@ -264,7 +264,7 @@ void java_record_outputs( output.operands().resize(2); const symbolt &return_symbol= - symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL); + *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL); output.op0()= address_of_exprt( @@ -282,7 +282,7 @@ void java_record_outputs( param_number++) { const symbolt &p_symbol= - symbol_table.lookup(parameters[param_number].get_identifier()); + *symbol_table.lookup(parameters[param_number].get_identifier()); if(p_symbol.type.id()==ID_pointer) { @@ -306,7 +306,7 @@ void java_record_outputs( output.operands().resize(2); // retrieve the exception variable - const symbolt exc_symbol=symbol_table.lookup( + const symbolt exc_symbol=*symbol_table.lookup( JAVA_ENTRY_POINT_EXCEPTION_SYMBOL); output.op0()=address_of_exprt( diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index fdf03006318..be244ee0313 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -168,7 +168,7 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( /// \return the type of data fields in java Strings. typet string_data_type(const symbol_tablet &symbol_table) { - symbolt sym=symbol_table.lookup("java::java.lang.String"); + symbolt sym=*symbol_table.lookup("java::java.lang.String"); typet concrete_type=sym.type; struct_typet struct_type=to_struct_type(concrete_type); std::size_t index=struct_type.component_number("data"); @@ -384,7 +384,7 @@ typet java_string_library_preprocesst::get_data_type( PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); if(type.id()==ID_symbol) { - symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); CHECK_RETURN(sym.type.id()!=ID_symbol); return get_data_type(sym.type, symbol_table); } @@ -403,7 +403,7 @@ typet java_string_library_preprocesst::get_length_type( PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); if(type.id()==ID_symbol) { - symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); CHECK_RETURN(sym.type.id()!=ID_symbol); return get_length_type(sym.type, symbol_table); } @@ -711,7 +711,7 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( code_blockt code; // A String has a field Object with @clsid = String and @lock = false: - const symbolt &jlo_symbol=symbol_table.lookup("java::java.lang.Object"); + const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object"); const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type); struct_exprt jlo_init(jlo_struct); jlo_init.copy_to_operands(constant_exprt( @@ -797,7 +797,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( typet deref_type; if(rhs.type().subtype().id()==ID_symbol) deref_type=symbol_table.lookup( - to_symbol_type(rhs.type().subtype()).get_identifier()).type; + to_symbol_type(rhs.type().subtype()).get_identifier())->get().type; else deref_type=rhs.type().subtype(); @@ -1252,10 +1252,11 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( // Check that the type of the object is in the symbol table, // otherwise there is no safe way of finding its value. - if(symbol_table.has_symbol(object_type.get_identifier())) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(object_type.get_identifier()); + if(maybe_symbol) { - struct_typet struct_type=to_struct_type( - symbol_table.lookup(object_type.get_identifier()).type); + struct_typet struct_type=to_struct_type(maybe_symbol->get().type); // Check that the type has a value field const struct_union_typet::componentt value_comp= struct_type.get_component("value"); @@ -1500,7 +1501,7 @@ codet java_string_library_preprocesst::make_object_get_class_code( // > Class class1; pointer_typet class_type= - java_reference_type(symbol_table.lookup("java::java.lang.Class").type); + java_reference_type(symbol_table.lookup("java::java.lang.Class")->get().type); symbolt class1_sym=get_fresh_aux_symbol( class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table); symbol_exprt class1=class1_sym.symbol_expr(); @@ -1536,8 +1537,8 @@ codet java_string_library_preprocesst::make_object_get_class_code( code.add(code_assignt(string_expr_sym1, string_expr1)); // string1 = (String*) string_expr - pointer_typet string_ptr_type= - java_reference_type(symbol_table.lookup("java::java.lang.String").type); + pointer_typet string_ptr_type=java_reference_type( + symbol_table.lookup("java::java.lang.String")->get().type); exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code); code.add( code_assign_string_expr_to_new_java_string( diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp index 1b0bf9c02c2..3bc44fa41e1 100644 --- a/src/jsil/jsil_convert.cpp +++ b/src/jsil/jsil_convert.cpp @@ -48,9 +48,11 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree) if(convert_code(new_symbol, to_code(new_symbol.value))) return true; - if(symbol_table.has_symbol(new_symbol.name)) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(new_symbol.name); + if(maybe_symbol) { - const symbolt &s=symbol_table.lookup(new_symbol.name); + const symbolt &s=*maybe_symbol; if(s.value.id()=="no-body-just-yet") { symbol_table.remove(s.name); diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp index e82a6967dc0..ecc36288bae 100644 --- a/src/jsil/jsil_typecheck.cpp +++ b/src/jsil/jsil_typecheck.cpp @@ -42,13 +42,15 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type) { const irep_idt &id=to_symbol_expr(expr).get_identifier(); - if(!symbol_table.has_symbol(id)) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(id); + if(!maybe_symbol) { error() << "unexpected symbol: " << id << eom; throw 0; } - symbolt &s=symbol_table.get_writeable(id); + symbolt &s=*maybe_symbol; if(s.type.id().empty() || s.type.is_nil()) s.type=type; else @@ -747,9 +749,10 @@ void jsil_typecheckt::typecheck_function_call( { const irep_idt &id=to_symbol_expr(f).get_identifier(); - if(symbol_table.has_symbol(id)) + symbol_tablet::opt_const_symbol_reft maybe_symbol=symbol_table.lookup(id); + if(maybe_symbol) { - const symbolt &s=symbol_table.lookup(id); + const symbolt &s=*maybe_symbol; if(s.type.id()==ID_code) { @@ -894,7 +897,7 @@ void jsil_typecheckt::typecheck() // recursively doing base classes first. for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.get_writeable(id); + symbolt &symbol=*symbol_table.get_writeable(id); if(symbol.is_type) typecheck_type_symbol(symbol); } @@ -902,7 +905,7 @@ void jsil_typecheckt::typecheck() // We now check all non-type symbols for(const irep_idt &id : identifiers) { - symbolt &symbol=symbol_table.get_writeable(id); + symbolt &symbol=*symbol_table.get_writeable(id); if(!symbol.is_type) typecheck_non_type_symbol(symbol); } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 83edd589077..d71ad02768a 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -1210,7 +1210,7 @@ void linkingt::rename_symbols(const id_sett &needs_to_be_renamed) for(const irep_idt &id : needs_to_be_renamed) { - symbolt &new_symbol=src_symbol_table.get_writeable(id); + symbolt &new_symbol=*src_symbol_table.get_writeable(id); irep_idt new_identifier; @@ -1273,7 +1273,7 @@ void linkingt::copy_symbols() // Now do the collisions for(const irep_idt &collision : collisions) { - symbolt &old_symbol=main_symbol_table.get_writeable(collision); + symbolt &old_symbol=*main_symbol_table.get_writeable(collision); symbolt &new_symbol=src_symbols.at(collision); if(new_symbol.is_type) @@ -1290,7 +1290,7 @@ void linkingt::copy_symbols() named_symbol.second.value.is_not_nil()) { object_type_updates( - main_symbol_table.get_writeable(named_symbol.first).value); + main_symbol_table.get_writeable(named_symbol.first)->get().value); } } } diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 8fe0d160739..4d96670cafd 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -31,10 +31,11 @@ bool static_lifetime_init( { namespacet ns(symbol_table); - if(!symbol_table.has_symbol(INITIALIZE_FUNCTION)) + symbol_tablet::opt_symbol_reft maybe_symbol= + symbol_table.get_writeable(INITIALIZE_FUNCTION); + if(!maybe_symbol) return false; - - symbolt &init_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION); + symbolt &init_symbol=*maybe_symbol; init_symbol.value=code_blockt(); init_symbol.value.add_source_location()=source_location; @@ -101,7 +102,7 @@ bool static_lifetime_init( { // C standard 6.9.2, paragraph 5 // adjust the type to an array of size 1 - symbolt &symbol=symbol_table.get_writeable(identifier); + symbolt &symbol=*symbol_table.get_writeable(identifier); symbol.type=type; symbol.type.set(ID_size, from_integer(1, size_type())); } diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index f066427a13e..16e4131339e 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -51,7 +51,7 @@ void add_failed_symbol(const symbolt &symbol, symbol_tablet &symbol_table) if(symbol.type.get(ID_C_failed_symbol)!="") return; - add_failed_symbol(symbol_table.get_writeable(symbol.name), symbol_table); + add_failed_symbol(*symbol_table.get_writeable(symbol.name), symbol_table); } void add_failed_symbols(symbol_tablet &symbol_table) diff --git a/src/util/config.cpp b/src/util/config.cpp index 4048cfd417a..0e8f3d692c8 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1177,10 +1177,11 @@ void configt::set_object_bits_from_symbol_table( return; // set object_bits according to entry point language - if(symbol_table.has_symbol(CPROVER_PREFIX "_start")) + symbol_tablet::opt_const_symbol_reft maybe_symbol= + symbol_table.lookup(CPROVER_PREFIX "_start"); + if(maybe_symbol) { - const symbolt &entry_point_symbol= - symbol_table.lookup(CPROVER_PREFIX "_start"); + const symbolt &entry_point_symbol=*maybe_symbol; if(entry_point_symbol.mode==ID_java) bv_encoding.object_bits=java.default_object_bits; diff --git a/src/util/language.cpp b/src/util/language.cpp index 7f89a0b92c3..62f77edc40b 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -87,7 +87,7 @@ void languaget::generate_opaque_method_stubs(symbol_tablet &symbol_table) if(is_symbol_opaque_function(symbol_entry.second)) { symbolt &symbol= - symbol_table.get_writeable(symbol_entry.second.name); + *symbol_table.get_writeable(symbol_entry.second.name); generate_opaque_parameter_symbols(symbol, symbol_table); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index cf26879d324..bf6da83e3e8 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -24,14 +24,13 @@ bool symbol_tablet::add(const symbolt &symbol) /// \param symbol: The symbol to be added to the symbol table /// \return Returns an optional reference to the newly inserted symbol, without /// a value if a symbol with the same name already exists in the symbol table -optionalt> symbol_tablet::insert( - symbolt &&symbol) +symbol_tablet::opt_symbol_reft symbol_tablet::insert(symbolt &&symbol) { // Add the symbol to the table or retrieve existing symbol with the same name std::pair result= internal_symbols.emplace(symbol.name, std::move(symbol)); if(!result.second) - return optionalt>(); + return opt_symbol_reft(); add_base_and_module(result.first); return std::ref(result.first->second); } @@ -158,26 +157,25 @@ void symbol_tablet::show(std::ostream &out) const /// found. /// \param identifier: The name of the symbol to look for /// \return The symbol in the symbol table with the correct name -const symbolt &symbol_tablet::lookup(const irep_idt &identifier) const +symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup( + const irep_idt &identifier) const { symbolst::const_iterator it=symbols.find(identifier); - if(it==symbols.end()) - throw "symbol "+id2string(identifier)+" not found"; - - return it->second; + return opt_const_symbol_reft(); + return std::ref(it->second); } /// Find a symbol in the symbol table. /// \param identifier: The name of the symbol to look for /// \return The symbol in the symbol table with the correct name -symbolt &symbol_tablet::get_writeable(const irep_idt &identifier) +symbol_tablet::opt_symbol_reft symbol_tablet::get_writeable( + const irep_idt &identifier) { symbolst::iterator it=internal_symbols.find(identifier); - INVARIANT( - it!=symbols.end(), - "symbol "+id2string(identifier)+" should be in the symbol map"); - return it->second; + if(it==symbols.end()) + return opt_symbol_reft(); + return std::ref(it->second); } /// Print the contents of the symbol table diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 6729f28f2f5..e4c9a370007 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -41,6 +41,9 @@ class symbol_tablet { public: typedef std::unordered_map symbolst; + typedef optionalt> + opt_const_symbol_reft; + typedef optionalt> opt_symbol_reft; private: symbolst internal_symbols; @@ -95,8 +98,15 @@ class symbol_tablet return *this; } + bool has_symbol(const irep_idt &name) const + { + return symbols.find(name)!=symbols.end(); + } + opt_const_symbol_reft lookup(const irep_idt &identifier) const; + opt_symbol_reft get_writeable(const irep_idt &identifier); + bool add(const symbolt &symbol); - optionalt> insert(symbolt &&symbol); + opt_symbol_reft insert(symbolt &&symbol); bool move(symbolt &symbol, symbolt *&new_symbol); private: void add_base_and_module(symbolst::iterator added_symbol); @@ -121,14 +131,6 @@ class symbol_tablet internal_symbol_base_map.swap(other.internal_symbol_base_map); internal_symbol_module_map.swap(other.internal_symbol_module_map); } - - bool has_symbol(const irep_idt &name) const - { - return symbols.find(name)!=symbols.end(); - } - - const symbolt &lookup(const irep_idt &identifier) const; - symbolt &get_writeable(const irep_idt &identifier); }; std::ostream &operator << ( diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index e8932306ee9..e328ac936a3 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -29,7 +29,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::I"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::I"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -44,7 +44,7 @@ SCENARIO("java_bytecode_convert_abstract_class", load_java_class("A", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::A"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::A"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -59,7 +59,7 @@ SCENARIO("java_bytecode_convert_abstract_class", load_java_class("C", "./java_bytecode/java_bytecode_convert_class"); THEN("The symbol type should not be abstract") { - const symbolt &class_symbol=new_symbol_table.lookup("java::C"); + const symbolt &class_symbol=*new_symbol_table.lookup("java::C"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -77,7 +77,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should not be abstract") { const symbolt &class_symbol= - new_symbol_table.lookup("java::Implementor"); + *new_symbol_table.lookup("java::Implementor"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); @@ -95,7 +95,7 @@ SCENARIO("java_bytecode_convert_abstract_class", THEN("The symbol type should not be abstract") { const symbolt &class_symbol= - new_symbol_table.lookup("java::Extender"); + *new_symbol_table.lookup("java::Extender"); const typet &symbol_type=class_symbol.type; REQUIRE(symbol_type.id()==ID_struct); diff --git a/unit/src/java_bytecode/load_java_class.cpp b/unit/src/java_bytecode/load_java_class.cpp index bfcb662ffa2..5956012b853 100644 --- a/unit/src/java_bytecode/load_java_class.cpp +++ b/unit/src/java_bytecode/load_java_class.cpp @@ -54,7 +54,7 @@ symbol_tablet load_java_class( // Verify that the class was loaded const std::string class_symbol_name="java::"+java_class_name; REQUIRE(new_symbol_table.has_symbol(class_symbol_name)); - const symbolt &class_symbol=new_symbol_table.lookup(class_symbol_name); + const symbolt &class_symbol=*new_symbol_table.lookup(class_symbol_name); REQUIRE(class_symbol.is_type); const typet &class_type=class_symbol.type; REQUIRE(class_type.id()==ID_struct); From e35f2fc66c12e8aaf6e5689595731db2a5bb1f54 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 25 Sep 2017 20:05:26 +0100 Subject: [PATCH 07/11] Misc review requests --- src/cpp/cpp_typecheck_compound_type.cpp | 4 ++-- src/java_bytecode/java_utils.cpp | 3 ++- src/util/symbol_table.cpp | 3 ++- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 6887d3163ce..ef7038d641a 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -536,7 +536,7 @@ void cpp_typecheckt::typecheck_compound_declarator( vt_symb_type.type.set(ID_name, vt_symb_type.name); vt_symb_type.is_type=true; - bool failed=!symbol_table.insert(std::move(vt_symb_type)); + const bool failed=!symbol_table.insert(std::move(vt_symb_type)); assert(!failed); // add a virtual-table pointer @@ -612,7 +612,7 @@ void cpp_typecheckt::typecheck_compound_declarator( arg.set(ID_C_identifier, arg_symb.name); // add the parameter to the symbol table - bool failed=!symbol_table.insert(std::move(arg_symb)); + const bool failed=!symbol_table.insert(std::move(arg_symb)); assert(!failed); } diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 8307d39568d..b823dd59baf 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -86,7 +86,8 @@ void generate_class_stub( new_symbol.mode=ID_java; new_symbol.is_type=true; - auto res=symbol_table.insert(std::move(new_symbol)); + optionalt> res= + symbol_table.insert(std::move(new_symbol)); if(!res) { diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index bf6da83e3e8..2c1733bf98e 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -115,7 +115,8 @@ void symbol_tablet::erase(const symbolst::const_iterator &entry) const symbolt &symbol=entry->second; symbol_base_mapt::const_iterator - base_it=symbol_base_map.lower_bound(entry->second.base_name), + base_it=symbol_base_map.lower_bound(entry->second.base_name); + symbol_base_mapt::const_iterator base_it_end=symbol_base_map.upper_bound(entry->second.base_name); while(base_it!=base_it_end && base_it->second!=symbol.name) ++base_it; From 9f4e933701e34120e9e2c08c34dd86fa167fccc7 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 28 Sep 2017 13:22:51 +0100 Subject: [PATCH 08/11] Changed interface to symbol_tablet::insert --- src/ansi-c/ansi_c_entry_point.cpp | 2 +- src/cpp/cpp_typecheck_compound_type.cpp | 6 +- src/cpp/cpp_typecheck_namespace.cpp | 2 +- src/cpp/cpp_typecheck_virtual_table.cpp | 2 +- src/java_bytecode/java_entry_point.cpp | 2 +- src/java_bytecode/java_utils.cpp | 7 +- src/jsil/jsil_entry_point.cpp | 2 +- src/util/fresh_symbol.cpp | 8 +- src/util/symbol_table.cpp | 97 ++++++++++--------------- src/util/symbol_table.h | 13 +++- 10 files changed, 64 insertions(+), 77 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index dece5734526..47dfd3e03d3 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -478,7 +478,7 @@ bool generate_ansi_c_start_function( new_symbol.value.swap(init_code); new_symbol.mode=symbol.mode; - if(!symbol_table.insert(std::move(new_symbol))) + if(!symbol_table.insert(std::move(new_symbol)).second) { messaget message; message.set_message_handler(message_handler); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index ef7038d641a..4796f5e3d76 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -536,7 +536,7 @@ void cpp_typecheckt::typecheck_compound_declarator( vt_symb_type.type.set(ID_name, vt_symb_type.name); vt_symb_type.is_type=true; - const bool failed=!symbol_table.insert(std::move(vt_symb_type)); + const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second; assert(!failed); // add a virtual-table pointer @@ -612,7 +612,7 @@ void cpp_typecheckt::typecheck_compound_declarator( arg.set(ID_C_identifier, arg_symb.name); // add the parameter to the symbol table - const bool failed=!symbol_table.insert(std::move(arg_symb)); + const bool failed=!symbol_table.insert(std::move(arg_symb)).second; assert(!failed); } @@ -670,7 +670,7 @@ void cpp_typecheckt::typecheck_compound_declarator( // add the function to the symbol table { - const bool failed=!symbol_table.insert(std::move(func_symb)); + const bool failed=!symbol_table.insert(std::move(func_symb)).second; assert(!failed); } diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index f41ebe2b196..c64d6020a82 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -73,7 +73,7 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) symbol.module=module; symbol.type=typet(ID_namespace); - if(!symbol_table.insert(std::move(symbol))) + if(!symbol_table.insert(std::move(symbol)).second) { error().source_location=symbol.location; error() << "cpp_typecheckt::convert_namespace: symbol_table.move() failed" diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 2b65c0ca7d3..328efabbcaf 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -95,7 +95,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) } vt_symb_var.value=values; - bool failed=!symbol_table.insert(std::move(vt_symb_var)); + bool failed=!symbol_table.insert(std::move(vt_symb_var)).second; assert(!failed); } } diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index fa77deeb671..e9863e51152 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -668,7 +668,7 @@ bool generate_java_start_function( new_symbol.value.swap(init_code); new_symbol.mode=ID_java; - if(!symbol_table.insert(std::move(new_symbol))) + if(!symbol_table.insert(std::move(new_symbol)).second) { message.error() << "failed to move main symbol" << messaget::eom; return true; diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index b823dd59baf..9cb7fab0492 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -86,10 +86,9 @@ void generate_class_stub( new_symbol.mode=ID_java; new_symbol.is_type=true; - optionalt> res= - symbol_table.insert(std::move(new_symbol)); + std::pair res=symbol_table.insert(std::move(new_symbol)); - if(!res) + if(!res.second) { messaget message(message_handler); message.warning() << @@ -100,7 +99,7 @@ void generate_class_stub( else { // create the class identifier etc - java_root_class(*res); + java_root_class(res.first); } } diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 50b3e5e54aa..991ca1c226c 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -162,7 +162,7 @@ bool jsil_entry_point( new_symbol.type.swap(main_type); new_symbol.value.swap(init_code); - if(!symbol_table.insert(std::move(new_symbol))) + if(!symbol_table.insert(std::move(new_symbol)).second) { messaget message; message.set_message_handler(message_handler); diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 3acd78f97f4..e1795890721 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -40,9 +40,8 @@ symbolt &get_fresh_aux_symbol( { auxiliary_symbolt new_symbol; - optionalt> res; // Loop until find a name that doesn't clash with a non-auxilliary symbol - while(!res) + while(true) { // Distinguish local variables with the same name new_symbol.base_name= @@ -54,7 +53,8 @@ symbolt &get_fresh_aux_symbol( new_symbol.type=type; new_symbol.location=source_location; new_symbol.mode=symbol_mode; - res=symbol_table.insert(std::move(new_symbol)); + std::pair res=symbol_table.insert(std::move(new_symbol)); + if(res.second) + return res.first; } - return *res; } diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 2c1733bf98e..b6c28d05a89 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -11,28 +11,38 @@ /// there is a symbol with the same name already in the symbol table. bool symbol_tablet::add(const symbolt &symbol) { - std::pair result= - internal_symbols.emplace(symbol.name, symbol); - if(!result.second) - return true; - add_base_and_module(result.first); - return false; + return !insert(symbol).second; } -/// Move a new symbol to the symbol table -/// \remark: This is a nicer interface than move but achieves the same result -/// \param symbol: The symbol to be added to the symbol table -/// \return Returns an optional reference to the newly inserted symbol, without -/// a value if a symbol with the same name already exists in the symbol table -symbol_tablet::opt_symbol_reft symbol_tablet::insert(symbolt &&symbol) +std::pair symbol_tablet::insert(symbolt symbol) { // Add the symbol to the table or retrieve existing symbol with the same name std::pair result= internal_symbols.emplace(symbol.name, std::move(symbol)); - if(!result.second) - return opt_symbol_reft(); - add_base_and_module(result.first); - return std::ref(result.first->second); + symbolt &new_symbol=result.first->second; + if(result.second) + { + try + { + symbol_base_mapt::iterator base_result= + internal_symbol_base_map.emplace(new_symbol.base_name, new_symbol.name); + try + { + internal_symbol_module_map.emplace(new_symbol.module, new_symbol.name); + } + catch(...) + { + internal_symbol_base_map.erase(base_result); + throw; + } + } + catch(...) + { + internal_symbols.erase(result.first); + throw; + } + } + return std::make_pair(std::ref(new_symbol), result.second); } /// Move a symbol into the symbol table. If there is already a symbol with the @@ -53,49 +63,22 @@ symbol_tablet::opt_symbol_reft symbol_tablet::insert(symbolt &&symbol) bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) { // Add an empty symbol to the table or retrieve existing symbol with same name - std::pair result= - internal_symbols.emplace(symbol.name, symbolt()); - - if(!result.second) - { - // Return the address of the symbol that already existed in the table - new_symbol=&result.first->second; - return true; - } - - // Move the provided symbol into the symbol table - result.first->second.swap(symbol); - - add_base_and_module(result.first); - - // Return the address of the new symbol in the table - new_symbol=&result.first->second; - - return false; -} - -void symbol_tablet::add_base_and_module(symbolst::iterator added_symbol) -{ - symbolt &symbol=added_symbol->second; - try - { - symbol_base_mapt::iterator base_result= - internal_symbol_base_map.emplace(symbol.base_name, symbol.name); - try - { - internal_symbol_module_map.emplace(symbol.module, symbol.name); - } - catch(...) - { - internal_symbol_base_map.erase(base_result); - throw; - } - } - catch(...) + symbolt temp_symbol; + // This is not copying the symbol, this is passing the three required + // parameters to insert (just in the symbol) + temp_symbol.name=symbol.name; + temp_symbol.base_name=symbol.base_name; + temp_symbol.module=symbol.module; + std::pair result=insert(std::move(temp_symbol)); + if(result.second) { - internal_symbols.erase(added_symbol); - throw; + // Move the provided symbol into the symbol table, this can't be done + // earlier + result.first.swap(symbol); } + // Return the address of the symbol in the table + new_symbol=&result.first; + return !result.second; } /// Remove a symbol from the symbol table diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index e4c9a370007..835ea5127c8 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -106,12 +106,17 @@ class symbol_tablet opt_symbol_reft get_writeable(const irep_idt &identifier); bool add(const symbolt &symbol); - opt_symbol_reft insert(symbolt &&symbol); + /// Move or copy a new symbol to the symbol table + /// \remark: This is a nicer interface than move and achieves the same + /// result as both move and add + /// \param symbol: The symbol to be added to the symbol table - can be + /// moved or copied in + /// \return Returns a reference to the newly inserted symbol or to the + /// existing symbol if a symbol with the same name already exists in the + /// symbol table, along with a bool that is true if a new symbol was inserted. + std::pair insert(symbolt symbol); bool move(symbolt &symbol, symbolt *&new_symbol); -private: - void add_base_and_module(symbolst::iterator added_symbol); -public: void clear() { internal_symbols.clear(); From 53e1ca2c8b086ef32ca8a481c4c2d1f1501e8e16 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 28 Sep 2017 14:13:31 +0100 Subject: [PATCH 09/11] Made move constructor strong exception safe --- src/util/symbol_table.h | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 835ea5127c8..f9648699ff3 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -74,10 +74,8 @@ class symbol_tablet symbol_tablet &operator=(const symbol_tablet &other) { - internal_symbols=other.internal_symbols; - internal_symbol_base_map=other.internal_symbol_base_map; - internal_symbol_module_map=other.symbol_module_map; - return *this; + // Copy to temp and then call move assignment + return *this=symbol_tablet(other); } symbol_tablet(symbol_tablet &&other) From d3201870c8b97b15b6204ce12835c11eab36428d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 4 Oct 2017 16:13:37 +0100 Subject: [PATCH 10/11] Linter fixes --- src/goto-instrument/goto_program2code.cpp | 4 +++- src/java_bytecode/java_string_library_preprocess.cpp | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index a299159d8dc..99444893dfb 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1669,7 +1669,9 @@ void goto_program2codet::remove_const(typet &type) return; symbolt &symbol=*symbol_table.get_writeable(identifier); - assert(symbol.is_type); + INVARIANT( + symbol.is_type, + "Symbol "+id2string(identifier)+" should be a type"); remove_const(symbol.type); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index be244ee0313..ce053f25185 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1501,7 +1501,8 @@ codet java_string_library_preprocesst::make_object_get_class_code( // > Class class1; pointer_typet class_type= - java_reference_type(symbol_table.lookup("java::java.lang.Class")->get().type); + java_reference_type( + symbol_table.lookup("java::java.lang.Class")->get().type); symbolt class1_sym=get_fresh_aux_symbol( class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table); symbol_exprt class1=class1_sym.symbol_expr(); From 679419143119ccd5b96c8949530928e24cf8c477 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 5 Oct 2017 10:32:56 +0100 Subject: [PATCH 11/11] Improve symbol table documentation No functional changes --- src/util/symbol_table.cpp | 20 +++++++++++++++----- src/util/symbol_table.h | 12 ++++-------- 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index b6c28d05a89..0cf07f24683 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -14,6 +14,14 @@ bool symbol_tablet::add(const symbolt &symbol) return !insert(symbol).second; } +/// Move or copy a new symbol to the symbol table +/// \remark: This is a nicer interface than move and achieves the same +/// result as both move and add +/// \param symbol: The symbol to be added to the symbol table - can be +/// moved or copied in +/// \return Returns a reference to the newly inserted symbol or to the +/// existing symbol if a symbol with the same name already exists in the +/// symbol table, along with a bool that is true if a new symbol was inserted. std::pair symbol_tablet::insert(symbolt symbol) { // Add the symbol to the table or retrieve existing symbol with the same name @@ -84,6 +92,7 @@ bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol) /// Remove a symbol from the symbol table /// \param name: The name of the symbol to remove /// \return Returns a boolean indicating whether the process failed +/// i.e. false if the symbol was removed, or true if it didn't exist. bool symbol_tablet::remove(const irep_idt &name) { symbolst::const_iterator entry=symbols.find(name); @@ -93,6 +102,8 @@ bool symbol_tablet::remove(const irep_idt &name) return false; } +/// Remove a symbol from the symbol table +/// \param entry: an iterator pointing at the symbol to remove void symbol_tablet::erase(const symbolst::const_iterator &entry) { const symbolt &symbol=entry->second; @@ -137,10 +148,9 @@ void symbol_tablet::show(std::ostream &out) const out << it->second; } -/// Find a symbol in the symbol table. Throws a string if no such symbol is -/// found. +/// Find a symbol in the symbol table for read-only access. /// \param identifier: The name of the symbol to look for -/// \return The symbol in the symbol table with the correct name +/// \return an optional reference, set if found, unset otherwise. symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup( const irep_idt &identifier) const { @@ -150,9 +160,9 @@ symbol_tablet::opt_const_symbol_reft symbol_tablet::lookup( return std::ref(it->second); } -/// Find a symbol in the symbol table. +/// Find a symbol in the symbol table for read-write access. /// \param identifier: The name of the symbol to look for -/// \return The symbol in the symbol table with the correct name +/// \return an optional reference, set if found, unset otherwise. symbol_tablet::opt_symbol_reft symbol_tablet::get_writeable( const irep_idt &identifier) { diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index f9648699ff3..4fb920a179d 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -100,19 +100,15 @@ class symbol_tablet { return symbols.find(name)!=symbols.end(); } + opt_const_symbol_reft lookup(const irep_idt &identifier) const; + opt_symbol_reft get_writeable(const irep_idt &identifier); bool add(const symbolt &symbol); - /// Move or copy a new symbol to the symbol table - /// \remark: This is a nicer interface than move and achieves the same - /// result as both move and add - /// \param symbol: The symbol to be added to the symbol table - can be - /// moved or copied in - /// \return Returns a reference to the newly inserted symbol or to the - /// existing symbol if a symbol with the same name already exists in the - /// symbol table, along with a bool that is true if a new symbol was inserted. + std::pair insert(symbolt symbol); + bool move(symbolt &symbol, symbolt *&new_symbol); void clear()