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 
78  bool act_as_as86=
79  base_name=="as86" ||
80  base_name.find("goto-as86")!=std::string::npos;
81 
82  if((cmdline.isset('v') && act_as_as86) ||
83  cmdline.isset("version"))
84  {
85  if(act_as_as86)
86  status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
87  << eom;
88  else
89  status() << "GNU assembler version 2.20.51.0.7 20100318"
90  << " (goto-cc " << CBMC_VERSION << ")" << eom;
91 
92  status()
93  << '\n'
94  << "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
95  << "CBMC version: " << CBMC_VERSION << '\n'
96  << "Architecture: " << config.this_architecture() << '\n'
97  << "OS: " << config.this_operating_system() << eom;
98 
99  return EX_OK; // Exit!
100  }
101 
102  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
105  cmdline.get_value("verbosity"), default_verbosity, message_handler);
106 
107  if(act_as_as86)
108  {
110  debug() << "AS86 mode (hybrid)" << eom;
111  else
112  debug() << "AS86 mode" << eom;
113  }
114  else
115  {
117  debug() << "AS mode (hybrid)" << eom;
118  else
119  debug() << "AS mode" << eom;
120  }
121 
122  // get configuration
123  config.set(cmdline);
124 
125  // determine actions to be undertaken
126  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
127 
128  if(cmdline.isset('b')) // as86 only
129  {
131  debug() << "Compiling and linking an executable" << eom;
132  }
133  else
134  {
135  compiler.mode=compilet::COMPILE_LINK;
136  debug() << "Compiling and linking a library" << eom;
137  }
138 
140 
141  compiler.object_file_extension="o";
142 
143  if(cmdline.isset('o'))
144  {
145  compiler.output_file_object=cmdline.get_value('o');
147  }
148  else if(cmdline.isset('b')) // as86 only
149  {
150  compiler.output_file_object=cmdline.get_value('b');
152  }
153  else
154  {
155  compiler.output_file_object="a.out";
156  compiler.output_file_executable="a.out";
157  }
158 
159  // We now iterate over any input files
160 
161  temp_dirt temp_dir("goto-cc-XXXXXX");
162 
163  for(goto_cc_cmdlinet::parsed_argvt::iterator
164  arg_it=cmdline.parsed_argv.begin();
165  arg_it!=cmdline.parsed_argv.end();
166  arg_it++)
167  {
168  if(!arg_it->is_infile_name)
169  continue;
170 
171  // extract the preprocessed source from the file
172  std::string infile=arg_it->arg=="-"?cmdline.stdin_file:arg_it->arg;
173  std::ifstream is(infile);
174  if(!is.is_open())
175  {
176  error() << "Failed to open input source " << infile << eom;
177  return 1;
178  }
179 
180  // there could be multiple source files in case GCC's --combine
181  // was used
182  unsigned outputs=0;
183  std::string line;
184  std::ofstream os;
185  std::string dest;
186 
187  const std::string comment2=act_as_as86 ? "::" : "##";
188 
189  // search for comment2 GOTO-CC
190  // strip comment2 from all subsequent lines
191  while(std::getline(is, line))
192  {
193  if(line==comment2+" GOTO-CC")
194  {
195  if(outputs>0)
196  {
197  assert(!dest.empty());
198  compiler.add_input_file(dest);
199  os.close();
200  }
201 
202  ++outputs;
203  std::string new_name=
204  get_base_name(infile, true)+"_"+
205  std::to_string(outputs)+".i";
206  dest=temp_dir(new_name);
207 
208  os.open(dest);
209  if(!os.is_open())
210  {
211  error() << "Failed to tmp output file " << dest << eom;
212  return 1;
213  }
214 
215  continue;
216  }
217  else if(outputs==0)
218  continue;
219 
220  if(line.size()>2)
221  os << line.substr(2) << '\n';
222  }
223 
224  if(outputs>0)
225  {
226  assert(!dest.empty());
227  compiler.add_input_file(dest);
228  }
229  else
230  warning() << "No GOTO-CC section found in " << arg_it->arg << eom;
231  }
232 
233  // Revert to as in case there is no source to compile
234 
235  if(compiler.source_files.empty())
236  return run_as(); // exit!
237 
238  // do all the rest
239  if(compiler.doit())
240  return 1; // GCC exit code for all kinds of errors
241 
242  // We can generate hybrid ELF and Mach-O binaries
243  // containing both executable machine code and the goto-binary.
245  return as_hybrid_binary(compiler);
246 
247  return EX_OK;
248 }
249 
252 {
253  assert(!cmdline.parsed_argv.empty());
254 
255  // build new argv
256  std::vector<std::string> new_argv;
257  new_argv.reserve(cmdline.parsed_argv.size());
258  for(const auto &a : cmdline.parsed_argv)
259  new_argv.push_back(a.arg);
260 
261  // overwrite argv[0]
262  new_argv[0]=native_tool_name;
263 
264  #if 0
265  std::cout << "RUN:";
266  for(std::size_t i=0; i<new_argv.size(); i++)
267  std::cout << " " << new_argv[i];
268  std::cout << '\n';
269  #endif
270 
271  return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
272 }
273 
275 {
276  std::string output_file="a.out";
277 
278  if(cmdline.isset('o'))
279  {
280  output_file=cmdline.get_value('o');
281  }
282  else if(cmdline.isset('b')) // as86 only
283  output_file=cmdline.get_value('b');
284 
285  if(output_file=="/dev/null")
286  return EX_OK;
287 
288  debug() << "Running " << native_tool_name
289  << " to generate hybrid binary" << eom;
290 
291  // save the goto-cc output file
292  std::string saved = output_file + ".goto-cc-saved";
293  try
294  {
295  file_rename(output_file, saved);
296  }
297  catch(const cprover_exception_baset &e)
298  {
299  error() << "Rename failed: " << e.what() << eom;
300  return 1;
301  }
302 
303  int result = run_as();
304 
305  if(result == 0)
306  {
309  saved,
310  output_file,
313  }
314 
315  return result;
316 }
317 
320 {
321  std::cout << "goto-as understands the options of as plus the following.\n\n";
322 }
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:48
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
messaget::status
mstreamt & status() const
Definition: message.h:414
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:57
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
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
version.h
tempdir.h
as_modet::run_as
int run_as()
run as or as86 with original command line
Definition: as_mode.cpp:251
as_mode.h
Assembler Mode.
as_modet::as_hybrid_binary
int as_hybrid_binary(const compilet &compiler)
Definition: as_mode.cpp:274
cmdlinet
Definition: cmdline.h:21
CBMC_VERSION
const char * CBMC_VERSION
compilet::output_file_object
std::string output_file_object
Definition: compile.h:58
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
compilet::mode
enum compilet::@2 mode
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:55
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.
compilet::COMPILE_LINK
@ COMPILE_LINK
Definition: compile.h:43
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:1402
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:54
get_base_name.h
goto_cc_modet::cmdline
goto_cc_cmdlinet & cmdline
Definition: goto_cc_mode.h:37
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:44
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:1302
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
messaget::M_WARNING
@ M_WARNING
Definition: message.h:170
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
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:319
goto_cc_modet
Definition: goto_cc_mode.h:22
config.h
configt::ansi_ct::flavourt::GCC
@ GCC
messaget::debug
mstreamt & debug() const
Definition: message.h:429
goto_cc_modet::help
void help()
display command line help
Definition: goto_cc_mode.cpp:47
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
messaget::warning
mstreamt & warning() const
Definition: message.h:404
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