cprover
ld_mode.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: LD Mode
4 
5 Author: 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 <algorithm>
23 #include <cstddef>
24 #include <cstdio>
25 #include <cstring>
26 #include <fstream>
27 #include <iostream>
28 #include <iterator>
29 #include <numeric>
30 #include <sstream>
31 
32 #include <json/json_parser.h>
33 
34 #include <util/arith_tools.h>
35 #include <util/c_types.h>
36 #include <util/config.h>
37 #include <util/expr.h>
38 #include <util/get_base_name.h>
39 #include <util/invariant.h>
40 #include <util/prefix.h>
41 #include <util/replace_symbol.h>
42 #include <util/run.h>
43 #include <util/suffix.h>
44 #include <util/tempdir.h>
45 #include <util/tempfile.h>
46 
48 
49 #include "hybrid_binary.h"
50 #include "linker_script_merge.h"
51 
52 static std::string
53 linker_name(const cmdlinet &cmdline, const std::string &base_name)
54 {
55  if(cmdline.isset("native-linker"))
56  return cmdline.get_value("native-linker");
57 
58  std::string::size_type pos = base_name.find("goto-ld");
59 
60  if(
61  pos == std::string::npos || base_name == "goto-gcc" ||
62  base_name == "goto-ld")
63  return "ld";
64 
65  std::string result = base_name;
66  result.replace(pos, 7, "ld");
67 
68  return result;
69 }
70 
71 ld_modet::ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name)
72  : goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
73  goto_binary_tmp_suffix(".goto-cc-saved")
74 {
75 }
76 
79 {
80  if(cmdline.isset("help"))
81  {
82  help();
83  return EX_OK;
84  }
85 
87 
88  if(cmdline.isset("version") || cmdline.isset("print-sysroot"))
89  return run_ld();
90 
93 
94  compilet compiler(cmdline, gcc_message_handler, false);
95 
96  // determine actions to be undertaken
97  compiler.mode = compilet::LINK_LIBRARY;
98 
99  // get configuration
100  config.set(cmdline);
101 
102  compiler.object_file_extension = "o";
103 
104  if(cmdline.isset('L'))
105  compiler.library_paths = cmdline.get_values('L');
106  // Don't add the system paths!
107 
108  if(cmdline.isset('l'))
109  compiler.libraries = cmdline.get_values('l');
110 
111  if(cmdline.isset("static"))
112  compiler.libraries.push_back("c");
113 
114  if(cmdline.isset('o'))
115  {
116  // given gcc -o file1 -o file2,
117  // gcc will output to file2, not file1
118  compiler.output_file_object = cmdline.get_values('o').back();
119  compiler.output_file_executable = cmdline.get_values('o').back();
120  }
121  else
122  {
123  compiler.output_file_object = "";
124  compiler.output_file_executable = "a.out";
125  }
126 
127  // We now iterate over any input files
128 
129  for(const auto &arg : cmdline.parsed_argv)
130  if(arg.is_infile_name)
131  compiler.add_input_file(arg.arg);
132 
133  // Revert to gcc in case there is no source to compile
134  // and no binary to link.
135 
136  if(compiler.source_files.empty() && compiler.object_files.empty())
137  return run_ld(); // exit!
138 
139  // do all the rest
140  if(compiler.doit())
141  return 1; // LD exit code for all kinds of errors
142 
143  // We can generate hybrid ELF and Mach-O binaries
144  // containing both executable machine code and the goto-binary.
145  return ld_hybrid_binary(compiler);
146 }
147 
149 {
150  PRECONDITION(!cmdline.parsed_argv.empty());
151 
152  // build new argv
153  std::vector<std::string> new_argv;
154  new_argv.reserve(cmdline.parsed_argv.size());
155  for(const auto &a : cmdline.parsed_argv)
156  new_argv.push_back(a.arg);
157 
158  // overwrite argv[0]
159  new_argv[0] = native_tool_name;
160 
161  debug() << "RUN:";
162  for(std::size_t i = 0; i < new_argv.size(); i++)
163  debug() << " " << new_argv[i];
164  debug() << eom;
165 
166  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
167 }
168 
170 {
171  std::string output_file;
172 
173  if(cmdline.isset('o'))
174  {
175  output_file = cmdline.get_value('o');
176 
177  if(output_file == "/dev/null")
178  return EX_OK;
179  }
180  else
181  output_file = "a.out";
182 
183  debug() << "Running " << native_tool_name << " to generate hybrid binary"
184  << eom;
185 
186  // save the goto-cc output file
187  std::string goto_binary = output_file + goto_binary_tmp_suffix;
188 
189  int result;
190 
191  result = rename(output_file.c_str(), goto_binary.c_str());
192  if(result != 0)
193  {
194  error() << "Rename failed: " << std::strerror(errno) << eom;
195  return result;
196  }
197 
198  result = run_ld();
199 
200  if(result == 0 && cmdline.isset('T'))
201  {
202  linker_script_merget ls_merge(
203  compiler, output_file, goto_binary, cmdline, get_message_handler());
205  }
206 
207  if(result == 0)
208  {
209  std::string native_linker = linker_name(cmdline, base_name);
210 
212  native_linker, goto_binary, output_file, get_message_handler());
213  }
214 
215  return result;
216 }
217 
220 {
221  std::cout << "goto-ld understands the options of "
222  << "ld plus the following.\n\n";
223 }
ld_modet::gcc_message_handler
gcc_message_handlert gcc_message_handler
Definition: ld_mode.h:35
tempfile.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
linker_script_merge.h
Merge linker script-defined symbols into a goto-program.
arith_tools.h
goto_cc_cmdlinet::parsed_argv
parsed_argvt parsed_argv
Definition: goto_cc_cmdline.h:63
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:27
linker_name
static std::string linker_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: ld_mode.cpp:53
goto_cc_cmdlinet::stdin_file
std::string stdin_file
Definition: goto_cc_cmdline.h:74
pos
literalt pos(literalt a)
Definition: literal.h:193
ld_modet::help_mode
void help_mode() final
display command line help
Definition: ld_mode.cpp:219
linker_script_merget::add_linker_script_definitions
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
Definition: linker_script_merge.cpp:28
replace_symbol.h
prefix.h
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:47
invariant.h
linker_script_merget
Synthesise definitions of symbols that are defined in linker scripts.
Definition: linker_script_merge.h:65
goto_cc_modet::base_name
const std::string base_name
Definition: goto_cc_mode.h:38
messaget::eom
static eomt eom
Definition: message.h:284
run.h
tempdir.h
ld_modet::native_tool_name
std::string native_tool_name
Definition: ld_mode.h:37
expr.h
json_parser.h
ld_mode.h
cmdlinet
Definition: cmdline.h:19
ld_modet::ld_modet
ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name)
Definition: ld_mode.cpp:71
messaget::result
mstreamt & result() const
Definition: message.h:396
messaget::error
mstreamt & error() const
Definition: message.h:386
hybrid_binary
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.
Definition: hybrid_binary.cpp:19
ld_modet::ld_hybrid_binary
int ld_hybrid_binary(compilet &compiler)
Definition: ld_mode.cpp:169
messaget::M_ERROR
Definition: message.h:160
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:45
get_base_name.h
goto_cc_modet::cmdline
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:37
ld_modet::doit
int doit() final
does it.
Definition: ld_mode.cpp:78
read_goto_binary.h
config
configt config
Definition: config.cpp:24
hybrid_binary.h
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
ld_modet::goto_binary_tmp_suffix
const std::string goto_binary_tmp_suffix
Definition: ld_mode.h:39
suffix.h
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
goto_cc_modet
Definition: goto_cc_mode.h:21
compilet::LINK_LIBRARY
Definition: compile.h:40
config.h
messaget::debug
mstreamt & debug() const
Definition: message.h:416
goto_cc_modet::help
virtual void help()
display command line help
Definition: goto_cc_mode.cpp:47
compilet
Definition: compile.h:25
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
messaget::eval_verbosity
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:98
ld_modet::run_ld
int run_ld()
call ld with original command line
Definition: ld_mode.cpp:148
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
goto_cc_cmdlinet
Definition: goto_cc_cmdline.h:19
c_types.h