lazy_goto_model.h

Go to the documentation of this file.

 
 
#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
 
#include <langapi/language_file.h>
 
#include <goto-programs/abstract_goto_model.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/goto_model.h>
 
#include "lazy_goto_functions_map.h"
 
class optionst;
 
class lazy_goto_modelt : public abstract_goto_modelt
{
public:
  typedef std::function<
    void(goto_model_functiont &function, const abstract_goto_modelt &model)>
    post_process_functiont;
 
  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
 
  typedef lazy_goto_functions_mapt::can_generate_function_bodyt
    can_generate_function_bodyt;
 
  typedef lazy_goto_functions_mapt::generate_function_bodyt
    generate_function_bodyt;
 
  explicit lazy_goto_modelt(
    post_process_functiont post_process_function,
    post_process_functionst post_process_functions,
    can_generate_function_bodyt driver_program_can_generate_function_body,
    generate_function_bodyt driver_program_generate_function_body,
    message_handlert &message_handler);
 
  lazy_goto_modelt(lazy_goto_modelt &&other);
 
  lazy_goto_modelt &operator=(lazy_goto_modelt &&other)
  {
    goto_model = std::move(other.goto_model);
    language_files = std::move(other.language_files);
    return *this;
  }
 
  template <typename THandler>
  static lazy_goto_modelt from_handler_object(
    THandler &handler,
    const optionst &options,
    message_handlert &message_handler)
  {
    return lazy_goto_modelt(
      [&handler,
       &options](goto_model_functiont &fun, const abstract_goto_modelt &model) {
        handler.process_goto_function(fun, model, options);
      },
      [&handler, &options](goto_modelt &goto_model) -> bool {
        return handler.process_goto_functions(goto_model, options);
      },
      [&handler](const irep_idt &name) -> bool {
        return handler.can_generate_function_body(name);
      },
      [&handler](
        const irep_idt &function_name,
        symbol_table_baset &symbol_table,
        goto_functiont &function,
        bool is_first_chance) {
        return handler.generate_function_body(
          function_name, symbol_table, function, is_first_chance);
      },
      message_handler);
  }
 
  void
  initialize(const std::vector<std::string> &files, const optionst &options);
 
  void load_all_functions() const;
 
  language_filet &add_language_file(const std::string &filename)
  {
    return language_files.add_file(filename);
  }
 
  static std::unique_ptr<goto_modelt>
  process_whole_model_and_freeze(lazy_goto_modelt &&model)
  {
    if(model.finalize())
      return nullptr;
    return std::move(model.goto_model);
  }
 
  // Implement the abstract_goto_modelt interface:
 
  const goto_functionst &get_goto_functions() const override
  {
    return goto_model->goto_functions;
  }
 
  const symbol_tablet &get_symbol_table() const override
  {
    return symbol_table;
  }
 
  bool can_produce_function(const irep_idt &id) const override;
 
  const goto_functionst::goto_functiont &
  get_goto_function(const irep_idt &id) override
  {
    return goto_functions.at(id);
  }
 
  void validate(
    const validation_modet vm = validation_modet::INVARIANT,
    const goto_model_validation_optionst &goto_model_validation_options =
      goto_model_validation_optionst{}) const override
  {
    goto_model->validate(vm, goto_model_validation_options);
  }
 
private:
  std::unique_ptr<goto_modelt> goto_model;
 
public:
  symbol_tablet &symbol_table;
 
private:
  const lazy_goto_functions_mapt goto_functions;
  language_filest language_files;
 
  // Function/module processing functions
  const post_process_functiont post_process_function;
  const post_process_functionst post_process_functions;
  const can_generate_function_bodyt driver_program_can_generate_function_body;
  const generate_function_bodyt driver_program_generate_function_body;
 
  message_handlert &message_handler;
 
  bool finalize();
};
 
#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H