Linking: perform macro expansion and type updates just once

This reduces the Linux kernel link time by more than 90% as the previous
approach would repeatedly attempt renamings and replacements across all
hitherto read goto program instructions.

Author: tautschnig

src/goto-programs/link_goto_model.cpp

@@ -58,8 +58,7 @@ 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> &weak_symbols,
-  const replace_symbolt &object_type_updates)
+  const std::unordered_set<irep_idt> &weak_symbols)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
@@ -120,6 +119,51 @@ static bool link_functions(
     }
   }
 
+  return false;
+}
+
+void link_goto_model(
+  goto_modelt &dest,
+  goto_modelt &src,
+  replace_symbolt &object_type_updates,
+  message_handlert &message_handler)
+{
+  std::unordered_set<irep_idt> weak_symbols;
+
+  for(const auto &symbol_pair : dest.symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_weak)
+      weak_symbols.insert(symbol_pair.first);
+  }
+
+  linkingt linking(dest.symbol_table, src.symbol_table, message_handler);
+
+  if(linking.typecheck_main())
+    throw invalid_source_file_exceptiont("typechecking main failed");
+
+  if(link_functions(
+       dest.symbol_table,
+       dest.goto_functions,
+       src.symbol_table,
+       src.goto_functions,
+       linking.rename_symbol,
+       weak_symbols))
+  {
+    throw invalid_source_file_exceptiont("linking failed");
+  }
+
+  object_type_updates.get_expr_map().insert(
+    linking.object_type_updates.get_expr_map().begin(),
+    linking.object_type_updates.get_expr_map().end());
+}
+
+void finalize_linking(
+  goto_modelt &dest,
+  const replace_symbolt &object_type_updates)
+{
+  goto_functionst &dest_functions = dest.goto_functions;
+  symbol_tablet &dest_symbol_table = dest.symbol_table;
+
   // apply macros
   rename_symbolt macro_application;
 
@@ -164,40 +208,4 @@ static bool link_functions(
         });
       }
   }
-
-  return false;
-}
-
-void link_goto_model(
-  goto_modelt &dest,
-  goto_modelt &src,
-  message_handlert &message_handler)
-{
-  std::unordered_set<irep_idt> weak_symbols;
-
-  for(const auto &symbol_pair : dest.symbol_table.symbols)
-  {
-    if(symbol_pair.second.is_weak)
-      weak_symbols.insert(symbol_pair.first);
-  }
-
-  linkingt linking(dest.symbol_table,
-                   src.symbol_table,
-                   message_handler);
-
-  if(linking.typecheck_main())
-  {
-    throw invalid_source_file_exceptiont("typechecking main failed");
-  }
-  if(link_functions(
-       dest.symbol_table,
-       dest.goto_functions,
-       src.symbol_table,
-       src.goto_functions,
-       linking.rename_symbol,
-       weak_symbols,
-       linking.object_type_updates))
-  {
-    throw invalid_source_file_exceptiont("linking failed");
-  }
 }

src/goto-programs/link_goto_model.h

@@ -14,10 +14,16 @@ Author: Daniel Kroening, [email protected]
 
 class goto_modelt;
 class message_handlert;
+class replace_symbolt;
 
 void link_goto_model(
   goto_modelt &dest,
   goto_modelt &src,
+  replace_symbolt &object_type_updates,
   message_handlert &);
 
+void finalize_linking(
+  goto_modelt &dest,
+  const replace_symbolt &object_type_updates);
+
 #endif // CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H

src/goto-programs/read_goto_binary.cpp

@@ -14,11 +14,12 @@ Module: Read Goto Programs
 #include <fstream>
 #include <unordered_set>
 
+#include <util/config.h>
 #include <util/message.h>
-#include <util/unicode.h>
-#include <util/tempfile.h>
 #include <util/rename_symbol.h>
-#include <util/config.h>
+#include <util/replace_symbol.h>
+#include <util/tempfile.h>
+#include <util/unicode.h>
 
 #include "goto_model.h"
 #include "link_goto_model.h"
@@ -265,11 +266,13 @@ bool is_goto_binary(
 /// \brief reads an object file, and also updates config
 /// \param file_name: file name of the goto binary
 /// \param dest: the goto model returned
+/// \param [out] object_type_updates: collects type replacements to be applied
 /// \param message_handler: for diagnostics
 /// \return true on error, false otherwise
 static bool read_object_and_link(
   const std::string &file_name,
   goto_modelt &dest,
+  replace_symbolt &object_type_updates,
   message_handlert &message_handler)
 {
   messaget(message_handler).status()
@@ -282,7 +285,7 @@ static bool read_object_and_link(
 
   try
   {
-    link_goto_model(dest, *temp_model, message_handler);
+    link_goto_model(dest, *temp_model, object_type_updates, message_handler);
   }
   catch(...)
   {
@@ -300,14 +303,19 @@ bool read_objects_and_link(
   if(file_names.empty())
     return false;
 
+  replace_symbolt object_type_updates;
+
   for(const auto &file_name : file_names)
   {
-    const bool failed = read_object_and_link(file_name, dest, message_handler);
+    const bool failed = read_object_and_link(
+      file_name, dest, object_type_updates, message_handler);
 
     if(failed)
       return true;
   }
 
+  finalize_linking(dest, object_type_updates);
+
   // reading successful, let's update config
   config.set_from_symbol_table(dest.symbol_table);