Update initializer and expression types after linking

Non-symbol types may have been updated during linking; those updates had not
been propagated to initializers or goto programs.

Author: tautschnig

regression/cbmc/Linking6/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+void set();
+
+char buffer[10];
+
+void init() {
+  int i;
+  for (i = 0; i < 10; i++) {buffer[i] = 0;}
+}
+
+void print() {
+  printf("buffer = %s\n",buffer);
+}
+
+void main () {
+  init();
+  set();
+  print();
+}
+
+
+

regression/cbmc/Linking6/module.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+extern char buffer[];
+
+static size_t _debug_tempBufferHead = ((size_t)(&buffer));
+
+void set() {
+  *(char *)_debug_tempBufferHead = 'a';
+}

regression/cbmc/Linking6/test.desc

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

src/ansi-c/c_typecheck_base.cpp

@@ -210,27 +210,6 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
   }
   else
   {
-    if(symbol.type.id()==ID_array &&
-       to_array_type(symbol.type).size().is_nil() &&
-       !symbol.is_type)
-    {
-      // Insert a new type symbol for the array.
-      // We do this because we want a convenient way
-      // of adjusting the size of the type later on.
-
-      type_symbolt new_symbol(symbol.type);
-      new_symbol.name=id2string(symbol.name)+"$type";
-      new_symbol.base_name=id2string(symbol.base_name)+"$type";
-      new_symbol.location=symbol.location;
-      new_symbol.mode=symbol.mode;
-      new_symbol.module=symbol.module;
-
-      symbol.type=symbol_typet(new_symbol.name);
-
-      symbolt *new_sp;
-      symbol_table.move(new_symbol, new_sp);
-    }
-
     // check the initializer
     do_initializer(symbol);
   }

src/goto-programs/read_goto_binary.cpp

@@ -289,7 +289,8 @@ static bool link_functions(
   const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
   const rename_symbolt &rename_symbol,
-  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols)
+  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols,
+  const replace_symbolt &object_type_updates)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
@@ -381,6 +382,16 @@ static bool link_functions(
     Forall_goto_functions(dest_it, dest_functions)
       rename_symbols_in_function(dest_it->second, macro_application);
 
+  if(!object_type_updates.expr_map.empty())
+  {
+    Forall_goto_functions(dest_it, dest_functions)
+      Forall_goto_program_instructions(iit, dest_it->second.body)
+      {
+        object_type_updates(iit->code);
+        object_type_updates(iit->guard);
+      }
+  }
+
   return false;
 }
 
@@ -427,9 +438,14 @@ bool read_object_and_link(
   if(linking.typecheck_main())
     return true;
 
-  if(link_functions(symbol_table, functions,
-                    temp_model.symbol_table, temp_model.goto_functions,
-                    linking.rename_symbol, weak_symbols))
+  if(link_functions(
+      symbol_table,
+      functions,
+      temp_model.symbol_table,
+      temp_model.goto_functions,
+      linking.rename_symbol,
+      weak_symbols,
+      linking.object_type_updates))
     return true;
 
   return false;

src/linking/linking.cpp

@@ -1100,6 +1100,8 @@ void linkingt::duplicate_object_symbol(
     }
     else if(set_to_new)
       old_symbol.type=new_symbol.type;
+
+    object_type_updates.insert(old_symbol.name, old_symbol.symbol_expr());
   }
 
   // care about initializers
@@ -1508,6 +1510,15 @@ void linkingt::copy_symbols()
     else
       duplicate_non_type_symbol(old_symbol, new_symbol);
   }
+
+  // Apply type updates to initializers
+  Forall_symbols(s_it, main_symbol_table.symbols)
+  {
+    if(!s_it->second.is_type &&
+       !s_it->second.is_macro &&
+       s_it->second.value.is_not_nil())
+      object_type_updates(s_it->second.value);
+  }
 }
 
 /*******************************************************************\

src/linking/linking_class.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/namespace.h>
 #include <util/rename_symbol.h>
+#include <util/replace_symbol.h>
 #include <util/typecheck.h>
 #include <util/std_expr.h>
 
@@ -31,6 +32,7 @@ class linkingt:public typecheckt
   virtual void typecheck();
 
   rename_symbolt rename_symbol;
+  replace_symbolt object_type_updates;
 
 protected:
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;