Merge pull request #2254 from tautschnig/linear-linking

Linking: perform macro expansion and type updates just once

Author: tautschnig

jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -126,9 +126,7 @@ void lazy_goto_modelt::initialize(
       "language");
   }
 
-  std::vector<std::string> binaries, sources;
-  binaries.reserve(files.size());
-  sources.reserve(files.size());
+  std::list<std::string> binaries, sources;
 
   for(const auto &file : files)
   {
@@ -211,18 +209,8 @@ void lazy_goto_modelt::initialize(
     }
   }
 
-  for(const std::string &file : binaries)
-  {
-    msg.status() << "Reading GOTO program from file" << messaget::eom;
-
-    if(read_object_and_link(file, *goto_model, message_handler))
-    {
-      source_locationt source_location;
-      source_location.set_file(file);
-      throw incorrect_goto_program_exceptiont(
-        "failed to read/link goto model", source_location);
-    }
-  }
+  if(read_objects_and_link(binaries, *goto_model, message_handler))
+    throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};
 
   bool binaries_provided_start =
     symbol_table.has_symbol(goto_functionst::entry_point());

regression/goto-gcc/archives/test.desc

@@ -3,7 +3,7 @@ CORE
 main.c -L. -lour_archive --verbosity
 ^EXIT=0$
 ^SIGNAL=0$
-^Reading: .*/foo.o$
+^Reading GOTO program from file .*/foo.o$
 --
 ^warning: ignoring
 ^CONVERSION ERROR$

src/goto-cc/compile.cpp

@@ -322,11 +322,8 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
   convert_symbols(goto_model);
 
   // parse object files
-  for(const auto &file_name : object_files)
-  {
-    if(read_object_and_link(file_name, goto_model, log.get_message_handler()))
-      return true;
-  }
+  if(read_objects_and_link(object_files, goto_model, log.get_message_handler()))
+    return true;
 
   // produce entry point?
 

src/goto-programs/initialize_goto_model.cpp

@@ -71,9 +71,7 @@ goto_modelt initialize_goto_model(
       "one or more paths to program files");
   }
 
-  std::vector<std::string> binaries, sources;
-  binaries.reserve(files.size());
-  sources.reserve(files.size());
+  std::list<std::string> binaries, sources;
 
   for(const auto &file : files)
   {
@@ -135,15 +133,10 @@ goto_modelt initialize_goto_model(
     }
   }
 
-  for(const auto &file : binaries)
+  if(read_objects_and_link(binaries, goto_model, message_handler))
   {
-    msg.status() << "Reading GOTO program from file" << messaget::eom;
-
-    if(read_object_and_link(file, goto_model, message_handler))
-    {
-      throw invalid_source_file_exceptiont(
-        "failed to read object or link in file '" + file + '\'');
-    }
+    throw invalid_source_file_exceptiont{
+      "failed to read object or link in files"};
   }
 
   bool binaries_provided_start=

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,59 +271,46 @@ 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
-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)
 {
-  messaget(message_handler).statistics() << "Reading: "
-                                         << file_name << messaget::eom;
+  messaget(message_handler).status()
+    << "Reading GOTO program from file " << file_name << messaget::eom;
 
   // 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;
-  }
-
-  // reading successful, let's update config
-  config.set_from_symbol_table(dest.symbol_table);
+    return {};
 
-  return false;
+  return link_goto_model(dest, std::move(*temp_model), message_handler);
 }
 
-/// \brief reads an object file, and also updates the config
-/// \param file_name: file name of the goto binary
-/// \param dest_symbol_table: symbol table to update
-/// \param dest_functions: collection of goto functions to update
-/// \param message_handler: for diagnostics
-/// \return true on error, false otherwise
-bool read_object_and_link(
-  const std::string &file_name,
-  symbol_tablet &dest_symbol_table,
-  goto_functionst &dest_functions,
+bool read_objects_and_link(
+  const std::list<std::string> &file_names,
+  goto_modelt &dest,
   message_handlert &message_handler)
 {
-  goto_modelt goto_model;
+  if(file_names.empty())
+    return false;
+
+  replace_symbolt::expr_mapt object_type_updates;
 
-  goto_model.symbol_table.swap(dest_symbol_table);
-  goto_model.goto_functions.swap(dest_functions);
+  for(const auto &file_name : file_names)
+  {
+    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());
+  }
 
-  bool result=read_object_and_link(
-    file_name,
-    goto_model,
-    message_handler);
+  finalize_linking(dest, object_type_updates);
 
-  goto_model.symbol_table.swap(dest_symbol_table);
-  goto_model.goto_functions.swap(dest_functions);
+  // reading successful, let's update config
+  config.set_from_symbol_table(dest.symbol_table);
 
-  return result;
+  return false;
 }

src/goto-programs/read_goto_binary.h

@@ -12,29 +12,27 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
 #define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H
 
+#include <list>
 #include <string>
 
 #include <util/optional.h>
 
-class goto_functionst;
 class goto_modelt;
 class message_handlert;
-class symbol_tablet;
 
 optionalt<goto_modelt>
 read_goto_binary(const std::string &filename, message_handlert &);
 
 bool is_goto_binary(const std::string &filename, message_handlert &);
 
-bool read_object_and_link(
-  const std::string &file_name,
-  symbol_tablet &,
-  goto_functionst &,
-  message_handlert &);
-
-bool read_object_and_link(
-  const std::string &file_name,
-  goto_modelt &,
-  message_handlert &);
+/// Reads object files and updates the config if any files were read.
+/// \param file_names: file names of goto binaries; if empty, just returns false
+/// \param dest: goto model to update
+/// \param message_handler: for diagnostics
+/// \return True on error, false otherwise
+bool read_objects_and_link(
+  const std::list<std::string> &file_names,
+  goto_modelt &dest,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H

src/symtab2gb/module_dependencies.txt

@@ -3,3 +3,4 @@ json-symtab-language
 langapi
 goto-programs
 ansi-c
+linking