From e1339642867f946db1ea04a6219524b351273b06 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 23 Feb 2018 12:02:32 +0000 Subject: [PATCH 1/3] C front-end: Section/ASM renaming also needs to be applied to aliases The example taken from the Linux kernel shows that people mix weak aliases with section attributes. Not updating the alias name results in a namespace lookup failure. gcc_attributes11 is a reduced example taken from SV-COMP, where the same problem arises. --- regression/ansi-c/gcc_attributes11/main.c | 18 ++++++++++++++++++ regression/ansi-c/gcc_attributes11/test.desc | 8 ++++++++ regression/ansi-c/gcc_attributes9/main.c | 12 ++++++++++++ src/ansi-c/c_typecheck_base.cpp | 7 ++++++- 4 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 regression/ansi-c/gcc_attributes11/main.c create mode 100644 regression/ansi-c/gcc_attributes11/test.desc diff --git a/regression/ansi-c/gcc_attributes11/main.c b/regression/ansi-c/gcc_attributes11/main.c new file mode 100644 index 00000000000..b69ac3e0e63 --- /dev/null +++ b/regression/ansi-c/gcc_attributes11/main.c @@ -0,0 +1,18 @@ +#ifdef __GNUC__ +// example extracted from SV-COMP's ldv-linux-3.4-simple/ +// 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640 +static int __attribute__((__section__(".init.text"))) +__attribute__((no_instrument_function)) dp83640_init(void) +{ + return 0; +} +int init_module(void) __attribute__((alias("dp83640_init"))); +#endif + +int main() +{ +#ifdef __GNUC__ + dp83640_init(); +#endif + return 0; +} diff --git a/regression/ansi-c/gcc_attributes11/test.desc b/regression/ansi-c/gcc_attributes11/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/gcc_attributes11/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/regression/ansi-c/gcc_attributes9/main.c b/regression/ansi-c/gcc_attributes9/main.c index f18e17aa773..76c7aeeca27 100644 --- a/regression/ansi-c/gcc_attributes9/main.c +++ b/regression/ansi-c/gcc_attributes9/main.c @@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar(); volatile int __attribute__((__section__(".init.data1"))) txt_heap_base1; volatile int __attribute__((__section__(".init.data3"))) txt_heap_base, __attribute__((__section__(".init.data4"))) txt_heap_size; +int __attribute__((__section__(".init.text"))) __attribute__((__cold__)) +__alloc_bootmem_huge_page(void *h); +int __attribute__((__section__(".init.text"))) __attribute__((__cold__)) +alloc_bootmem_huge_page(void *h); +int alloc_bootmem_huge_page(void *h) + __attribute__((weak, alias("__alloc_bootmem_huge_page"))); +int __alloc_bootmem_huge_page(void *h) +{ + return 1; +} #endif int main() { #ifdef __GNUC__ + int r = alloc_bootmem_huge_page(0); + static int __attribute__((section(".data.unlikely"))) __warned; __warned=1; return __warned; diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 1d213aa8f0a..ad72ea59f61 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -708,7 +708,12 @@ void c_typecheck_baset::typecheck_declaration( // alias function need not have been declared yet, thus // can't lookup - symbol.value=symbol_exprt(full_spec.alias); + // also cater for renaming/placement in sections + const auto &renaming_entry = asm_label_map.find(full_spec.alias); + if(renaming_entry == asm_label_map.end()) + symbol.value = symbol_exprt(full_spec.alias); + else + symbol.value = symbol_exprt(renaming_entry->second); symbol.is_macro=true; } From 9c66a66b745fdc725e18e47a0dc185f29bec59f7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 7 Aug 2017 09:30:21 +0000 Subject: [PATCH 2/3] fixup! Support __attribute__((section("x")) --- src/ansi-c/expr2c.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c97b1a9bdb8..1ab40b2004d 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2c.h" +#include #include #include #include @@ -89,6 +90,9 @@ static std::string clean_identifier(const irep_idt &id) *it2='_'; } + // rewrite . as used in ELF section names + std::replace(dest.begin(), dest.end(), '.', '_'); + return dest; } From 2a45e61be9468bfafe237cfcb57e82f047cfa6eb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 16 Feb 2018 13:35:59 +0000 Subject: [PATCH 3/3] Only the top-level section should be considered for renaming The Linux kernel first places `jiffies64` in .data, and later refines that to .data..cacheline_aligned. The latter still is within the .data section, though, so just use the .data part for renaming. --- src/ansi-c/c_typecheck_base.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index ad72ea59f61..890815fcc86 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -721,8 +721,18 @@ void c_typecheck_baset::typecheck_declaration( apply_asm_label(full_spec.asm_label, symbol); else { - std::string asm_name; - asm_name=id2string(full_spec.section)+"$$"; + // section name is not empty, do a bit of parsing + std::string asm_name = id2string(full_spec.section); + if(asm_name[0] != '.') + { + warning().source_location = symbol.location; + warning() << "section name `" << asm_name + << "' expected to start with `.'" << eom; + } + std::string::size_type primary_section = asm_name.find('.', 1); + if(primary_section != std::string::npos) + asm_name.resize(primary_section); + asm_name += "$$"; if(!full_spec.asm_label.empty()) asm_name+=id2string(full_spec.asm_label); else