Do not pass the compiler object to linker-script merging

There is no need to access the goto model stored in compilet as we read
the goto binary that compilet wrote anyway. This avoids tight coupling
and enables removing public class members from compilet.

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -91,11 +91,11 @@ warning: Included by graph for 'expr.h' not generated, too many nodes (88), thre
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'message.h' not generated, too many nodes (115), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (245), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/goto-cc/compile.cpp

@@ -556,32 +556,33 @@ bool compilet::parse_stdin(languaget &language)
   return false;
 }
 
-/// Writes the goto functions of \p src_goto_model to a binary format object
-/// file.
-/// \param file_name: Target file to serialize \p src_goto_model to
-/// \param src_goto_model: goto model to serialize
-/// \return true on error, false otherwise
 bool compilet::write_bin_object_file(
   const std::string &file_name,
-  const goto_modelt &src_goto_model)
+  const goto_modelt &src_goto_model,
+  bool validate_goto_model,
+  message_handlert &message_handler)
 {
+  messaget log(message_handler);
+
   if(validate_goto_model)
   {
-    status() << "Validating goto model" << eom;
+    log.status() << "Validating goto model" << messaget::eom;
     src_goto_model.validate();
   }
 
-  statistics() << "Writing binary format object '" << file_name << "'" << eom;
+  log.statistics() << "Writing binary format object '" << file_name << "'"
+                   << messaget::eom;
 
   // symbols
-  statistics() << "Symbols in table: "
-               << src_goto_model.symbol_table.symbols.size() << eom;
+  log.statistics() << "Symbols in table: "
+                   << src_goto_model.symbol_table.symbols.size()
+                   << messaget::eom;
 
   std::ofstream outfile(file_name, std::ios::binary);
 
   if(!outfile.is_open())
   {
-    error() << "Error opening file '" << file_name << "'" << eom;
+    log.error() << "Error opening file '" << file_name << "'" << messaget::eom;
     return true;
   }
 
@@ -590,12 +591,11 @@ bool compilet::write_bin_object_file(
 
   const auto cnt = function_body_count(src_goto_model.goto_functions);
 
-  statistics() << "Functions: "
-               << src_goto_model.goto_functions.function_map.size() << "; "
-               << cnt << " have a body." << eom;
+  log.statistics() << "Functions: "
+                   << src_goto_model.goto_functions.function_map.size() << "; "
+                   << cnt << " have a body." << messaget::eom;
 
   outfile.close();
-  wrote_object=true;
 
   return false;
 }
@@ -661,8 +661,7 @@ compilet::~compilet()
     delete_directory(dir);
 }
 
-std::size_t
-compilet::function_body_count(const goto_functionst &functions) const
+std::size_t compilet::function_body_count(const goto_functionst &functions)
 {
   std::size_t count = 0;
 

src/goto-cc/compile.h

@@ -68,7 +68,18 @@ class compilet : public messaget
 
   bool parse_source(const std::string &);
 
-  bool write_bin_object_file(const std::string &, const goto_modelt &);
+  /// Writes the goto functions of \p src_goto_model to a binary format object
+  /// file.
+  /// \param file_name: Target file to serialize \p src_goto_model to
+  /// \param src_goto_model: goto model to serialize
+  /// \param validate_goto_model: enable goto-model validation
+  /// \param message_handler: message handler
+  /// \return true on error, false otherwise
+  static bool write_bin_object_file(
+    const std::string &file_name,
+    const goto_modelt &src_goto_model,
+    bool validate_goto_model,
+    message_handlert &message_handler);
 
   /// \brief Has this compiler written any object files?
   bool wrote_object_files() const { return wrote_object; }
@@ -88,8 +99,6 @@ class compilet : public messaget
   }
 
 protected:
-  namespacet ns;
-
   std::string working_directory;
   std::string override_language;
 
@@ -105,7 +114,22 @@ class compilet : public messaget
   /// \brief String to include in all mangled names
   const std::string file_local_mangle_suffix;
 
-  std::size_t function_body_count(const goto_functionst &) const;
+  static std::size_t function_body_count(const goto_functionst &);
+
+  bool write_bin_object_file(
+    const std::string &file_name,
+    const goto_modelt &src_goto_model)
+  {
+    if(write_bin_object_file(
+         file_name, src_goto_model, validate_goto_model, get_message_handler()))
+    {
+      return true;
+    }
+
+    wrote_object = true;
+
+    return false;
+  }
 
   void add_compiler_specific_defines() const;
 

src/goto-cc/gcc_mode.cpp

@@ -972,8 +972,10 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
      output_files.size()==1)
   {
     linker_script_merget ls_merge(
-      compiler, output_files.front(), goto_binaries.front(),
-      cmdline, gcc_message_handler);
+      output_files.front(),
+      goto_binaries.front(),
+      cmdline,
+      gcc_message_handler);
     result=ls_merge.add_linker_script_definitions();
   }
 

src/goto-cc/ld_mode.cpp

@@ -145,7 +145,7 @@ int ld_modet::doit()
 
   // We can generate hybrid ELF and Mach-O binaries
   // containing both executable machine code and the goto-binary.
-  return ld_hybrid_binary(compiler);
+  return ld_hybrid_binary(compiler.mode == compilet::COMPILE_LINK_EXECUTABLE);
 }
 
 int ld_modet::run_ld()
@@ -170,7 +170,7 @@ int ld_modet::run_ld()
   return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
-int ld_modet::ld_hybrid_binary(compilet &compiler)
+int ld_modet::ld_hybrid_binary(bool building_executable)
 {
   std::string output_file;
 
@@ -206,7 +206,7 @@ int ld_modet::ld_hybrid_binary(compilet &compiler)
   if(result == 0 && cmdline.isset('T'))
   {
     linker_script_merget ls_merge(
-      compiler, output_file, goto_binary, cmdline, message_handler);
+      output_file, goto_binary, cmdline, message_handler);
     result = ls_merge.add_linker_script_definitions();
   }
 
@@ -218,7 +218,7 @@ int ld_modet::ld_hybrid_binary(compilet &compiler)
       native_linker,
       goto_binary,
       output_file,
-      compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
+      building_executable,
       message_handler);
   }
 

src/goto-cc/ld_mode.h

@@ -40,7 +40,7 @@ class ld_modet : public goto_cc_modet
   /// \brief call ld with original command line
   int run_ld();
 
-  int ld_hybrid_binary(compilet &compiler);
+  int ld_hybrid_binary(bool);
 };
 
 #endif // CPROVER_GOTO_CC_LD_MODE_H

src/goto-cc/linker_script_merge.cpp

@@ -25,16 +25,28 @@ Author: Kareem Khazem <[email protected]>, 2017
 
 #include <goto-programs/read_goto_binary.h>
 
+#include "compile.h"
+
 int linker_script_merget::add_linker_script_definitions()
 {
   if(!cmdline.isset('T'))
     return 0;
 
+  auto original_goto_model =
+    read_goto_binary(goto_binary, log.get_message_handler());
+
+  if(!original_goto_model.has_value())
+  {
+    log.error() << "Unable to read goto binary for linker script merging"
+                << messaget::eom;
+    return 1;
+  }
+
   temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
   std::list<irep_idt> linker_defined_symbols;
   int fail = get_linker_script_data(
     linker_defined_symbols,
-    compiler.goto_model.symbol_table,
+    original_goto_model->symbol_table,
     elf_binary,
     linker_def_outfile());
   // ignore linker script parsing failures until the code is tested more widely
@@ -57,16 +69,6 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  auto original_goto_model =
-    read_goto_binary(goto_binary, log.get_message_handler());
-
-  if(!original_goto_model.has_value())
-  {
-    log.error() << "Unable to read goto binary for linker script merging"
-                << messaget::eom;
-    return 1;
-  }
-
   fail=1;
   linker_valuest linker_values;
   const auto &pair =
@@ -106,7 +108,11 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  fail = compiler.write_bin_object_file(goto_binary, *original_goto_model);
+  fail = compilet::write_bin_object_file(
+    goto_binary,
+    *original_goto_model,
+    cmdline.isset("validate-goto-model"),
+    log.get_message_handler());
 
   if(fail!=0)
   {
@@ -118,13 +124,11 @@ int linker_script_merget::add_linker_script_definitions()
 }
 
 linker_script_merget::linker_script_merget(
-  compilet &compiler,
   const std::string &elf_binary,
   const std::string &goto_binary,
   const cmdlinet &cmdline,
   message_handlert &message_handler)
-  : compiler(compiler),
-    elf_binary(elf_binary),
+  : elf_binary(elf_binary),
     goto_binary(goto_binary),
     cmdline(cmdline),
     log(message_handler),

src/goto-cc/linker_script_merge.h

@@ -8,10 +8,15 @@
 #include <functional>
 
 #include <util/json.h>
+#include <util/message.h>
+#include <util/std_expr.h>
 
-#include "compile.h"
 #include "gcc_cmdline.h"
 
+class goto_modelt;
+class goto_programt;
+class symbol_tablet;
+
 /// \brief Patterns of expressions that should be replaced
 ///
 /// Each instance of this class describes an expression 'shape' that should be
@@ -79,14 +84,12 @@ class linker_script_merget
   typedef std::map<irep_idt, std::pair<symbol_exprt, exprt>> linker_valuest;
 
   linker_script_merget(
-    compilet &,
     const std::string &elf_binary,
     const std::string &goto_binary,
     const cmdlinet &,
     message_handlert &);
 
 protected:
-  compilet &compiler;
   const std::string &elf_binary;
   const std::string &goto_binary;
   const cmdlinet &cmdline;