cprover
as_mode.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Assembler Mode
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
11 
12 #include "as_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 <fstream>
23 #include <iostream>
24 #include <cstring>
25 
26 #include <util/config.h>
27 #include <util/cout_message.h>
28 #include <util/get_base_name.h>
29 #include <util/run.h>
30 #include <util/tempdir.h>
31 #include <util/version.h>
32 
33 #include "compile.h"
34 
35 static std::string assembler_name(
36  const cmdlinet &cmdline,
37  const std::string &base_name)
38 {
39  if(cmdline.isset("native-assembler"))
40  return cmdline.get_value("native-assembler");
41 
42  if(base_name=="as86" ||
43  base_name.find("goto-as86")!=std::string::npos)
44  return "as86";
45 
46  std::string::size_type pos=base_name.find("goto-as");
47 
48  if(pos==std::string::npos)
49  return "as";
50 
51  std::string result=base_name;
52  result.replace(pos, 7, "as");
53 
54  return result;
55 }
56 
58  goto_cc_cmdlinet &_cmdline,
59  const std::string &_base_name,
60  bool _produce_hybrid_binary):
61  goto_cc_modet(_cmdline, _base_name, message_handler),
62  produce_hybrid_binary(_produce_hybrid_binary),
63  native_tool_name(assembler_name(cmdline, base_name))
64 {
65 }
66 
69 {
70  if(cmdline.isset('?') ||
71  cmdline.isset("help"))
72  {
73  help();
74  return EX_OK;
75  }
76 
77  bool act_as_as86=
78  base_name=="as86" ||
79  base_name.find("goto-as86")!=std::string::npos;
80 
81  if((cmdline.isset('v') && act_as_as86) ||
82  cmdline.isset("version"))
83  {
84  if(act_as_as86)
85  status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
86  << eom;
87  else
88  status() << "GNU assembler version 2.20.51.0.7 20100318"
89  << " (goto-cc " << CBMC_VERSION << ")" << eom;
90 
91  status()
92  << '\n'
93  << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
94  << "CBMC version: " << CBMC_VERSION << '\n'
95  << "Architecture: " << config.this_architecture() << '\n'
96  << "OS: " << config.this_operating_system() << eom;
97 
98  return EX_OK; // Exit!
99  }
100 
101  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
104  cmdline.get_value("verbosity"), default_verbosity, message_handler);
105 
106  if(act_as_as86)
107  {
109  debug() << "AS86 mode (hybrid)" << eom;
110  else
111  debug() << "AS86 mode" << eom;
112  }
113  else
114  {
116  debug() << "AS mode (hybrid)" << eom;
117  else
118  debug() << "AS mode" << eom;
119  }
120 
121  // get configuration
122  config.set(cmdline);
123 
124  // determine actions to be undertaken
125  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
126 
127  if(cmdline.isset('b')) // as86 only
128  {
130  debug() << "Compiling and linking an executable" << eom;
131  }
132  else
133  {
134  compiler.mode=compilet::COMPILE_LINK;
135  debug() << "Compiling and linking a library" << eom;
136  }
137 
139 
140  compiler.object_file_extension="o";
141 
142  if(cmdline.isset('o'))
143  {
144  compiler.output_file_object=cmdline.get_value('o');
145  compiler.output_file_executable=cmdline.get_value('o');
146  }
147  else if(cmdline.isset('b')) // as86 only
148  {
149  compiler.output_file_object=cmdline.get_value('b');
150  compiler.output_file_executable=cmdline.get_value('b');
151  }
152  else
153  {
154  compiler.output_file_object="a.out";
155  compiler.output_file_executable="a.out";
156  }
157 
158  // We now iterate over any input files
159 
160  temp_dirt temp_dir("goto-cc-XXXXXX");
161 
162  for(goto_cc_cmdlinet::parsed_argvt::iterator
163  arg_it=cmdline.parsed_argv.begin();
164  arg_it!=cmdline.parsed_argv.end();
165  arg_it++)
166  {
167  if(!arg_it->is_infile_name)
168  continue;
169 
170  // extract the preprocessed source from the file
171  std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
172  std::ifstream is(infile);
173  if(!is.is_open())
174  {
175  error() << "Failed to open input source " << infile << eom;
176  return 1;
177  }
178 
179  // there could be multiple source files in case GCC's --combine
180  // was used
181  unsigned outputs=0;
182  std::string line;
183  std::ofstream os;
184  std::string dest;
185 
186  const std::string comment2=act_as_as86 ? "::" : "##";
187 
188  // search for comment2 GOTO-CC
189  // strip comment2 from all subsequent lines
190  while(std::getline(is, line))
191  {
192  if(line==comment2+" GOTO-CC")
193  {
194  if(outputs>0)
195  {
196  assert(!dest.empty());
197  compiler.add_input_file(dest);
198  os.close();
199  }
200 
201  ++outputs;
202  std::string new_name=
203  get_base_name(infile, true)+"_"+
204  std::to_string(outputs)+".i";
205  dest=temp_dir(new_name);
206 
207  os.open(dest);
208  if(!os.is_open())
209  {
210  error() << "Failed to tmp output file " << dest << eom;
211  return 1;
212  }
213 
214  continue;
215  }
216  else if(outputs==0)
217  continue;
218 
219  if(line.size()>2)
220  os << line.substr(2) << '\n';
221  }
222 
223  if(outputs>0)
224  {
225  assert(!dest.empty());
226  compiler.add_input_file(dest);
227  }
228  else
229  warning() << "No GOTO-CC section found in " << arg_it->arg << eom;
230  }
231 
232  // Revert to as in case there is no source to compile
233 
234  if(compiler.source_files.empty())
235  return run_as(); // exit!
236 
237  // do all the rest
238  if(compiler.doit())
239  return 1; // GCC exit code for all kinds of errors
240 
241  // We can generate hybrid ELF and Mach-O binaries
242  // containing both executable machine code and the goto-binary.
244  return as_hybrid_binary();
245 
246  return EX_OK;
247 }
248 
251 {
252  assert(!cmdline.parsed_argv.empty());
253 
254  // build new argv
255  std::vector<std::string> new_argv;
256  new_argv.reserve(cmdline.parsed_argv.size());
257  for(const auto &a : cmdline.parsed_argv)
258  new_argv.push_back(a.arg);
259 
260  // overwrite argv[0]
261  new_argv[0]=native_tool_name;
262 
263  #if 0
264  std::cout << "RUN:";
265  for(std::size_t i=0; i<new_argv.size(); i++)
266  std::cout << " " << new_argv[i];
267  std::cout << '\n';
268  #endif
269 
270  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
271 }
272 
274 {
275  std::string output_file="a.out";
276 
277  if(cmdline.isset('o'))
278  {
279  output_file=cmdline.get_value('o');
280  }
281  else if(cmdline.isset('b')) // as86 only
282  output_file=cmdline.get_value('b');
283 
284  if(output_file=="/dev/null")
285  return EX_OK;
286 
287  debug() << "Running " << native_tool_name
288  << " to generate hybrid binary" << eom;
289 
290  // save the goto-cc output file
291  int result=rename(
292  output_file.c_str(),
293  (output_file+".goto-cc-saved").c_str());
294  if(result!=0)
295  {
296  error() << "Rename failed: " << std::strerror(errno) << eom;
297  return result;
298  }
299 
300  result=run_as();
301 
302  // merge output from as with goto-binaries
303  // using objcopy, or do cleanup if an earlier call failed
304  debug() << "merging " << output_file << eom;
305  std::string saved=output_file+".goto-cc-saved";
306 
307  #if defined(__linux__) || defined(__FreeBSD_kernel__)
308  if(result==0)
309  {
310  // remove any existing goto-cc section
311  std::vector<std::string> objcopy_argv;
312 
313  objcopy_argv.push_back("objcopy");
314  objcopy_argv.push_back("--remove-section=goto-cc");
315  objcopy_argv.push_back(output_file);
316 
317  result = run(objcopy_argv[0], objcopy_argv);
318  }
319 
320  if(result==0)
321  {
322  // now add goto-binary as goto-cc section
323  std::vector<std::string> objcopy_argv;
324 
325  objcopy_argv.push_back("objcopy");
326  objcopy_argv.push_back("--add-section");
327  objcopy_argv.push_back("goto-cc="+saved);
328  objcopy_argv.push_back(output_file);
329 
330  result = run(objcopy_argv[0], objcopy_argv);
331  }
332 
333  int remove_result=remove(saved.c_str());
334  if(remove_result!=0)
335  {
336  error() << "Remove failed: " << std::strerror(errno) << eom;
337  if(result==0)
338  result=remove_result;
339  }
340 
341  #elif defined(__APPLE__)
342  // Mac
343  if(result==0)
344  {
345  std::vector<std::string> lipo_argv;
346 
347  // now add goto-binary as hppa7100LC section
348  lipo_argv.push_back("lipo");
349  lipo_argv.push_back(output_file);
350  lipo_argv.push_back("-create");
351  lipo_argv.push_back("-arch");
352  lipo_argv.push_back("hppa7100LC");
353  lipo_argv.push_back(saved);
354  lipo_argv.push_back("-output");
355  lipo_argv.push_back(output_file);
356 
357  result = run(lipo_argv[0], lipo_argv);
358  }
359 
360  int remove_result=remove(saved.c_str());
361  if(remove_result!=0)
362  {
363  error() << "Remove failed: " << std::strerror(errno) << eom;
364  if(result==0)
365  result=remove_result;
366  }
367 
368  #else
369  error() << "binary merging not implemented for this platform" << eom;
370  result = 1;
371  #endif
372 
373  return result;
374 }
375 
378 {
379  std::cout << "goto-as understands the options of as plus the following.\n\n";
380 }
struct configt::ansi_ct ansi_c
virtual int doit()
does it.
Definition: as_mode.cpp:68
std::string stdin_file
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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
literalt pos(literalt a)
Definition: literal.h:193
std::string get_value(char option) const
Definition: cmdline.cpp:45
Assembler Mode.
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const bool produce_hybrid_binary
Definition: as_mode.h:34
configt config
Definition: config.cpp:24
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
mstreamt & warning() const
Definition: message.h:391
bool set(const cmdlinet &cmdline)
Definition: config.cpp:767
virtual bool isset(char option) const
Definition: cmdline.cpp:27
flavourt mode
Definition: config.h:115
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:37
mstreamt & error() const
Definition: message.h:386
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:47
int as_hybrid_binary()
Definition: as_mode.cpp:273
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: as_mode.cpp:35
static eomt eom
Definition: message.h:284
Compile and link source and object files.
static irep_idt this_operating_system()
Definition: config.cpp:1368
virtual void help_mode()
display command line help
Definition: as_mode.cpp:377
mstreamt & result() const
Definition: message.h:396
gcc_message_handlert message_handler
Definition: as_mode.h:33
mstreamt & status() const
Definition: message.h:401
const char * CBMC_VERSION
Definition: version.cpp:1
virtual void help()
display command line help
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
Definition: as_mode.cpp:57
int run_as()
run as or as86 with original command line
Definition: as_mode.cpp:250
parsed_argvt parsed_argv
mstreamt & debug() const
Definition: message.h:416
const std::string native_tool_name
Definition: as_mode.h:35
const std::string base_name
Definition: goto_cc_mode.h:38
static irep_idt this_architecture()
Definition: config.cpp:1268
enum compilet::@3 mode