compile.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Compile and link source and object files.
 
Author: CM Wintersteiger
 
Date: June 2006
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CC_COMPILE_H
#define CPROVER_GOTO_CC_COMPILE_H
 
#include <util/message.h>
#include <util/std_types.h>
#include <util/symbol.h>
 
#include <list>
#include <map>
 
class cmdlinet;
class goto_functionst;
class goto_modelt;
class language_filest;
class languaget;
class symbol_tablet;
 
class compilet
{
public:
  // configuration
  bool echo_file_name;
  bool validate_goto_model = false;
 
  enum { PREPROCESS_ONLY, // gcc -E
         COMPILE_ONLY, // gcc -c
         ASSEMBLE_ONLY, // gcc -S
         LINK_LIBRARY, // ld -r
         COMPILE_LINK, // gcc -shared
         COMPILE_LINK_EXECUTABLE // gcc
       } mode;
 
  std::list<std::string> library_paths;
  std::list<std::string> source_files;
  std::list<std::string> object_files;
  std::list<std::string> libraries;
 
  std::string object_file_extension;
  std::string output_file_executable;
 
  // the two options below are mutually exclusive -- use either or
  std::string output_file_object, output_directory_object;
 
  compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror);
 
  ~compilet();
 
  bool add_input_file(const std::string &);
  bool find_library(const std::string &);
  bool add_files_from_archive(const std::string &file_name, bool thin_archive);
 
  bool parse(const std::string &filename, language_filest &);
  bool parse_stdin(languaget &);
  bool doit();
  std::optional<symbol_tablet> compile();
  bool link(std::optional<symbol_tablet> &&symbol_table);
 
  std::optional<symbol_tablet> parse_source(const std::string &);
 
  static bool write_bin_object_file(
    const std::string &file_name,
    const goto_modelt &src_goto_model,
    bool validate_goto_model,
    message_handlert &message_handler);
 
  bool wrote_object_files() const { return wrote_object; }
 
  void cprover_macro_arities(std::map<irep_idt,
                                      std::size_t> &cprover_macros) const
  {
    PRECONDITION(wrote_object);
    for(const auto &pair : written_macros)
      cprover_macros.insert({pair.first,
        to_code_type(pair.second.type).parameters().size()});
  }
 
protected:
  std::string working_directory;
  std::string override_language;
 
  std::list<std::string> tmp_dirs;
  std::list<irep_idt> seen_modes;
 
  messaget log;
  cmdlinet &cmdline;
  bool warning_is_fatal;
 
  const bool keep_file_local;
 
  const std::string file_local_mangle_suffix;
 
  static std::size_t function_body_count(const goto_functionst &);
 
  bool write_bin_object_file(
    const std::string &file_name,
    const goto_modelt &src_goto_model)
  {
    if(write_bin_object_file(
         file_name,
         src_goto_model,
         validate_goto_model,
         log.get_message_handler()))
    {
      return true;
    }
 
    wrote_object = true;
 
    return false;
  }
 
  void add_compiler_specific_defines() const;
 
  void convert_symbols(goto_modelt &);
 
  bool add_written_cprover_symbols(const symbol_tablet &symbol_table);
  std::map<irep_idt, symbolt> written_macros;
 
  // clients must only call add_written_cprover_symbols() if an object
  // file has been written. The case where an object file was written
  // but there were no __CPROVER symbols in the goto-program is distinct
  // from the case where the user forgot to write an object file before
  // calling add_written_cprover_symbols().
  bool wrote_object;
};
 
#endif // CPROVER_GOTO_CC_COMPILE_H