goto-gcc hybrid binaries on OS X

regression/goto-gcc/CMakeLists.txt

@@ -2,3 +2,16 @@
 # isn't marked as an executable (target), which CMake requires. Thus construct a
 # path in the same way the symbolic link is created in the goto-cc directory.
 add_test_pl_tests("$<TARGET_FILE_DIR:goto-cc>/goto-gcc")
+
+add_custom_command(OUTPUT "${CMAKE_CURRENT_SOURCE_DIR}/archives/libour_archive.a"
+    COMMAND "$<TARGET_FILE_DIR:goto-cc>/goto-gcc" -c foo.c
+    COMMAND ${CMAKE_AR} rcs libour_archive.a foo.o
+    DEPENDS
+      "$<TARGET_FILE_DIR:goto-cc>/goto-gcc"
+      "${CMAKE_CURRENT_SOURCE_DIR}/archives/foo.c"
+    WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}/archives"
+)
+
+add_custom_target(libour_archive.a ALL
+    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/archives/libour_archive.a"
+)

regression/goto-gcc/Makefile

@@ -9,14 +9,20 @@ test:
 tests.log: ../test.pl
 
 else
-test:
-	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+test: ../../src/goto-cc/goto-gcc
 	@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
 
-tests.log: ../test.pl
-	-@ln -s goto-cc ../../src/goto-cc/goto-gcc
+tests.log: ../test.pl ../../src/goto-cc/goto-gcc
 	@../test.pl -e -p -c ../../../src/goto-cc/goto-gcc
 
+../../src/goto-cc/goto-gcc: ../../src/goto-cc/goto-cc
+	@ln -sf goto-cc ../../src/goto-cc/goto-gcc
+
+test tests.log: archives/libour_archive.a
+archives/libour_archive.a: archives/foo.c ../../src/goto-cc/goto-gcc
+	@cd archives && \
+		../../../src/goto-cc/goto-gcc -c foo.c && \
+		$(AR) rcs libour_archive.a foo.o
 endif
 
 show:
@@ -30,4 +36,4 @@ clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
 	find -name '*.goto-cc-saved' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log archives/lib_ourarchive.a archives/foo.o

regression/goto-gcc/archives/foo.c

@@ -0,0 +1,4 @@
+int foo()
+{
+  return 0;
+}

regression/goto-gcc/archives/main.c

@@ -0,0 +1,6 @@
+int foo();
+
+int main()
+{
+  return foo();
+}

regression/goto-gcc/archives/test.desc

@@ -0,0 +1,14 @@
+CORE
+10
+main.c -L. -lour_archive --verbosity
+^EXIT=0$
+^SIGNAL=0$
+^Reading: .*/foo.o$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+We need to make sure main.c is listed before the archive for the Linux linker to
+pick up dependencies - thus "main.c" is given as an argument on line 3 in this
+file and the "10" in line 2 is a dummy to be appended at the end, setting the
+verbosity as needed.

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

@@ -985,7 +985,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

@@ -212,7 +212,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;

src/goto-programs/module_dependencies.txt

@@ -1,5 +1,6 @@
 analyses # dubious - concerns call_graph and does_remove_const
 ansi-c # for GraphML witnesses
+architecture # system
 goto-programs
 goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
 json