From 0d95cc56c161b490ff80bf3b9afe1754854db522 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 27 May 2018 10:44:29 +0100 Subject: [PATCH 1/6] missing const method qualifiers --- src/goto-cc/compile.cpp | 2 +- src/goto-cc/compile.h | 2 +- src/goto-cc/linker_script_merge.cpp | 6 +++--- src/goto-cc/linker_script_merge.h | 16 ++++++++-------- 4 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index fd92c7aeb63..1a29d8bf6c1 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -662,7 +662,7 @@ compilet::~compilet() delete_directory(*it); } -unsigned compilet::function_body_count(const goto_functionst &functions) +unsigned compilet::function_body_count(const goto_functionst &functions) const { int fbs=0; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index 839e340e792..920d01378ae 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -94,7 +94,7 @@ class compilet:public language_uit cmdlinet &cmdline; bool warning_is_fatal; - unsigned function_body_count(const goto_functionst &); + unsigned function_body_count(const goto_functionst &) const; void add_compiler_specific_defines(class configt &config) const; diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 94e6cfb4a3d..9c357b1132d 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -114,9 +114,9 @@ int linker_script_merget::add_linker_script_definitions() linker_script_merget::linker_script_merget( compilet &compiler, - std::list &elf_binaries, - std::list &goto_binaries, - cmdlinet &cmdline, + const std::list &elf_binaries, + const std::list &goto_binaries, + const cmdlinet &cmdline, message_handlert &message_handler) : messaget(message_handler), compiler(compiler), elf_binaries(elf_binaries), goto_binaries(goto_binaries), diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h index af3f22e2587..66b7820e4a2 100644 --- a/src/goto-cc/linker_script_merge.h +++ b/src/goto-cc/linker_script_merge.h @@ -82,17 +82,17 @@ class linker_script_merget:public messaget typedef std::map> linker_valuest; linker_script_merget( - compilet &compiler, - std::list &elf_binaries, - std::list &goto_binaries, - cmdlinet &cmdline, - message_handlert &message_handler); + compilet &, + const std::list &elf_binaries, + const std::list &goto_binaries, + const cmdlinet &, + message_handlert &); protected: compilet &compiler; - std::list &elf_binaries; - std::list &goto_binaries; - cmdlinet &cmdline; + const std::list &elf_binaries; + const std::list &goto_binaries; + const cmdlinet &cmdline; /// \brief The "shapes" of expressions to be replaced by a pointer /// From cd967dbab42cd3916503a819d54359f190bdc988 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 28 May 2018 10:08:09 +0100 Subject: [PATCH 2/6] update year + add Michael --- src/goto-cc/goto_cc_mode.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index b6802103f30..81fda73ecbb 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/src/goto-cc/goto_cc_mode.cpp @@ -47,9 +47,9 @@ void goto_cc_modet::help() std::cout << "\n" // NOLINTNEXTLINE(whitespace/line_length) - "* * goto-cc " CBMC_VERSION " - Copyright (C) 2006-2014 * *\n" - "* * Daniel Kroening, Christoph Wintersteiger * *\n" - "* * kroening@kroening.com * *\n" + "* * goto-cc " CBMC_VERSION " - Copyright (C) 2006-2018 * *\n" + "* * Daniel Kroening, Michael Tautschnig, * *\n" + "* * Christoph Wintersteiger * *\n" "\n"; help_mode(); From b9127f328d1766cb35c162cc9f51a655530df6d6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 28 May 2018 09:26:39 +0100 Subject: [PATCH 3/6] linker_script_merget now takes exactly one ELF + goto binary --- src/goto-cc/gcc_mode.cpp | 8 ++++++-- src/goto-cc/linker_script_merge.cpp | 21 ++++++++++++--------- src/goto-cc/linker_script_merge.h | 14 +++++++------- 3 files changed, 25 insertions(+), 18 deletions(-) diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index e989c886307..00eb6fc867f 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -937,10 +937,14 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) int result=run_gcc(compiler); - if(result==0) + if(result==0 && + cmdline.isset('T') && + goto_binaries.size()==1 && + output_files.size()==1) { linker_script_merget ls_merge( - compiler, output_files, goto_binaries, cmdline, gcc_message_handler); + compiler, output_files.front(), goto_binaries.front(), + cmdline, gcc_message_handler); result=ls_merge.add_linker_script_definitions(); } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 9c357b1132d..459dbdc7bf2 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -27,10 +27,8 @@ Author: Kareem Khazem , 2017 int linker_script_merget::add_linker_script_definitions() { - if(!cmdline.isset('T') || elf_binaries.size()!=1) + if(!cmdline.isset('T')) return 0; - const std::string &elf_file=*elf_binaries.begin(); - const std::string &goto_file=*goto_binaries.begin(); temporary_filet linker_def_outfile("goto-cc-linker-info", ".json"); std::list linker_defined_symbols; @@ -38,7 +36,7 @@ int linker_script_merget::add_linker_script_definitions() get_linker_script_data( linker_defined_symbols, compiler.symbol_table, - elf_file, + elf_binary, linker_def_outfile()); // ignore linker script parsing failures until the code is tested more widely if(fail!=0) @@ -62,8 +60,10 @@ int linker_script_merget::add_linker_script_definitions() symbol_tablet original_st; goto_functionst original_gf; - fail=read_goto_binary(goto_file, original_st, original_gf, + + fail=read_goto_binary(goto_binary, original_st, original_gf, get_message_handler()); + if(fail!=0) { error() << "Unable to read goto binary for linker script merging" << eom; @@ -100,26 +100,29 @@ int linker_script_merget::add_linker_script_definitions() fail=pointerize_linker_defined_symbols(original_gf, original_st, linker_values); + if(fail!=0) { error() << "Could not pointerize all linker-defined expressions" << eom; return fail; } - fail=compiler.write_object_file(goto_file, original_st, original_gf); + fail=compiler.write_object_file(goto_binary, original_st, original_gf); + if(fail!=0) error() << "Could not write linkerscript-augmented binary" << eom; + return fail; } linker_script_merget::linker_script_merget( compilet &compiler, - const std::list &elf_binaries, - const std::list &goto_binaries, + const std::string &elf_binary, + const std::string &goto_binary, const cmdlinet &cmdline, message_handlert &message_handler) : messaget(message_handler), compiler(compiler), - elf_binaries(elf_binaries), goto_binaries(goto_binaries), + elf_binary(elf_binary), goto_binary(goto_binary), cmdline(cmdline), replacement_predicates( { diff --git a/src/goto-cc/linker_script_merge.h b/src/goto-cc/linker_script_merge.h index 66b7820e4a2..e260247387f 100644 --- a/src/goto-cc/linker_script_merge.h +++ b/src/goto-cc/linker_script_merge.h @@ -82,16 +82,16 @@ class linker_script_merget:public messaget typedef std::map> linker_valuest; linker_script_merget( - compilet &, - const std::list &elf_binaries, - const std::list &goto_binaries, - const cmdlinet &, - message_handlert &); + compilet &, + const std::string &elf_binary, + const std::string &goto_binary, + const cmdlinet &, + message_handlert &); protected: compilet &compiler; - const std::list &elf_binaries; - const std::list &goto_binaries; + const std::string &elf_binary; + const std::string &goto_binary; const cmdlinet &cmdline; /// \brief The "shapes" of expressions to be replaced by a pointer From 524091ffcb86dc1b3ec393166b3d637e12d6fde6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 28 May 2018 09:57:27 +0100 Subject: [PATCH 4/6] factor out creation of hybrid binaries --- src/goto-cc/Makefile | 1 + src/goto-cc/gcc_mode.cpp | 89 ++++------------------------- src/goto-cc/hybrid_binary.cpp | 102 ++++++++++++++++++++++++++++++++++ src/goto-cc/hybrid_binary.h | 33 +++++++++++ 4 files changed, 146 insertions(+), 79 deletions(-) create mode 100644 src/goto-cc/hybrid_binary.cpp create mode 100644 src/goto-cc/hybrid_binary.h diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 7263f1b62d4..01d24c8b33a 100644 --- a/src/goto-cc/Makefile +++ b/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 \ diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 00eb6fc867f..47b02e18e04 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -48,6 +48,7 @@ Author: CM Wintersteiger, 2006 #include +#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,6 +936,13 @@ 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::const_iterator @@ -955,74 +950,10 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) 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 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 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 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; diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp new file mode 100644 index 00000000000..fa5f0f0dd64 --- /dev/null +++ b/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 +#include + +#include + +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 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 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; +} diff --git a/src/goto-cc/hybrid_binary.h b/src/goto-cc/hybrid_binary.h new file mode 100644 index 00000000000..3b5ac97bcb0 --- /dev/null +++ b/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 + +#include + +/// \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 From 303908f6a4bf71086cd8a60363d670a5702dcf40 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 26 May 2018 13:33:24 +0100 Subject: [PATCH 5/6] add separate path for ld --- src/goto-cc/Makefile | 1 + src/goto-cc/goto_cc_main.cpp | 11 +- src/goto-cc/ld_mode.cpp | 225 +++++++++++++++++++++++++++++++++++ src/goto-cc/ld_mode.h | 47 ++++++++ 4 files changed, 279 insertions(+), 5 deletions(-) create mode 100644 src/goto-cc/ld_mode.cpp create mode 100644 src/goto-cc/ld_mode.h diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 01d24c8b33a..f056c1258c1 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -14,6 +14,7 @@ SRC = armcc_cmdline.cpp \ goto_cc_mode.cpp \ hybrid_binary.cpp \ ld_cmdline.cpp \ + ld_mode.cpp \ linker_script_merge.cpp \ ms_cl_cmdline.cpp \ ms_cl_mode.cpp \ diff --git a/src/goto-cc/goto_cc_main.cpp b/src/goto-cc/goto_cc_main.cpp index 8d76e897c77..ab601a2c00a 100644 --- a/src/goto-cc/goto_cc_main.cpp +++ b/src/goto-cc/goto_cc_main.cpp @@ -25,11 +25,12 @@ Date: May 2006 #include "as_cmdline.h" #include "as86_cmdline.h" -#include "gcc_mode.h" -#include "cw_mode.h" -#include "ms_cl_mode.h" #include "armcc_mode.h" #include "as_mode.h" +#include "cw_mode.h" +#include "gcc_mode.h" +#include "ld_mode.h" +#include "ms_cl_mode.h" std::string to_lower_string(const std::string &s) { @@ -106,8 +107,8 @@ int main(int argc, const char **argv) { // this simulates "ld" for linking ld_cmdlinet cmdline; - gcc_modet gcc_mode(cmdline, base_name, true); - return gcc_mode.main(argc, argv); + ld_modet ld_mode(cmdline, base_name); + return ld_mode.main(argc, argv); } else if(base_name.find("goto-bcc")!=std::string::npos) { diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp new file mode 100644 index 00000000000..84dd936b986 --- /dev/null +++ b/src/goto-cc/ld_mode.cpp @@ -0,0 +1,225 @@ +/*******************************************************************\ + +Module: LD Mode + +Author: CM Wintersteiger, 2006 + +\*******************************************************************/ + +/// \file +/// LD Mode + +#include "ld_mode.h" + +#ifdef _WIN32 +#define EX_OK 0 +#define EX_USAGE 64 +#define EX_SOFTWARE 70 +#else +#include +#endif + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include + +#include "hybrid_binary.h" +#include "linker_script_merge.h" + +static std::string +linker_name(const cmdlinet &cmdline, const std::string &base_name) +{ + if(cmdline.isset("native-linker")) + return cmdline.get_value("native-linker"); + + std::string::size_type pos = base_name.find("goto-ld"); + + if( + pos == std::string::npos || base_name == "goto-gcc" || + base_name == "goto-ld") + return "ld"; + + std::string result = base_name; + result.replace(pos, 7, "ld"); + + return result; +} + +ld_modet::ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name) + : goto_cc_modet(_cmdline, _base_name, gcc_message_handler), + goto_binary_tmp_suffix(".goto-cc-saved") +{ +} + +/// does it. +int ld_modet::doit() +{ + if(cmdline.isset("help")) + { + help(); + return EX_OK; + } + + native_tool_name = linker_name(cmdline, base_name); + + if(cmdline.isset("version") || cmdline.isset("print-sysroot")) + return run_ld(); + + eval_verbosity( + cmdline.get_value("verbosity"), messaget::M_ERROR, gcc_message_handler); + + compilet compiler(cmdline, gcc_message_handler, false); + + // determine actions to be undertaken + compiler.mode = compilet::LINK_LIBRARY; + + // get configuration + config.set(cmdline); + + compiler.object_file_extension = "o"; + + if(cmdline.isset('L')) + compiler.library_paths = cmdline.get_values('L'); + // Don't add the system paths! + + if(cmdline.isset('l')) + compiler.libraries = cmdline.get_values('l'); + + if(cmdline.isset("static")) + compiler.libraries.push_back("c"); + + if(cmdline.isset('o')) + { + // given gcc -o file1 -o file2, + // gcc will output to file2, not file1 + compiler.output_file_object = cmdline.get_values('o').back(); + compiler.output_file_executable = cmdline.get_values('o').back(); + } + else + { + compiler.output_file_object = ""; + compiler.output_file_executable = "a.out"; + } + + // We now iterate over any input files + + for(const auto &arg : cmdline.parsed_argv) + if(arg.is_infile_name) + compiler.add_input_file(arg.arg); + + // Revert to gcc in case there is no source to compile + // and no binary to link. + + if(compiler.source_files.empty() && compiler.object_files.empty()) + return run_ld(); // exit! + + // do all the rest + if(compiler.doit()) + return 1; // LD exit code for all kinds of errors + + // We can generate hybrid ELF and Mach-O binaries + // containing both executable machine code and the goto-binary. + return ld_hybrid_binary(compiler); +} + +int ld_modet::run_ld() +{ + PRECONDITION(!cmdline.parsed_argv.empty()); + + // build new argv + std::vector new_argv; + new_argv.reserve(cmdline.parsed_argv.size()); + for(const auto &a : cmdline.parsed_argv) + new_argv.push_back(a.arg); + + // overwrite argv[0] + new_argv[0] = native_tool_name; + + debug() << "RUN:"; + for(std::size_t i = 0; i < new_argv.size(); i++) + debug() << " " << new_argv[i]; + debug() << eom; + + return run(new_argv[0], new_argv, cmdline.stdin_file, ""); +} + +int ld_modet::ld_hybrid_binary(compilet &compiler) +{ + std::string output_file; + + if(cmdline.isset('o')) + { + output_file = cmdline.get_value('o'); + + if(output_file == "/dev/null") + return EX_OK; + } + else + output_file = "a.out"; + + debug() << "Running " << native_tool_name << " to generate hybrid binary" + << eom; + + // save the goto-cc output file + std::string goto_binary = output_file + goto_binary_tmp_suffix; + + int result; + + result = rename(output_file.c_str(), goto_binary.c_str()); + if(result != 0) + { + error() << "Rename failed: " << std::strerror(errno) << eom; + return result; + } + + result = run_ld(); + + if(result == 0 && cmdline.isset('T')) + { + linker_script_merget ls_merge( + compiler, output_file, goto_binary, cmdline, get_message_handler()); + result = ls_merge.add_linker_script_definitions(); + } + + if(result == 0) + { + std::string native_linker = linker_name(cmdline, base_name); + + result = hybrid_binary( + native_linker, goto_binary, output_file, get_message_handler()); + } + + return result; +} + +/// display command line help +void ld_modet::help_mode() +{ + std::cout << "goto-ld understands the options of " + << "ld plus the following.\n\n"; +} diff --git a/src/goto-cc/ld_mode.h b/src/goto-cc/ld_mode.h new file mode 100644 index 00000000000..4485c325161 --- /dev/null +++ b/src/goto-cc/ld_mode.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Base class for command line interpretation + +Author: CM Wintersteiger + +Date: June 2006 + +\*******************************************************************/ + +/// \file +/// Base class for command line interpretation + +#ifndef CPROVER_GOTO_CC_LD_MODE_H +#define CPROVER_GOTO_CC_LD_MODE_H + +#include "compile.h" +#include "goto_cc_mode.h" + +#include + +#include + +class ld_modet : public goto_cc_modet +{ +public: + int doit() final; + void help_mode() final; + + ld_modet( + goto_cc_cmdlinet &_cmdline, + const std::string &_base_name); + +protected: + gcc_message_handlert gcc_message_handler; + + std::string native_tool_name; + + const std::string goto_binary_tmp_suffix; + + /// \brief call ld with original command line + int run_ld(); + + int ld_hybrid_binary(compilet &compiler); +}; + +#endif // CPROVER_GOTO_CC_LD_MODE_H From 4c2cb3a2198fceae7f00b3f74cc71e8ed9ea191c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 28 May 2018 10:44:22 +0100 Subject: [PATCH 6/6] remove linker mode from gcc_mode --- src/goto-cc/gcc_mode.cpp | 46 +++++++++++----------------------------- src/goto-cc/gcc_mode.h | 1 - 2 files changed, 12 insertions(+), 35 deletions(-) diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp index 47b02e18e04..3fa138a05ca 100644 --- a/src/goto-cc/gcc_mode.cpp +++ b/src/goto-cc/gcc_mode.cpp @@ -107,8 +107,6 @@ gcc_modet::gcc_modet( bool _produce_hybrid_binary): goto_cc_modet(_cmdline, _base_name, gcc_message_handler), produce_hybrid_binary(_produce_hybrid_binary), - act_as_ld(base_name=="ld" || - base_name.find("goto-ld")!=std::string::npos), goto_binary_tmp_suffix(".goto-cc-saved"), // Keys are architectures specified in configt::set_arch(). @@ -327,8 +325,6 @@ int gcc_modet::doit() } native_tool_name= - act_as_ld ? - linker_name(cmdline, base_name) : compiler_name(cmdline, base_name); auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ? @@ -346,10 +342,7 @@ int gcc_modet::doit() // "-v" a) prints the version and b) increases verbosity. // Compilation continues, don't exit! - if(act_as_ld) - std::cout << "GNU ld version 2.16.91 20050610 (goto-cc " CBMC_VERSION - << ")\n"; - else if(act_as_bcc) + if(act_as_bcc) std::cout << "bcc: version 0.16.17 (goto-cc " CBMC_VERSION ")\n"; else std::cout << "gcc version 3.4.4 (goto-cc " CBMC_VERSION ")\n"; @@ -396,14 +389,7 @@ int gcc_modet::doit() return EX_OK; } - if(act_as_ld) - { - if(produce_hybrid_binary) - debug() << "LD mode (hybrid)" << eom; - else - debug() << "LD mode" << eom; - } - else if(act_as_bcc) + if(act_as_bcc) { if(produce_hybrid_binary) debug() << "BCC mode (hybrid)" << eom; @@ -419,9 +405,7 @@ int gcc_modet::doit() } // determine actions to be undertaken - if(act_as_ld) - compiler.mode=compilet::LINK_LIBRARY; - else if(cmdline.isset('S')) + if(cmdline.isset('S')) compiler.mode=compilet::ASSEMBLE_ONLY; else if(cmdline.isset('c')) compiler.mode=compilet::COMPILE_ONLY; @@ -438,13 +422,10 @@ int gcc_modet::doit() // * preprocessing (-E) // * no input files given - if(act_as_ld) - { - } - else if(cmdline.isset('M') || - cmdline.isset("MM") || - cmdline.isset('E') || - !cmdline.have_infile_arg()) + if(cmdline.isset('M') || + cmdline.isset("MM") || + cmdline.isset('E') || + !cmdline.have_infile_arg()) return run_gcc(compiler); // exit! // get configuration @@ -820,7 +801,7 @@ int gcc_modet::run_gcc(const compilet &compiler) for(const auto &a : cmdline.parsed_argv) new_argv.push_back(a.arg); - if(!act_as_ld && compiler.wrote_object_files()) + if(compiler.wrote_object_files()) { // Undefine all __CPROVER macros for the system compiler std::map arities; @@ -953,7 +934,8 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler) std::string goto_binary=*it+goto_binary_tmp_suffix; if(result==0) - result = hybrid_binary(native_tool, goto_binary, *it, get_message_handler()); + result = hybrid_binary( + native_tool, goto_binary, *it, get_message_handler()); } return result; @@ -1047,10 +1029,6 @@ int gcc_modet::asm_output( /// display command line help void gcc_modet::help_mode() { - if(act_as_ld) - std::cout << "goto-ld understands the options of " - << "ld plus the following.\n\n"; - else - std::cout << "goto-cc understands the options of " - << "gcc plus the following.\n\n"; + std::cout << "goto-cc understands the options of " + << "gcc plus the following.\n\n"; } diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h index e0a5fc9f4dd..10cfb9e7bb1 100644 --- a/src/goto-cc/gcc_mode.h +++ b/src/goto-cc/gcc_mode.h @@ -37,7 +37,6 @@ class gcc_modet:public goto_cc_modet const bool produce_hybrid_binary; - const bool act_as_ld; std::string native_tool_name; const std::string goto_binary_tmp_suffix;