diff --git a/regression/goto-gcc/CMakeLists.txt b/regression/goto-gcc/CMakeLists.txt index 47bc31b4a76..fe4828f81b6 100644 --- a/regression/goto-gcc/CMakeLists.txt +++ b/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("$/goto-gcc") + +add_custom_command(OUTPUT "${CMAKE_CURRENT_SOURCE_DIR}/archives/libour_archive.a" + COMMAND "$/goto-gcc" -c foo.c + COMMAND ${CMAKE_AR} rcs libour_archive.a foo.o + DEPENDS + "$/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" +) diff --git a/regression/goto-gcc/Makefile b/regression/goto-gcc/Makefile index acfeddbad98..969707b8f44 100644 --- a/regression/goto-gcc/Makefile +++ b/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 diff --git a/regression/goto-gcc/archives/foo.c b/regression/goto-gcc/archives/foo.c new file mode 100644 index 00000000000..e05eb7e694a --- /dev/null +++ b/regression/goto-gcc/archives/foo.c @@ -0,0 +1,4 @@ +int foo() +{ + return 0; +} diff --git a/regression/goto-gcc/archives/main.c b/regression/goto-gcc/archives/main.c new file mode 100644 index 00000000000..5be0864eeee --- /dev/null +++ b/regression/goto-gcc/archives/main.c @@ -0,0 +1,6 @@ +int foo(); + +int main() +{ + return foo(); +} diff --git a/regression/goto-gcc/archives/test.desc b/regression/goto-gcc/archives/test.desc new file mode 100644 index 00000000000..b04efe0097e --- /dev/null +++ b/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. diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp index 95efc9fc4dc..d45a58a5bf3 100644 --- a/src/goto-cc/as_mode.cpp +++ b/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; diff --git a/src/goto-cc/as_mode.h b/src/goto-cc/as_mode.h index 61fe9c8bfcd..c07bba20f3e 100644 --- a/src/goto-cc/as_mode.h +++ b/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 diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 358708157dd..4e8aca96eb1 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/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; diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp index 5f0730d7037..31b82fe672b 100644 --- a/src/goto-cc/hybrid_binary.cpp +++ b/src/goto-cc/hybrid_binary.cpp @@ -20,6 +20,7 @@ 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); @@ -27,6 +28,9 @@ int hybrid_binary( 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 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; diff --git a/src/goto-cc/hybrid_binary.h b/src/goto-cc/hybrid_binary.h index 054218d35a7..a4308a8379f 100644 --- a/src/goto-cc/hybrid_binary.h +++ b/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 diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp index e00a6746436..e2d2ffbc04c 100644 --- a/src/goto-cc/ld_mode.cpp +++ b/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; diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt index b63faa217a6..ed04acda91c 100644 --- a/src/goto-programs/module_dependencies.txt +++ b/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 diff --git a/src/goto-programs/osx_fat_reader.cpp b/src/goto-programs/osx_fat_reader.cpp index 08847cc3e5f..10dbbd5dc93 100644 --- a/src/goto-programs/osx_fat_reader.cpp +++ b/src/goto-programs/osx_fat_reader.cpp @@ -15,32 +15,49 @@ Module: Read Mach-O #include #include +// we define file-type magic values for all platforms to detect when we find a +// file that we might not be able to process +#define CPROVER_FAT_MAGIC 0xcafebabe +#define CPROVER_FAT_CIGAM 0xbebafeca +#define CPROVER_MH_MAGIC 0xfeedface +#define CPROVER_MH_CIGAM 0xcefaedfe +#define CPROVER_MH_MAGIC_64 0xfeedfacf +#define CPROVER_MH_CIGAM_64 0xcffaedfe + #ifdef __APPLE__ -#include +# include +# include +# include +# include + +# if(CPROVER_FAT_MAGIC != FAT_MAGIC) || (CPROVER_FAT_CIGAM != FAT_CIGAM) || \ + (CPROVER_MH_MAGIC != MH_MAGIC) || (CPROVER_MH_CIGAM != MH_CIGAM) || \ + (CPROVER_MH_MAGIC_64 != MH_MAGIC_64) || \ + (CPROVER_MH_CIGAM_64 != MH_CIGAM_64) +# error "Mach-O magic has inconsistent value" +# endif #endif #include bool is_osx_fat_magic(char hdr[4]) { -#ifdef __APPLE__ uint32_t *magic=reinterpret_cast(hdr); switch(*magic) { - case FAT_MAGIC: - case FAT_CIGAM: - return true; + case CPROVER_FAT_MAGIC: + case CPROVER_FAT_CIGAM: + return true; } -#else - (void)hdr; // unused parameter -#endif return false; } -osx_fat_readert::osx_fat_readert(std::ifstream &in) : - has_gb_arch(false) +osx_fat_readert::osx_fat_readert( + std::ifstream &in, + message_handlert &message_handler) + : log(message_handler), has_gb_arch(false) { #ifdef __APPLE__ // NOLINTNEXTLINE(readability/identifiers) @@ -79,6 +96,9 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) : } #else (void)in; // unused parameter + + log.warning() << "Cannot read OSX fat archive on this platform" + << messaget::eom; #endif } @@ -92,3 +112,214 @@ bool osx_fat_readert::extract_gb( "lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source}) != 0; } + +// guided by https://lowlevelbits.org/parsing-mach-o-files/ +bool is_osx_mach_object(char hdr[4]) +{ + uint32_t *magic = reinterpret_cast(hdr); + + switch(*magic) + { + case CPROVER_MH_MAGIC: + case CPROVER_MH_CIGAM: + case CPROVER_MH_MAGIC_64: + case CPROVER_MH_CIGAM_64: + return true; + } + + return false; +} + +void osx_mach_o_readert::process_sections_32(uint32_t nsects, bool need_swap) +{ +#ifdef __APPLE__ + for(uint32_t i = 0; i < nsects; ++i) + { + // NOLINTNEXTLINE(readability/identifiers) + struct section s; + in.read(reinterpret_cast(&s), sizeof(s)); + + if(!in) + throw deserialization_exceptiont("failed to read Mach-O section"); + + if(need_swap) + swap_section(&s, 1, NXHostByteOrder()); + + sections.emplace(s.sectname, sectiont(s.sectname, s.offset, s.size)); + } +#else + // unused parameters + (void)nsects; + (void)need_swap; +#endif +} + +void osx_mach_o_readert::process_sections_64(uint32_t nsects, bool need_swap) +{ +#ifdef __APPLE__ + for(uint32_t i = 0; i < nsects; ++i) + { + // NOLINTNEXTLINE(readability/identifiers) + struct section_64 s; + in.read(reinterpret_cast(&s), sizeof(s)); + + if(!in) + throw deserialization_exceptiont("failed to read 64-bit Mach-O section"); + + if(need_swap) + swap_section_64(&s, 1, NXHostByteOrder()); + + sections.emplace(s.sectname, sectiont(s.sectname, s.offset, s.size)); + } +#else + // unused parameters + (void)nsects; + (void)need_swap; +#endif +} + +void osx_mach_o_readert::process_commands( + uint32_t ncmds, + std::size_t offset, + bool need_swap) +{ +#ifdef __APPLE__ + for(uint32_t i = 0; i < ncmds; ++i) + { + in.seekg(offset); + + // NOLINTNEXTLINE(readability/identifiers) + struct load_command lc; + in.read(reinterpret_cast(&lc), sizeof(lc)); + + if(!in) + throw deserialization_exceptiont("failed to read Mach-O command"); + + if(need_swap) + swap_load_command(&lc, NXHostByteOrder()); + + // we may need to re-read the command once we have figured out its type; in + // particular, segment commands contain additional information that we have + // now just read a prefix of + in.seekg(offset); + + switch(lc.cmd) + { + case LC_SEGMENT: + { + // NOLINTNEXTLINE(readability/identifiers) + struct segment_command seg; + in.read(reinterpret_cast(&seg), sizeof(seg)); + + if(!in) + throw deserialization_exceptiont("failed to read Mach-O segment"); + + if(need_swap) + swap_segment_command(&seg, NXHostByteOrder()); + + process_sections_32(seg.nsects, need_swap); + break; + } + case LC_SEGMENT_64: + { + // NOLINTNEXTLINE(readability/identifiers) + struct segment_command_64 seg; + in.read(reinterpret_cast(&seg), sizeof(seg)); + + if(!in) + throw deserialization_exceptiont("failed to read Mach-O segment"); + + if(need_swap) + swap_segment_command_64(&seg, NXHostByteOrder()); + + process_sections_64(seg.nsects, need_swap); + break; + } + default: + break; + } + + offset += lc.cmdsize; + } +#else + // unused parameters + (void)ncmds; + (void)offset; + (void)need_swap; +#endif +} + +osx_mach_o_readert::osx_mach_o_readert( + std::istream &_in, + message_handlert &message_handler) + : log(message_handler), in(_in) +{ + // read magic + uint32_t magic; + in.read(reinterpret_cast(&magic), sizeof(magic)); + + if(!in) + throw deserialization_exceptiont("failed to read Mach-O magic"); + +#ifdef __APPLE__ + bool is_64 = false, need_swap = false; + switch(magic) + { + case CPROVER_MH_CIGAM: + need_swap = true; + break; + case CPROVER_MH_MAGIC: + break; + case CPROVER_MH_CIGAM_64: + need_swap = true; + is_64 = true; + break; + case CPROVER_MH_MAGIC_64: + is_64 = true; + break; + default: + throw deserialization_exceptiont("no Mach-O magic"); + } + + uint32_t ncmds = 0; + std::size_t offset = 0; + + // re-read from the beginning, now reading the full header + in.seekg(0); + + if(!is_64) + { + // NOLINTNEXTLINE(readability/identifiers) + struct mach_header mh; + in.read(reinterpret_cast(&mh), sizeof(mh)); + + if(!in) + throw deserialization_exceptiont("failed to read 32-bit Mach-O header"); + + if(need_swap) + swap_mach_header(&mh, NXHostByteOrder()); + + ncmds = mh.ncmds; + offset = sizeof(mh); + } + else + { + // NOLINTNEXTLINE(readability/identifiers) + struct mach_header_64 mh; + in.read(reinterpret_cast(&mh), sizeof(mh)); + + if(!in) + throw deserialization_exceptiont("failed to read 64-bit Mach-O header"); + + if(need_swap) + swap_mach_header_64(&mh, NXHostByteOrder()); + + ncmds = mh.ncmds; + offset = sizeof(mh); + } + + process_commands(ncmds, offset, need_swap); +#else + log.warning() << "Cannot read OSX Mach-O on this platform" << messaget::eom; +#endif +} diff --git a/src/goto-programs/osx_fat_reader.h b/src/goto-programs/osx_fat_reader.h index 715fc9f1eec..c079d339607 100644 --- a/src/goto-programs/osx_fat_reader.h +++ b/src/goto-programs/osx_fat_reader.h @@ -12,7 +12,10 @@ Module: Read OS X Fat Binaries #ifndef CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H #define CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H +#include + #include +#include #include // we follow @@ -21,7 +24,7 @@ Module: Read OS X Fat Binaries class osx_fat_readert { public: - explicit osx_fat_readert(std::ifstream &in); + osx_fat_readert(std::ifstream &, message_handlert &); bool has_gb() const { return has_gb_arch; } @@ -30,9 +33,47 @@ class osx_fat_readert const std::string &dest) const; private: + messaget log; bool has_gb_arch; }; bool is_osx_fat_magic(char hdr[4]); +class osx_mach_o_readert +{ +public: + osx_mach_o_readert(std::istream &, message_handlert &); + + struct sectiont + { + sectiont(const std::string &_name, std::size_t _offset, std::size_t _size) + : name(_name), offset(_offset), size(_size) + { + } + + std::string name; + std::size_t offset; + std::size_t size; + }; + + using sectionst = std::map; + sectionst sections; + + bool has_section(const std::string &name) const + { + return sections.find(name) != sections.end(); + } + +private: + messaget log; + std::istream ∈ + + void process_commands(uint32_t ncmds, std::size_t offset, bool need_swap); + + void process_sections_32(uint32_t nsects, bool need_swap); + void process_sections_64(uint32_t nsects, bool need_swap); +}; + +bool is_osx_mach_object(char hdr[4]); + #endif // CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index 82650552c20..f71f35555ff 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -120,7 +120,7 @@ static bool read_goto_binary( // Mach-O universal binary // This _may_ have a goto binary as hppa7100LC architecture - osx_fat_readert osx_fat_reader(in); + osx_fat_readert osx_fat_reader(in, message_handler); if(osx_fat_reader.has_gb()) { @@ -146,6 +146,34 @@ static bool read_goto_binary( message.error() << "failed to find goto binary in Mach-O file" << messaget::eom; } + else if(is_osx_mach_object(hdr)) + { + messaget message(message_handler); + + // Mach-O object file, may contain a goto-cc section + try + { + osx_mach_o_readert mach_o_reader(in, message_handler); + + osx_mach_o_readert::sectionst::const_iterator entry = + mach_o_reader.sections.find("goto-cc"); + if(entry != mach_o_reader.sections.end()) + { + in.seekg(entry->second.offset); + return read_bin_goto_object( + in, filename, symbol_table, goto_functions, message_handler); + } + + // section not found + messaget(message_handler).error() + << "failed to find goto-cc section in Mach-O binary" << messaget::eom; + } + + catch(const deserialization_exceptiont &e) + { + messaget(message_handler).error() << e.what() << messaget::eom; + } + } else { messaget(message_handler).error() << @@ -155,7 +183,9 @@ static bool read_goto_binary( return true; } -bool is_goto_binary(const std::string &filename, message_handlert &) +bool is_goto_binary( + const std::string &filename, + message_handlert &message_handler) { #ifdef _MSC_VER std::ifstream in(widen(filename), std::ios::binary); @@ -202,7 +232,7 @@ bool is_goto_binary(const std::string &filename, message_handlert &) try { in.seekg(0); - osx_fat_readert osx_fat_reader(in); + osx_fat_readert osx_fat_reader(in, message_handler); if(osx_fat_reader.has_gb()) return true; } @@ -212,6 +242,22 @@ bool is_goto_binary(const std::string &filename, message_handlert &) // ignore any errors } } + else if(is_osx_mach_object(hdr)) + { + // this _may_ have a goto-cc section + try + { + in.seekg(0); + osx_mach_o_readert mach_o_reader(in, message_handler); + if(mach_o_reader.has_section("goto-cc")) + return true; + } + + catch(...) + { + // ignore any errors + } + } return false; }