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/file_util.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 #include "hybrid_binary.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 
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  {
89  log.status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
90  << messaget::eom;
91  }
92  else
93  {
94  log.status() << "GNU assembler version 2.20.51.0.7 20100318"
95  << " (goto-cc " << CBMC_VERSION << ")" << messaget::eom;
96  }
97 
98  log.status()
99  << '\n'
100  << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
101  << "CBMC version: " << CBMC_VERSION << '\n'
102  << "Architecture: " << config.this_architecture() << '\n'
103  << "OS: " << config.this_operating_system() << messaget::eom;
104 
105  return EX_OK; // Exit!
106  }
107 
108  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
111  cmdline.get_value("verbosity"), default_verbosity, message_handler);
112 
113  if(act_as_as86)
114  {
116  log.debug() << "AS86 mode (hybrid)" << messaget::eom;
117  else
118  log.debug() << "AS86 mode" << messaget::eom;
119  }
120  else
121  {
123  log.debug() << "AS mode (hybrid)" << messaget::eom;
124  else
125  log.debug() << "AS mode" << messaget::eom;
126  }
127 
128  // get configuration
129  config.set(cmdline);
130 
131  // determine actions to be undertaken
132  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
133 
134  if(cmdline.isset('b')) // as86 only
135  {
137  log.debug() << "Compiling and linking an executable" << messaget::eom;
138  }
139  else
140  {
141  compiler.mode=compilet::COMPILE_LINK;
142  log.debug() << "Compiling and linking a library" << messaget::eom;
143  }
144 
146 
147  compiler.object_file_extension="o";
148 
149  if(cmdline.isset('o'))
150  {
151  compiler.output_file_object=cmdline.get_value('o');
153  }
154  else if(cmdline.isset('b')) // as86 only
155  {
156  compiler.output_file_object=cmdline.get_value('b');
158  }
159  else
160  {
161  compiler.output_file_object="a.out";
162  compiler.output_file_executable="a.out";
163  }
164 
165  // We now iterate over any input files
166 
167  temp_dirt temp_dir("goto-cc-XXXXXX");
168 
169  for(goto_cc_cmdlinet::parsed_argvt::iterator
170  arg_it=cmdline.parsed_argv.begin();
171  arg_it!=cmdline.parsed_argv.end();
172  arg_it++)
173  {
174  if(!arg_it->is_infile_name)
175  continue;
176 
177  // extract the preprocessed source from the file
178  std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
179  std::ifstream is(infile);
180  if(!is.is_open())
181  {
182  log.error() << "Failed to open input source " << infile << messaget::eom;
183  return 1;
184  }
185 
186  // there could be multiple source files in case GCC's --combine
187  // was used
188  unsigned outputs=0;
189  std::string line;
190  std::ofstream os;
191  std::string dest;
192 
193  const std::string comment2=act_as_as86 ? "::" : "##";
194 
195  // search for comment2 GOTO-CC
196  // strip comment2 from all subsequent lines
197  while(std::getline(is, line))
198  {
199  if(line==comment2+" GOTO-CC")
200  {
201  if(outputs>0)
202  {
203  assert(!dest.empty());
204  compiler.add_input_file(dest);
205  os.close();
206  }
207 
208  ++outputs;
209  std::string new_name=
210  get_base_name(infile, true)+"_"+
211  std::to_string(outputs)+".i";
212  dest=temp_dir(new_name);
213 
214  os.open(dest);
215  if(!os.is_open())
216  {
217  log.error() << "Failed to tmp output file " << dest << messaget::eom;
218  return 1;
219  }
220 
221  continue;
222  }
223  else if(outputs==0)
224  continue;
225 
226  if(line.size()>2)
227  os << line.substr(2) << '\n';
228  }
229 
230  if(outputs>0)
231  {
232  assert(!dest.empty());
233  compiler.add_input_file(dest);
234  }
235  else
236  {
237  log.warning() << "No GOTO-CC section found in " << arg_it->arg
238  << messaget::eom;
239  }
240  }
241 
242  // Revert to as in case there is no source to compile
243 
244  if(compiler.source_files.empty())
245  return run_as(); // exit!
246 
247  // do all the rest
248  if(compiler.doit())
249  return 1; // GCC exit code for all kinds of errors
250 
251  // We can generate hybrid ELF and Mach-O binaries
252  // containing both executable machine code and the goto-binary.
254  return as_hybrid_binary(compiler);
255 
256  return EX_OK;
257 }
258 
261 {
262  assert(!cmdline.parsed_argv.empty());
263 
264  // build new argv
265  std::vector<std::string> new_argv;
266  new_argv.reserve(cmdline.parsed_argv.size());
267  for(const auto &a : cmdline.parsed_argv)
268  new_argv.push_back(a.arg);
269 
270  // overwrite argv[0]
271  new_argv[0]=native_tool_name;
272 
273  #if 0
274  std::cout << "RUN:";
275  for(std::size_t i=0; i<new_argv.size(); i++)
276  std::cout << " " << new_argv[i];
277  std::cout << '\n';
278  #endif
279 
280  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
281 }
282 
284 {
285  std::string output_file="a.out";
286 
287  if(cmdline.isset('o'))
288  {
289  output_file=cmdline.get_value('o');
290  }
291  else if(cmdline.isset('b')) // as86 only
292  output_file=cmdline.get_value('b');
293 
294  if(output_file=="/dev/null")
295  return EX_OK;
296 
298  log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
299  << messaget::eom;
300 
301  // save the goto-cc output file
302  std::string saved = output_file + ".goto-cc-saved";
303  try
304  {
305  file_rename(output_file, saved);
306  }
307  catch(const cprover_exception_baset &e)
308  {
309  log.error() << "Rename failed: " << e.what() << messaget::eom;
310  return 1;
311  }
312 
313  int result = run_as();
314 
315  if(result == 0)
316  {
317  result = hybrid_binary(
319  saved,
320  output_file,
323  }
324 
325  return result;
326 }
327 
330 {
331  std::cout << "goto-as understands the options of as plus the following.\n\n";
332 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
get_base_name
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
Definition: get_base_name.cpp:16
goto_cc_cmdlinet::parsed_argv
parsed_argvt parsed_argv
Definition: goto_cc_cmdline.h:64
as_modet::native_tool_name
const std::string native_tool_name
Definition: as_mode.h:36
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:42
goto_cc_cmdlinet::stdin_file
std::string stdin_file
Definition: goto_cc_cmdline.h:68
pos
literalt pos(literalt a)
Definition: literal.h:194
file_util.h
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:58
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:38
goto_cc_modet::base_name
const std::string base_name
Definition: goto_cc_mode.h:38
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
configt::ansi_c
struct configt::ansi_ct ansi_c
run.h
compilet::COMPILE_LINK
@ COMPILE_LINK
Definition: compile.h:37
version.h
tempdir.h
as_modet::run_as
int run_as()
run as or as86 with original command line
Definition: as_mode.cpp:260
as_mode.h
Assembler Mode.
as_modet::as_hybrid_binary
int as_hybrid_binary(const compilet &compiler)
Definition: as_mode.cpp:283
cmdlinet
Definition: cmdline.h:21
CBMC_VERSION
const char * CBMC_VERSION
compilet::output_file_object
std::string output_file_object
Definition: compile.h:50
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:47
cprover_exception_baset::what
virtual std::string what() const =0
A human readable description of what went wrong.
temp_dirt
Definition: tempdir.h:20
messaget::M_ERROR
@ M_ERROR
Definition: message.h:170
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
compile.h
Compile and link source and object files.
as_modet::as_modet
as_modet(goto_cc_cmdlinet &_cmdline, const std::string &_base_name, bool _produce_hybrid_binary)
Definition: as_mode.cpp:58
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1425
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:46
get_base_name.h
goto_cc_modet::cmdline
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:37
as_modet::message_handler
gcc_message_handlert message_handler
Definition: as_mode.h:34
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
as_modet::produce_hybrid_binary
const bool produce_hybrid_binary
Definition: as_mode.h:35
hybrid_binary.h
Create hybrid binary with goto-binary section.
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1325
configt::ansi_ct::mode
flavourt mode
Definition: config.h:196
compilet::mode
enum compilet::@4 mode
messaget::M_WARNING
@ M_WARNING
Definition: message.h:170
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:797
assembler_name
static std::string assembler_name(const cmdlinet &cmdline, const std::string &base_name)
Definition: as_mode.cpp:36
as_modet::help_mode
virtual void help_mode()
display command line help
Definition: as_mode.cpp:329
goto_cc_modet
Definition: goto_cc_mode.h:22
config.h
configt::ansi_ct::flavourt::GCC
@ GCC
goto_cc_modet::help
void help()
display command line help
Definition: goto_cc_mode.cpp:46
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
as_modet::doit
virtual int doit()
does it.
Definition: as_mode.cpp:69
goto_cc_cmdlinet
Definition: goto_cc_cmdline.h:20
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