Linking can safely clean up duplicates of static inline functions

This will avoid some occurrences of function$linkN names that are confusing to
users, in particular when specifying loop unwinding limits.

Author: tautschnig

regression/ansi-c/linking2/foo.h

@@ -0,0 +1,6 @@
+static inline void foo(int x)
+{
+  x = x + 1;
+}
+
+void bar(int);

regression/ansi-c/linking2/main.c

@@ -0,0 +1,8 @@
+#include "foo.h"
+
+int main(int argc, char *argv[])
+{
+  foo(argc);
+  bar(argc);
+  return 0;
+}

regression/ansi-c/linking2/other.c

@@ -0,0 +1,14 @@
+#ifndef TEST2
+#  include "foo.h"
+#else
+inline void foo(int x)
+{
+  x = 0;
+}
+#endif
+
+void bar(int y)
+{
+  foo(y);
+  y = 2;
+}

regression/ansi-c/linking2/test1.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+other.c --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^Functions: 5; 5 have a body.$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+The implementation of a function named "foo" (static inline void foo(int x)) is
+the same in both translation units, thus linking can safely discard one of the
+copies and does not need to do any renaming.

regression/ansi-c/linking2/test2.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+other.c --verbosity 10 -DTEST2
+^EXIT=0$
+^SIGNAL=0$
+^Functions: 6; 6 have a body.$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+The implementation of a function named "foo" (void foo(int x)) differs between
+translation units; as at least one of them is static this is acceptable at link
+time and can be resolved by renaming one of them.

regression/ansi-c/static2/main2.c

@@ -1,4 +1,4 @@
 static int foo(int a)
 {
-  return a+1;
+  return a + 2;
 }

regression/ansi-c/static3/main2.c

@@ -1,4 +1,4 @@
 static int foo(int a)
 {
-  return a+1;
+  return a + 2;
 }

src/goto-programs/link_goto_model.cpp

@@ -48,15 +48,45 @@ static bool link_functions(
   goto_functionst &dest_functions,
   const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
-  const rename_symbolt &rename_symbol,
+  rename_symbolt &rename_symbol,
   const std::unordered_set<irep_idt> &weak_symbols)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
 
+  // remove any unnecessary duplicates
+  std::unordered_set<irep_idt> duplicates;
+  for(const auto &f_pair : src_functions.function_map)
+  {
+    rename_symbolt::expr_mapt::iterator rename_it =
+      rename_symbol.expr_map.find(f_pair.first);
+    if(rename_it == rename_symbol.expr_map.end())
+      continue;
+
+    std::string new_name = id2string(rename_it->second);
+    std::string::size_type suffix_pos = new_name.find("$link");
+    if(suffix_pos == std::string::npos)
+      continue;
+
+    irep_idt original_name = new_name.substr(0, suffix_pos);
+    goto_functionst::function_mapt::iterator existing_func =
+      dest_functions.function_map.find(original_name);
+    if(existing_func == dest_functions.function_map.end())
+      continue;
+
+    if(f_pair.second.body.equals(existing_func->second.body))
+    {
+      duplicates.insert(f_pair.first);
+      rename_symbol.expr_map.erase(rename_it);
+    }
+  }
+
   // merge functions
   for(auto &gf_entry : src_functions.function_map)
   {
+    if(duplicates.find(gf_entry.first) != duplicates.end())
+      continue;
+
     // the function might have been renamed
     rename_symbolt::expr_mapt::const_iterator e_it =
       rename_symbol.expr_map.find(gf_entry.first);

src/linking/linking.cpp

@@ -537,11 +537,9 @@ bool linkingt::needs_renaming_non_type(
   // 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;
+  return (new_symbol.is_file_local || old_symbol.is_file_local) &&
+         (new_symbol.type.id() != ID_code || new_symbol.is_compiled() ||
+          new_symbol.value != old_symbol.value);
 }
 
 void linkingt::duplicate_code_symbol(
@@ -848,19 +846,18 @@ void linkingt::duplicate_code_symbol(
       object_type_updates.insert(
         old_symbol.symbol_expr(), old_symbol.symbol_expr());
     }
-    else if(to_code_type(old_symbol.type).get_inlined())
-    {
-      // ok, silently ignore
-    }
     else if(old_symbol.type == new_symbol.type)
     {
-      // keep the one in old_symbol -- libraries come last!
-      debug().source_location = new_symbol.location;
+      if(!new_symbol.is_file_local || !old_symbol.is_file_local)
+      {
+        // keep the one in old_symbol -- libraries come last!
+        debug().source_location = new_symbol.location;
 
-      debug() << "function '" << old_symbol.name << "' in module '"
-              << new_symbol.module
-              << "' is shadowed by a definition in module '"
-              << old_symbol.module << "'" << eom;
+        debug() << "function '" << old_symbol.name << "' in module '"
+                << new_symbol.module
+                << "' is shadowed by a definition in module '"
+                << old_symbol.module << "'" << eom;
+      }
     }
     else
       link_error(