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