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
56ld_modet::ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name)
57 : goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
58 goto_binary_tmp_suffix(".goto-cc-saved")
59{
60}
61
64{
65 if(cmdline.isset("help"))
66 {
67 help();
68 return EX_OK;
69 }
70
72
73 if(cmdline.isset("version") || cmdline.isset("print-sysroot"))
74 return run_ld();
75
78
79 compilet compiler(cmdline, gcc_message_handler, false);
80
81 // determine actions to be undertaken
83
84 // model validation
85 compiler.validate_goto_model = cmdline.isset("validate-goto-model");
86
87 // get configuration
89
90 compiler.object_file_extension = "o";
91
92 if(cmdline.isset('L'))
93 compiler.library_paths = cmdline.get_values('L');
94 // Don't add the system paths!
95
96 if(cmdline.isset('l'))
97 compiler.libraries = cmdline.get_values('l');
98
99 if(cmdline.isset("static"))
100 compiler.libraries.push_back("c");
101
102 if(cmdline.isset('o'))
103 {
104 // given gcc -o file1 -o file2,
105 // gcc will output to file2, not file1
106 compiler.output_file_object = cmdline.get_values('o').back();
107 compiler.output_file_executable = cmdline.get_values('o').back();
108 }
109 else
110 {
111 compiler.output_file_object.clear();
112 compiler.output_file_executable = "a.out";
113 }
114
115 // We now iterate over any input files
116
117 for(const auto &arg : cmdline.parsed_argv)
118 if(arg.is_infile_name)
119 compiler.add_input_file(arg.arg);
120
121 // Revert to gcc in case there is no source to compile
122 // and no binary to link.
123
124 if(compiler.source_files.empty() && compiler.object_files.empty())
125 return run_ld(); // exit!
126
127 // do all the rest
128 if(compiler.doit())
129 return 1; // LD exit code for all kinds of errors
130
131 // We can generate hybrid ELF and Mach-O binaries
132 // containing both executable machine code and the goto-binary.
133 return ld_hybrid_binary(
135}
136
138{
140
141 // build new argv
142 std::vector<std::string> new_argv;
143 new_argv.reserve(cmdline.parsed_argv.size());
144 for(const auto &a : cmdline.parsed_argv)
145 new_argv.push_back(a.arg);
146
147 // overwrite argv[0]
148 new_argv[0] = native_tool_name;
149
151 log.debug() << "RUN:";
152 for(std::size_t i = 0; i < new_argv.size(); i++)
153 log.debug() << " " << new_argv[i];
154 log.debug() << messaget::eom;
155
156 return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
157}
158
160 bool building_executable,
161 const std::list<std::string> &object_files)
162{
163 std::string output_file;
164
165 if(cmdline.isset('o'))
166 {
167 output_file = cmdline.get_value('o');
168
169 if(output_file == "/dev/null")
170 return EX_OK;
171 }
172 else
173 output_file = "a.out";
174
176 log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
177 << messaget::eom;
178
179 // save the goto-cc output file
180 std::string goto_binary = output_file + goto_binary_tmp_suffix;
181
182 try
183 {
184 file_rename(output_file, goto_binary);
185 }
186 catch(const cprover_exception_baset &e)
187 {
188 log.error() << "Rename failed: " << e.what() << messaget::eom;
189 return 1;
190 }
191
192 const bool linking_efi = cmdline.get_value('m') == "i386pep";
193
194#ifdef __linux__
195 if(linking_efi)
196 {
197 const std::string objcopy_cmd = objcopy_command(native_tool_name);
198
199 for(const auto &object_file : object_files)
200 {
201 log.debug() << "stripping goto-cc sections before building EFI binary"
202 << messaget::eom;
203 // create a backup copy
204 const std::string bin_name = object_file + goto_binary_tmp_suffix;
205
206 std::ifstream in(object_file, std::ios::binary);
207 std::ofstream out(bin_name, std::ios::binary);
208 out << in.rdbuf();
209
210 // remove any existing goto-cc section
211 std::vector<std::string> objcopy_argv;
212
213 objcopy_argv.push_back(objcopy_cmd);
214 objcopy_argv.push_back("--remove-section=goto-cc");
215 objcopy_argv.push_back(object_file);
216
217 if(run(objcopy_argv[0], objcopy_argv) != 0)
218 {
219 log.debug() << "EFI binary preparation: removing goto-cc section failed"
220 << messaget::eom;
221 }
222 }
223 }
224#else
225 (void)object_files; // unused parameter
226#endif
227
228 int result = run_ld();
229
230 if(result == 0 && cmdline.isset('T'))
231 {
232 linker_script_merget ls_merge(
233 output_file, goto_binary, cmdline, message_handler);
234 result = ls_merge.add_linker_script_definitions();
235 }
236
237#ifdef __linux__
238 if(linking_efi)
239 {
240 log.debug() << "arch set with " << object_files.size() << messaget::eom;
241 for(const auto &object_file : object_files)
242 {
243 log.debug() << "EFI binary preparation: restoring object files"
244 << messaget::eom;
245 const std::string bin_name = object_file + goto_binary_tmp_suffix;
246 const int mv_result = rename(bin_name.c_str(), object_file.c_str());
247 if(mv_result != 0)
248 {
249 log.debug() << "Rename failed: " << std::strerror(errno)
250 << messaget::eom;
251 }
252 }
253 }
254#endif
255
256 if(result == 0)
257 {
258 std::string native_linker = linker_name(cmdline, base_name);
259
260 result = hybrid_binary(
261 native_linker,
262 goto_binary,
263 output_file,
264 building_executable,
266 linking_efi);
267 }
268
269 return result;
270}
271
274{
275 std::cout << "goto-ld understands the options of "
276 << "ld plus the following.\n\n";
277}
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
std::string output_file_object
Definition: compile.h:54
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:173
std::list< std::string > libraries
Definition: compile.h:48
std::list< std::string > object_files
Definition: compile.h:47
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:60
std::list< std::string > source_files
Definition: compile.h:46
std::string object_file_extension
Definition: compile.h:50
bool validate_goto_model
Definition: compile.h:35
enum compilet::@3 mode
std::list< std::string > library_paths
Definition: compile.h:45
std::string output_file_executable
Definition: compile.h:51
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
Base class for exceptions thrown in the cprover project.
virtual std::string what() const =0
A human readable description of what went wrong.
parsed_argvt parsed_argv
std::string stdin_file
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:38
message_handlert & message_handler
Definition: goto_cc_mode.h:40
const std::string base_name
Definition: goto_cc_mode.h:39
void help()
display command line help
void help_mode() final
display command line help
Definition: ld_mode.cpp:273
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:137
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:159
Synthesise definitions of symbols that are defined in linker scripts.
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
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.
configt config
Definition: config.cpp:25
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
Definition: file_util.cpp:240
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