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).

Author: tautschnig

regression/ansi-c/always_inline1/main.c

@@ -0,0 +1,34 @@
+// 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))]));
+}
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  kfree_rcu(42);
+#endif
+
+  return 0;
+}

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.

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

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

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;

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

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;
+  bool is_typedef, is_extern, is_static, is_register, is_inline,
+    is_thread_local, is_weak, is_always_inline;
 
   // __attribute__((alias("foo")))
   irep_idt alias;
@@ -52,16 +53,19 @@ 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 &&
            is_register==other.is_register &&
            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;
+    // clang-format on
   }
 
   bool operator!=(const c_storage_spect &other) const
@@ -78,6 +82,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())

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

src/ansi-c/c_typecheck_expr.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/std_types.h>
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
@@ -25,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/replace_symbol.h>
 
 #include "builtin_factory.h"
 #include "c_typecast.h"
@@ -1912,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.
       // Is this a builtin?
@@ -1954,6 +1959,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 &parameters = 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

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: