cprover
hybrid_binary.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Create hybrid binary with goto-binary section
4 
5 Author: Michael Tautschnig, 2018
6 
7 \*******************************************************************/
8 
11 
12 #include "hybrid_binary.h"
13 
14 #include <util/run.h>
15 #include <util/suffix.h>
16 
17 #include <cstring>
18 
20  const std::string &compiler_or_linker,
21  const std::string &goto_binary_file,
22  const std::string &output_file,
24 {
25  messaget message(message_handler);
26 
27  int result;
28 
29 #if defined(__linux__) || defined(__FreeBSD_kernel__)
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 }
int run(const std::string &what, const std::vector< std::string > &argv, const std::string &std_input, const std::string &std_output, const std::string &std_error)
Definition: run.cpp:82
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Create hybrid binary with goto-binary section.
mstreamt & error() const
Definition: message.h:302
int hybrid_binary(const std::string &compiler_or_linker, const std::string &goto_binary_file, const std::string &output_file, message_handlert &message_handler)
Merges a goto binary into an object file (e.g.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
mstreamt & debug() const
Definition: message.h:332