From 929852671d4dd35c2ab4aa2db5c9a94262176b18 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jan 2021 11:14:30 +0000 Subject: [PATCH] Follow-up to 090790a467: attribute __used__ requires unique names With 090790a467 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. --- regression/ansi-c/gcc_attribute_used1/main.c | 6 ++++++ regression/ansi-c/gcc_attribute_used1/other.c | 15 +++++++++++++++ regression/ansi-c/gcc_attribute_used1/test.desc | 8 ++++++++ .../gcc_attribute_used1/test.desc | 2 +- src/ansi-c/ansi_c_declaration.cpp | 12 +++--------- src/ansi-c/ansi_c_declaration.h | 10 ---------- src/ansi-c/c_typecheck_base.cpp | 17 ++++++++++++++++- 7 files changed, 49 insertions(+), 21 deletions(-) create mode 100644 regression/ansi-c/gcc_attribute_used1/main.c create mode 100644 regression/ansi-c/gcc_attribute_used1/other.c create mode 100644 regression/ansi-c/gcc_attribute_used1/test.desc diff --git a/regression/ansi-c/gcc_attribute_used1/main.c b/regression/ansi-c/gcc_attribute_used1/main.c new file mode 100644 index 00000000000..34e8a77dea1 --- /dev/null +++ b/regression/ansi-c/gcc_attribute_used1/main.c @@ -0,0 +1,6 @@ +static int foo __attribute__((used)) = 42; + +int main() +{ + return 0; +} diff --git a/regression/ansi-c/gcc_attribute_used1/other.c b/regression/ansi-c/gcc_attribute_used1/other.c new file mode 100644 index 00000000000..87fc64f8ccf --- /dev/null +++ b/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"); +} diff --git a/regression/ansi-c/gcc_attribute_used1/test.desc b/regression/ansi-c/gcc_attribute_used1/test.desc new file mode 100644 index 00000000000..5297a015e56 --- /dev/null +++ b/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$ diff --git a/regression/goto-instrument/gcc_attribute_used1/test.desc b/regression/goto-instrument/gcc_attribute_used1/test.desc index ef8311e5230..e0b171de89e 100644 --- a/regression/goto-instrument/gcc_attribute_used1/test.desc +++ b/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$ diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 7d45ee0a1df..a888e993ed2 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/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; } } diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index d3d1f87bc29..a23c7351021 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/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; diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 4870c033487..19742a50a07 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #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