Skip to content

Commit 524091f

Browse files
kroeningkroening
committed
factor out creation of hybrid binaries
1 parent b9127f3 commit 524091f

File tree

4 files changed

+146
-79
lines changed

4 files changed

+146
-79
lines changed

‎src/goto-cc/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ SRC = armcc_cmdline.cpp \
1212
goto_cc_languages.cpp \
1313
goto_cc_main.cpp \
1414
goto_cc_mode.cpp \
15+
hybrid_binary.cpp \
1516
ld_cmdline.cpp \
1617
linker_script_merge.cpp \
1718
ms_cl_cmdline.cpp \

‎src/goto-cc/gcc_mode.cpp‎

Lines changed: 10 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ Author: CM Wintersteiger, 2006
4848

4949
#include <cbmc/version.h>
5050

51+
#include "hybrid_binary.h"
5152
#include "linker_script_merge.h"
5253

5354
static std::string compiler_name(
@@ -922,19 +923,6 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
922923
goto_binaries.push_back(bin_name);
923924
}
924925

925-
std::string objcopy_cmd;
926-
if(has_suffix(linker_name(cmdline, base_name), "-ld"))
927-
{
928-
objcopy_cmd=linker_name(cmdline, base_name);
929-
objcopy_cmd.erase(objcopy_cmd.size()-2);
930-
}
931-
else if(has_suffix(compiler_name(cmdline, base_name), "-gcc"))
932-
{
933-
objcopy_cmd=compiler_name(cmdline, base_name);
934-
objcopy_cmd.erase(objcopy_cmd.size()-3);
935-
}
936-
objcopy_cmd+="objcopy";
937-
938926
int result=run_gcc(compiler);
939927

940928
if(result==0 &&
@@ -948,81 +936,24 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
948936
result=ls_merge.add_linker_script_definitions();
949937
}
950938

939+
std::string native_tool;
940+
941+
if(has_suffix(linker_name(cmdline, base_name), "-ld"))
942+
native_tool=linker_name(cmdline, base_name);
943+
else if(has_suffix(compiler_name(cmdline, base_name), "-gcc"))
944+
native_tool=compiler_name(cmdline, base_name);
945+
951946
// merge output from gcc with goto-binaries
952947
// using objcopy, or do cleanup if an earlier call failed
953948
for(std::list<std::string>::const_iterator
954949
it=output_files.begin();
955950
it!=output_files.end();
956951
it++)
957952
{
958-
debug() << "merging " << *it << eom;
959-
std::string saved=*it+goto_binary_tmp_suffix;
960-
961-
#ifdef __linux__
962-
if(result==0 && !cmdline.isset('c'))
963-
{
964-
// remove any existing goto-cc section
965-
std::vector<std::string> objcopy_argv;
966-
967-
objcopy_argv.push_back(objcopy_cmd);
968-
objcopy_argv.push_back("--remove-section=goto-cc");
969-
objcopy_argv.push_back(*it);
970-
971-
result=run(objcopy_argv[0], objcopy_argv, "", "");
972-
}
953+
std::string goto_binary=*it+goto_binary_tmp_suffix;
973954

974955
if(result==0)
975-
{
976-
// now add goto-binary as goto-cc section
977-
std::vector<std::string> objcopy_argv;
978-
979-
objcopy_argv.push_back(objcopy_cmd);
980-
objcopy_argv.push_back("--add-section");
981-
objcopy_argv.push_back("goto-cc="+saved);
982-
objcopy_argv.push_back(*it);
983-
984-
result=run(objcopy_argv[0], objcopy_argv, "", "");
985-
}
986-
987-
int remove_result=remove(saved.c_str());
988-
if(remove_result!=0)
989-
{
990-
error() << "Remove failed: " << std::strerror(errno) << eom;
991-
if(result==0)
992-
result=remove_result;
993-
}
994-
995-
#elif defined(__APPLE__)
996-
// Mac
997-
if(result==0)
998-
{
999-
std::vector<std::string> lipo_argv;
1000-
1001-
// now add goto-binary as hppa7100LC section
1002-
lipo_argv.push_back("lipo");
1003-
lipo_argv.push_back(*it);
1004-
lipo_argv.push_back("-create");
1005-
lipo_argv.push_back("-arch");
1006-
lipo_argv.push_back("hppa7100LC");
1007-
lipo_argv.push_back(saved);
1008-
lipo_argv.push_back("-output");
1009-
lipo_argv.push_back(*it);
1010-
1011-
result=run(lipo_argv[0], lipo_argv, "", "");
1012-
}
1013-
1014-
int remove_result=remove(saved.c_str());
1015-
if(remove_result!=0)
1016-
{
1017-
error() << "Remove failed: " << std::strerror(errno) << eom;
1018-
if(result==0)
1019-
result=remove_result;
1020-
}
1021-
1022-
#else
1023-
error() << "binary merging not implemented for this platform" << eom;
1024-
return 1;
1025-
#endif
956+
result = hybrid_binary(native_tool, goto_binary, *it, get_message_handler());
1026957
}
1027958

1028959
return result;

‎src/goto-cc/hybrid_binary.cpp‎

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/*******************************************************************\
2+
3+
Module: Create hybrid binary with goto-binary section
4+
5+
Author: Michael Tautschnig, 2018
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Create hybrid binary with goto-binary section
11+
12+
#include "hybrid_binary.h"
13+
14+
#include <util/run.h>
15+
#include <util/suffix.h>
16+
17+
#include <cstring>
18+
19+
int hybrid_binary(
20+
const std::string &compiler_or_linker,
21+
const std::string &goto_binary_file,
22+
const std::string &output_file,
23+
message_handlert &message_handler)
24+
{
25+
messaget message(message_handler);
26+
27+
int result;
28+
29+
#ifdef __linux__
30+
std::string objcopy_cmd;
31+
32+
if(has_suffix(compiler_or_linker, "-ld"))
33+
{
34+
objcopy_cmd = compiler_or_linker;
35+
objcopy_cmd.erase(objcopy_cmd.size() - 2);
36+
objcopy_cmd += "objcopy";
37+
}
38+
else
39+
objcopy_cmd = "objcopy";
40+
41+
// merge output from gcc or ld with goto-binary using objcopy
42+
43+
message.debug() << "merging " << output_file << " and " << goto_binary_file
44+
<< " using " << objcopy_cmd
45+
<< messaget::eom;
46+
47+
{
48+
// Now add goto-binary as goto-cc section.
49+
// Remove if it exists before, or otherwise adding fails.
50+
std::vector<std::string> objcopy_argv = {
51+
objcopy_cmd,
52+
"--remove-section", "goto-cc",
53+
"--add-section", "goto-cc=" + goto_binary_file, output_file};
54+
55+
result = run(objcopy_argv[0], objcopy_argv, "", "");
56+
}
57+
58+
// delete the goto binary
59+
int remove_result = remove(goto_binary_file.c_str());
60+
if(remove_result != 0)
61+
{
62+
message.error() << "Remove failed: " << std::strerror(errno)
63+
<< messaget::eom;
64+
if(result == 0)
65+
result = remove_result;
66+
}
67+
68+
#elif defined(__APPLE__)
69+
// Mac
70+
71+
message.debug() << "merging " << output_file << " and " << goto_binary_file
72+
<< " using lipo"
73+
<< messaget::eom;
74+
75+
{
76+
// Add goto-binary as hppa7100LC section.
77+
// This overwrites if there's already one.
78+
std::vector<std::string> lipo_argv = {
79+
"lipo", output_file, "-create", "-arch", "hppa7100LC", goto_binary_file,
80+
"-output", output_file };
81+
82+
result = run(lipo_argv[0], lipo_argv, "", "");
83+
}
84+
85+
// delete the goto binary
86+
int remove_result = remove(goto_binary_file.c_str());
87+
if(remove_result != 0)
88+
{
89+
message.error() << "Remove failed: " << std::strerror(errno)
90+
<< messaget::eom;
91+
if(result == 0)
92+
result = remove_result;
93+
}
94+
95+
#else
96+
message.error() << "binary merging not implemented for this platform"
97+
<< messaget::eom;
98+
result = 1;
99+
#endif
100+
101+
return result;
102+
}

‎src/goto-cc/hybrid_binary.h‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*******************************************************************\
2+
3+
Module: Create hybrid binary with goto-binary section
4+
5+
Author: Daniel Kroening
6+
7+
Date: May 2018
8+
9+
\*******************************************************************/
10+
11+
/// \file
12+
/// Create hybrid binary with goto-binary section
13+
14+
#ifndef CPROVER_GOTO_CC_HYBRID_BINARY_H
15+
#define CPROVER_GOTO_CC_HYBRID_BINARY_H
16+
17+
#include <util/message.h>
18+
19+
#include <string>
20+
21+
/// \brief Merges a goto binary into an object file (e.g. ELF)
22+
/// \param compiler_or_linker The name of the gcc or ld executable,
23+
/// used to deduce the name of objcopy
24+
/// \param goto_binary_file The file name of the goto binary
25+
/// \param output_file The name of the object file; the result is
26+
/// stored here.
27+
int hybrid_binary(
28+
const std::string &compiler_or_linker,
29+
const std::string &goto_binary_file,
30+
const std::string &output_file,
31+
message_handlert &);
32+
33+
#endif // CPROVER_GOTO_CC_HYBRID_BINARY_H

0 commit comments

Comments
 (0)