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 <cstring>
17 #include <fstream>
18 #include <iostream>
19 
20 #include <util/cmdline.h>
21 #include <util/config.h>
22 #include <util/file_util.h>
23 #include <util/get_base_name.h>
24 #include <util/suffix.h>
26 #include <util/tempdir.h>
27 #include <util/unicode.h>
28 #include <util/version.h>
29 
30 #include <ansi-c/ansi_c_language.h>
32 
37 
38 #include <langapi/language_file.h>
39 #include <langapi/mode.h>
40 
42 
43 #define DOTGRAPHSETTINGS "color=black;" \
44  "orientation=portrait;" \
45  "fontsize=20;"\
46  "compound=true;"\
47  "size=\"30,40\";"\
48  "ratio=compress;"
49 
50 // the following are for chdir
51 
52 #if defined(__linux__) || \
53  defined(__FreeBSD_kernel__) || \
54  defined(__GNU__) || \
55  defined(__unix__) || \
56  defined(__CYGWIN__) || \
57  defined(__MACH__)
58 #include <unistd.h>
59 #endif
60 
61 #ifdef _WIN32
62 #include <util/pragma_push.def>
63 #ifdef _MSC_VER
64 #pragma warning(disable:4668)
65  // using #if/#elif on undefined macro
66 #endif
67 #include <direct.h>
68 #include <windows.h>
69 #define chdir _chdir
70 #define popen _popen
71 #define pclose _pclose
72 #include <util/pragma_pop.def>
73 #endif
74 
79 {
81 
83 
84  // Parse command line for source and object file names
85  for(const auto &arg : cmdline.args)
86  if(add_input_file(arg))
87  return true;
88 
89  for(const auto &library : libraries)
90  {
91  if(!find_library(library))
92  // GCC is going to complain if this doesn't exist
93  debug() << "Library not found: " << library << " (ignoring)" << eom;
94  }
95 
96  statistics() << "No. of source files: " << source_files.size() << eom;
97  statistics() << "No. of object files: " << object_files.size() << eom;
98 
99  // Work through the given source files
100 
101  if(source_files.empty() && object_files.empty())
102  {
103  error() << "no input files" << eom;
104  return true;
105  }
106 
107  if(mode==LINK_LIBRARY && !source_files.empty())
108  {
109  error() << "cannot link source files" << eom;
110  return true;
111  }
112 
113  if(mode==PREPROCESS_ONLY && !object_files.empty())
114  {
115  error() << "cannot preprocess object files" << eom;
116  return true;
117  }
118 
119  const unsigned warnings_before=
121 
122  if(!source_files.empty())
123  if(compile())
124  return true;
125 
126  if(mode==LINK_LIBRARY ||
127  mode==COMPILE_LINK ||
129  {
130  if(link())
131  return true;
132  }
133 
134  return
137  warnings_before;
138 }
139 
140 enum class file_typet
141 {
143  UNKNOWN,
144  SOURCE_FILE,
146  THIN_ARCHIVE,
147  GOTO_BINARY,
148  ELF_OBJECT
149 };
150 
151 static file_typet detect_file_type(const std::string &file_name)
152 {
153  // first of all, try to open the file
154  std::ifstream in(file_name);
155  if(!in)
157 
158  const std::string::size_type r = file_name.rfind('.');
159 
160  const std::string ext =
161  r == std::string::npos ? "" : file_name.substr(r + 1, file_name.length());
162 
163  if(
164  ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
165  ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
166  ext == "jar" || ext == "jsil")
167  {
169  }
170 
171  char hdr[8];
172  in.get(hdr, 8);
173  if((ext == "a" || ext == "o") && strncmp(hdr, "!<thin>", 8) == 0)
175 
176  if(ext == "a")
178 
179  if(is_goto_binary(file_name))
181 
182  if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
183  return file_typet::ELF_OBJECT;
184 
185  return file_typet::UNKNOWN;
186 }
187 
190 bool compilet::add_input_file(const std::string &file_name)
191 {
192  switch(detect_file_type(file_name))
193  {
195  warning() << "failed to open file `" << file_name
196  << "': " << std::strerror(errno) << eom;
197  return warning_is_fatal; // generously ignore unless -Werror
198 
199  case file_typet::UNKNOWN:
200  // unknown extension, not a goto binary, will silently ignore
201  debug() << "unknown file type in `" << file_name << "'" << eom;
202  return false;
203 
205  // ELF file without goto-cc section, silently ignore
206  debug() << "ELF object without goto-cc section: `" << file_name << "'"
207  << eom;
208  return false;
209 
211  source_files.push_back(file_name);
212  return false;
213 
215  return add_files_from_archive(file_name, false);
216 
218  return add_files_from_archive(file_name, true);
219 
221  object_files.push_back(file_name);
222  return false;
223  }
224 
225  UNREACHABLE;
226 }
227 
231  const std::string &file_name,
232  bool thin_archive)
233 {
234  std::stringstream cmd;
235  FILE *stream;
236 
237  std::string tstr = working_directory;
238 
239  if(!thin_archive)
240  {
241  tstr = get_temporary_directory("goto-cc.XXXXXX");
242 
243  if(tstr=="")
244  {
245  error() << "Cannot create temporary directory" << eom;
246  return true;
247  }
248 
249  tmp_dirs.push_back(tstr);
250  if(chdir(tmp_dirs.back().c_str())!=0)
251  {
252  error() << "Cannot switch to temporary directory" << eom;
253  return true;
254  }
255 
256  // unpack now
257  cmd << "ar x " << concat_dir_file(working_directory, file_name);
258 
259  stream=popen(cmd.str().c_str(), "r");
260  pclose(stream);
261 
262  cmd.clear();
263  cmd.str("");
264  }
265 
266  // add the files from "ar t"
267  cmd << "ar t " << concat_dir_file(working_directory, file_name);
268 
269  stream = popen(cmd.str().c_str(), "r");
270 
271  if(stream != nullptr)
272  {
273  std::string line;
274  int ch; // fgetc returns an int, not char
275  while((ch = fgetc(stream)) != EOF)
276  {
277  if(ch != '\n')
278  {
279  line += static_cast<char>(ch);
280  }
281  else
282  {
283  std::string t = concat_dir_file(tstr, line);
284 
285  if(is_goto_binary(t))
286  object_files.push_back(t);
287  else
288  debug() << "Object file is not a goto binary: " << line << eom;
289 
290  line = "";
291  }
292  }
293 
294  pclose(stream);
295  }
296 
297  if(!thin_archive && chdir(working_directory.c_str()) != 0)
298  error() << "Could not change back to working directory" << eom;
299 
300  return false;
301 }
302 
306 bool compilet::find_library(const std::string &name)
307 {
308  std::string tmp;
309 
310  for(const auto &library_path : library_paths)
311  {
312  #ifdef _WIN32
313  tmp = library_path + "\\lib";
314  #else
315  tmp = library_path + "/lib";
316  #endif
317 
318  std::ifstream in(tmp+name+".a");
319 
320  if(in.is_open())
321  return !add_input_file(tmp+name+".a");
322  else
323  {
324  std::string libname=tmp+name+".so";
325 
326  switch(detect_file_type(libname))
327  {
329  return !add_input_file(libname);
330 
332  warning() << "Warning: Cannot read ELF library " << libname << eom;
333  return warning_is_fatal;
334 
335  default:
336  break;
337  }
338  }
339  }
340 
341  return false;
342 }
343 
347 {
348  // "compile" hitherto uncompiled functions
349  statistics() << "Compiling functions" << eom;
351 
352  // parse object files
353  for(const auto &file_name : object_files)
354  {
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
367 
371 
372  const bool error = ansi_c_entry_point(
376 
377  if(error)
378  return true;
379 
380  // entry_point may (should) add some more functions.
382  }
383 
385  return true;
386 
388 }
389 
394 {
395  while(!source_files.empty())
396  {
397  std::string file_name=source_files.front();
398  source_files.pop_front();
399 
400  // Visual Studio always prints the name of the file it's doing
401  // onto stdout. The name of the directory is stripped.
402  if(echo_file_name)
403  std::cout << get_base_name(file_name, false) << '\n' << std::flush;
404 
405  bool r=parse_source(file_name); // don't break the program!
406 
407  if(r)
408  {
409  const std::string &debug_outfile=
410  cmdline.get_value("print-rejected-preprocessed-source");
411  if(!debug_outfile.empty())
412  {
413  std::ifstream in(file_name, std::ios::binary);
414  std::ofstream out(debug_outfile, std::ios::binary);
415  out << in.rdbuf();
416  warning() << "Failed sources in " << debug_outfile << eom;
417  }
418 
419  return true; // parser/typecheck error
420  }
421 
423  {
424  // output an object file for every source file
425 
426  // "compile" functions
428 
429  std::string cfn;
430 
431  if(output_file_object=="")
432  {
433  const std::string file_name_with_obj_ext =
434  get_base_name(file_name, true) + "." + object_file_extension;
435 
436  if(!output_directory_object.empty())
437  cfn = concat_dir_file(output_directory_object, file_name_with_obj_ext);
438  else
439  cfn = file_name_with_obj_ext;
440  }
441  else
442  cfn = output_file_object;
443 
444  if(write_object_file(cfn, goto_model))
445  return true;
446 
448  return true;
449 
450  goto_model.clear(); // clean symbol table for next source file.
451  }
452  }
453 
454  return false;
455 }
456 
460  const std::string &file_name,
461  language_filest &language_files)
462 {
463  if(file_name=="-")
464  return parse_stdin();
465 
466  #ifdef _MSC_VER
467  std::ifstream infile(widen(file_name));
468  #else
469  std::ifstream infile(file_name);
470  #endif
471 
472  if(!infile)
473  {
474  error() << "failed to open input file `" << file_name << "'" << eom;
475  return true;
476  }
477 
478  std::unique_ptr<languaget> languagep;
479 
480  // Using '-x', the type of a file can be overridden;
481  // otherwise, it's guessed from the extension.
482 
483  if(override_language!="")
484  {
485  if(override_language=="c++" || override_language=="c++-header")
486  languagep = get_language_from_mode(ID_cpp);
487  else
488  languagep = get_language_from_mode(ID_C);
489  }
490  else
491  languagep=get_language_from_filename(file_name);
492 
493  if(languagep==nullptr)
494  {
495  error() << "failed to figure out type of file `" << file_name << "'" << eom;
496  return true;
497  }
498 
500 
501  language_filet &lf=language_files.add_file(file_name);
502  lf.language=std::move(languagep);
503 
504  if(mode==PREPROCESS_ONLY)
505  {
506  statistics() << "Preprocessing: " << file_name << eom;
507 
508  std::ostream *os = &std::cout;
509  std::ofstream ofs;
510 
511  if(cmdline.isset('o'))
512  {
513  ofs.open(cmdline.get_value('o'));
514  os = &ofs;
515 
516  if(!ofs.is_open())
517  {
518  error() << "failed to open output file `"
519  << cmdline.get_value('o') << "'" << eom;
520  return true;
521  }
522  }
523 
524  lf.language->preprocess(infile, file_name, *os);
525  }
526  else
527  {
528  statistics() << "Parsing: " << file_name << eom;
529 
530  if(lf.language->parse(infile, file_name))
531  {
532  error() << "PARSING ERROR" << eom;
533  return true;
534  }
535  }
536 
537  lf.get_modules();
538  return false;
539 }
540 
544 {
545  ansi_c_languaget language;
546 
548 
549  statistics() << "Parsing: (stdin)" << eom;
550 
551  if(mode==PREPROCESS_ONLY)
552  {
553  std::ostream *os = &std::cout;
554  std::ofstream ofs;
555 
556  if(cmdline.isset('o'))
557  {
558  ofs.open(cmdline.get_value('o'));
559  os = &ofs;
560 
561  if(!ofs.is_open())
562  {
563  error() << "failed to open output file `"
564  << cmdline.get_value('o') << "'" << eom;
565  return true;
566  }
567  }
568 
569  language.preprocess(std::cin, "", *os);
570  }
571  else
572  {
573  if(language.parse(std::cin, ""))
574  {
575  error() << "PARSING ERROR" << eom;
576  return true;
577  }
578  }
579 
580  return false;
581 }
582 
588  const std::string &file_name,
589  const goto_modelt &goto_model)
590 {
591  return write_bin_object_file(file_name, goto_model);
592 }
593 
599  const std::string &file_name,
600  const goto_modelt &goto_model)
601 {
602  statistics() << "Writing binary format object `"
603  << file_name << "'" << eom;
604 
605  // symbols
606  statistics() << "Symbols in table: " << goto_model.symbol_table.symbols.size()
607  << eom;
608 
609  std::ofstream outfile(file_name, std::ios::binary);
610 
611  if(!outfile.is_open())
612  {
613  error() << "Error opening file `" << file_name << "'" << eom;
614  return true;
615  }
616 
617  if(write_goto_binary(outfile, goto_model))
618  return true;
619 
621 
622  statistics() << "Functions: " << goto_model.goto_functions.function_map.size()
623  << "; " << cnt << " have a body." << eom;
624 
625  outfile.close();
626  wrote_object=true;
627 
628  return false;
629 }
630 
633 bool compilet::parse_source(const std::string &file_name)
634 {
635  language_filest language_files;
636  language_files.set_message_handler(get_message_handler());
637 
638  if(parse(file_name, language_files))
639  return true;
640 
641  // we just typecheck one file here
642  if(language_files.typecheck(goto_model.symbol_table))
643  {
644  error() << "CONVERSION ERROR" << eom;
645  return true;
646  }
647 
648  if(language_files.final(goto_model.symbol_table))
649  {
650  error() << "CONVERSION ERROR" << eom;
651  return true;
652  }
653 
654  return false;
655 }
656 
659 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
660  : messaget(mh),
661  ns(goto_model.symbol_table),
662  cmdline(_cmdline),
663  warning_is_fatal(Werror)
664 {
666  echo_file_name=false;
667  wrote_object=false;
669 }
670 
674 {
675  // clean up temp dirs
676 
677  for(const auto &dir : tmp_dirs)
678  delete_directory(dir);
679 }
680 
681 std::size_t
683 {
684  std::size_t count = 0;
685 
686  for(const auto &f : functions.function_map)
687  if(f.second.body_available())
688  count++;
689 
690  return count;
691 }
692 
694 {
695  config.ansi_c.defines.push_back(
696  std::string("__GOTO_CC_VERSION__=") + CBMC_VERSION);
697 }
698 
700 {
701  symbol_table_buildert symbol_table_builder =
703 
704  goto_convert_functionst converter(
705  symbol_table_builder, get_message_handler());
706 
707  // the compilation may add symbols!
708 
710 
711  while(before != symbol_table_builder.symbols.size())
712  {
713  before = symbol_table_builder.symbols.size();
714 
715  typedef std::set<irep_idt> symbols_sett;
716  symbols_sett symbols;
717 
718  for(const auto &named_symbol : symbol_table_builder.symbols)
719  symbols.insert(named_symbol.first);
720 
721  // the symbol table iterators aren't stable
722  for(const auto &symbol : symbols)
723  {
724  symbol_tablet::symbolst::const_iterator s_it =
725  symbol_table_builder.symbols.find(symbol);
726  CHECK_RETURN(s_it != symbol_table_builder.symbols.end());
727 
728  if(
729  s_it->second.is_function() && !s_it->second.is_compiled() &&
730  s_it->second.value.is_not_nil())
731  {
732  debug() << "Compiling " << s_it->first << eom;
733  converter.convert_function(s_it->first, dest.function_map[s_it->first]);
734  symbol_table_builder.get_writeable_ref(symbol).set_compiled();
735  }
736  }
737  }
738 }
739 
741 {
742  for(const auto &pair : symbol_table.symbols)
743  {
744  const irep_idt &name=pair.second.name;
745  const typet &new_type=pair.second.type;
746  if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
747  continue;
748 
749  bool inserted;
750  std::map<irep_idt, symbolt>::iterator old;
751  std::tie(old, inserted)=written_macros.insert({name, pair.second});
752 
753  if(!inserted && old->second.type!=new_type)
754  {
755  error() << "Incompatible CPROVER macro symbol types:" << eom
756  << old->second.type.pretty() << "(at " << old->second.location
757  << ")" << eom << "and" << eom << new_type.pretty()
758  << "(at " << pair.second.location << ")" << eom;
759  return true;
760  }
761  }
762  return false;
763 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:141
The type of an expression, extends irept.
Definition: type.h:27
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
Definition: compile.cpp:190
struct configt::ansi_ct ansi_c
std::string output_file_executable
Definition: compile.h:53
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_modelt goto_model
Definition: compile.h:30
Globally accessible architectural configuration.
Definition: config.h:24
bool final(symbol_table_baset &symbol_table)
static file_typet detect_file_type(const std::string &file_name)
Definition: compile.cpp:151
std::wstring widen(const char *s)
Definition: unicode.cpp:52
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
#define CPROVER_PREFIX
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:119
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
std::list< std::string > tmp_dirs
Definition: compile.h:49
cmdlinet & cmdline
Definition: compile.h:96
std::list< std::string > libraries
Definition: compile.h:48
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::list< std::string > defines
Definition: config.h:121
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
std::list< std::string > library_paths
Definition: compile.h:45
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
std::string get_value(char option) const
Definition: cmdline.cpp:45
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:659
function_mapt function_map
unsignedbv_typet size_type()
Definition: c_types.cpp:58
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:78
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:101
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:306
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bool parse(std::istream &instream, const std::string &path) override
configt config
Definition: config.cpp:24
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
file_typet
Definition: compile.cpp:140
std::string get_current_working_directory()
Definition: file_util.cpp:48
bool parse_stdin()
parses a source file (low-level parsing)
Definition: compile.cpp:543
mstreamt & warning() const
Definition: message.h:391
std::unique_ptr< languaget > language
Definition: language_file.h:46
const irep_idt & id() const
Definition: irep.h:259
bool write_bin_object_file(const std::string &, const goto_modelt &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:598
argst args
Definition: cmdline.h:44
virtual bool isset(char option) const
Definition: cmdline.cpp:27
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
Definition: compile.cpp:393
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
bool write_object_file(const std::string &, const goto_modelt &)
writes the goto functions in the function table to a binary format object file.
Definition: compile.cpp:587
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool warning_is_fatal
Definition: compile.h:97
bool parse_source(const std::string &)
parses a source file
Definition: compile.cpp:633
#define INITIALIZE_FUNCTION
void delete_directory(const std::string &path)
deletes all files in 'path' and then the directory itself
Definition: file_util.cpp:100
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:386
bool typecheck(symbol_tablet &symbol_table)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A collection of goto functions.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bool wrote_object
Definition: compile.h:113
bool echo_file_name
Definition: compile.h:33
const symbolst & symbols
std::string working_directory
Definition: compile.h:34
void clear()
Definition: goto_model.h:34
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:106
static eomt eom
Definition: message.h:284
Compile and link source and object files.
bool add_files_from_archive(const std::string &file_name, bool thin_archive)
extracts goto binaries from AR archive and add them as input files.
Definition: compile.cpp:230
message_handlert & get_message_handler()
Definition: message.h:174
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
std::string get_temporary_directory(const std::string &name_template)
Definition: tempdir.cpp:38
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
void convert_symbols(goto_functionst &dest)
Definition: compile.cpp:699
const char * CBMC_VERSION
Definition: version.cpp:1
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
std::size_t function_body_count(const goto_functionst &) const
Definition: compile.cpp:682
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
std::size_t get_message_count(unsigned level) const
Definition: message.h:51
Program Transformation.
std::string object_file_extension
Definition: compile.h:52
Author: Diffblue Ltd.
std::list< std::string > source_files
Definition: compile.h:46
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:459
std::list< std::string > object_files
Definition: compile.h:47
mstreamt & debug() const
Definition: message.h:416
bool link()
parses object files and links them
Definition: compile.cpp:346
void add_compiler_specific_defines(class configt &config) const
Definition: compile.cpp:693
std::string output_directory_object
Definition: compile.h:56
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
std::string override_language
Definition: compile.h:35
Write GOTO binaries.
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:740
std::string output_file_object
Definition: compile.h:56
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
mstreamt & statistics() const
Definition: message.h:406
enum compilet::@3 mode
~compilet()
cleans up temporary files
Definition: compile.cpp:673