Move link_goto_model to read_goto_binary.cpp

This is the only code that uses the functions from
link_goto_model.{h,cpp}, and those functions weren't an easily usable
API anyway as a certain protocol needs to be followed.

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -82,7 +82,7 @@
 warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'goto_model.h' not generated, too many nodes (108), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/goto-programs/Makefile

@@ -30,7 +30,6 @@ SRC = add_malloc_may_fail_variable_initializations.cpp \
       json_expr.cpp \
       json_goto_trace.cpp \
       label_function_pointer_call_sites.cpp \
-      link_goto_model.cpp \
       link_to_library.cpp \
       loop_ids.cpp \
       mm_io.cpp \

src/goto-programs/README.md

@@ -567,15 +567,6 @@ deserialises the passed file into a temporary `::goto_modelt` instance, and
 then it performs 'linking' of the temporary into a passed destination
 `::goto_modelt` instance.
 
-Details about linking of `::goto_modelt` instances can be found
-[here](\ref section-linking-goto-models).
-
-\section section-linking-goto-models Linking Goto Models
-
-C++ modules:
-  - `link_goto_model.h`
-  - `link_goto_model.cpp`
-
 Dependencies:
   - [linking folder](\ref linking).
   - [typecheck](\ref section-goto-typecheck).

src/goto-programs/link_goto_model.cpp

@@ -14,19 +14,212 @@ Module: Read Goto Programs
 #include <fstream>
 #include <unordered_set>
 
+#include <util/base_type.h>
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/message.h>
 #include <util/rename_symbol.h>
 #include <util/replace_symbol.h>
+#include <util/symbol.h>
 #include <util/tempfile.h>
 #include <util/unicode.h>
 
+#include <linking/linking_class.h>
+
 #include "goto_model.h"
-#include "link_goto_model.h"
 #include "read_bin_goto_object.h"
 #include "elf_reader.h"
 #include "osx_fat_reader.h"
 
+static void rename_symbols_in_function(
+  goto_functionst::goto_functiont &function,
+  irep_idt &new_function_name,
+  const rename_symbolt &rename_symbol)
+{
+  for(auto &identifier : function.parameter_identifiers)
+  {
+    auto entry = rename_symbol.expr_map.find(identifier);
+    if(entry != rename_symbol.expr_map.end())
+      identifier = entry->second;
+  }
+
+  goto_programt &program = function.body;
+
+  Forall_goto_program_instructions(iit, program)
+  {
+    rename_symbol(iit->code);
+
+    if(iit->has_condition())
+    {
+      exprt c = iit->get_condition();
+      rename_symbol(c);
+      iit->set_condition(c);
+    }
+  }
+}
+
+/// Link a set of goto functions, considering weak symbols
+/// and symbol renaming
+static bool link_functions(
+  symbol_tablet &dest_symbol_table,
+  goto_functionst &dest_functions,
+  const symbol_tablet &src_symbol_table,
+  goto_functionst &src_functions,
+  const rename_symbolt &rename_symbol,
+  const std::unordered_set<irep_idt> &weak_symbols)
+{
+  namespacet ns(dest_symbol_table);
+  namespacet src_ns(src_symbol_table);
+
+  // merge functions
+  for(auto &gf_entry : src_functions.function_map)
+  {
+    // the function might have been renamed
+    rename_symbolt::expr_mapt::const_iterator e_it =
+      rename_symbol.expr_map.find(gf_entry.first);
+
+    irep_idt final_id = gf_entry.first;
+
+    if(e_it != rename_symbol.expr_map.end())
+      final_id = e_it->second;
+
+    // already there?
+    goto_functionst::function_mapt::iterator dest_f_it =
+      dest_functions.function_map.find(final_id);
+
+    goto_functionst::goto_functiont &src_func = gf_entry.second;
+    if(dest_f_it == dest_functions.function_map.end()) // not there yet
+    {
+      rename_symbols_in_function(src_func, final_id, rename_symbol);
+      dest_functions.function_map.emplace(final_id, std::move(src_func));
+    }
+    else // collision!
+    {
+      goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
+
+      if(
+        in_dest_symbol_table.body.instructions.empty() ||
+        weak_symbols.find(final_id) != weak_symbols.end())
+      {
+        // the one with body wins!
+        rename_symbols_in_function(src_func, final_id, rename_symbol);
+
+        in_dest_symbol_table.body.swap(src_func.body);
+        in_dest_symbol_table.parameter_identifiers.swap(
+          src_func.parameter_identifiers);
+      }
+      else if(
+        src_func.body.instructions.empty() ||
+        src_ns.lookup(gf_entry.first).is_weak)
+      {
+        // just keep the old one in dest
+      }
+      else if(to_code_type(ns.lookup(final_id).type).get_inlined())
+      {
+        // ok, we silently ignore
+      }
+      else
+      {
+        // the linking code will have ensured that types match
+      }
+    }
+  }
+
+  return false;
+}
+
+static void link_goto_model(
+  goto_modelt &dest,
+  goto_modelt &src,
+  unchecked_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());
+}
+
+static void finalize_linking(
+  goto_modelt &dest,
+  const unchecked_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;
+
+  for(const auto &symbol_pair : dest_symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
+    {
+      const symbolt &symbol = symbol_pair.second;
+
+      INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
+      const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
+
+#if 0
+      if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
+      {
+        std::cerr << symbol << '\n';
+        std::cerr << ns.lookup(id) << '\n';
+      }
+      INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
+                "type matches");
+#endif
+
+      macro_application.insert_expr(symbol.name, id);
+    }
+  }
+
+  if(!macro_application.expr_map.empty())
+  {
+    for(auto &gf_entry : dest_functions.function_map)
+    {
+      irep_idt final_id = gf_entry.first;
+      rename_symbols_in_function(gf_entry.second, final_id, macro_application);
+    }
+  }
+
+  if(!object_type_updates.empty())
+  {
+    for(auto &gf_entry : dest_functions.function_map)
+    {
+      Forall_goto_program_instructions(iit, gf_entry.second.body)
+      {
+        iit->transform([&object_type_updates](exprt expr) {
+          object_type_updates(expr);
+          return expr;
+        });
+      }
+    }
+  }
+}
+
 static bool read_goto_binary(
   const std::string &filename,
   symbol_tablet &,