Use get_writeable_symbol() to avoid redundant search

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -605,9 +605,9 @@ void convert_synchronized_methods(
   message_handlert &message_handler)
 {
   namespacet ns(symbol_table);
-  for(const auto &entry : symbol_table)
+  for(auto s_it = symbol_table.begin(); s_it != symbol_table.end(); ++s_it)
   {
-    const symbolt &symbol = entry.second;
+    const symbolt &symbol = s_it->second;
 
     if(symbol.type.id() != ID_code)
       continue;
@@ -619,11 +619,10 @@ void convert_synchronized_methods(
     if(symbol.type.get_bool(ID_is_static))
     {
       messaget message(message_handler);
-      message.warning() << "Java method '" << entry.first
+      message.warning() << "Java method '" << s_it->first
                         << "' is static and synchronized."
                         << " This is unsupported, the synchronized keyword"
-                        << " will be ignored."
-                        << messaget::eom;
+                        << " will be ignored." << messaget::eom;
       continue;
     }
 
@@ -638,7 +637,7 @@ void convert_synchronized_methods(
       continue;
 
     // get writeable reference and instrument the method
-    symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first);
+    symbolt &w_symbol = s_it.get_writeable_symbol();
     instrument_synchronized_code(
       symbol_table, w_symbol, it->second.symbol_expr());
   }

src/ansi-c/c_typecheck_type.cpp

@@ -1422,13 +1422,12 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
   enum_tag_symbol.type.add_subtype() = underlying_type;
 
   // is it in the symbol table already?
-  symbol_table_baset::symbolst::const_iterator s_it =
-    symbol_table.symbols.find(identifier);
+  symbolt *existing_symbol = symbol_table.get_writeable(identifier);
 
-  if(s_it!=symbol_table.symbols.end())
+  if(existing_symbol)
   {
     // Yes.
-    const symbolt &symbol=s_it->second;
+    const symbolt &symbol = *existing_symbol;
 
     if(symbol.type.id() != ID_c_enum)
     {
@@ -1441,7 +1440,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_ref(symbol.name).type=enum_tag_symbol.type;
+      existing_symbol->type = enum_tag_symbol.type;
     }
     else
     {

src/cpp/cpp_typecheck.cpp

@@ -158,7 +158,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
 
   for(const irep_idt &d_it : dynamic_initializations)
   {
-    const symbolt &symbol = symbol_table.lookup_ref(d_it);
+    symbolt &symbol = symbol_table.get_writeable_ref(d_it);
 
     if(symbol.is_extern)
       continue;
@@ -182,7 +182,7 @@ void cpp_typecheckt::static_and_dynamic_initialization()
 
       // Make it nil to get zero initialization by
       // __CPROVER_initialize
-      symbol_table.get_writeable_ref(d_it).value.make_nil();
+      symbol.value.make_nil();
     }
     else
     {
@@ -220,9 +220,9 @@ void cpp_typecheckt::do_not_typechecked()
   {
     cont = false;
 
-    for(const auto &named_symbol : symbol_table.symbols)
+    for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
     {
-      const symbolt &symbol=named_symbol.second;
+      const symbolt &symbol = it->second;
 
       if(
         symbol.value.id() == ID_cpp_not_typechecked &&
@@ -248,30 +248,28 @@ void cpp_typecheckt::do_not_typechecked()
         else
           UNREACHABLE; // Don't know what to do!
 
-        symbolt &writable_symbol =
-          symbol_table.get_writeable_ref(named_symbol.first);
+        symbolt &writable_symbol = it.get_writeable_symbol();
         writable_symbol.value.swap(value);
         convert_function(writable_symbol);
       }
     }
   }
   while(cont);
 
-  for(const auto &named_symbol : symbol_table.symbols)
+  for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
   {
-    if(named_symbol.second.value.id() == ID_cpp_not_typechecked)
-      symbol_table.get_writeable_ref(named_symbol.first).value.make_nil();
+    if(it->second.value.id() == ID_cpp_not_typechecked)
+      it.get_writeable_symbol().value.make_nil();
   }
 }
 
 void cpp_typecheckt::clean_up()
 {
-  symbol_table_baset::symbolst::const_iterator it =
-    symbol_table.symbols.begin();
+  auto it = symbol_table.begin();
 
-  while(it!=symbol_table.symbols.end())
+  while(it != symbol_table.end())
   {
-    symbol_table_baset::symbolst::const_iterator cur_it = it;
+    auto cur_it = it;
     it++;
 
     const symbolt &symbol=cur_it->second;
@@ -288,8 +286,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_ref(cur_it->first).type);
+      struct_union_typet &struct_union_type =
+        to_struct_union_type(cur_it.get_writeable_symbol().type);
 
       const struct_union_typet::componentst &components=
         struct_union_type.components();

src/cpp/cpp_typecheck_declaration.cpp

@@ -60,7 +60,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
   new_code.add_to_operands(code_frontend_declt(cpp_symbol_expr(symbol)));
 
   // do scoping
-  symbolt union_symbol =
+  symbolt &union_symbol =
     symbol_table.get_writeable_ref(follow(symbol.type).get(ID_name));
 
   for(const auto &c : to_union_type(union_symbol.type).components())
@@ -89,8 +89,7 @@ codet cpp_typecheckt::convert_anonymous_union(cpp_declarationt &declaration)
     id.is_member=true;
   }
 
-  symbol_table.get_writeable_ref(union_symbol.name)
-    .type.set(ID_C_unnamed_object, symbol.base_name);
+  union_symbol.type.set(ID_C_unnamed_object, symbol.base_name);
 
   return new_code;
 }

src/cpp/cpp_typecheck_expr.cpp

@@ -1230,14 +1230,10 @@ void cpp_typecheckt::typecheck_expr_member(
   if(expr.type().id()==ID_code)
   {
     // Check if the function body has to be typechecked
-    symbol_table_baset::symbolst::const_iterator it =
-      symbol_table.symbols.find(component_name);
+    symbolt &component_symbol = symbol_table.get_writeable_ref(component_name);
 
-    CHECK_RETURN(it != symbol_table.symbols.end());
-
-    if(it->second.value.id() == ID_cpp_not_typechecked)
-      symbol_table.get_writeable_ref(component_name)
-        .value.set(ID_is_used, true);
+    if(component_symbol.value.id() == ID_cpp_not_typechecked)
+      component_symbol.value.set(ID_is_used, true);
   }
 }
 
@@ -1938,9 +1934,9 @@ void cpp_typecheckt::typecheck_method_application(
   exprt member_expr;
   member_expr.swap(expr.function());
 
-  const symbolt &symbol=lookup(member_expr.get(ID_component_name));
-  symbolt &method_symbol=symbol_table.get_writeable_ref(symbol.name);
-  const symbolt &tag_symbol = lookup(symbol.type.get(ID_C_member_name));
+  symbolt &method_symbol =
+    symbol_table.get_writeable_ref(member_expr.get(ID_component_name));
+  const symbolt &tag_symbol = lookup(method_symbol.type.get(ID_C_member_name));
 
   // build the right template map
   // if this is an instantiated template class method
@@ -1954,21 +1950,21 @@ void cpp_typecheckt::typecheck_method_application(
       static_cast<const cpp_template_args_tct &>(template_args));
     add_method_body(&method_symbol);
 #ifdef DEBUG
-    std::cout << "MAP for " << symbol << ":\n";
+    std::cout << "MAP for " << method_symbol << ":\n";
     template_map.print(std::cout);
 #endif
   }
   else
     add_method_body(&method_symbol);
 
   // build new function expression
-  exprt new_function(cpp_symbol_expr(symbol));
+  exprt new_function(cpp_symbol_expr(method_symbol));
   new_function.add_source_location()=member_expr.source_location();
   expr.function().swap(new_function);
 
   if(!expr.function().type().get_bool(ID_C_is_static))
   {
-    const code_typet &func_type=to_code_type(symbol.type);
+    const code_typet &func_type = to_code_type(method_symbol.type);
     typet this_type=func_type.parameters().front().type();
 
     // Special case. Make it a reference.
@@ -2002,10 +1998,10 @@ void cpp_typecheckt::typecheck_method_application(
   }
 
   if(
-    symbol.value.id() == ID_cpp_not_typechecked &&
-    !symbol.value.get_bool(ID_is_used))
+    method_symbol.value.id() == ID_cpp_not_typechecked &&
+    !method_symbol.value.get_bool(ID_is_used))
   {
-    symbol_table.get_writeable_ref(symbol.name).value.set(ID_is_used, true);
+    method_symbol.value.set(ID_is_used, true);
   }
 }
 
@@ -2253,13 +2249,11 @@ void cpp_typecheckt::typecheck_expr_function_identifier(exprt &expr)
   if(expr.id()==ID_symbol)
   {
     // Check if the function body has to be typechecked
-    symbol_table_baset::symbolst::const_iterator it =
-      symbol_table.symbols.find(expr.get(ID_identifier));
-
-    CHECK_RETURN(it != symbol_table.symbols.end());
+    symbolt &function_symbol =
+      symbol_table.get_writeable_ref(expr.get(ID_identifier));
 
-    if(it->second.value.id() == ID_cpp_not_typechecked)
-      symbol_table.get_writeable_ref(it->first).value.set(ID_is_used, true);
+    if(function_symbol.value.id() == ID_cpp_not_typechecked)
+      function_symbol.value.set(ID_is_used, true);
   }
 
   c_typecheck_baset::typecheck_expr_function_identifier(expr);

src/cpp/cpp_typecheck_template.cpp

@@ -240,28 +240,28 @@ void cpp_typecheckt::typecheck_function_template(
 
   // check if we have it already
 
-  symbol_table_baset::symbolst::const_iterator previous_symbol =
-    symbol_table.symbols.find(symbol_name);
+  symbolt *previous_symbol = symbol_table.get_writeable(symbol_name);
 
-  if(previous_symbol!=symbol_table.symbols.end())
+  if(previous_symbol)
   {
-    bool previous_has_value =
-     to_cpp_declaration(previous_symbol->second.type).
-       declarators()[0].find(ID_value).is_not_nil();
+    bool previous_has_value = to_cpp_declaration(previous_symbol->type)
+                                .declarators()[0]
+                                .find(ID_value)
+                                .is_not_nil();
 
     if(has_value && previous_has_value)
     {
       error().source_location=cpp_name.source_location();
       error() << "function template symbol '" << base_name
               << "' declared previously\n"
               << "location of previous definition: "
-              << previous_symbol->second.location << eom;
+              << previous_symbol->location << eom;
       throw 0;
     }
 
     if(has_value)
     {
-      symbol_table.get_writeable_ref(symbol_name).type.swap(declaration);
+      previous_symbol->type.swap(declaration);
       cpp_scopes.id_map[symbol_name]=&template_scope;
     }
 

src/goto-cc/linker_script_merge.cpp

@@ -225,26 +225,26 @@ int linker_script_merget::pointerize_linker_defined_symbols(
 
   // Next, find all occurrences of linker-defined symbols that are _values_
   // of some symbol in the symbol table, and pointerize them too
-  for(const auto &pair : goto_model.symbol_table.symbols)
+  for(auto it = goto_model.symbol_table.begin();
+      it != goto_model.symbol_table.end();
+      ++it)
   {
     std::list<symbol_exprt> to_pointerize;
-    symbols_to_pointerize(linker_values, pair.second.value, to_pointerize);
+    symbols_to_pointerize(linker_values, it->second.value, to_pointerize);
 
     if(to_pointerize.empty())
       continue;
-    log.debug() << "Pointerizing the symbol-table value of symbol "
-                << pair.first << messaget::eom;
+    log.debug() << "Pointerizing the symbol-table value of symbol " << it->first
+                << messaget::eom;
     int fail = pointerize_subexprs_of(
-      goto_model.symbol_table.get_writeable_ref(pair.first).value,
-      to_pointerize,
-      linker_values);
+      it.get_writeable_symbol().value, to_pointerize, linker_values);
     if(to_pointerize.empty() && fail==0)
       continue;
     ret=1;
     for(const auto &sym : to_pointerize)
     {
       log.error() << " Could not pointerize '" << sym.get_identifier()
-                  << "' in symbol table entry " << pair.first << ". Pretty:\n"
+                  << "' in symbol table entry " << it->first << ". Pretty:\n"
                   << sym.pretty() << "\n";
     }
     log.error() << messaget::eom;

src/goto-instrument/dump_c.cpp

@@ -83,9 +83,10 @@ void dump_ct::operator()(std::ostream &os)
   // add copies of struct types when ID_C_transparent_union is only
   // annotated to parameter
   symbol_tablet additional_symbols;
-  for(const auto &named_symbol : copied_symbol_table.symbols)
+  for(auto it = copied_symbol_table.begin(); it != copied_symbol_table.end();
+      ++it)
   {
-    const symbolt &symbol=named_symbol.second;
+    const symbolt &symbol = it->second;
 
     if(
       (symbol.type.id() == ID_union || symbol.type.id() == ID_struct) &&
@@ -99,8 +100,7 @@ void dump_ct::operator()(std::ostream &os)
       else
         UNREACHABLE;
       type_symbolt ts{tag_name, symbol.type, symbol.mode};
-      typet &type =
-        copied_symbol_table.get_writeable_ref(named_symbol.first).type;
+      typet &type = it.get_writeable_symbol().type;
       if(ts.type.id() == ID_union)
         type = union_tag_typet{ts.name};
       else
@@ -111,8 +111,7 @@ 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_ref(named_symbol.first).type);
+    code_typet &code_type = to_code_type(it.get_writeable_symbol().type);
     code_typet::parameterst &parameters=code_type.parameters();
 
     for(code_typet::parameterst::iterator
@@ -149,9 +148,10 @@ void dump_ct::operator()(std::ostream &os)
   // add tags to anonymous union/struct/enum,
   // and prepare lexicographic order
   std::set<std::string> symbols_sorted;
-  for(const auto &named_symbol : copied_symbol_table.symbols)
+  for(auto it = copied_symbol_table.begin(); it != copied_symbol_table.end();
+      ++it)
   {
-    symbolt &symbol = copied_symbol_table.get_writeable_ref(named_symbol.first);
+    symbolt &symbol = it.get_writeable_symbol();
     bool tag_added=false;
 
     // TODO we could get rid of some of the ID_anonymous by looking up
@@ -172,7 +172,7 @@ void dump_ct::operator()(std::ostream &os)
       tag_added=true;
     }
 
-    const std::string name_str=id2string(named_symbol.first);
+    const std::string name_str = id2string(it->first);
     if(symbol.is_type &&
        (symbol.type.id()==ID_union ||
         symbol.type.id()==ID_struct ||

src/goto-programs/name_mangler.h

@@ -88,16 +88,17 @@ class function_name_manglert
     for(const auto &sym : old_syms)
       model.symbol_table.erase(sym);
 
-    for(const auto &sym_pair : model.symbol_table)
+    for(auto it = model.symbol_table.begin(); it != model.symbol_table.end();
+        ++it)
     {
-      const symbolt &sym = sym_pair.second;
+      const symbolt &sym = it->second;
 
       exprt e = sym.value;
       typet t = sym.type;
       if(rename(e) && rename(t))
         continue;
 
-      symbolt &new_sym = model.symbol_table.get_writeable_ref(sym.name);
+      symbolt &new_sym = it.get_writeable_symbol();
       new_sym.value = e;
       new_sym.type = t;
     }