C front-end: support constructor/destructor attribute with priority argument

regression/cbmc/constructor_priority/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+
+#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;
+}

regression/cbmc/constructor_priority/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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<const exprt &>(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<const exprt &>(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)

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)
   {
   }

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<mp_integer, std::list<std::reference_wrapper<const symbolt>>>
+    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<const exprt &>(
+        code_type.return_type().find(ID_destructor_priority));
+      if(priority.is_nil())
+        destructors_by_priority[1].push_back(symbol);
+      else
+      {
+        std::optional<mp_integer> priority_int_opt =
+          numeric_cast<mp_integer>(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));
     }
   }

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); }
         ;

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<mp_integer, std::list<std::reference_wrapper<const symbolt>>>
+    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<const exprt &>(
+        code_type.return_type().find(ID_constructor_priority));
+      if(priority.is_nil())
+        constructors_by_priority[-1].push_back(symbol);
+      else
+      {
+        std::optional<mp_integer> priority_int_opt =
+          numeric_cast<mp_integer>(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}});
     }
   }
 }

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)