Revert "Fully interpret __attribute__((always_inline))"

This partly reverts commit 9c93f59. The regression test stays in place, but is now marked as KNOWNBUG.
NathanJPhillips · Jul 7, 2018 · 016ad92 · 016ad92
1 parent d20a12e
commit 016ad92
Show file tree

Hide file tree

Showing 11 changed files with 4 additions and 123 deletions.
diff --git a/regression/ansi-c/always_inline1/test.desc b/regression/ansi-c/always_inline1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$

diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
@@ -171,8 +171,6 @@ 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
@@ -81,8 +81,6 @@ 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";
@@ -166,9 +164,6 @@ 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
@@ -205,16 +205,6 @@ 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
@@ -34,8 +34,6 @@ 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
@@ -36,14 +36,13 @@ 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, is_always_inline;
+  bool is_typedef, is_extern, is_static, is_register,
+       is_inline, is_thread_local, is_weak, is_used;
 
   // __attribute__((alias("foo")))
   irep_idt alias;
@@ -54,7 +53,6 @@ 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 &&
@@ -63,11 +61,9 @@ 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
@@ -85,7 +81,6 @@ 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
@@ -689,7 +689,6 @@ 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
@@ -18,11 +18,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
-#include <util/expr_util.h>
 #include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
@@ -1920,10 +1918,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     if(entry!=asm_label_map.end())
       identifier=entry->second;
 
-    symbol_tablet::symbolst::const_iterator sym_entry =
-      symbol_table.symbols.find(identifier);
-
-    if(sym_entry == symbol_table.symbols.end())
+    if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
     {
       // This is an undeclared function.
       // Is this a builtin?
@@ -1965,87 +1960,6 @@ 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

diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
@@ -150,7 +150,6 @@ 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"
@@ -1548,8 +1547,6 @@ 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
@@ -1590,9 +1590,6 @@ __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/util/irep_ids.def b/src/util/irep_ids.def
@@ -673,8 +673,6 @@ 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)
 IREP_ID_ONE(is_inner_class)
 
 // Projects depending on this code base that wish to extend the list of