diff --git a/regression/ansi-c/always_inline1/main.c b/regression/ansi-c/always_inline1/main.c new file mode 100644 index 00000000000..8d8512c54a2 --- /dev/null +++ b/regression/ansi-c/always_inline1/main.c @@ -0,0 +1,40 @@ +// this is a GCC extension + +#ifdef __GNUC__ +static inline __attribute__((always_inline)) _Bool +__is_kfree_rcu_offset(unsigned long offset) +{ + return offset < 4096; +} + +static inline __attribute__((always_inline)) void +kfree_rcu(unsigned long offset) +{ + // immediate use of a constant as argument to __builtin_constant_p + ((void)sizeof(char[1 - 2 * !!(!__builtin_constant_p(offset))])); + // inlining required to turn the array size into a compile-time constant + ((void)sizeof(char[1 - 2 * !!(!__is_kfree_rcu_offset(offset))])); +} + +static inline __attribute__((always_inline)) void unused(unsigned long offset) +{ + // this would not be constant as it's never used, the front-end needs to + // discard it + ((void)sizeof(char[1 - 2 * !!(!__builtin_constant_p(offset))])); +} + +// unused, but no 'static' +inline __attribute__((__always_inline__)) int also_unused(int _c) +{ + return _c; +} +#endif + +int main() +{ +#ifdef __GNUC__ + kfree_rcu(42); +#endif + + return 0; +} diff --git a/regression/ansi-c/always_inline1/test.desc b/regression/ansi-c/always_inline1/test.desc new file mode 100644 index 00000000000..c6ac7d7513d --- /dev/null +++ b/regression/ansi-c/always_inline1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ +-- +The static asserts (arrays that may have a negative size if the assertion fails) +can only be evaluated if always_inline is correctly applied. diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index e30503ae627..cc40c75214a 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -171,6 +171,8 @@ void ansi_c_convert_typet::read_rec(const typet &type) c_storage_spec.is_weak=true; else if(type.id() == ID_used) c_storage_spec.is_used = true; + else if(type.id() == ID_always_inline) + c_storage_spec.is_always_inline = true; else if(type.id()==ID_auto) { // ignore diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp index 5287fa6cfb6..d757d119dc0 100644 --- a/src/ansi-c/ansi_c_declaration.cpp +++ b/src/ansi-c/ansi_c_declaration.cpp @@ -81,6 +81,8 @@ void ansi_c_declarationt::output(std::ostream &out) const out << " is_extern"; if(get_is_static_assert()) out << " is_static_assert"; + if(get_is_always_inline()) + out << " is_always_inline"; out << "\n"; out << "Type: " << type().pretty() << "\n"; @@ -164,6 +166,9 @@ void ansi_c_declarationt::to_symbol( symbol.is_extern=false; else if(get_is_extern()) // traditional GCC symbol.is_file_local=true; + + if(get_is_always_inline()) + symbol.is_macro = true; } // GCC __attribute__((__used__)) - do not treat those as file-local diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index 4dfdb2b8478..3cbe9b52eb1 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -205,6 +205,16 @@ class ansi_c_declarationt:public exprt set(ID_is_used, is_used); } + bool get_is_always_inline() const + { + return get_bool(ID_is_always_inline); + } + + void set_is_always_inline(bool is_always_inline) + { + set(ID_is_always_inline, is_always_inline); + } + void to_symbol( const ansi_c_declaratort &, symbolt &symbol) const; diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp index e3e0aa4ef99..008a0098e4e 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -34,6 +34,8 @@ void c_storage_spect::read(const typet &type) is_weak=true; else if(type.id() == ID_used) is_used = true; + else if(type.id() == ID_always_inline) + is_always_inline = true; else if(type.id()==ID_auto) { // ignore diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h index 3061f5ce9af..e2ff9f2fe69 100644 --- a/src/ansi-c/c_storage_spec.h +++ b/src/ansi-c/c_storage_spec.h @@ -36,13 +36,14 @@ class c_storage_spect is_inline=false; is_weak=false; is_used = false; + is_always_inline = false; alias.clear(); asm_label.clear(); section.clear(); } - bool is_typedef, is_extern, is_static, is_register, - is_inline, is_thread_local, is_weak, is_used; + bool is_typedef, is_extern, is_static, is_register, is_inline, + is_thread_local, is_weak, is_used, is_always_inline; // __attribute__((alias("foo"))) irep_idt alias; @@ -53,6 +54,7 @@ class c_storage_spect bool operator==(const c_storage_spect &other) const { + // clang-format off return is_typedef==other.is_typedef && is_extern==other.is_extern && is_static==other.is_static && @@ -61,9 +63,11 @@ class c_storage_spect is_inline==other.is_inline && is_weak==other.is_weak && is_used == other.is_used && + is_always_inline == other.is_always_inline && alias==other.alias && asm_label==other.asm_label && section==other.section; + // clang-format on } bool operator!=(const c_storage_spect &other) const @@ -81,6 +85,7 @@ class c_storage_spect is_thread_local |=other.is_thread_local; is_weak |=other.is_weak; is_used |=other.is_used; + is_always_inline |= other.is_always_inline; if(alias.empty()) alias=other.alias; if(asm_label.empty()) diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index ae3d38921f2..512d790ba4d 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -689,6 +689,7 @@ void c_typecheck_baset::typecheck_declaration( declaration.set_is_typedef(full_spec.is_typedef); declaration.set_is_weak(full_spec.is_weak); declaration.set_is_used(full_spec.is_used); + declaration.set_is_always_inline(full_spec.is_always_inline); symbolt symbol; declaration.to_symbol(*d_it, symbol); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 142966aa0fa..8860b632e7e 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -18,9 +18,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include +#include #include #include @@ -1918,7 +1920,10 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(entry!=asm_label_map.end()) identifier=entry->second; - if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) + symbol_tablet::symbolst::const_iterator sym_entry = + symbol_table.symbols.find(identifier); + + if(sym_entry == symbol_table.symbols.end()) { // This is an undeclared function. // Is this a builtin? @@ -1960,6 +1965,87 @@ void c_typecheck_baset::typecheck_side_effect_function_call( warning() << "function `" << identifier << "' is not declared" << eom; } } + else if( + sym_entry->second.type.get_bool(ID_C_inlined) && + sym_entry->second.is_macro && sym_entry->second.value.is_not_nil()) + { + // calling a function marked as always_inline + const symbolt &func_sym = sym_entry->second; + const code_typet &func_type = to_code_type(func_sym.type); + + replace_symbolt replace; + + const code_typet::parameterst ¶meters = func_type.parameters(); + auto p_it = parameters.begin(); + for(const auto &arg : expr.arguments()) + { + if(p_it == parameters.end()) + { + // we don't support varargs with always_inline + err_location(f_op); + error() << "function call has additional arguments, " + << "cannot apply always_inline" << eom; + throw 0; + } + + irep_idt p_id = p_it->get_identifier(); + if(p_id.empty()) + { + p_id = id2string(func_sym.base_name) + "::" + + id2string(p_it->get_base_name()); + } + replace.insert(p_id, arg); + + ++p_it; + } + + if(p_it != parameters.end()) + { + err_location(f_op); + error() << "function call has missing arguments, " + << "cannot apply always_inline" << eom; + throw 0; + } + + codet body = to_code(func_sym.value); + replace(body); + + side_effect_exprt side_effect_expr( + ID_statement_expression, func_type.return_type()); + body.make_block(); + + // simulates parts of typecheck_function_body + typet cur_return_type = return_type; + return_type = func_type.return_type(); + typecheck_code(body); + return_type.swap(cur_return_type); + + // replace final return by an ID_expression + codet &last = to_code_block(body).find_last_statement(); + + if(last.get_statement() == ID_return) + last.set_statement(ID_expression); + + // NOLINTNEXTLINE(whitespace/braces) + const bool has_returns = has_subexpr(body, [&](const exprt &e) { + return e.id() == ID_code && to_code(e).get_statement() == ID_return; + }); + if(has_returns) + { + // we don't support multiple return statements with always_inline + err_location(last); + error() << "function has multiple return statements, " + << "cannot apply always_inline" << eom; + throw 0; + } + + side_effect_expr.copy_to_operands(body); + typecheck_side_effect_statement_expression(side_effect_expr); + + expr.swap(side_effect_expr); + + return; + } } // typecheck it now diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 636bb7330b2..164eb34eb09 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -150,6 +150,7 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" %token TOK_GCC_ATTRIBUTE_FALLTHROUGH "fallthrough" %token TOK_GCC_ATTRIBUTE_USED "used" +%token TOK_GCC_ATTRIBUTE_ALWAYS_INLINE "always_inline" %token TOK_GCC_LABEL "__label__" %token TOK_MSC_ASM "__asm" %token TOK_MSC_BASED "__based" @@ -1547,6 +1548,8 @@ gcc_type_attribute: { $$=$1; set($$, ID_destructor); } | TOK_GCC_ATTRIBUTE_USED { $$=$1; set($$, ID_used); } + | TOK_GCC_ATTRIBUTE_ALWAYS_INLINE + { $$=$1; set($$, ID_always_inline); } ; gcc_attribute: diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index 765a30fbf0f..61b69ff98d7 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1590,6 +1590,9 @@ __decltype { if(PARSER.cpp98 && "used" | "__used__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_USED; } +"always_inline" | +"__always_inline__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_ALWAYS_INLINE; } + {ws} { /* ignore */ } {newline} { /* ignore */ } {identifier} { BEGIN(GCC_ATTRIBUTE4); } diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index d563278ff52..e628a513be2 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -126,7 +126,7 @@ void remove_internal_symbols( is_file_local=false; } - if(is_type) + if(is_type || symbol.is_macro) { // never EXPORTED by itself } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 99e1374dec5..f3e0f474c7a 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -671,6 +671,8 @@ IREP_ID_TWO(C_abstract, #abstract) IREP_ID_ONE(synthetic) IREP_ID_ONE(interface) IREP_ID_TWO(C_must_not_throw, #must_not_throw) +IREP_ID_ONE(always_inline) +IREP_ID_ONE(is_always_inline) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.h in their source tree and diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index e568758661f..6eb8b19563b 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -100,6 +100,10 @@ bool replace_symbolt::replace( if(c_sizeof_type.is_not_nil() && have_to_replace(c_sizeof_type)) result &= replace(static_cast(dest.add(ID_C_c_sizeof_type))); + const typet &type_arg = static_cast(dest.find(ID_type_arg)); + if(type_arg.is_not_nil() && have_to_replace(type_arg)) + result &= replace(static_cast(dest.add(ID_type_arg))); + const typet &va_arg_type = static_cast(dest.find(ID_C_va_arg_type)); if(va_arg_type.is_not_nil() && have_to_replace(va_arg_type)) @@ -136,6 +140,12 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const if(have_to_replace(static_cast(c_sizeof_type))) return true; + const irept &type_arg = dest.find(ID_type_arg); + + if(type_arg.is_not_nil()) + if(have_to_replace(static_cast(type_arg))) + return true; + const irept &va_arg_type=dest.find(ID_C_va_arg_type); if(va_arg_type.is_not_nil())