Merge pull request #8167 from tautschnig/bugfixes/linking-rename-local

Linking: only rename file-local symbols

Author: tautschnig

regression/cbmc/Linking9/f1.c

@@ -0,0 +1,8 @@
+static void f()
+{
+}
+void g()
+{
+  f();
+  int x = 42;
+}

regression/cbmc/Linking9/f2.c

@@ -0,0 +1,4 @@
+void f()
+{
+  __CPROVER_assert(0, "unreachable");
+}

regression/cbmc/Linking9/f3.c

@@ -0,0 +1,9 @@
+extern void f();
+extern void g();
+
+int main()
+{
+  g();
+  f();
+  return 0;
+}

regression/cbmc/Linking9/test.desc

@@ -0,0 +1,8 @@
+CORE
+f3.c
+f1.c f2.c
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-programs/link_goto_model.cpp

@@ -22,7 +22,6 @@ Author: Michael Tautschnig, Daniel Kroening
 
 static void rename_symbols_in_function(
   goto_functionst::goto_functiont &function,
-  irep_idt &new_function_name,
   const rename_symbolt &rename_symbol)
 {
   for(auto &identifier : function.parameter_identifiers)
@@ -48,22 +47,39 @@ static bool link_functions(
   goto_functionst &dest_functions,
   const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
-  const rename_symbolt &rename_symbol,
+  const rename_symbolt &rename_dest_symbol,
+  const rename_symbolt &rename_src_symbol,
   const std::unordered_set<irep_idt> &weak_symbols)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
 
+  // rename existing functions if linking requires us to do so
+  for(const auto &rename_entry : rename_dest_symbol.expr_map)
+  {
+    auto fn_candidate = dest_functions.function_map.find(rename_entry.first);
+    if(fn_candidate == dest_functions.function_map.end())
+      continue;
+
+    dest_functions.function_map.insert(
+      {rename_entry.second, std::move(fn_candidate->second)});
+    dest_functions.function_map.erase(fn_candidate);
+  }
+
+  // rename symbols in existing functions
+  for(auto &dest_entry : dest_functions.function_map)
+    rename_symbols_in_function(dest_entry.second, rename_dest_symbol);
+
   // merge functions
   for(auto &gf_entry : src_functions.function_map)
   {
     // the function might have been renamed
     rename_symbolt::expr_mapt::const_iterator e_it =
-      rename_symbol.expr_map.find(gf_entry.first);
+      rename_src_symbol.expr_map.find(gf_entry.first);
 
     irep_idt final_id = gf_entry.first;
 
-    if(e_it!=rename_symbol.expr_map.end())
+    if(e_it != rename_src_symbol.expr_map.end())
       final_id=e_it->second;
 
     // already there?
@@ -73,7 +89,7 @@ static bool link_functions(
     goto_functionst::goto_functiont &src_func = gf_entry.second;
     if(dest_f_it==dest_functions.function_map.end()) // not there yet
     {
-      rename_symbols_in_function(src_func, final_id, rename_symbol);
+      rename_symbols_in_function(src_func, rename_src_symbol);
       dest_functions.function_map.emplace(final_id, std::move(src_func));
     }
     else // collision!
@@ -84,7 +100,7 @@ static bool link_functions(
          weak_symbols.find(final_id)!=weak_symbols.end())
       {
         // the one with body wins!
-        rename_symbols_in_function(src_func, final_id, rename_symbol);
+        rename_symbols_in_function(src_func, rename_src_symbol);
 
         in_dest_symbol_table.body.swap(src_func.body);
         in_dest_symbol_table.parameter_identifiers.swap(
@@ -133,7 +149,8 @@ std::optional<replace_symbolt::expr_mapt> link_goto_model(
        dest.goto_functions,
        src.symbol_table,
        src.goto_functions,
-       linking.rename_symbol,
+       linking.rename_main_symbol,
+       linking.rename_new_symbol,
        weak_symbols))
   {
     messaget log{message_handler};
@@ -184,10 +201,7 @@ void finalize_linking(
   if(!macro_application.expr_map.empty())
   {
     for(auto &gf_entry : dest_functions.function_map)
-    {
-      irep_idt final_id = gf_entry.first;
-      rename_symbols_in_function(gf_entry.second, final_id, macro_application);
-    }
+      rename_symbols_in_function(gf_entry.second, macro_application);
   }
 
   if(!object_type_updates.empty())

src/linking/linking.cpp

@@ -539,18 +539,19 @@ linkingt::rename(const symbol_table_baset &src_symbol_table, const irep_idt &id)
   }
 }
 
-bool linkingt::needs_renaming_non_type(
+linkingt::renamingt linkingt::needs_renaming_non_type(
   const symbolt &old_symbol,
   const symbolt &new_symbol)
 {
   // We first take care of file-local non-type symbols.
   // These are static functions, or static variables
   // inside static function bodies.
-  if(new_symbol.is_file_local ||
-     old_symbol.is_file_local)
-    return true;
-
-  return false;
+  if(new_symbol.is_file_local)
+    return renamingt::RENAME_NEW;
+  else if(old_symbol.is_file_local)
+    return renamingt::RENAME_OLD;
+  else
+    return renamingt::NO_RENAMING;
 }
 
 void linkingt::duplicate_code_symbol(
@@ -839,8 +840,8 @@ void linkingt::duplicate_code_symbol(
     if(old_symbol.value.is_nil())
     {
       // the one with body wins!
-      rename_symbol(new_symbol.value);
-      rename_symbol(new_symbol.type);
+      rename_new_symbol(new_symbol.value);
+      rename_new_symbol(new_symbol.type);
       old_symbol.value=new_symbol.value;
       old_symbol.type=new_symbol.type; // for parameter identifiers
       old_symbol.is_weak=new_symbol.is_weak;
@@ -1312,45 +1313,53 @@ void linkingt::duplicate_type_symbol(
     "unexpected difference between type symbols");
 }
 
-bool linkingt::needs_renaming_type(
+linkingt::renamingt linkingt::needs_renaming_type(
   const symbolt &old_symbol,
   const symbolt &new_symbol)
 {
   PRECONDITION(new_symbol.is_type);
 
   if(!old_symbol.is_type)
-    return true;
+    return renamingt::RENAME_NEW;
 
   if(old_symbol.type==new_symbol.type)
-    return false;
+    return renamingt::NO_RENAMING;
 
   if(
     old_symbol.type.id() == ID_struct &&
     to_struct_type(old_symbol.type).is_incomplete() &&
     new_symbol.type.id() == ID_struct &&
     !to_struct_type(new_symbol.type).is_incomplete())
-    return false; // not different
+  {
+    return renamingt::NO_RENAMING; // not different
+  }
 
   if(
     old_symbol.type.id() == ID_struct &&
     !to_struct_type(old_symbol.type).is_incomplete() &&
     new_symbol.type.id() == ID_struct &&
     to_struct_type(new_symbol.type).is_incomplete())
-    return false; // not different
+  {
+    return renamingt::NO_RENAMING; // not different
+  }
 
   if(
     old_symbol.type.id() == ID_union &&
     to_union_type(old_symbol.type).is_incomplete() &&
     new_symbol.type.id() == ID_union &&
     !to_union_type(new_symbol.type).is_incomplete())
-    return false; // not different
+  {
+    return renamingt::NO_RENAMING; // not different
+  }
 
   if(
     old_symbol.type.id() == ID_union &&
     !to_union_type(old_symbol.type).is_incomplete() &&
     new_symbol.type.id() == ID_union &&
     to_union_type(new_symbol.type).is_incomplete())
-    return false; // not different
+  {
+    return renamingt::NO_RENAMING; // not different
+  }
 
   if(
     old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
@@ -1359,14 +1368,18 @@ bool linkingt::needs_renaming_type(
   {
     if(to_array_type(old_symbol.type).size().is_nil() &&
        to_array_type(new_symbol.type).size().is_not_nil())
-      return false; // not different
+    {
+      return renamingt::NO_RENAMING; // not different
+    }
 
     if(to_array_type(new_symbol.type).size().is_nil() &&
        to_array_type(old_symbol.type).size().is_not_nil())
-      return false; // not different
+    {
+      return renamingt::NO_RENAMING; // not different
+    }
   }
 
-  return true; // different
+  return renamingt::RENAME_NEW; // different
 }
 
 static void do_type_dependencies(
@@ -1445,9 +1458,9 @@ std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
 #endif
 
     if(new_symbol.is_type)
-      rename_symbol.insert_type(id, new_identifier);
+      rename_new_symbol.insert_type(id, new_identifier);
     else
-      rename_symbol.insert_expr(id, new_identifier);
+      rename_new_symbol.insert_expr(id, new_identifier);
   }
 
   return new_identifiers;
@@ -1463,8 +1476,8 @@ void linkingt::copy_symbols(
   {
     symbolt symbol=named_symbol.second;
     // apply the renaming
-    rename_symbol(symbol.type);
-    rename_symbol(symbol.value);
+    rename_new_symbol(symbol.type);
+    rename_new_symbol(symbol.value);
     auto it = new_identifiers.find(named_symbol.first);
     if(it != new_identifiers.end())
       symbol.name = it->second;
@@ -1537,16 +1550,50 @@ bool linkingt::link(const symbol_table_baset &src_symbol_table)
     symbol_table_baset::symbolst::const_iterator m_it =
       main_symbol_table.symbols.find(symbol_pair.first);
 
-    if(
-      m_it != main_symbol_table.symbols.end() && // duplicate
-      needs_renaming(m_it->second, symbol_pair.second))
+    if(m_it != main_symbol_table.symbols.end())
     {
-      needs_to_be_renamed.insert(symbol_pair.first);
-      #ifdef DEBUG
-      messaget log{message_handler};
-      log.debug() << "LINKING: needs to be renamed: " << symbol_pair.first
-                  << messaget::eom;
+      // duplicate
+      switch(needs_renaming(m_it->second, symbol_pair.second))
+      {
+      case renamingt::NO_RENAMING:
+        break;
+      case renamingt::RENAME_OLD:
+      {
+        symbolt renamed_symbol = m_it->second;
+        renamed_symbol.name = rename(src_symbol_table, symbol_pair.first);
+        if(m_it->second.is_type)
+          rename_main_symbol.insert_type(m_it->first, renamed_symbol.name);
+        else
+          rename_main_symbol.insert_expr(m_it->first, renamed_symbol.name);
+        main_symbol_table.erase(m_it);
+        main_symbol_table.insert(std::move(renamed_symbol));
+        break;
+      }
+      case renamingt::RENAME_NEW:
+      {
+        needs_to_be_renamed.insert(symbol_pair.first);
+#ifdef DEBUG
+        messaget log{message_handler};
+        log.debug() << "LINKING: needs to be renamed: " << symbol_pair.first
+                    << messaget::eom;
 #endif
+        break;
+      }
+      }
+    }
+  }
+
+  // rename within main symbol table
+  for(auto &symbol_pair : main_symbol_table)
+  {
+    symbolt tmp = symbol_pair.second;
+    bool unmodified = rename_main_symbol(tmp.value);
+    unmodified &= rename_main_symbol(tmp.type);
+    if(!unmodified)
+    {
+      symbolt *sym_ptr = main_symbol_table.get_writeable(symbol_pair.first);
+      CHECK_RETURN(sym_ptr);
+      *sym_ptr = std::move(tmp);
     }
   }
 

src/linking/linking_class.h

@@ -48,21 +48,24 @@ class linkingt
   /// \return True, iff linking failed with unresolvable conflicts.
   bool link(const symbol_table_baset &src_symbol_table);
 
-  rename_symbolt rename_symbol;
+  rename_symbolt rename_main_symbol, rename_new_symbol;
   casting_replace_symbolt object_type_updates;
 
 protected:
-  bool needs_renaming_type(
-    const symbolt &old_symbol,
-    const symbolt &new_symbol);
+  enum renamingt
+  {
+    NO_RENAMING,
+    RENAME_OLD,
+    RENAME_NEW
+  };
 
-  bool needs_renaming_non_type(
-    const symbolt &old_symbol,
-    const symbolt &new_symbol);
+  renamingt
+  needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol);
 
-  bool needs_renaming(
-    const symbolt &old_symbol,
-    const symbolt &new_symbol)
+  renamingt
+  needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol);
+
+  renamingt needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
   {
     if(new_symbol.is_type)
       return needs_renaming_type(old_symbol, new_symbol);