Gcc asm labels and attribute "alias" support

regression/ansi-c/asm3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 other.c
 ^EXIT=0$

regression/cbmc/gcc_attribute_alias1/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+int foo(int a)
+{
+  return a;
+}
+
+// this is a GCC extension
+
+int bar(int b) __attribute__((alias("foo")));
+
+__typeof__(foo) bar2 __attribute__((alias("foo")));
+
+int main()
+{
+  #ifdef __GNUC__
+  assert(bar(42)==42);
+  assert(bar2(42)==42);
+  #endif
+  return 0;
+}

regression/cbmc/gcc_attribute_alias1/test.desc

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

src/ansi-c/ansi_c_convert_type.cpp

@@ -72,10 +72,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     c_qualifiers.is_ptr64=true;
   else if(type.id()==ID_volatile)
     c_qualifiers.is_volatile=true;
-  else if(type.id()==ID_asm)
+  else if(type.id()==ID_asm &&
+          type.has_subtype() &&
+          type.subtype().id()==ID_string_constant)
   {
-    // These are called 'asm labels' by GCC.
-    // ignore for now
+    c_storage_spec.asm_label=type.subtype().get(ID_value);
   }
   else if(type.id()==ID_const)
     c_qualifiers.is_constant=true;
@@ -233,6 +234,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     constructor=true;
   else if(type.id()==ID_destructor)
     destructor=true;
+  else if(type.id()==ID_alias &&
+          type.has_subtype() &&
+          type.subtype().id()==ID_string_constant)
+  {
+    c_storage_spec.alias=type.subtype().get(ID_value);
+  }
   else
     other.push_back(type);
 }

src/ansi-c/c_storage_spec.cpp

@@ -55,4 +55,16 @@ void c_storage_spect::read(const typet &type)
       if(it->id()==ID_thread)
         is_thread_local=true;
   }
+  else if(type.id()==ID_alias &&
+          type.has_subtype() &&
+          type.subtype().id()==ID_string_constant)
+  {
+    alias=type.subtype().get(ID_value);
+  }
+  else if(type.id()==ID_asm &&
+          type.has_subtype() &&
+          type.subtype().id()==ID_string_constant)
+  {
+    asm_label=type.subtype().get(ID_value);
+  }
 }

src/ansi-c/c_storage_spec.h

@@ -34,10 +34,18 @@ class c_storage_spect
     is_register=false;
     is_inline=false;
     is_weak=false;
+    alias.clear();
+    asm_label.clear();
   }
 
   bool is_typedef, is_extern, is_static, is_register,
        is_inline, is_thread_local, is_weak;
+
+  // __attribute__((alias("foo")))
+  irep_idt alias;
+
+  // GCC asm labels __asm__("foo") - these change the symbol name
+  irep_idt asm_label;
 
   friend bool operator == (
     const c_storage_spect &a,
@@ -49,7 +57,9 @@ class c_storage_spect
            a.is_register==b.is_register &&
            a.is_thread_local==b.is_thread_local &&
            a.is_inline==b.is_inline &&
-           a.is_weak==b.is_weak;
+           a.is_weak==b.is_weak &&
+           a.alias==b.alias &&
+           a.asm_label==b.asm_label;
   }
 
   friend bool operator != (
@@ -70,6 +80,8 @@ class c_storage_spect
     a.is_inline       |=b.is_inline;
     a.is_thread_local |=b.is_thread_local;
     a.is_weak         |=b.is_weak;
+    if(!b.alias.empty()) a.alias=b.alias;
+    if(!b.asm_label.empty()) a.asm_label=b.asm_label;
 
     return a;
   }

src/ansi-c/c_typecheck_base.cpp

@@ -193,7 +193,8 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
 
   if(symbol.type.id()==ID_code)
   {
-    if(symbol.value.is_not_nil())
+    if(symbol.value.is_not_nil() &&
+       !symbol.is_macro)
       typecheck_function_body(symbol);
     else
     {
@@ -359,7 +360,8 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
   }
 
   // do initializer, this may change the type
-  if(follow(new_symbol.type).id()!=ID_code)
+  if(follow(new_symbol.type).id()!=ID_code &&
+     !new_symbol.is_macro)
     do_initializer(new_symbol);
 
   const typet &final_new=follow(new_symbol.type);
@@ -462,7 +464,10 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
         old_symbol.is_weak=true;
       }
 
-      typecheck_function_body(new_symbol);
+      if(new_symbol.is_macro)
+        old_symbol.is_macro=true;
+      else
+        typecheck_function_body(new_symbol);
 
       // overwrite location
       old_symbol.location=new_symbol.location;
@@ -590,6 +595,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
     {
       old_symbol.value=new_symbol.value;
       old_symbol.type=new_symbol.type;
+      old_symbol.is_macro=new_symbol.is_macro;
     }
   }
 
@@ -688,6 +694,89 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
 
 /*******************************************************************\
 
+Function: c_typecheck_baset::apply_asm_label
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void c_typecheck_baset::apply_asm_label(
+  const irep_idt &asm_label,
+  symbolt &symbol)
+{
+  const irep_idt orig_name=symbol.name;
+
+  // restrict renaming to functions and global variables;
+  // procedure-local ones would require fixing the scope, as we
+  // do for parameters below
+  if(!asm_label.empty() &&
+     !symbol.is_type &&
+     (symbol.type.id()==ID_code || symbol.is_static_lifetime))
+  {
+    symbol.name=asm_label;
+    symbol.base_name=asm_label;
+  }
+
+  if(symbol.name!=orig_name)
+  {
+    if(!asm_label_map.insert(
+        std::make_pair(orig_name, asm_label)).second)
+    {
+      err_location(symbol.location);
+      if(asm_label_map[orig_name]==asm_label)
+      {
+        str << "duplicate (consistent) asm renaming";
+        warning_msg();
+      }
+      else
+      {
+        str << "error: conflicting asm renaming";
+        throw 0;
+      }
+    }
+  }
+  else if(asm_label.empty())
+  {
+    asm_label_mapt::const_iterator entry=
+      asm_label_map.find(symbol.name);
+    if(entry!=asm_label_map.end())
+    {
+      symbol.name=entry->second;
+      symbol.base_name=entry->second;
+    }
+  }
+
+  if(symbol.name!=orig_name &&
+     symbol.type.id()==ID_code &&
+     symbol.value.is_not_nil() && !symbol.is_macro)
+  {
+    const code_typet &code_type=to_code_type(symbol.type);
+
+    for(code_typet::parameterst::const_iterator
+        p_it=code_type.parameters().begin();
+        p_it!=code_type.parameters().end();
+        ++p_it)
+    {
+      const irep_idt &p_bn=p_it->get_base_name();
+      if(p_bn.empty())
+        continue;
+
+      irep_idt p_id=id2string(orig_name)+"::"+id2string(p_bn);
+      irep_idt p_new_id=id2string(symbol.name)+"::"+id2string(p_bn);
+
+      if(!asm_label_map.insert(
+          std::make_pair(p_id, p_new_id)).second)
+        assert(asm_label_map[p_id]==p_new_id);
+    }
+  }
+}
+
+/*******************************************************************\
+
 Function: c_typecheck_baset::typecheck_declaration
 
   Inputs:
@@ -749,11 +838,24 @@ void c_typecheck_baset::typecheck_declaration(
 
       symbolt symbol;
       declaration.to_symbol(*d_it, symbol);
-      irep_idt identifier=symbol.name;
 
       // now check other half of type
       typecheck_type(symbol.type);
 
+      if(!full_spec.alias.empty())
+      {
+        if(symbol.value.is_not_nil())
+          throw "alias attribute cannot be used with a body";
+
+        // alias function need not have been declared yet, thus
+        // can't lookup
+        symbol.value=symbol_exprt(full_spec.alias);
+        symbol.is_macro=true;
+      }
+
+      apply_asm_label(full_spec.asm_label, symbol);
+      irep_idt identifier=symbol.name;
+
       typecheck_symbol(symbol);
 
       // add code contract (if any); we typecheck this after the

src/ansi-c/c_typecheck_base.h

@@ -283,6 +283,11 @@ class c_typecheck_baset:
            src.id()==ID_c_enum_tag ||
            src.id()==ID_c_bit_field;
   }
+
+  typedef hash_map_cont<irep_idt, irep_idt, irep_id_hash> asm_label_mapt;
+  asm_label_mapt asm_label_map;
+
+  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
 };
 
 #endif

src/ansi-c/c_typecheck_expr.cpp

@@ -789,7 +789,7 @@ Function: c_typecheck_baset::typecheck_expr_symbol
 
 void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
 {
-  const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
+  irep_idt identifier=to_symbol_expr(expr).get_identifier();
 
   // Is it a parameter? We do this while checking parameter lists.
   id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
@@ -801,6 +801,15 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
     return;
   }
 
+  // renaming via GCC asm label
+  asm_label_mapt::const_iterator entry=
+    asm_label_map.find(identifier);
+  if(entry!=asm_label_map.end())
+  {
+    identifier=entry->second;
+    to_symbol_expr(expr).set_identifier(identifier);
+  }
+
   // look it up
   const symbolt *symbol_ptr;
   if(lookup(identifier, symbol_ptr))
@@ -828,11 +837,13 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
     // preserve enum key
     irep_idt base_name=expr.get(ID_C_base_name);
 
-    expr=symbol.value;
+    follow_macros(expr);
 
     if(expr.id()==ID_constant &&
        !base_name.empty())
       expr.set(ID_C_cformat, base_name);
+    else
+      typecheck_expr(expr);
 
     // preserve location
     expr.add_source_location()=source_location;
@@ -2143,8 +2154,12 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
   if(f_op.id()==ID_symbol)
   {
-    const irep_idt &identifier=
-      to_symbol_expr(f_op).get_identifier();
+    irep_idt identifier=to_symbol_expr(f_op).get_identifier();
+
+    asm_label_mapt::const_iterator entry=
+      asm_label_map.find(identifier);
+    if(entry!=asm_label_map.end())
+      identifier=entry->second;
 
     if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
     {