cprover
compile.h
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 #ifndef CPROVER_GOTO_CC_COMPILE_H
15 #define CPROVER_GOTO_CC_COMPILE_H
16 
17 #include <util/cmdline.h>
18 #include <util/message.h>
19 #include <util/rename_symbol.h>
20 
22 
23 class language_filest;
24 class languaget;
25 
26 class compilet : public messaget
27 {
28 public:
29  // compilation results
32 
33  // configuration
35  std::string working_directory;
36  std::string override_language;
37  bool validate_goto_model = false;
38 
39  enum { PREPROCESS_ONLY, // gcc -E
40  COMPILE_ONLY, // gcc -c
41  ASSEMBLE_ONLY, // gcc -S
42  LINK_LIBRARY, // ld -r
43  COMPILE_LINK, // gcc -shared
45  } mode;
46 
47  std::list<std::string> library_paths;
48  std::list<std::string> source_files;
49  std::list<std::string> object_files;
50  std::list<std::string> libraries;
51  std::list<std::string> tmp_dirs;
52  std::list<irep_idt> seen_modes;
53 
54  std::string object_file_extension;
56 
57  // the two options below are mutually exclusive -- use either or
59 
60  compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror);
61 
62  ~compilet();
63 
64  bool add_input_file(const std::string &);
65  bool find_library(const std::string &);
66  bool add_files_from_archive(const std::string &file_name, bool thin_archive);
67 
68  bool parse(const std::string &filename, language_filest &);
69  bool parse_stdin(languaget &);
70  bool doit();
71  bool compile();
72  bool link();
73 
74  bool parse_source(const std::string &);
75 
76  bool write_bin_object_file(const std::string &, const goto_modelt &);
77 
79  bool wrote_object_files() const { return wrote_object; }
80 
87  std::size_t> &cprover_macros) const
88  {
90  for(const auto &pair : written_macros)
91  cprover_macros.insert({pair.first,
92  to_code_type(pair.second.type).parameters().size()});
93  }
94 
95 protected:
98 
100  const bool keep_file_local;
101 
103  const std::string file_local_mangle_suffix;
104 
105  std::size_t function_body_count(const goto_functionst &) const;
106 
107  void add_compiler_specific_defines() const;
108 
109  void convert_symbols(goto_functionst &dest);
110 
111  bool add_written_cprover_symbols(const symbol_tablet &symbol_table);
112  std::map<irep_idt, symbolt> written_macros;
113 
114  // clients must only call add_written_cprover_symbols() if an object
115  // file has been written. The case where an object file was written
116  // but there were no __CPROVER symbols in the goto-program is distinct
117  // from the case where the user forgot to write an object file before
118  // calling add_written_cprover_symbols().
120 };
121 
122 #endif // CPROVER_GOTO_CC_COMPILE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
compilet::wrote_object
bool wrote_object
Definition: compile.h:119
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
compilet::echo_file_name
bool echo_file_name
Definition: compile.h:34
compilet::source_files
std::list< std::string > source_files
Definition: compile.h:48
compilet::parse
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
Definition: compile.cpp:438
compilet::add_files_from_archive
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:211
compilet::parse_stdin
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
Definition: compile.cpp:523
compilet::ASSEMBLE_ONLY
@ ASSEMBLE_ONLY
Definition: compile.h:41
compilet::function_body_count
std::size_t function_body_count(const goto_functionst &) const
Definition: compile.cpp:665
compilet::doit
bool doit()
reads and source and object files, compiles and links them into goto program objects.
Definition: compile.cpp:57
goto_model.h
Symbol Table + CFG.
compilet::libraries
std::list< std::string > libraries
Definition: compile.h:50
goto_modelt
Definition: goto_model.h:26
compilet::cmdline
cmdlinet & cmdline
Definition: compile.h:96
rename_symbol.h
compilet::LINK_LIBRARY
@ LINK_LIBRARY
Definition: compile.h:42
compilet::validate_goto_model
bool validate_goto_model
Definition: compile.h:37
compilet::wrote_object_files
bool wrote_object_files() const
Has this compiler written any object files?
Definition: compile.h:79
compilet::add_compiler_specific_defines
void add_compiler_specific_defines() const
Definition: compile.cpp:676
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
compilet::link
bool link()
parses object files and links them
Definition: compile.cpp:311
compilet::written_macros
std::map< irep_idt, symbolt > written_macros
Definition: compile.h:112
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
cmdlinet
Definition: cmdline.h:21
compilet::output_file_object
std::string output_file_object
Definition: compile.h:58
compilet::object_files
std::list< std::string > object_files
Definition: compile.h:49
compilet::add_written_cprover_symbols
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
Definition: compile.cpp:723
compilet::working_directory
std::string working_directory
Definition: compile.h:35
compilet::mode
enum compilet::@2 mode
compilet::file_local_mangle_suffix
const std::string file_local_mangle_suffix
String to include in all mangled names.
Definition: compile.h:103
compilet::compilet
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
Definition: compile.cpp:631
compilet::output_file_executable
std::string output_file_executable
Definition: compile.h:55
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
compilet::convert_symbols
void convert_symbols(goto_functionst &dest)
Definition: compile.cpp:682
compilet::library_paths
std::list< std::string > library_paths
Definition: compile.h:47
compilet::COMPILE_LINK
@ COMPILE_LINK
Definition: compile.h:43
compilet::object_file_extension
std::string object_file_extension
Definition: compile.h:54
message_handlert
Definition: message.h:28
compilet::warning_is_fatal
bool warning_is_fatal
Definition: compile.h:97
compilet::~compilet
~compilet()
cleans up temporary files
Definition: compile.cpp:656
compilet::COMPILE_LINK_EXECUTABLE
@ COMPILE_LINK_EXECUTABLE
Definition: compile.h:44
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
compilet::override_language
std::string override_language
Definition: compile.h:36
compilet::PREPROCESS_ONLY
@ PREPROCESS_ONLY
Definition: compile.h:39
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
compilet::output_directory_object
std::string output_directory_object
Definition: compile.h:58
compilet::find_library
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
Definition: compile.cpp:270
compilet::keep_file_local
const bool keep_file_local
Whether to keep implementations of file-local symbols.
Definition: compile.h:100
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
compilet::compile
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
Definition: compile.cpp:365
compilet::parse_source
bool parse_source(const std::string &)
parses a source file
Definition: compile.cpp:605
cmdline.h
compilet::write_bin_object_file
bool write_bin_object_file(const std::string &, const goto_modelt &)
Writes the goto functions of src_goto_model to a binary format object file.
Definition: compile.cpp:564
languaget
Definition: language.h:40
compilet::seen_modes
std::list< irep_idt > seen_modes
Definition: compile.h:52
compilet::tmp_dirs
std::list< std::string > tmp_dirs
Definition: compile.h:51
compilet::ns
namespacet ns
Definition: compile.h:30
compilet::goto_model
goto_modelt goto_model
Definition: compile.h:31
compilet
Definition: compile.h:27
message.h
compilet::COMPILE_ONLY
@ COMPILE_ONLY
Definition: compile.h:40
compilet::cprover_macro_arities
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities
Definition: compile.h:86
language_filest
Definition: language_file.h:62