Section renaming must be applied across translation units

The Unix linker starts with symbols placed in the "common"
pseudo-section and will then match them with definitions located in
other sections. Similarly, we need to make sure that symbols across
translation units are matched up, and macros will make sure that's the
case.

Author: tautschnig

regression/linking-goto-binaries/gcc_section1/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int in_other_section(void);
+int also_in_other_section(void);
+
+int main()
+{
+#ifdef __GNUC__
+  assert(in_other_section() == 42);
+  assert(also_in_other_section() == 42);
+#endif
+  return 0;
+}

regression/linking-goto-binaries/gcc_section1/section.c

@@ -0,0 +1,13 @@
+#ifdef __GNUC__
+int in_other_section(void);
+
+int __attribute__((__section__(".init.text"))) in_other_section(void)
+{
+  return 42;
+}
+
+int __attribute__((__section__(".init.text"))) also_in_other_section(void)
+{
+  return 42;
+}
+#endif

regression/linking-goto-binaries/gcc_section1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+section.c
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_base.cpp

@@ -758,6 +758,28 @@ void c_typecheck_baset::typecheck_declaration(
         else
           asm_name+=id2string(symbol.name);
 
+        if(!symbol.is_file_local)
+        {
+          // create a macro to apply section renaming across translation units
+          symbolt section_macro = symbol;
+          section_macro.value = symbol_exprt::typeless(asm_name);
+          section_macro.is_macro = true;
+
+          // replace a preceding "extern" declaration, or try to insert a new
+          // symbol
+          auto dest = symbol_table.get_writeable(symbol.name);
+          if(dest && dest->value.is_nil())
+          {
+            *dest = section_macro;
+          }
+          else if(!symbol_table.insert(section_macro).second)
+          {
+            warning().source_location = symbol.location;
+            warning() << "symbol '" << symbol.name
+                      << "' exists in multiple sections" << eom;
+          }
+        }
+
         apply_asm_label(asm_name, symbol);
       }
 

src/goto-programs/goto_convert_functions.cpp

@@ -160,9 +160,11 @@ void goto_convert_functionst::convert_function(
   f.set_parameter_identifiers(code_type);
 
   if(
-    symbol.value.is_nil() ||
+    symbol.is_macro || symbol.value.is_nil() ||
     symbol.is_compiled()) /* goto_inline may have removed the body */
+  {
     return;
+  }
 
   // we have a body, make sure all parameter names are valid
   for(const auto &p : f.parameter_identifiers)

src/linking/remove_internal_symbols.cpp

@@ -135,10 +135,17 @@ void remove_internal_symbols(
         is_file_local=false;
     }
 
-    if(is_type || symbol.is_macro)
+    if(is_type)
     {
       // never EXPORTED by itself
     }
+    else if(
+      symbol.is_macro &&
+      static_cast<const exprt &>(symbol.value).type() != typet{})
+    {
+      // only (typeless) export macros that do renaming, e.g., section renaming
+      // as implemented in the C front-end
+    }
     else if(is_function)
     {
       // body? not local (i.e., "static")?