OS X hybrid binaries: use sections for object files

lipo/fat binaries only work properly for executables as it isn't possible to
build archives of fat binaries containing goto-cc sections (ranlib complains
about invalid object files); conversely, adding additional sections isn't
possible with executables, but fat binaries work fine.

Author: tautschnig

src/goto-cc/as_mode.cpp

@@ -241,7 +241,7 @@ int as_modet::doit()
   // We can generate hybrid ELF and Mach-O binaries
   // containing both executable machine code and the goto-binary.
   if(produce_hybrid_binary)
-    return as_hybrid_binary();
+    return as_hybrid_binary(compiler);
 
   return EX_OK;
 }
@@ -270,7 +270,7 @@ int as_modet::run_as()
   return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
 }
 
-int as_modet::as_hybrid_binary()
+int as_modet::as_hybrid_binary(const compilet &compiler)
 {
   std::string output_file="a.out";
 
@@ -301,7 +301,11 @@ int as_modet::as_hybrid_binary()
   if(result == 0)
   {
     result = hybrid_binary(
-      native_tool_name, saved, output_file, get_message_handler());
+      native_tool_name,
+      saved,
+      output_file,
+      compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
+      get_message_handler());
   }
 
   return result;

src/goto-cc/as_mode.h

@@ -17,6 +17,8 @@ Date: July 2016
 #include "gcc_message_handler.h"
 #include "goto_cc_mode.h"
 
+class compilet;
+
 class as_modet:public goto_cc_modet
 {
 public:
@@ -35,7 +37,7 @@ class as_modet:public goto_cc_modet
 
   int run_as(); // call as with original command line
 
-  int as_hybrid_binary();
+  int as_hybrid_binary(const compilet &compiler);
 };
 
 #endif // CPROVER_GOTO_CC_AS_MODE_H

src/goto-cc/gcc_mode.cpp

@@ -982,7 +982,11 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
 
     if(result==0)
       result = hybrid_binary(
-        native_tool, goto_binary, *it, get_message_handler());
+        native_tool,
+        goto_binary,
+        *it,
+        compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
+        get_message_handler());
   }
 
   return result;

src/goto-cc/hybrid_binary.cpp

@@ -20,13 +20,17 @@ int hybrid_binary(
   const std::string &compiler_or_linker,
   const std::string &goto_binary_file,
   const std::string &output_file,
+  bool building_executable,
   message_handlert &message_handler)
 {
   messaget message(message_handler);
 
   int result;
 
 #if defined(__linux__) || defined(__FreeBSD_kernel__)
+  // we can use objcopy for both object files and executables
+  (void)building_executable;
+
   std::string objcopy_cmd;
 
   if(has_suffix(compiler_or_linker, "-ld"))
@@ -69,9 +73,10 @@ int hybrid_binary(
   // Mac
 
   message.debug() << "merging " << output_file << " and " << goto_binary_file
-                  << " using lipo"
+                  << " using " << (building_executable ? "lipo" : "ld")
                   << messaget::eom;
 
+  if(building_executable)
   {
     // Add goto-binary as hppa7100LC section.
     // This overwrites if there's already one.
@@ -81,6 +86,21 @@ int hybrid_binary(
 
     result = run(lipo_argv[0], lipo_argv);
   }
+  else
+  {
+    // This fails if there's already one.
+    std::vector<std::string> ld_argv = {"ld",
+                                        "-r",
+                                        "-sectcreate",
+                                        "__TEXT",
+                                        "goto-cc",
+                                        goto_binary_file,
+                                        output_file,
+                                        "-o",
+                                        output_file};
+
+    result = run(ld_argv[0], ld_argv);
+  }
 
   // delete the goto binary
   int remove_result = remove(goto_binary_file.c_str());
@@ -97,6 +117,7 @@ int hybrid_binary(
   (void)compiler_or_linker;
   (void)goto_binary_file;
   (void)output_file;
+  (void)building_executable;
   message.error() << "binary merging not implemented for this platform"
                   << messaget::eom;
   result = 1;

src/goto-cc/hybrid_binary.h

@@ -23,10 +23,13 @@ Date: May 2018
 ///   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.
+/// \param building_executable: The \p output_file is an executable.
+/// \param message_handler: Message handler for output.
 int hybrid_binary(
   const std::string &compiler_or_linker,
   const std::string &goto_binary_file,
   const std::string &output_file,
-  message_handlert &);
+  bool building_executable,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_CC_HYBRID_BINARY_H

src/goto-cc/ld_mode.cpp

@@ -209,7 +209,11 @@ int ld_modet::ld_hybrid_binary(compilet &compiler)
     std::string native_linker = linker_name(cmdline, base_name);
 
     result = hybrid_binary(
-      native_linker, goto_binary, output_file, get_message_handler());
+      native_linker,
+      goto_binary,
+      output_file,
+      compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
+      get_message_handler());
   }
 
   return result;