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

@@ -17,7 +17,6 @@ Author: Michael Tautschnig, Daniel Kroening
 #include <util/rename_symbol.h>
 
 #include <linking/linking_class.h>
-#include <util/exception_utils.h>
 
 #include "goto_model.h"
 
@@ -54,8 +53,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);
@@ -109,6 +107,58 @@ static bool link_functions(
     }
   }
 
+  return false;
+}
+
+optionalt<replace_symbolt::expr_mapt> 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())
+  {
+    messaget log{message_handler};
+    log.error() << "typechecking main failed" << messaget::eom;
+    return {};
+  }
+
+  if(link_functions(
+       dest.symbol_table,
+       dest.goto_functions,
+       src.symbol_table,
+       src.goto_functions,
+       linking.rename_symbol,
+       weak_symbols))
+  {
+    messaget log{message_handler};
+    log.error() << "linking failed" << messaget::eom;
+    return {};
+  }
+
+  return linking.object_type_updates.get_expr_map();
+}
+
+void finalize_linking(
+  goto_modelt &dest,
+  const replace_symbolt::expr_mapt &type_updates)
+{
+  unchecked_replace_symbolt object_type_updates;
+  object_type_updates.get_expr_map().insert(
+    type_updates.begin(), type_updates.end());
+
+  goto_functionst &dest_functions = dest.goto_functions;
+  symbol_tablet &dest_symbol_table = dest.symbol_table;
+
   // apply macros
   rename_symbolt macro_application;
 
@@ -157,40 +207,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

@@ -12,12 +12,24 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 
+#include <util/nodiscard.h>
+#include <util/replace_symbol.h>
+
 class goto_modelt;
 class message_handlert;
 
-void link_goto_model(
+/// Link goto model \p src into goto model \p dest, invalidating \p src in this
+/// process. Linking may require updates to object types contained in \p dest,
+/// which need to be applied using \ref finalize_linking.
+/// \return nullopt if linking fails, else a (possibly empty) collection of
+///   replacements to be applied.
+NODISCARD optionalt<replace_symbolt::expr_mapt>
+link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
+
+/// Apply \p type_updates to \p dest, where \p type_updates were constructed
+/// from one or more calls to \p link_goto_model.
+void finalize_linking(
   goto_modelt &dest,
-  goto_modelt &src,
-  message_handlert &);
+  const replace_symbolt::expr_mapt &type_updates);
 
 #endif // CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H

src/goto-programs/read_goto_binary.cpp

@@ -15,6 +15,7 @@ Module: Read Goto Programs
 
 #include <util/config.h>
 #include <util/message.h>
+#include <util/replace_symbol.h>
 #include <util/tempfile.h>
 
 #ifdef _MSC_VER
@@ -270,8 +271,8 @@ bool is_goto_binary(
 /// \param file_name: file name of the goto binary
 /// \param dest: the goto model returned
 /// \param message_handler: for diagnostics
-/// \return true on error, false otherwise
-static bool read_object_and_link(
+/// \return nullopt on error, type replacements to be applied otherwise
+static optionalt<replace_symbolt::expr_mapt> read_object_and_link(
   const std::string &file_name,
   goto_modelt &dest,
   message_handlert &message_handler)
@@ -282,18 +283,9 @@ static bool read_object_and_link(
   // we read into a temporary model
   auto temp_model = read_goto_binary(file_name, message_handler);
   if(!temp_model.has_value())
-    return true;
-
-  try
-  {
-    link_goto_model(dest, *temp_model, message_handler);
-  }
-  catch(...)
-  {
-    return true;
-  }
+    return {};
 
-  return false;
+  return link_goto_model(dest, std::move(*temp_model), message_handler);
 }
 
 bool read_objects_and_link(
@@ -304,14 +296,19 @@ bool read_objects_and_link(
   if(file_names.empty())
     return false;
 
+  replace_symbolt::expr_mapt object_type_updates;
+
   for(const auto &file_name : file_names)
   {
-    const bool failed = read_object_and_link(file_name, dest, message_handler);
-
-    if(failed)
+    auto updates_opt = read_object_and_link(file_name, dest, message_handler);
+    if(!updates_opt.has_value())
       return true;
+
+    object_type_updates.insert(updates_opt->begin(), updates_opt->end());
   }
 
+  finalize_linking(dest, object_type_updates);
+
   // reading successful, let's update config
   config.set_from_symbol_table(dest.symbol_table);