Encapsulate reading and linking multiple files

We do the same work in multiple places, and can optimize the linking process
when knowing about all files to be linked in one step.

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/read_goto_binary.cpp

@@ -271,13 +271,13 @@ bool is_goto_binary(
 /// \param dest: the goto model returned
 /// \param message_handler: for diagnostics
 /// \return true on error, false otherwise
-bool read_object_and_link(
+static bool 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);
@@ -293,36 +293,27 @@ bool read_object_and_link(
     return true;
   }
 
-  // reading successful, let's update config
-  config.set_from_symbol_table(dest.symbol_table);
-
   return false;
 }
 
-/// \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;
 
-  goto_model.symbol_table.swap(dest_symbol_table);
-  goto_model.goto_functions.swap(dest_functions);
+  for(const auto &file_name : file_names)
+  {
+    const bool failed = read_object_and_link(file_name, dest, message_handler);
 
-  bool result=read_object_and_link(
-    file_name,
-    goto_model,
-    message_handler);
+    if(failed)
+      return true;
+  }
 
-  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