factor out creation of hybrid binaries

Author: Daniel Kroening

src/goto-cc/Makefile

@@ -12,6 +12,7 @@ SRC = armcc_cmdline.cpp \
       goto_cc_languages.cpp \
       goto_cc_main.cpp \
       goto_cc_mode.cpp \
+      hybrid_binary.cpp \
       ld_cmdline.cpp \
       linker_script_merge.cpp \
       ms_cl_cmdline.cpp \

src/goto-cc/gcc_mode.cpp

@@ -48,6 +48,7 @@ Author: CM Wintersteiger, 2006
 
 #include <cbmc/version.h>
 
+#include "hybrid_binary.h"
 #include "linker_script_merge.h"
 
 static std::string compiler_name(
@@ -922,19 +923,6 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
     goto_binaries.push_back(bin_name);
   }
 
-  std::string objcopy_cmd;
-  if(has_suffix(linker_name(cmdline, base_name), "-ld"))
-  {
-    objcopy_cmd=linker_name(cmdline, base_name);
-    objcopy_cmd.erase(objcopy_cmd.size()-2);
-  }
-  else if(has_suffix(compiler_name(cmdline, base_name), "-gcc"))
-  {
-    objcopy_cmd=compiler_name(cmdline, base_name);
-    objcopy_cmd.erase(objcopy_cmd.size()-3);
-  }
-  objcopy_cmd+="objcopy";
-
   int result=run_gcc(compiler);
 
   if(result==0 &&
@@ -948,81 +936,24 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
     result=ls_merge.add_linker_script_definitions();
   }
 
+  std::string native_tool;
+
+  if(has_suffix(linker_name(cmdline, base_name), "-ld"))
+    native_tool=linker_name(cmdline, base_name);
+  else if(has_suffix(compiler_name(cmdline, base_name), "-gcc"))
+    native_tool=compiler_name(cmdline, base_name);
+
   // merge output from gcc with goto-binaries
   // using objcopy, or do cleanup if an earlier call failed
   for(std::list<std::string>::const_iterator
       it=output_files.begin();
       it!=output_files.end();
       it++)
   {
-    debug() << "merging " << *it << eom;
-    std::string saved=*it+goto_binary_tmp_suffix;
-
-    #ifdef __linux__
-    if(result==0 && !cmdline.isset('c'))
-    {
-      // remove any existing goto-cc section
-      std::vector<std::string> objcopy_argv;
-
-      objcopy_argv.push_back(objcopy_cmd);
-      objcopy_argv.push_back("--remove-section=goto-cc");
-      objcopy_argv.push_back(*it);
-
-      result=run(objcopy_argv[0], objcopy_argv, "", "");
-    }
+    std::string goto_binary=*it+goto_binary_tmp_suffix;
 
     if(result==0)
-    {
-      // now add goto-binary as goto-cc section
-      std::vector<std::string> objcopy_argv;
-
-      objcopy_argv.push_back(objcopy_cmd);
-      objcopy_argv.push_back("--add-section");
-      objcopy_argv.push_back("goto-cc="+saved);
-      objcopy_argv.push_back(*it);
-
-      result=run(objcopy_argv[0], objcopy_argv, "", "");
-    }
-
-    int remove_result=remove(saved.c_str());
-    if(remove_result!=0)
-    {
-      error() << "Remove failed: " << std::strerror(errno) << eom;
-      if(result==0)
-        result=remove_result;
-    }
-
-    #elif defined(__APPLE__)
-    // Mac
-    if(result==0)
-    {
-      std::vector<std::string> lipo_argv;
-
-      // now add goto-binary as hppa7100LC section
-      lipo_argv.push_back("lipo");
-      lipo_argv.push_back(*it);
-      lipo_argv.push_back("-create");
-      lipo_argv.push_back("-arch");
-      lipo_argv.push_back("hppa7100LC");
-      lipo_argv.push_back(saved);
-      lipo_argv.push_back("-output");
-      lipo_argv.push_back(*it);
-
-      result=run(lipo_argv[0], lipo_argv, "", "");
-    }
-
-    int remove_result=remove(saved.c_str());
-    if(remove_result!=0)
-    {
-      error() << "Remove failed: " << std::strerror(errno) << eom;
-      if(result==0)
-        result=remove_result;
-    }
-
-    #else
-    error() << "binary merging not implemented for this platform" << eom;
-    return 1;
-    #endif
+      result = hybrid_binary(native_tool, goto_binary, *it, get_message_handler());
   }
 
   return result;

src/goto-cc/hybrid_binary.cpp

@@ -0,0 +1,102 @@
+/*******************************************************************\
+
+Module: Create hybrid binary with goto-binary section
+
+Author: Michael Tautschnig, 2018
+
+\*******************************************************************/
+
+/// \file
+/// Create hybrid binary with goto-binary section
+
+#include "hybrid_binary.h"
+
+#include <util/run.h>
+#include <util/suffix.h>
+
+#include <cstring>
+
+int hybrid_binary(
+  const std::string &compiler_or_linker,
+  const std::string &goto_binary_file,
+  const std::string &output_file,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  int result;
+
+#ifdef __linux__
+  std::string objcopy_cmd;
+
+  if(has_suffix(compiler_or_linker, "-ld"))
+  {
+    objcopy_cmd = compiler_or_linker;
+    objcopy_cmd.erase(objcopy_cmd.size() - 2);
+    objcopy_cmd += "objcopy";
+  }
+  else
+    objcopy_cmd = "objcopy";
+
+  // merge output from gcc or ld with goto-binary using objcopy
+
+  message.debug() << "merging " << output_file << " and " << goto_binary_file
+                  << " using " << objcopy_cmd
+                  << messaget::eom;
+
+  {
+    // Now add goto-binary as goto-cc section.
+    // Remove if it exists before, or otherwise adding fails.
+    std::vector<std::string> objcopy_argv = {
+      objcopy_cmd,
+      "--remove-section", "goto-cc",
+      "--add-section", "goto-cc=" + goto_binary_file, output_file};
+
+    result = run(objcopy_argv[0], objcopy_argv, "", "");
+  }
+
+  // delete the goto binary
+  int remove_result = remove(goto_binary_file.c_str());
+  if(remove_result != 0)
+  {
+    message.error() << "Remove failed: " << std::strerror(errno)
+                    << messaget::eom;
+    if(result == 0)
+      result = remove_result;
+  }
+
+#elif defined(__APPLE__)
+  // Mac
+
+  message.debug() << "merging " << output_file << " and " << goto_binary_file
+                  << " using lipo"
+                  << messaget::eom;
+
+  {
+    // Add goto-binary as hppa7100LC section.
+    // This overwrites if there's already one.
+    std::vector<std::string> lipo_argv = {
+      "lipo", output_file, "-create", "-arch", "hppa7100LC", goto_binary_file,
+      "-output", output_file };
+
+    result = run(lipo_argv[0], lipo_argv, "", "");
+  }
+
+  // delete the goto binary
+  int remove_result = remove(goto_binary_file.c_str());
+  if(remove_result != 0)
+  {
+    message.error() << "Remove failed: " << std::strerror(errno)
+                    << messaget::eom;
+    if(result == 0)
+      result = remove_result;
+  }
+
+#else
+  message.error() << "binary merging not implemented for this platform"
+                  << messaget::eom;
+  result = 1;
+#endif
+
+  return result;
+}

src/goto-cc/hybrid_binary.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Create hybrid binary with goto-binary section
+
+Author: Daniel Kroening
+
+Date: May 2018
+
+\*******************************************************************/
+
+/// \file
+/// Create hybrid binary with goto-binary section
+
+#ifndef CPROVER_GOTO_CC_HYBRID_BINARY_H
+#define CPROVER_GOTO_CC_HYBRID_BINARY_H
+
+#include <util/message.h>
+
+#include <string>
+
+/// \brief Merges a goto binary into an object file (e.g. ELF)
+/// \param compiler_or_linker The name of the gcc or ld executable,
+///        used to deduce the name of objcopy
+/// \param goto_binary_file The file name of the goto binary
+/// \param output_file The name of the object file; the result is
+///        stored here.
+int hybrid_binary(
+  const std::string &compiler_or_linker,
+  const std::string &goto_binary_file,
+  const std::string &output_file,
+  message_handlert &);
+
+#endif // CPROVER_GOTO_CC_HYBRID_BINARY_H