Follow-up to 090790a: attribute __used__ requires unique names

With 090790a we made sure that symbols marked with
__attribute__((__used__)) are not discarded. Linking multiple files that
use symbols marked as such still must not result in conflicting
declarations on such symbols, thus use the DJB name mangler to generate
unique names.

Author: tautschnig

regression/ansi-c/gcc_attribute_used1/main.c

@@ -0,0 +1,6 @@
+static int foo __attribute__((used)) = 42;
+
+int main()
+{
+  return 0;
+}

regression/ansi-c/gcc_attribute_used1/other.c

@@ -0,0 +1,15 @@
+struct bar
+{
+  char *ptr;
+};
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data")));
+
+static struct bar foo __attribute__((used))
+__attribute__((__section__(".ref.data"))) = {0};
+
+void use_foo()
+{
+  __CPROVER_assert(foo.ptr == 0, "null");
+}

regression/ansi-c/gcc_attribute_used1/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+other.c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/goto-instrument/gcc_attribute_used1/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^[[:space:]]*ASSIGN foo := 42$
+^[[:space:]]*ASSIGN .*foo := 42$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$

src/ansi-c/ansi_c_declaration.cpp

@@ -173,10 +173,6 @@ void ansi_c_declarationt::to_symbol(
         else  if(get_is_extern()) // traditional GCC
           symbol.is_file_local=true;
       }
-
-      // GCC __attribute__((__used__)) - do not treat those as file-local
-      if(get_is_used())
-        symbol.is_file_local = false;
     }
   }
   else // non-function
@@ -190,10 +186,8 @@ void ansi_c_declarationt::to_symbol(
       (!symbol.is_static_lifetime && !get_is_extern()) ||
       get_is_thread_local();
 
-    symbol.is_file_local=
-      symbol.is_macro ||
-      (!get_is_global() && !get_is_extern()) ||
-      (get_is_global() && get_is_static() && !get_is_used()) ||
-      symbol.is_parameter;
+    symbol.is_file_local =
+      symbol.is_macro || (!get_is_global() && !get_is_extern()) ||
+      (get_is_global() && get_is_static()) || symbol.is_parameter;
   }
 }

src/ansi-c/ansi_c_declaration.h

@@ -195,16 +195,6 @@ class ansi_c_declarationt:public exprt
     set(ID_is_weak, is_weak);
   }
 
-  bool get_is_used() const
-  {
-    return get_bool(ID_is_used);
-  }
-
-  void set_is_used(bool is_used)
-  {
-    set(ID_is_used, is_used);
-  }
-
   void to_symbol(
     const ansi_c_declaratort &,
     symbolt &symbol) const;

src/ansi-c/c_typecheck_base.cpp

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/symbol_table_base.h>
 
+#include <goto-programs/name_mangler.h>
+
 #include "ansi_c_declaration.h"
 #include "c_storage_spec.h"
 #include "expr2c.h"
@@ -758,7 +760,6 @@ void c_typecheck_baset::typecheck_declaration(
       declaration.set_is_register(full_spec.is_register);
       declaration.set_is_typedef(full_spec.is_typedef);
       declaration.set_is_weak(full_spec.is_weak);
-      declaration.set_is_used(full_spec.is_used);
 
       symbolt symbol;
       declaration.to_symbol(declarator, symbol);
@@ -788,6 +789,20 @@ void c_typecheck_baset::typecheck_declaration(
         symbol.is_macro=true;
       }
 
+      if(full_spec.is_used && symbol.is_file_local)
+      {
+        // GCC __attribute__((__used__)) - do not treat those as file-local, but
+        // make sure the name is unique
+        symbol.is_file_local = false;
+
+        symbolt symbol_for_renaming = symbol;
+        if(!full_spec.asm_label.empty())
+          symbol_for_renaming.name = full_spec.asm_label;
+        full_spec.asm_label = djb_manglert{}(
+          symbol_for_renaming,
+          id2string(symbol_for_renaming.location.get_file()));
+      }
+
       if(full_spec.section.empty())
         apply_asm_label(full_spec.asm_label, symbol);
       else