cprover
Loading...
Searching...
No Matches
ld_mode.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: LD Mode
4
5Author: CM Wintersteiger, 2006
6
7\*******************************************************************/
8
11
12#include "ld_mode.h"
13
14#ifdef _WIN32
15#define EX_OK 0
16#define EX_USAGE 64
17#define EX_SOFTWARE 70
18#else
19#include <sysexits.h>
20#endif
21
22#include <cstring>
23#include <fstream>
24#include <iostream>
25
26#include <util/cmdline.h>
27#include <util/config.h>
28#include <util/file_util.h>
29#include <util/invariant.h>
30#include <util/run.h>
31
32#include "compile.h"
33#include "goto_cc_cmdline.h"
34#include "hybrid_binary.h"
35#include "linker_script_merge.h"
36
37static std::string
38linker_name(const cmdlinet &cmdline, const std::string &base_name)
39{
40 if(cmdline.isset("native-linker"))
41 return cmdline.get_value("native-linker");
42
43 std::string::size_type pos = base_name.find("goto-ld");
44
45 if(
46 pos == std::string::npos || base_name == "goto-gcc" ||
47 base_name == "goto-ld")
48 return "ld";
49
50 std::string result = base_name;
51 result.replace(pos, 7, "ld");
52
53 return result;
54}
55
57 : goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
58 goto_binary_tmp_suffix(".goto-cc-saved")
59{
60}
61
64{
66
67 // When --help is requested, just reproduce the output of the original
68 // compiler. This is so as not to confuse configure scripts that depend on
69 // particular information (such as the list of supported targets).
70 if(
71 cmdline.isset("help") || cmdline.isset("version") ||
72 cmdline.isset("print-sysroot"))
73 {
74 help();
75 return run_ld();
76 }
77
80
82
83 // determine actions to be undertaken
85
86 // model validation
87 compiler.validate_goto_model = cmdline.isset("validate-goto-model");
88
89 // get configuration
91
92 compiler.object_file_extension = "o";
93
94 if(cmdline.isset('L'))
95 compiler.library_paths = cmdline.get_values('L');
96 // Don't add the system paths!
97
98 if(cmdline.isset('l'))
99 compiler.libraries = cmdline.get_values('l');
100
101 if(cmdline.isset("static"))
102 compiler.libraries.push_back("c");
103
104 if(cmdline.isset('o'))
105 {
106 // given gcc -o file1 -o file2,
107 // gcc will output to file2, not file1
108 compiler.output_file_object = cmdline.get_values('o').back();
109 compiler.output_file_executable = cmdline.get_values('o').back();
110 }
111 else
112 {
113 compiler.output_file_object.clear();
114 compiler.output_file_executable = "a.out";
115 }
116
117 // We now iterate over any input files
118
119 for(const auto &arg : cmdline.parsed_argv)
120 if(arg.is_infile_name)
121 compiler.add_input_file(arg.arg);
122
123 // Revert to gcc in case there is no source to compile
124 // and no binary to link.
125
126 if(compiler.source_files.empty() && compiler.object_files.empty())
127 return run_ld(); // exit!
128
129 // do all the rest
130 if(compiler.doit())
131 return 1; // LD exit code for all kinds of errors
132
133 // We can generate hybrid ELF and Mach-O binaries
134 // containing both executable machine code and the goto-binary.
135 return ld_hybrid_binary(
137}
138
140{
142
143 // build new argv
144 std::vector<std::string> new_argv;
145 new_argv.reserve(cmdline.parsed_argv.size());
146 for(const auto &a : cmdline.parsed_argv)
147 new_argv.push_back(a.arg);
148
149 // overwrite argv[0]
151
153 log.debug() << "RUN:";
154 for(std::size_t i = 0; i < new_argv.size(); i++)
155 log.debug() << " " << new_argv[i];
156 log.debug() << messaget::eom;
157
158 return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
159}
160
163 const std::list<std::string> &object_files)
164{
165 std::string output_file;
166
167 if(cmdline.isset('o'))
168 {
170
171 if(output_file == "/dev/null")
172 return EX_OK;
173 }
174 else
175 output_file = "a.out";
176
178 log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
179 << messaget::eom;
180
181 // save the goto-cc output file
182 std::string goto_binary = output_file + goto_binary_tmp_suffix;
183
184 try
185 {
186 file_rename(output_file, goto_binary);
187 }
188 catch(const cprover_exception_baset &e)
189 {
190 log.error() << "Rename failed: " << e.what() << messaget::eom;
191 return 1;
192 }
193
194 const bool linking_efi = cmdline.get_value('m') == "i386pep";
195
196#ifdef __linux__
197 if(linking_efi)
198 {
199 const std::string objcopy_cmd = objcopy_command(native_tool_name);
200
201 for(const auto &object_file : object_files)
202 {
203 log.debug() << "stripping goto-cc sections before building EFI binary"
204 << messaget::eom;
205 // create a backup copy
206 const std::string bin_name = object_file + goto_binary_tmp_suffix;
207
208 std::ifstream in(object_file, std::ios::binary);
209 std::ofstream out(bin_name, std::ios::binary);
210 out << in.rdbuf();
211
212 // remove any existing goto-cc section
213 std::vector<std::string> objcopy_argv;
214
215 objcopy_argv.push_back(objcopy_cmd);
216 objcopy_argv.push_back("--remove-section=goto-cc");
217 objcopy_argv.push_back(object_file);
218
219 if(run(objcopy_argv[0], objcopy_argv) != 0)
220 {
221 log.debug() << "EFI binary preparation: removing goto-cc section failed"
222 << messaget::eom;
223 }
224 }
225 }
226#else
227 (void)object_files; // unused parameter
228#endif
229
230 int result = run_ld();
231
232 if(result == 0 && cmdline.isset('T'))
233 {
235 output_file, goto_binary, cmdline, message_handler);
236 result = ls_merge.add_linker_script_definitions();
237 }
238
239#ifdef __linux__
240 if(linking_efi)
241 {
242 log.debug() << "arch set with " << object_files.size() << messaget::eom;
243 for(const auto &object_file : object_files)
244 {
245 log.debug() << "EFI binary preparation: restoring object files"
246 << messaget::eom;
247 const std::string bin_name = object_file + goto_binary_tmp_suffix;
248 const int mv_result = rename(bin_name.c_str(), object_file.c_str());
249 if(mv_result != 0)
250 {
251 log.debug() << "Rename failed: " << std::strerror(errno)
252 << messaget::eom;
253 }
254 }
255 }
256#endif
257
258 if(result == 0)
259 {
261
262 result = hybrid_binary(
264 goto_binary,
269 }
270
271 return result;
272}
273
276{
277 std::cout << "goto-ld understands the options of "
278 << "ld plus the following.\n\n";
279}
configt config
Definition config.cpp:25
virtual void clear()
Reset the abstract state.
Definition ai.h:266
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition cmdline.cpp:109
@ LINK_LIBRARY
Definition compile.h:40
@ COMPILE_LINK_EXECUTABLE
Definition compile.h:42
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
virtual std::string what() const
A human readable description of what went wrong.
parsed_argvt parsed_argv
std::string stdin_file
goto_cc_cmdlinet & cmdline
message_handlert & message_handler
const std::string base_name
void help()
display command line help
void help_mode() final
display command line help
Definition ld_mode.cpp:275
const std::string goto_binary_tmp_suffix
Definition ld_mode.h:35
std::string native_tool_name
Definition ld_mode.h:33
gcc_message_handlert gcc_message_handler
Definition ld_mode.h:31
int run_ld()
call ld with original command line
Definition ld_mode.cpp:139
int doit() final
does it.
Definition ld_mode.cpp:63
ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name)
Definition ld_mode.cpp:56
int ld_hybrid_binary(bool building_executable, const std::list< std::string > &object_files)
Build an ELF or Mach-O binary containing a goto-cc section.
Definition ld_mode.cpp:161
Synthesise definitions of symbols that are defined in linker scripts.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition message.cpp:105
@ M_ERROR
Definition message.h:170
static eomt eom
Definition message.h:297
Compile and link source and object files.
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
Definition gcc_mode.cpp:75
Command line interpretation for goto-cc.
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, bool linking_efi)
Merges a goto binary into an object file (e.g.
std::string objcopy_command(const std::string &compiler_or_linker)
Return the name of the objcopy tool matching the chosen compiler or linker command.
Create hybrid binary with goto-binary section.
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
Definition ld_mode.cpp:38
Base class for command line interpretation.
Merge linker script-defined symbols into a goto-program.
literalt pos(literalt a)
Definition literal.h:194
int run(const std::string &what, const std::vector< std::string > &argv)
Definition run.cpp:48
#define PRECONDITION(CONDITION)
Definition invariant.h:463