Skip to content

goto-gcc hybrid binaries on OS X #3867

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 30, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions regression/goto-gcc/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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"
)
16 changes: 11 additions & 5 deletions regression/goto-gcc/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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
4 changes: 4 additions & 0 deletions regression/goto-gcc/archives/foo.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
int foo()
{
return 0;
}
6 changes: 6 additions & 0 deletions regression/goto-gcc/archives/main.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
int foo();

int main()
{
return foo();
}
14 changes: 14 additions & 0 deletions regression/goto-gcc/archives/test.desc
Original file line number Diff line number Diff line change
@@ -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.
10 changes: 7 additions & 3 deletions src/goto-cc/as_mode.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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";

Expand Down Expand Up @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion src/goto-cc/as_mode.h
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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
6 changes: 5 additions & 1 deletion src/goto-cc/gcc_mode.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
23 changes: 22 additions & 1 deletion src/goto-cc/hybrid_binary.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
Expand Down Expand Up @@ -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.
Expand All @@ -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());
Expand All @@ -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;
Expand Down
5 changes: 4 additions & 1 deletion src/goto-cc/hybrid_binary.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
6 changes: 5 additions & 1 deletion src/goto-cc/ld_mode.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions src/goto-programs/module_dependencies.txt
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Loading