Merge pull request #49 from tautschnig/weak-symbols

Linking and type checking for weak symbols

Author: Daniel Kroening

src/ansi-c/c_storage_spec.cpp

@@ -24,7 +24,8 @@ Function: c_storage_spect::read
 
 void c_storage_spect::read(const typet &type)
 {
-  if(type.id()==ID_merged_type)
+  if(type.id()==ID_merged_type ||
+     type.id()==ID_code)
   {
     forall_subtypes(it, type)
       read(*it);

src/ansi-c/c_typecheck_base.cpp

@@ -711,13 +711,6 @@ void c_typecheck_baset::typecheck_declaration(
   {
     // get storage spec
     c_storage_spect c_storage_spec(declaration.type());
-  
-    declaration.set_is_inline(c_storage_spec.is_inline);
-    declaration.set_is_static(c_storage_spec.is_static);
-    declaration.set_is_extern(c_storage_spec.is_extern);
-    declaration.set_is_thread_local(c_storage_spec.is_thread_local);
-    declaration.set_is_register(c_storage_spec.is_register);
-    declaration.set_is_typedef(c_storage_spec.is_typedef);
 
     // first typecheck the type of the declaration
     typecheck_type(declaration.type());
@@ -743,6 +736,17 @@ void c_typecheck_baset::typecheck_declaration(
         d_it!=declaration.declarators().end();
         d_it++)
     {
+      c_storage_spect full_spec(declaration.full_type(*d_it));
+      full_spec|=c_storage_spec;
+
+      declaration.set_is_inline(full_spec.is_inline);
+      declaration.set_is_static(full_spec.is_static);
+      declaration.set_is_extern(full_spec.is_extern);
+      declaration.set_is_thread_local(full_spec.is_thread_local);
+      declaration.set_is_register(full_spec.is_register);
+      declaration.set_is_typedef(full_spec.is_typedef);
+      declaration.set_is_weak(full_spec.is_weak);
+
       symbolt symbol;
       declaration.to_symbol(*d_it, symbol);
       irep_idt identifier=symbol.name;

src/goto-programs/read_goto_binary.cpp

@@ -281,11 +281,13 @@ Function: link_functions
 static bool link_functions(
   symbol_tablet &dest_symbol_table,
   goto_functionst &dest_functions,
-  symbol_tablet &src_symbol_table,
+  const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
-  const rename_symbolt &rename_symbol)
+  const rename_symbolt &rename_symbol,
+  const hash_set_cont<irep_idt, irep_id_hash> &weak_symbols)
 {
   namespacet ns(dest_symbol_table);
+  namespacet src_ns(src_symbol_table);
 
   // merge functions
   Forall_goto_functions(src_it, src_functions)
@@ -320,15 +322,17 @@ static bool link_functions(
 
       goto_functionst::goto_functiont &src_func=src_it->second;
 
-      if(in_dest_symbol_table.body.instructions.empty())
+      if(in_dest_symbol_table.body.instructions.empty() ||
+         weak_symbols.find(final_id)!=weak_symbols.end())
       {
         // the one with body wins!
         rename_symbols_in_function(src_func, rename_symbol);
 
         in_dest_symbol_table.body.swap(src_func.body);
         in_dest_symbol_table.type=src_func.type;
       }
-      else if(src_func.body.instructions.empty())
+      else if(src_func.body.instructions.empty() ||
+              src_ns.lookup(src_it->first).is_weak)
       {
         // just keep the old one in dest
       }
@@ -377,6 +381,12 @@ bool read_object_and_link(
       message_handler))
     return true;
 
+  typedef hash_set_cont<irep_idt, irep_id_hash> id_sett;
+  id_sett weak_symbols;
+  forall_symbols(it, symbol_table.symbols)
+    if(it->second.is_weak)
+      weak_symbols.insert(it->first);
+
   linkingt linking(symbol_table,
                    temp_model.symbol_table,
                    message_handler);
@@ -386,7 +396,7 @@ bool read_object_and_link(
 
   if(link_functions(symbol_table, functions,
                     temp_model.symbol_table, temp_model.goto_functions,
-                    linking.rename_symbol))
+                    linking.rename_symbol, weak_symbols))
     return true;
 
   return false;

src/linking/linking.cpp

@@ -576,6 +576,7 @@ void linkingt::duplicate_code_symbol(
 
       old_symbol.type=new_symbol.type;
       old_symbol.location=new_symbol.location;
+      old_symbol.is_weak=new_symbol.is_weak;
     }
     else if(!new_symbol.location.get_function().empty() &&
             new_symbol.value.is_nil())
@@ -595,6 +596,31 @@ void linkingt::duplicate_code_symbol(
       {
         old_symbol.type=new_symbol.type;
         old_symbol.location=new_symbol.location;
+        old_symbol.is_weak=new_symbol.is_weak;
+      }
+    }
+    // replace weak symbols
+    else if(old_symbol.is_weak)
+    {
+      if(new_symbol.value.is_nil())
+        link_warning(
+          old_symbol,
+          new_symbol,
+          "function declaration conflicts with with weak definition");
+      else
+        old_symbol.value.make_nil();
+    }
+    else if(new_symbol.is_weak)
+    {
+      if(new_symbol.value.is_nil() ||
+         old_symbol.value.is_not_nil())
+      {
+        new_symbol.value.make_nil();
+
+        link_warning(
+          old_symbol,
+          new_symbol,
+          "ignoring conflicting weak function declaration");
       }
     }
     // Linux kernel uses void f(void) as generic prototype
@@ -782,6 +808,7 @@ void linkingt::duplicate_code_symbol(
       rename_symbol(new_symbol.type);
       old_symbol.value=new_symbol.value;
       old_symbol.type=new_symbol.type; // for parameter identifiers
+      old_symbol.is_weak=new_symbol.is_weak;
     }
     else if(to_code_type(old_symbol.type).get_inlined())
     {
@@ -905,12 +932,13 @@ void linkingt::duplicate_object_symbol(
      !new_symbol.value.get_bool(ID_C_zero_initializer))
   {
     if(old_symbol.value.is_nil() ||
-       old_symbol.value.get_bool(ID_C_zero_initializer))
+       old_symbol.value.get_bool(ID_C_zero_initializer) ||
+       old_symbol.is_weak)
     {
       // new_symbol wins
       old_symbol.value=new_symbol.value;
     }
-    else
+    else if(!new_symbol.is_weak)
     {
       // try simplifier
       exprt tmp_old=old_symbol.value,