From 8eaf89e45ef814cb970554e719ab89e2036eb2f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Oct 2017 16:10:45 +0100 Subject: [PATCH 1/2] Apply symbol replacement in type_arg members This is used int the precursor of a typechecked sizeof expression. --- src/util/replace_symbol.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 14765af113f..8656b311dbf 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -104,6 +104,16 @@ bool replace_symbolt::replace( result=false; } + const irept &type_arg=dest.find(ID_type_arg); + + if(type_arg.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_type_arg)); + + if(!replace(type)) + result=false; + } + const irept &va_arg_type=dest.find(ID_C_va_arg_type); if(va_arg_type.is_not_nil()) @@ -139,6 +149,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()) From 2afe3779f8553b225a7162795ebf451c5c433cf0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Oct 2017 16:11:54 +0100 Subject: [PATCH 2/2] Fully interpret __attribute__((always_inline)) The Linux kernel uses tests on __builtin_constant_p that are required to evalute to true for compilationt to succeed. These can only evaluate to true when inlining is actually done (and expressions are simplified). --- regression/ansi-c/always_inline1/main.c | 32 ++++++++++ regression/ansi-c/always_inline1/test.desc | 8 +++ src/ansi-c/ansi_c_convert_type.cpp | 2 + src/ansi-c/ansi_c_declaration.cpp | 5 ++ src/ansi-c/ansi_c_declaration.h | 10 +++ src/ansi-c/c_storage_spec.cpp | 2 + src/ansi-c/c_storage_spec.h | 5 +- src/ansi-c/c_typecheck_base.cpp | 1 + src/ansi-c/c_typecheck_expr.cpp | 72 +++++++++++++++++++++- src/ansi-c/parser.y | 3 + src/ansi-c/scanner.l | 3 + src/util/irep_ids.def | 2 + 12 files changed, 143 insertions(+), 2 deletions(-) create mode 100644 regression/ansi-c/always_inline1/main.c create mode 100644 regression/ansi-c/always_inline1/test.desc diff --git a/regression/ansi-c/always_inline1/main.c b/regression/ansi-c/always_inline1/main.c new file mode 100644 index 00000000000..97f06f1a378 --- /dev/null +++ b/regression/ansi-c/always_inline1/main.c @@ -0,0 +1,32 @@ +// 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) +{ + ((void)sizeof(char[1 - 2*!!(!__builtin_constant_p(offset))])); + + ((void)sizeof(char[1 - 2*!!(!__is_kfree_rcu_offset(offset))])); +} + +static inline __attribute__((always_inline)) +void unused(unsigned long offset) +{ + ((void)sizeof(char[1 - 2*!!(!__builtin_constant_p(offset))])); +} +#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..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/always_inline1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 3c00f08f39d..93da9f89cf2 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -155,6 +155,8 @@ void ansi_c_convert_typet::read_rec(const typet &type) c_storage_spec.is_register=true; else if(type.id()==ID_weak) c_storage_spec.is_weak=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 74f05e926b5..73409b63911 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; } } } diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index af5db98e32e..88fc2982753 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -195,6 +195,16 @@ class ansi_c_declarationt:public exprt set(ID_is_weak, is_weak); } + 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 5ed8314bd42..ec6d1446559 100644 --- a/src/ansi-c/c_storage_spec.cpp +++ b/src/ansi-c/c_storage_spec.cpp @@ -32,6 +32,8 @@ void c_storage_spect::read(const typet &type) is_register=true; else if(type.id()==ID_weak) is_weak=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 5b392fe4d05..81c27a4bd66 100644 --- a/src/ansi-c/c_storage_spec.h +++ b/src/ansi-c/c_storage_spec.h @@ -35,13 +35,14 @@ class c_storage_spect is_register=false; is_inline=false; is_weak=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_inline, is_thread_local, is_weak, is_always_inline; // __attribute__((alias("foo"))) irep_idt alias; @@ -59,6 +60,7 @@ class c_storage_spect is_thread_local==other.is_thread_local && is_inline==other.is_inline && is_weak==other.is_weak && + is_always_inline==other.is_always_inline && alias==other.alias && asm_label==other.asm_label && section==other.section; @@ -78,6 +80,7 @@ class c_storage_spect is_inline |=other.is_inline; is_thread_local |=other.is_thread_local; is_weak |=other.is_weak; + 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 1d213aa8f0a..71a070cfd10 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -688,6 +688,7 @@ 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_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 00d68f46c35..84d1b1f0ce8 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include "c_typecast.h" #include "c_qualifiers.h" @@ -1913,7 +1914,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. Let's just add it. // We do a bit of return-type guessing, but just a bit. @@ -1945,6 +1949,72 @@ void c_typecheck_baset::typecheck_side_effect_function_call( warning().source_location=f_op.find_source_location(); 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()) + { + 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); + + 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 ce04136d8e2..888c1babd10 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -142,6 +142,7 @@ extern char *yyansi_ctext; %token TOK_GCC_ATTRIBUTE_NORETURN "noreturn" %token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor" %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" +%token TOK_GCC_ATTRIBUTE_ALWAYS_INLINE "always_inline" %token TOK_GCC_LABEL "__label__" %token TOK_MSC_ASM "__asm" %token TOK_MSC_BASED "__based" @@ -1531,6 +1532,8 @@ gcc_type_attribute: { $$=$1; set($$, ID_constructor); } | TOK_GCC_ATTRIBUTE_DESTRUCTOR { $$=$1; set($$, ID_destructor); } + | 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 7a97b0a7b89..270fe2b8cc3 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1537,6 +1537,9 @@ __decltype { if(PARSER.cpp98 && "destructor" | "__destructor__" { BEGIN(GCC_ATTRIBUTE3); loc(); return TOK_GCC_ATTRIBUTE_DESTRUCTOR; } +"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/util/irep_ids.def b/src/util/irep_ids.def index e5e998633c0..065fa9d201d 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -830,6 +830,8 @@ IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(generic_types, #generic_types) IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) +IREP_ID_ONE(always_inline) +IREP_ID_ONE(is_always_inline) #undef IREP_ID_ONE #undef IREP_ID_TWO