diff --git a/regression/cbmc/constructor_priority/main.c b/regression/cbmc/constructor_priority/main.c new file mode 100644 index 00000000000..9589d8988ac --- /dev/null +++ b/regression/cbmc/constructor_priority/main.c @@ -0,0 +1,51 @@ +#include + +#ifdef __GNUC__ +int x = 0, y = 0, w = 0; + +// Constructor with priority argument; name chosen to make sure lexicographic +// ordering does not incidentally produce the correct sequence. +__attribute__((constructor(101))) void z_init_priority(void) +{ + x = 1; +} + +// Constructor with priority argument +__attribute__((constructor(102))) void y_init_priority2(void) +{ + assert(x == 1); + x = 2; +} + +// Destructor with priority argument +__attribute__((destructor(201))) void fini_priority(void) +{ + assert(w == 4); + y = 2; +} + +// Constructor without priority (should still work, have lowest priority) +__attribute__((constructor)) void x_init_no_priority(void) +{ + assert(x == 2); + x = 3; +} + +// Destructor without priority (should still work, has highest priority) +__attribute__((destructor)) void fini_no_priority(void) +{ + w = 4; +} +#endif + +int main() +{ +#ifdef __GNUC__ + // All constructors should have run before main + assert(x == 3); + // Destructors haven't run yet + assert(y == 0); + assert(w == 0); +#endif + return 0; +} diff --git a/regression/cbmc/constructor_priority/test.desc b/regression/cbmc/constructor_priority/test.desc new file mode 100644 index 00000000000..fb1d02cbb6c --- /dev/null +++ b/regression/cbmc/constructor_priority/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring \ No newline at end of file diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index c7ed6453c90..0abe7b2111f 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -228,9 +228,23 @@ void ansi_c_convert_typet::read_rec(const typet &type) else if(type.id()==ID_noreturn) c_qualifiers.is_noreturn=true; else if(type.id()==ID_constructor) + { constructor=true; + + // may come with priority + const irept &priority_opt = type.find(ID_constructor_priority); + if(priority_opt.is_not_nil()) + constructor_priority = static_cast(priority_opt); + } else if(type.id()==ID_destructor) + { destructor=true; + + // may come with priority + const irept &priority_opt = type.find(ID_destructor_priority); + if(priority_opt.is_not_nil()) + destructor_priority = static_cast(priority_opt); + } else if( type.id() == ID_alias && type.has_subtype() && to_type_with_subtype(type).subtype().id() == ID_string_constant) @@ -363,7 +377,18 @@ void ansi_c_convert_typet::write(typet &type) throw 0; } - type_p->id(constructor ? ID_constructor : ID_destructor); + if(constructor) + { + type_p->id(ID_constructor); + if(constructor_priority.is_not_nil()) + type_p->add(ID_constructor_priority, constructor_priority); + } + else + { + type_p->id(ID_destructor); + if(destructor_priority.is_not_nil()) + type_p->add(ID_destructor_priority, destructor_priority); + } } } else if(constructor || destructor) diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 043198d8fb5..6b6204f6104 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -44,6 +44,7 @@ class ansi_c_convert_typet exprt vector_size, alignment, bv_width, fraction_width; exprt msc_based; // this is Visual Studio bool constructor, destructor; + exprt constructor_priority, destructor_priority; // contracts exprt::operandst c_assigns, c_frees, c_ensures, c_requires; @@ -113,6 +114,8 @@ class ansi_c_convert_typet msc_based(nil_exprt{}), constructor(false), destructor(false), + constructor_priority(nil_exprt{}), + destructor_priority(nil_exprt{}), message_handler(_message_handler) { } diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index f3c18659880..395edca769b 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -511,7 +511,10 @@ bool generate_ansi_c_start_function( record_function_outputs(symbol, init_code, symbol_table); - // now call destructor functions (a GCC extension) + // now call destructor functions (a GCC extension); compute required order + // first + std::map>> + destructors_by_priority; for(const auto &symbol_table_entry : symbol_table.symbols) { @@ -525,8 +528,39 @@ bool generate_ansi_c_start_function( code_type.return_type().id() == ID_destructor && code_type.parameters().empty()) { - code_function_callt destructor_call(symbol.symbol_expr()); - destructor_call.add_source_location() = symbol.location; + const exprt &priority = static_cast( + code_type.return_type().find(ID_destructor_priority)); + if(priority.is_nil()) + destructors_by_priority[1].push_back(symbol); + else + { + std::optional priority_int_opt = + numeric_cast(priority); + DATA_INVARIANT( + priority_int_opt.has_value() && *priority_int_opt >= 0, + "destructor priority expected to be non-negative integer"); + destructors_by_priority[-*priority_int_opt].push_back(symbol); + } + } + } + + // append all destructors with priority "default" to the otherwise + // lowest-priority destructor list + if( + destructors_by_priority.size() > 1 && + std::prev(destructors_by_priority.end())->first == 1) + { + auto &dest_list = destructors_by_priority.begin()->second; + dest_list.splice( + dest_list.begin(), std::prev(destructors_by_priority.end())->second); + } + + for(const auto &priority_pair : destructors_by_priority) + { + for(const auto &sym_ref : priority_pair.second) + { + code_function_callt destructor_call{sym_ref.get().symbol_expr()}; + destructor_call.add_source_location() = sym_ref.get().location; init_code.add(std::move(destructor_call)); } } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 91526b2b8e6..e721d1ff1e5 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -1699,8 +1699,20 @@ gcc_type_attribute: { $$=$1; set($$, ID_noreturn); } | TOK_GCC_ATTRIBUTE_CONSTRUCTOR { $$=$1; set($$, ID_constructor); } + | TOK_GCC_ATTRIBUTE_CONSTRUCTOR '(' TOK_INTEGER ')' + { + $$=$1; + set($$, ID_constructor); + parser_stack($$).set(ID_constructor_priority, parser_stack($3)); + } | TOK_GCC_ATTRIBUTE_DESTRUCTOR { $$=$1; set($$, ID_destructor); } + | TOK_GCC_ATTRIBUTE_DESTRUCTOR '(' TOK_INTEGER ')' + { + $$=$1; + set($$, ID_destructor); + parser_stack($$).set(ID_destructor_priority, parser_stack($3)); + } | TOK_GCC_ATTRIBUTE_USED { $$=$1; set($$, ID_used); } ; diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 336c848d7dd..9a1401726ae 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -142,7 +142,10 @@ void static_lifetime_init( dest.add(std::move(*code)); } - // now call designated "initialization" functions + // now call designated "initialization" functions; compute required order + // first + std::map>> + constructors_by_priority; for(const std::string &id : symbols) { @@ -156,8 +159,42 @@ void static_lifetime_init( code_type.return_type().id() == ID_constructor && code_type.parameters().empty()) { + const exprt &priority = static_cast( + code_type.return_type().find(ID_constructor_priority)); + if(priority.is_nil()) + constructors_by_priority[-1].push_back(symbol); + else + { + std::optional priority_int_opt = + numeric_cast(priority); + DATA_INVARIANT( + priority_int_opt.has_value() && *priority_int_opt >= 0, + "constructor priority expected to be non-negative integer"); + constructors_by_priority[*priority_int_opt].push_back(symbol); + } + } + } + + // append all constructors with priority "default" to the otherwise + // lowest-priority constructor list + if( + constructors_by_priority.size() > 1 && + constructors_by_priority.begin()->first == -1) + { + auto &dest_list = std::prev(constructors_by_priority.end())->second; + dest_list.splice(dest_list.end(), constructors_by_priority.begin()->second); + } + + for(const auto &priority_pair : constructors_by_priority) + { + for(const auto &sym_ref : priority_pair.second) + { + const code_typet &code_type = to_code_type(sym_ref.get().type); dest.add(code_expressiont{side_effect_expr_function_callt{ - symbol.symbol_expr(), {}, code_type.return_type(), source_location}}); + sym_ref.get().symbol_expr(), + {}, + code_type.return_type(), + source_location}}); } } } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 840741057dd..8dd7aa38517 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -422,6 +422,8 @@ IREP_ID_ONE(methods) IREP_ID_ONE(static_members) IREP_ID_ONE(constructor) IREP_ID_ONE(destructor) +IREP_ID_ONE(constructor_priority) +IREP_ID_ONE(destructor_priority) IREP_ID_ONE(bases) IREP_ID_ONE(base) IREP_ID_ONE(from_base)