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