CBMC
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 <util/cmdline.h>
23 #include <util/config.h>
24 #include <util/get_base_name.h>
25 #include <util/run.h>
26 #include <util/tempdir.h>
27 #include <util/version.h>
28 
29 #include "compile.h"
30 #include "goto_cc_cmdline.h"
31 #include "hybrid_binary.h"
32 
33 #include <filesystem>
34 #include <fstream> // IWYU pragma: keep
35 #include <iostream>
36 
37 static std::string assembler_name(
38  const cmdlinet &cmdline,
39  const std::string &base_name)
40 {
41  if(cmdline.isset("native-assembler"))
42  return cmdline.get_value("native-assembler");
43 
44  if(base_name=="as86" ||
45  base_name.find("goto-as86")!=std::string::npos)
46  return "as86";
47 
48  std::string::size_type pos=base_name.find("goto-as");
49 
50  if(pos==std::string::npos)
51  return "as";
52 
53  std::string result=base_name;
54  result.replace(pos, 7, "as");
55 
56  return result;
57 }
58 
60  goto_cc_cmdlinet &_cmdline,
61  const std::string &_base_name,
62  bool _produce_hybrid_binary):
63  goto_cc_modet(_cmdline, _base_name, message_handler),
64  produce_hybrid_binary(_produce_hybrid_binary),
65  native_tool_name(assembler_name(cmdline, base_name))
66 {
67 }
68 
71 {
72  if(cmdline.isset('?') ||
73  cmdline.isset("help"))
74  {
75  help();
76  return EX_OK;
77  }
78 
80 
81  bool act_as_as86=
82  base_name=="as86" ||
83  base_name.find("goto-as86")!=std::string::npos;
84 
85  if((cmdline.isset('v') && act_as_as86) ||
86  cmdline.isset("version"))
87  {
88  if(act_as_as86)
89  {
90  log.status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
91  << messaget::eom;
92  }
93  else
94  {
95  log.status() << "GNU assembler version 2.20.51.0.7 20100318"
96  << " (goto-cc " << CBMC_VERSION << ")" << messaget::eom;
97  }
98 
99  log.status()
100  << '\n'
101  << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
102  << "CBMC version: " << CBMC_VERSION << '\n'
103  << "Architecture: " << config.this_architecture() << '\n'
104  << "OS: " << config.this_operating_system() << messaget::eom;
105 
106  return EX_OK; // Exit!
107  }
108 
109  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
112  cmdline.get_value("verbosity"), default_verbosity, message_handler);
114 
115  if(act_as_as86)
116  {
118  log.debug() << "AS86 mode (hybrid)" << messaget::eom;
119  else
120  log.debug() << "AS86 mode" << messaget::eom;
121  }
122  else
123  {
125  log.debug() << "AS mode (hybrid)" << messaget::eom;
126  else
127  log.debug() << "AS mode" << messaget::eom;
128  }
129 
130  // get configuration
131  config.set(cmdline);
132 
133  // determine actions to be undertaken
134  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
135 
136  if(cmdline.isset('b')) // as86 only
137  {
139  log.debug() << "Compiling and linking an executable" << messaget::eom;
140  }
141  else
142  {
143  compiler.mode=compilet::COMPILE_LINK;
144  log.debug() << "Compiling and linking a library" << messaget::eom;
145  }
146 
148 
149  compiler.object_file_extension="o";
150 
151  if(cmdline.isset('o'))
152  {
153  compiler.output_file_object=cmdline.get_value('o');
155  }
156  else if(cmdline.isset('b')) // as86 only
157  {
158  compiler.output_file_object=cmdline.get_value('b');
160  }
161  else
162  {
163  compiler.output_file_object="a.out";
164  compiler.output_file_executable="a.out";
165  }
166 
167  // We now iterate over any input files
168 
169  temp_dirt temp_dir("goto-cc-XXXXXX");
170 
171  for(goto_cc_cmdlinet::parsed_argvt::iterator
172  arg_it=cmdline.parsed_argv.begin();
173  arg_it!=cmdline.parsed_argv.end();
174  arg_it++)
175  {
176  if(!arg_it->is_infile_name)
177  continue;
178 
179  // extract the preprocessed source from the file
180  std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
181  std::ifstream is(infile);
182  if(!is.is_open())
183  {
184  log.error() << "Failed to open input source " << infile << messaget::eom;
185  return 1;
186  }
187 
188  // there could be multiple source files in case GCC's --combine
189  // was used
190  unsigned outputs=0;
191  std::string line;
192  std::ofstream os;
193  std::string dest;
194 
195  const std::string comment2=act_as_as86 ? "::" : "##";
196 
197  // search for comment2 GOTO-CC
198  // strip comment2 from all subsequent lines
199  while(std::getline(is, line))
200  {
201  if(line==comment2+" GOTO-CC")
202  {
203  if(outputs>0)
204  {
205  PRECONDITION(!dest.empty());
206  compiler.add_input_file(dest);
207  os.close();
208  }
209 
210  ++outputs;
211  std::string new_name=
212  get_base_name(infile, true)+"_"+
213  std::to_string(outputs)+".i";
214  dest=temp_dir(new_name);
215 
216  os.open(dest);
217  if(!os.is_open())
218  {
219  log.error() << "Failed to tmp output file " << dest << messaget::eom;
220  return 1;
221  }
222 
223  continue;
224  }
225  else if(outputs==0)
226  continue;
227 
228  if(line.size()>2)
229  os << line.substr(2) << '\n';
230  }
231 
232  if(outputs>0)
233  {
234  PRECONDITION(!dest.empty());
235  compiler.add_input_file(dest);
236  }
237  else
238  {
239  log.warning() << "No GOTO-CC section found in " << arg_it->arg
240  << messaget::eom;
241  }
242  }
243 
244  // Revert to as in case there is no source to compile
245 
246  if(compiler.source_files.empty())
247  return run_as(); // exit!
248 
249  // do all the rest
250  if(compiler.doit())
251  return 1; // GCC exit code for all kinds of errors
252 
253  // We can generate hybrid ELF and Mach-O binaries
254  // containing both executable machine code and the goto-binary.
256  return as_hybrid_binary(compiler);
257 
258  return EX_OK;
259 }
260 
263 {
264  PRECONDITION(!cmdline.parsed_argv.empty());
265 
266  // build new argv
267  std::vector<std::string> new_argv;
268  new_argv.reserve(cmdline.parsed_argv.size());
269  for(const auto &a : cmdline.parsed_argv)
270  new_argv.push_back(a.arg);
271 
272  // overwrite argv[0]
273  new_argv[0]=native_tool_name;
274 
275  #if 0
276  std::cout << "RUN:";
277  for(std::size_t i=0; i<new_argv.size(); i++)
278  std::cout << " " << new_argv[i];
279  std::cout << '\n';
280  #endif
281 
282  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
283 }
284 
286 {
287  std::string output_file="a.out";
288 
289  if(cmdline.isset('o'))
290  {
291  output_file=cmdline.get_value('o');
292  }
293  else if(cmdline.isset('b')) // as86 only
294  output_file=cmdline.get_value('b');
295 
296  if(output_file=="/dev/null")
297  return EX_OK;
298 
300  log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
301  << messaget::eom;
302 
303  // save the goto-cc output file
304  std::string saved = output_file + ".goto-cc-saved";
305  try
306  {
307  std::filesystem::rename(output_file, saved);
308  }
309  catch(const std::filesystem::filesystem_error &e)
310  {
311  log.error() << "Rename failed: " << e.what() << messaget::eom;
312  return 1;
313  }
314 
315  int result = run_as();
316 
317  if(result == 0)
318  {
319  result = hybrid_binary(
321  saved,
322  output_file,
325  }
326 
327  return result;
328 }
329 
332 {
333  std::cout << "goto-as understands the options of as plus the following.\n\n";
334 }
configt config
Definition: config.cpp:25
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: as_mode.cpp:37
Assembler Mode.
int run_as()
run as or as86 with original command line
Definition: as_mode.cpp:262
virtual void help_mode()
display command line help
Definition: as_mode.cpp:331
virtual int doit()
does it.
Definition: as_mode.cpp:70
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
Definition: as_mode.cpp:59
const bool produce_hybrid_binary
Definition: as_mode.h:35
const std::string native_tool_name
Definition: as_mode.h:36
int as_hybrid_binary(const compilet &compiler)
Definition: as_mode.cpp:285
gcc_message_handlert message_handler
Definition: as_mode.h:34
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:43
@ COMPILE_LINK
Definition: compile.h:42
std::string output_file_object
Definition: compile.h:55
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:167
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:54
std::list< std::string > source_files
Definition: compile.h:47
std::string object_file_extension
Definition: compile.h:51
enum compilet::@3 mode
std::string output_file_executable
Definition: compile.h:52
bool set(const cmdlinet &cmdline)
Definition: config.cpp:863
static irep_idt this_architecture()
Definition: config.cpp:1442
static irep_idt this_operating_system()
Definition: config.cpp:1546
struct configt::ansi_ct ansi_c
void print_warnings_as_errors(bool yes)
With yes set to true, prefix warnings with "error:" instead of "warning:".
parsed_argvt parsed_argv
std::string stdin_file
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:38
const std::string base_name
Definition: goto_cc_mode.h:39
void help()
display command line help
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
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:105
@ M_ERROR
Definition: message.h:169
@ M_WARNING
Definition: message.h:169
static eomt eom
Definition: message.h:289
Compile and link source and object files.
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Command line interpretation for goto-cc.
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, bool linking_efi)
Merges a goto binary into an object file (e.g.
Create hybrid binary with goto-binary section.
literalt pos(literalt a)
Definition: literal.h:194
double log(double x)
Definition: math.c:2776
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:48
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
flavourt mode
Definition: config.h:256
#define size_type
Definition: unistd.c:347
const char * CBMC_VERSION