Skip to content

Commit 7795e1e

Browse files
authored
Merge pull request #2557 from tautschnig/efi-handling
goto-ld: handle EFI binaries gracefully
2 parents 598c554 + 5f993c1 commit 7795e1e

File tree

5 files changed

+107
-19
lines changed

5 files changed

+107
-19
lines changed

.github/workflows/build-and-test-Xen.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ jobs:
5656
ln -s goto-cc src/goto-cc/goto-g++
5757
5858
- name: Compile Xen with CBMC via one-line-scan, and check for goto-cc section
59-
run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc) -k || true
59+
run: one-line-scan/one-line-scan --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc --no-analysis --trunc-existing --extra-cflags -Wno-error -o CPROVER -j 3 -- make -C xen_4_13 xen -j $(nproc)
6060

6161
- name: Check for goto-cc section in xen-syms binary
6262
run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"

src/goto-cc/hybrid_binary.cpp

Lines changed: 27 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -21,31 +21,37 @@ Author: Michael Tautschnig, 2018
2121
# include <sys/stat.h>
2222
#endif
2323

24+
std::string objcopy_command(const std::string &compiler_or_linker)
25+
{
26+
if(has_suffix(compiler_or_linker, "-ld"))
27+
{
28+
std::string objcopy_cmd = compiler_or_linker;
29+
objcopy_cmd.erase(objcopy_cmd.size() - 2);
30+
objcopy_cmd += "objcopy";
31+
32+
return objcopy_cmd;
33+
}
34+
else
35+
return "objcopy";
36+
}
37+
2438
int hybrid_binary(
2539
const std::string &compiler_or_linker,
2640
const std::string &goto_binary_file,
2741
const std::string &output_file,
2842
bool building_executable,
29-
message_handlert &message_handler)
43+
message_handlert &message_handler,
44+
bool linking_efi)
3045
{
3146
messaget message(message_handler);
3247

33-
int result;
48+
int result = 0;
3449

3550
#if defined(__linux__) || defined(__FreeBSD_kernel__) || defined(__OpenBSD__)
3651
// we can use objcopy for both object files and executables
3752
(void)building_executable;
3853

39-
std::string objcopy_cmd;
40-
41-
if(has_suffix(compiler_or_linker, "-ld"))
42-
{
43-
objcopy_cmd = compiler_or_linker;
44-
objcopy_cmd.erase(objcopy_cmd.size() - 2);
45-
objcopy_cmd += "objcopy";
46-
}
47-
else
48-
objcopy_cmd = "objcopy";
54+
const std::string objcopy_cmd = objcopy_command(compiler_or_linker);
4955

5056
// merge output from gcc or ld with goto-binary using objcopy
5157

@@ -61,7 +67,15 @@ int hybrid_binary(
6167
"--remove-section", "goto-cc",
6268
"--add-section", "goto-cc=" + goto_binary_file, output_file};
6369

64-
result = run(objcopy_argv[0], objcopy_argv);
70+
const int add_section_result = run(objcopy_argv[0], objcopy_argv);
71+
if(add_section_result != 0)
72+
{
73+
if(linking_efi)
74+
message.warning() << "cannot merge EFI binaries: goto-cc section lost"
75+
<< messaget::eom;
76+
else
77+
result = add_section_result;
78+
}
6579
}
6680

6781
// delete the goto binary

src/goto-cc/hybrid_binary.h

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,19 @@ Date: May 2018
2525
/// \param output_file: The name of the object file; the result is stored here.
2626
/// \param building_executable: The \p output_file is an executable.
2727
/// \param message_handler: Message handler for output.
28+
/// \param linking_efi: Set to true if linking x86 EFI binaries to relax error
29+
/// checking.
2830
int hybrid_binary(
2931
const std::string &compiler_or_linker,
3032
const std::string &goto_binary_file,
3133
const std::string &output_file,
3234
bool building_executable,
33-
message_handlert &message_handler);
35+
message_handlert &message_handler,
36+
bool linking_efi = false);
37+
38+
/// Return the name of the objcopy tool matching the chosen compiler or linker
39+
/// command.
40+
/// \param compiler_or_linker: Compiler or linker commmand
41+
std::string objcopy_command(const std::string &compiler_or_linker);
3442

3543
#endif // CPROVER_GOTO_CC_HYBRID_BINARY_H

src/goto-cc/ld_mode.cpp

Lines changed: 62 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,8 @@ int ld_modet::doit()
145145

146146
// We can generate hybrid ELF and Mach-O binaries
147147
// containing both executable machine code and the goto-binary.
148-
return ld_hybrid_binary(compiler.mode == compilet::COMPILE_LINK_EXECUTABLE);
148+
return ld_hybrid_binary(
149+
compiler.mode == compilet::COMPILE_LINK_EXECUTABLE, compiler.object_files);
149150
}
150151

151152
int ld_modet::run_ld()
@@ -170,7 +171,9 @@ int ld_modet::run_ld()
170171
return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
171172
}
172173

173-
int ld_modet::ld_hybrid_binary(bool building_executable)
174+
int ld_modet::ld_hybrid_binary(
175+
bool building_executable,
176+
const std::list<std::string> &object_files)
174177
{
175178
std::string output_file;
176179

@@ -201,6 +204,42 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
201204
return 1;
202205
}
203206

207+
const bool linking_efi = cmdline.get_value('m') == "i386pep";
208+
209+
#ifdef __linux__
210+
if(linking_efi)
211+
{
212+
const std::string objcopy_cmd = objcopy_command(native_tool_name);
213+
214+
for(const auto &object_file : object_files)
215+
{
216+
log.debug() << "stripping goto-cc sections before building EFI binary"
217+
<< messaget::eom;
218+
// create a backup copy
219+
const std::string bin_name = object_file + goto_binary_tmp_suffix;
220+
221+
std::ifstream in(object_file, std::ios::binary);
222+
std::ofstream out(bin_name, std::ios::binary);
223+
out << in.rdbuf();
224+
225+
// remove any existing goto-cc section
226+
std::vector<std::string> objcopy_argv;
227+
228+
objcopy_argv.push_back(objcopy_cmd);
229+
objcopy_argv.push_back("--remove-section=goto-cc");
230+
objcopy_argv.push_back(object_file);
231+
232+
if(run(objcopy_argv[0], objcopy_argv) != 0)
233+
{
234+
log.debug() << "EFI binary preparation: removing goto-cc section failed"
235+
<< messaget::eom;
236+
}
237+
}
238+
}
239+
#else
240+
(void)object_files; // unused parameter
241+
#endif
242+
204243
int result = run_ld();
205244

206245
if(result == 0 && cmdline.isset('T'))
@@ -210,6 +249,25 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
210249
result = ls_merge.add_linker_script_definitions();
211250
}
212251

252+
#ifdef __linux__
253+
if(linking_efi)
254+
{
255+
log.debug() << "arch set with " << object_files.size() << messaget::eom;
256+
for(const auto &object_file : object_files)
257+
{
258+
log.debug() << "EFI binary preparation: restoring object files"
259+
<< messaget::eom;
260+
const std::string bin_name = object_file + goto_binary_tmp_suffix;
261+
const int mv_result = rename(bin_name.c_str(), object_file.c_str());
262+
if(mv_result != 0)
263+
{
264+
log.debug() << "Rename failed: " << std::strerror(errno)
265+
<< messaget::eom;
266+
}
267+
}
268+
}
269+
#endif
270+
213271
if(result == 0)
214272
{
215273
std::string native_linker = linker_name(cmdline, base_name);
@@ -219,7 +277,8 @@ int ld_modet::ld_hybrid_binary(bool building_executable)
219277
goto_binary,
220278
output_file,
221279
building_executable,
222-
message_handler);
280+
message_handler,
281+
linking_efi);
223282
}
224283

225284
return result;

src/goto-cc/ld_mode.h

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,14 @@ class ld_modet : public goto_cc_modet
4040
/// \brief call ld with original command line
4141
int run_ld();
4242

43-
int ld_hybrid_binary(bool);
43+
/// Build an ELF or Mach-O binary containing a goto-cc section.
44+
/// \param building_executable: set to true iff the target file is an
45+
/// executable
46+
/// \param object_files: object files to be linked
47+
/// \return zero, unless an error occurred
48+
int ld_hybrid_binary(
49+
bool building_executable,
50+
const std::list<std::string> &object_files);
4451
};
4552

4653
#endif // CPROVER_GOTO_CC_LD_MODE_H

0 commit comments

Comments
 (0)