cprover
compile.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Compile and link source and object files.
4 
5 Author: CM Wintersteiger
6 
7 Date: June 2006
8 
9 \*******************************************************************/
10 
13 
14 #include "compile.h"
15 
16 #include <fstream>
17 #include <sstream>
18 #include <iostream>
19 #include <cstdlib>
20 #include <algorithm>
21 
22 #include <util/config.h>
23 #include <util/tempdir.h>
24 #include <util/base_type.h>
25 #include <util/cmdline.h>
26 #include <util/file_util.h>
27 #include <util/unicode.h>
29 #include <util/suffix.h>
30 #include <util/get_base_name.h>
31 
32 #include <ansi-c/ansi_c_language.h>
34 
40 
41 #include <langapi/mode.h>
42 
43 #include <cbmc/version.h>
44 
45 #define DOTGRAPHSETTINGS "color=black;" \
46  "orientation=portrait;" \
47  "fontsize=20;"\
48  "compound=true;"\
49  "size=\"30,40\";"\
50  "ratio=compress;"
51 
52 // the following are for chdir
53 
54 #if defined(__linux__) || \
55  defined(__FreeBSD_kernel__) || \
56  defined(__GNU__) || \
57  defined(__unix__) || \
58  defined(__CYGWIN__) || \
59  defined(__MACH__)
60 #include <unistd.h>
61 #endif
62 
63 #ifdef _WIN32
64 #include <direct.h>
65 #include <windows.h>
66 #define chdir _chdir
67 #define popen _popen
68 #define pclose _pclose
69 #endif
70 
75 {
77 
79 
80  // Parse command line for source and object file names
81  for(std::size_t i=0; i<_cmdline.args.size(); i++)
83  return true;
84 
85  for(std::list<std::string>::const_iterator it = libraries.begin();
86  it!=libraries.end();
87  it++)
88  {
89  if(!find_library(*it))
90  // GCC is going to complain if this doesn't exist
91  debug() << "Library not found: " << *it << " (ignoring)" << eom;
92  }
93 
94  statistics() << "No. of source files: " << source_files.size() << eom;
95  statistics() << "No. of object files: " << object_files.size() << eom;
96 
97  // Work through the given source files
98 
99  if(source_files.empty() && object_files.empty())
100  {
101  error() << "no input files" << eom;
102  return true;
103  }
104 
105  if(mode==LINK_LIBRARY && !source_files.empty())
106  {
107  error() << "cannot link source files" << eom;
108  return true;
109  }
110 
111  if(mode==PREPROCESS_ONLY && !object_files.empty())
112  {
113  error() << "cannot preprocess object files" << eom;
114  return true;
115  }
116 
117  const unsigned warnings_before=
119 
120  if(!source_files.empty())
121  if(compile())
122  return true;
123 
124  if(mode==LINK_LIBRARY ||
125  mode==COMPILE_LINK ||
127  {
128  if(link())
129  return true;
130  }
131 
132  return
135  warnings_before;
136 }
137 
140 bool compilet::add_input_file(const std::string &file_name)
141 {
142  // first of all, try to open the file
143  {
144  std::ifstream in(file_name);
145  if(!in)
146  {
147  warning() << "failed to open file `" << file_name << "'" << eom;
148  return warning_is_fatal; // generously ignore unless -Werror
149  }
150  }
151 
152  size_t r=file_name.rfind('.', file_name.length()-1);
153 
154  if(r==std::string::npos)
155  {
156  // a file without extension; will ignore
157  warning() << "input file `" << file_name
158  << "' has no extension, not considered" << eom;
159  return warning_is_fatal;
160  }
161 
162  std::string ext = file_name.substr(r+1, file_name.length());
163 
164  if(ext=="c" ||
165  ext=="cc" ||
166  ext=="cp" ||
167  ext=="cpp" ||
168  ext=="CPP" ||
169  ext=="c++" ||
170  ext=="C" ||
171  ext=="i" ||
172  ext=="ii" ||
173  ext=="class" ||
174  ext=="jar" ||
175  ext=="jsil")
176  {
177  source_files.push_back(file_name);
178  }
179  else if(ext=="a")
180  {
181  #ifdef _WIN32
182  char td[MAX_PATH+1];
183  #else
184  char td[] = "goto-cc.XXXXXX";
185  #endif
186 
187  std::string tstr=get_temporary_directory(td);
188 
189  if(tstr=="")
190  {
191  error() << "Cannot create temporary directory" << eom;
192  return true;
193  }
194 
195  tmp_dirs.push_back(tstr);
196  std::stringstream cmd("");
197  if(chdir(tmp_dirs.back().c_str())!=0)
198  {
199  error() << "Cannot switch to temporary directory" << eom;
200  return true;
201  }
202 
203  // unpack now
204  cmd << "ar x " << concat_dir_file(working_directory, file_name);
205 
206  FILE *stream;
207 
208  stream=popen(cmd.str().c_str(), "r");
209  pclose(stream);
210 
211  cmd.clear();
212  cmd.str("");
213 
214  // add the files from "ar t"
215  #ifdef _WIN32
216  if(file_name[0]!='/' && file_name[1]!=':') // NOLINT(readability/braces)
217  #else
218  if(file_name[0]!='/') // NOLINT(readability/braces)
219  #endif
220  {
221  cmd << "ar t " <<
222  #ifdef _WIN32
223  working_directory << "\\" << file_name;
224  #else
225  working_directory << "/" << file_name;
226  #endif
227  }
228  else
229  {
230  cmd << "ar t " << file_name;
231  }
232 
233  stream=popen(cmd.str().c_str(), "r");
234 
235  if(stream!=nullptr)
236  {
237  std::string line;
238  int ch; // fgetc returns an int, not char
239  while((ch=fgetc(stream))!=EOF)
240  {
241  if(ch!='\n')
242  {
243  line+=static_cast<char>(ch);
244  }
245  else
246  {
247  std::string t;
248  #ifdef _WIN32
249  t = tmp_dirs.back() + '\\' + line;
250  #else
251  t = tmp_dirs.back() + '/' + line;
252  #endif
253 
254  if(is_goto_binary(t))
255  object_files.push_back(t);
256 
257  line = "";
258  }
259  }
260 
261  pclose(stream);
262  }
263 
264  cmd.str("");
265 
266  if(chdir(working_directory.c_str())!=0)
267  error() << "Could not change back to working directory" << eom;
268  }
269  else if(is_goto_binary(file_name))
270  object_files.push_back(file_name);
271  else
272  {
273  // unknown extension, not a goto binary, will silently ignore
274  }
275 
276  return false;
277 }
278 
282 bool compilet::find_library(const std::string &name)
283 {
284  std::string tmp;
285 
286  for(std::list<std::string>::const_iterator
287  it=library_paths.begin();
288  it!=library_paths.end();
289  it++)
290  {
291  #ifdef _WIN32
292  tmp = *it + "\\lib";
293  #else
294  tmp = *it + "/lib";
295  #endif
296 
297  std::ifstream in(tmp+name+".a");
298 
299  if(in.is_open())
300  return !add_input_file(tmp+name+".a");
301  else
302  {
303  std::string libname=tmp+name+".so";
304 
305  if(is_goto_binary(libname))
306  return !add_input_file(libname);
307  else if(is_elf_file(libname))
308  {
309  warning() << "Warning: Cannot read ELF library " << libname << eom;
310  return warning_is_fatal;
311  }
312  }
313  }
314 
315  return false;
316 }
317 
322 bool compilet::is_elf_file(const std::string &file_name)
323 {
324  std::fstream in;
325 
326  in.open(file_name, std::ios::in);
327  if(in.is_open())
328  {
329  char buf[4];
330  for(std::size_t i=0; i<4; i++)
331  buf[i] = in.get();
332  if(buf[0]==0x7f && buf[1]=='E' &&
333  buf[2]=='L' && buf[3]=='F')
334  return true;
335  }
336 
337  return false;
338 }
339 
343 {
344  // "compile" hitherto uncompiled functions
345  statistics() << "Compiling functions" << eom;
347 
348  // parse object files
349  while(!object_files.empty())
350  {
351  std::string file_name=object_files.front();
352  object_files.pop_front();
353 
354  if(read_object_and_link(file_name, symbol_table,
356  return true;
357  }
358 
359  // produce entry point?
360 
362  {
363  // new symbols may have been added to a previously linked file
364  // make sure a new entry point is created that contains all
365  // static initializers
366  compiled_functions.function_map.erase("__CPROVER_initialize");
367 
370 
372  return true;
373 
374  // entry_point may (should) add some more functions.
376  }
377 
380  return true;
381 
382  return false;
383 }
384 
389 {
390  while(!source_files.empty())
391  {
392  std::string file_name=source_files.front();
393  source_files.pop_front();
394 
395  // Visual Studio always prints the name of the file it's doing
396  if(echo_file_name)
397  status() << file_name << eom;
398 
399  bool r=parse_source(file_name); // don't break the program!
400 
401  if(r)
402  {
403  const std::string &debug_outfile=
404  cmdline.get_value("print-rejected-preprocessed-source");
405  if(!debug_outfile.empty())
406  {
407  std::ifstream in(file_name, std::ios::binary);
408  std::ofstream out(debug_outfile, std::ios::binary);
409  out << in.rdbuf();
410  warning() << "Failed sources in " << debug_outfile << eom;
411  }
412 
413  return true; // parser/typecheck error
414  }
415 
417  {
418  // output an object file for every source file
419 
420  // "compile" functions
422 
423  std::string cfn;
424 
425  if(output_file_object=="")
426  cfn=get_base_name(file_name, true)+"."+object_file_extension;
427  else
428  cfn=output_file_object;
429 
431  return true;
432 
433  symbol_table.clear(); // clean symbol table for next source file.
435  }
436  }
437 
438  return false;
439 }
440 
443 bool compilet::parse(const std::string &file_name)
444 {
445  if(file_name=="-")
446  return parse_stdin();
447 
448  #ifdef _MSC_VER
449  std::ifstream infile(widen(file_name));
450  #else
451  std::ifstream infile(file_name);
452  #endif
453 
454  if(!infile)
455  {
456  error() << "failed to open input file `" << file_name << "'" << eom;
457  return true;
458  }
459 
460  languaget *languagep;
461 
462  // Using '-x', the type of a file can be overridden;
463  // otherwise, it's guessed from the extension.
464 
465  if(override_language!="")
466  {
467  if(override_language=="c++" || override_language=="c++-header")
468  languagep=get_language_from_mode("cpp");
469  else
470  languagep=get_language_from_mode("C");
471  }
472  else
473  languagep=get_language_from_filename(file_name);
474 
475  if(languagep==nullptr)
476  {
477  error() << "failed to figure out type of file `" << file_name << "'" << eom;
478  return true;
479  }
480 
481  languaget &language=*languagep;
483 
484  language_filet language_file;
485 
486  std::pair<language_filest::file_mapt::iterator, bool>
487  res=language_files.file_map.insert(
488  std::pair<std::string, language_filet>(file_name, language_file));
489 
490  language_filet &lf=res.first->second;
491  lf.filename=file_name;
492  lf.language=languagep;
493 
494  if(mode==PREPROCESS_ONLY)
495  {
496  statistics() << "Preprocessing: " << file_name << eom;
497 
498  std::ostream *os = &std::cout;
499  std::ofstream ofs;
500 
501  if(cmdline.isset('o'))
502  {
503  ofs.open(cmdline.get_value('o'));
504  os = &ofs;
505 
506  if(!ofs.is_open())
507  {
508  error() << "failed to open output file `"
509  << cmdline.get_value('o') << "'" << eom;
510  return true;
511  }
512  }
513 
514  language.preprocess(infile, file_name, *os);
515  }
516  else
517  {
518  statistics() << "Parsing: " << file_name << eom;
519 
520  if(language.parse(infile, file_name))
521  {
523  error() << "PARSING ERROR" << eom;
524  return true;
525  }
526  }
527 
528  lf.get_modules();
529  return false;
530 }
531 
535 {
536  ansi_c_languaget language;
537 
539 
540  statistics() << "Parsing: (stdin)" << eom;
541 
542  if(mode==PREPROCESS_ONLY)
543  {
544  std::ostream *os = &std::cout;
545  std::ofstream ofs;
546 
547  if(cmdline.isset('o'))
548  {
549  ofs.open(cmdline.get_value('o'));
550  os = &ofs;
551 
552  if(!ofs.is_open())
553  {
554  error() << "failed to open output file `"
555  << cmdline.get_value('o') << "'" << eom;
556  return true;
557  }
558  }
559 
560  language.preprocess(std::cin, "", *os);
561  }
562  else
563  {
564  if(language.parse(std::cin, ""))
565  {
567  error() << "PARSING ERROR" << eom;
568  return true;
569  }
570  }
571 
572  return false;
573 }
574 
580  const std::string &file_name,
581  const symbol_tablet &lsymbol_table,
582  goto_functionst &functions)
583 {
584  return write_bin_object_file(file_name, lsymbol_table, functions);
585 }
586 
592  const std::string &file_name,
593  const symbol_tablet &lsymbol_table,
594  goto_functionst &functions)
595 {
596  statistics() << "Writing binary format object `"
597  << file_name << "'" << eom;
598 
599  // symbols
600  statistics() << "Symbols in table: "
601  << lsymbol_table.symbols.size() << eom;
602 
603  std::ofstream outfile(file_name, std::ios::binary);
604 
605  if(!outfile.is_open())
606  {
607  error() << "Error opening file `" << file_name << "'" << eom;
608  return true;
609  }
610 
611  if(write_goto_binary(outfile, lsymbol_table, functions))
612  return true;
613 
614  unsigned cnt=function_body_count(functions);
615 
616  statistics() << "Functions: " << functions.function_map.size()
617  << "; " << cnt << " have a body." << eom;
618 
619  outfile.close();
620 
621  return false;
622 }
623 
626 bool compilet::parse_source(const std::string &file_name)
627 {
628  if(parse(file_name))
629  return true;
630 
631  if(typecheck()) // we just want to typecheck this one file here
632  return true;
633 
634  if((has_suffix(file_name, ".class") ||
635  has_suffix(file_name, ".jar")) &&
636  final())
637  return true;
638 
639  // so we remove it from the list afterwards
640  language_files.file_map.erase(file_name);
641  return false;
642 }
643 
647  language_uit(_cmdline, mh),
648  ns(symbol_table),
649  cmdline(_cmdline),
650  warning_is_fatal(Werror)
651 {
653  echo_file_name=false;
655 }
656 
660 {
661  // clean up temp dirs
662 
663  for(std::list<std::string>::const_iterator it = tmp_dirs.begin();
664  it!=tmp_dirs.end();
665  it++)
666  delete_directory(*it);
667 }
668 
670 {
671  int fbs=0;
672 
673  for(goto_functionst::function_mapt::const_iterator it=
674  functions.function_map.begin();
675  it != functions.function_map.end();
676  it++)
677  if(it->second.body_available())
678  fbs++;
679 
680  return fbs;
681 }
682 
684 {
685  config.ansi_c.defines.push_back("__GOTO_CC_VERSION__=" CBMC_VERSION);
686 }
687 
689 {
691 
692  // the compilation may add symbols!
693 
695 
696  while(before!=symbol_table.symbols.size())
697  {
698  before=symbol_table.symbols.size();
699 
700  typedef std::set<irep_idt> symbols_sett;
701  symbols_sett symbols;
702 
704  symbols.insert(it->first);
705 
706  // the symbol table iterators aren't stable
707  for(symbols_sett::const_iterator
708  it=symbols.begin();
709  it!=symbols.end();
710  ++it)
711  {
712  symbol_tablet::symbolst::iterator s_it=symbol_table.symbols.find(*it);
713  assert(s_it!=symbol_table.symbols.end());
714 
715  if(s_it->second.type.id()==ID_code &&
716  !s_it->second.is_macro &&
717  !s_it->second.is_type &&
718  s_it->second.value.id()!="compiled" &&
719  s_it->second.value.is_not_nil())
720  {
721  debug() << "Compiling " << s_it->first << eom;
722  converter.convert_function(s_it->first);
723  s_it->second.value=exprt("compiled");
724  }
725  }
726  }
727 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:128
mstreamt & warning()
Definition: message.h:228
symbol_tablet symbol_table
Definition: language_ui.h:24
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:140
struct configt::ansi_ct ansi_c
std::string output_file_executable
Definition: compile.h:48
compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:646
static int8_t r
Definition: irep_hash.h:59
Globally accessible architectural configuration.
Definition: config.h:24
virtual bool parse()
Definition: language_ui.cpp:37
std::wstring widen(const char *s)
Definition: unicode.cpp:56
languaget * language
Definition: language_file.h:41
mstreamt & status()
Definition: message.h:238
uit get_ui()
Definition: language_ui.h:47
std::list< std::string > tmp_dirs
Definition: compile.h:44
cmdlinet & cmdline
Definition: compile.h:76
std::list< std::string > libraries
Definition: compile.h:43
std::list< std::string > defines
Definition: config.h:111
enum compilet::@2 mode
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
std::list< std::string > library_paths
Definition: compile.h:40
language_filest language_files
Definition: language_ui.h:23
unsigned function_body_count(const goto_functionst &)
Definition: compile.cpp:669
std::string get_value(char option) const
Definition: cmdline.cpp:46
virtual bool typecheck()
Definition: language_ui.cpp:99
const cmdlinet & _cmdline
Definition: language_ui.h:53
unsignedbv_typet size_type()
Definition: c_types.cpp:57
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:74
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:35
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:282
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool parse(std::istream &instream, const std::string &path) override
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 write_bin_object_file(const std::string &, const symbol_tablet &, goto_functionst &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:591
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
std::string get_current_working_directory()
Definition: file_util.cpp:44
bool parse_stdin()
parses a source file (low-level parsing)
Definition: compile.cpp:534
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
argst args
Definition: cmdline.h:35
virtual bool isset(char option) const
Definition: cmdline.cpp:30
symbolst symbols
Definition: symbol_table.h:57
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
Definition: compile.cpp:388
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool warning_is_fatal
Definition: compile.h:77
bool parse_source(const std::string &)
parses a source file
Definition: compile.cpp:626
goto_functionst compiled_functions
Definition: compile.h:27
void delete_directory(const std::string &path)
deletes all files in &#39;path&#39; and then the directory itself
Definition: file_util.cpp:95
The symbol table.
Definition: symbol_table.h:52
Function Inlining.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
namespacet ns
Definition: compile.h:26
bool read_object_and_link(const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads an object file
bool echo_file_name
Definition: compile.h:28
std::string working_directory
Definition: compile.h:29
binary irep conversions with hashing
mstreamt & statistics()
Definition: message.h:243
bool write_object_file(const std::string &, const symbol_tablet &, goto_functionst &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:579
bool is_elf_file(const std::string &)
checking if we can load an object file
Definition: compile.cpp:322
Compile and link source and object files.
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
bool ansi_c_entry_point(symbol_tablet &symbol_table, const std::string &standard_main, message_handlert &message_handler)
languaget * get_language_from_mode(const irep_idt &mode)
Definition: mode.cpp:40
Goto Programs with Functions.
std::string get_temporary_directory(const std::string &name_template)
Definition: tempdir.cpp:32
void convert_symbols(goto_functionst &dest)
Definition: compile.cpp:688
Base class for all expressions.
Definition: expr.h:46
languaget * get_language_from_filename(const std::string &filename)
Definition: mode.cpp:51
file_mapt file_map
Definition: language_file.h:63
Program Transformation.
std::string filename
Definition: language_file.h:42
mstreamt & error()
Definition: message.h:223
std::string object_file_extension
Definition: compile.h:47
std::list< std::string > source_files
Definition: compile.h:41
#define CBMC_VERSION
Definition: version.h:4
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
std::list< std::string > object_files
Definition: compile.h:42
bool write_goto_binary(std::ostream &out, const symbol_tablet &lsymbol_table, const goto_functionst &functions, int version)
Writes a goto program to disc.
virtual bool parse(std::istream &instream, const std::string &path)=0
bool link()
parses object files and links them
Definition: compile.cpp:342
Base Type Computation.
void add_compiler_specific_defines(class configt &config) const
Definition: compile.cpp:683
void convert_function(const irep_idt &identifier)
std::string override_language
Definition: compile.h:30
Write GOTO binaries.
std::string output_file_object
Definition: compile.h:48
~compilet()
cleans up temporary files
Definition: compile.cpp:659
unsigned get_message_count(unsigned level) const
Definition: message.h:47