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  // model validation
100  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
101 
102  // get configuration
103  config.set(cmdline);
104 
105  compiler.object_file_extension = "o";
106 
107  if(cmdline.isset('L'))
108  compiler.library_paths = cmdline.get_values('L');
109  // Don't add the system paths!
110 
111  if(cmdline.isset('l'))
112  compiler.libraries = cmdline.get_values('l');
113 
114  if(cmdline.isset("static"))
115  compiler.libraries.push_back("c");
116 
117  if(cmdline.isset('o'))
118  {
119  // given gcc -o file1 -o file2,
120  // gcc will output to file2, not file1
121  compiler.output_file_object = cmdline.get_values('o').back();
122  compiler.output_file_executable = cmdline.get_values('o').back();
123  }
124  else
125  {
126  compiler.output_file_object.clear();
127  compiler.output_file_executable = "a.out";
128  }
129 
130  // We now iterate over any input files
131 
132  for(const auto &arg : cmdline.parsed_argv)
133  if(arg.is_infile_name)
134  compiler.add_input_file(arg.arg);
135 
136  // Revert to gcc in case there is no source to compile
137  // and no binary to link.
138 
139  if(compiler.source_files.empty() && compiler.object_files.empty())
140  return run_ld(); // exit!
141 
142  // do all the rest
143  if(compiler.doit())
144  return 1; // LD exit code for all kinds of errors
145 
146  // We can generate hybrid ELF and Mach-O binaries
147  // containing both executable machine code and the goto-binary.
148  return ld_hybrid_binary(compiler);
149 }
150 
152 {
153  PRECONDITION(!cmdline.parsed_argv.empty());
154 
155  // build new argv
156  std::vector<std::string> new_argv;
157  new_argv.reserve(cmdline.parsed_argv.size());
158  for(const auto &a : cmdline.parsed_argv)
159  new_argv.push_back(a.arg);
160 
161  // overwrite argv[0]
162  new_argv[0] = native_tool_name;
163 
164  debug() << "RUN:";
165  for(std::size_t i = 0; i < new_argv.size(); i++)
166  debug() << " " << new_argv[i];
167  debug() << eom;
168 
169  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
170 }
171 
173 {
174  std::string output_file;
175 
176  if(cmdline.isset('o'))
177  {
178  output_file = cmdline.get_value('o');
179 
180  if(output_file == "/dev/null")
181  return EX_OK;
182  }
183  else
184  output_file = "a.out";
185 
186  debug() << "Running " << native_tool_name << " to generate hybrid binary"
187  << eom;
188 
189  // save the goto-cc output file
190  std::string goto_binary = output_file + goto_binary_tmp_suffix;
191 
192  try
193  {
194  file_rename(output_file, goto_binary);
195  }
196  catch(const cprover_exception_baset &e)
197  {
198  error() << "Rename failed: " << e.what() << eom;
199  return 1;
200  }
201 
202  int result = run_ld();
203 
204  if(result == 0 && cmdline.isset('T'))
205  {
206  linker_script_merget ls_merge(
207  compiler, output_file, goto_binary, cmdline, get_message_handler());
209  }
210 
211  if(result == 0)
212  {
213  std::string native_linker = linker_name(cmdline, base_name);
214 
216  native_linker,
217  goto_binary,
218  output_file,
221  }
222 
223  return result;
224 }
225 
228 {
229  std::cout << "goto-ld understands the options of "
230  << "ld plus the following.\n\n";
231 }
ld_modet::gcc_message_handler
gcc_message_handlert gcc_message_handler
Definition: ld_mode.h:34
tempfile.h
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:64
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:48
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:68
pos
literalt pos(literalt a)
Definition: literal.h:194
ld_modet::help_mode
void help_mode() final
display command line help
Definition: ld_mode.cpp:227
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
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:57
invariant.h
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
compilet::libraries
std::list< std::string > libraries
Definition: compile.h:50
linker_script_merget
Synthesise definitions of symbols that are defined in linker scripts.
Definition: linker_script_merge.h:63
goto_cc_modet::base_name
const std::string base_name
Definition: goto_cc_mode.h:38
messaget::eom
static eomt eom
Definition: message.h:297
run.h
tempdir.h
compilet::LINK_LIBRARY
@ LINK_LIBRARY
Definition: compile.h:42
ld_modet::native_tool_name
std::string native_tool_name
Definition: ld_mode.h:36
compilet::validate_goto_model
bool validate_goto_model
Definition: compile.h:37
expr.h
json_parser.h
ld_mode.h
Base class for command line interpretation.
cmdlinet
Definition: cmdline.h:21
compilet::output_file_object
std::string output_file_object
Definition: compile.h:58
ld_modet::ld_modet
ld_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name)
Definition: ld_mode.cpp:71
compilet::object_files
std::list< std::string > object_files
Definition: compile.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
compilet::mode
enum compilet::@2 mode
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:55
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
ld_modet::ld_hybrid_binary
int ld_hybrid_binary(compilet &compiler)
Definition: ld_mode.cpp:172
cprover_exception_baset::what
virtual std::string what() const =0
A human readable description of what went wrong.
messaget::M_ERROR
@ M_ERROR
Definition: message.h:170
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
compilet::library_paths
std::list< std::string > library_paths
Definition: compile.h:47
hybrid_binary
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)
Merges a goto binary into an object file (e.g.
Definition: hybrid_binary.cpp:24
compilet::object_file_extension
std::string object_file_extension
Definition: compile.h:54
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
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:44
read_goto_binary.h
Read Goto Programs.
compilet::add_input_file
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:171
config
configt config
Definition: config.cpp:24
hybrid_binary.h
Create hybrid binary with goto-binary section.
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
ld_modet::goto_binary_tmp_suffix
const std::string goto_binary_tmp_suffix
Definition: ld_mode.h:38
suffix.h
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
goto_cc_modet
Definition: goto_cc_mode.h:22
config.h
messaget::debug
mstreamt & debug() const
Definition: message.h:429
goto_cc_modet::help
void help()
display command line help
Definition: goto_cc_mode.cpp:47
compilet
Definition: compile.h:27
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:104
ld_modet::run_ld
int run_ld()
call ld with original command line
Definition: ld_mode.cpp:151
cmdlinet::get_values
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:108
goto_cc_cmdlinet
Definition: goto_cc_cmdline.h:20
c_types.h
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25
file_rename
void file_rename(const std::string &old_path, const std::string &new_path)
Rename a file.
Definition: file_util.cpp:240