cprover
lazy_goto_model.h
Go to the documentation of this file.
1 
5 
6 #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
7 #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
8 
10 
11 #include "abstract_goto_model.h"
12 #include "goto_model.h"
14 #include "goto_convert_functions.h"
15 
16 class cmdlinet;
17 class optionst;
18 
21 {
22 public:
23  typedef std::function<
24  void(goto_model_functiont &function, const abstract_goto_modelt &)>
26  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
31 
32  explicit lazy_goto_modelt(
38 
40 
42  {
43  goto_model = std::move(other.goto_model);
44  language_files = std::move(other.language_files);
45  return *this;
46  }
47 
55  template<typename THandler>
57  THandler &handler,
58  const optionst &options,
60  {
61  return lazy_goto_modelt(
62  [&handler,
63  &options](goto_model_functiont &fun, const abstract_goto_modelt &model) {
64  handler.process_goto_function(fun, model, options);
65  },
66  [&handler, &options](goto_modelt &goto_model) -> bool {
67  return handler.process_goto_functions(goto_model, options);
68  },
69  [&handler](const irep_idt &name) -> bool {
70  return handler.can_generate_function_body(name);
71  },
72  [&handler]
73  (const irep_idt &function_name,
75  goto_functiont &function,
76  bool is_first_chance)
77  {
78  return
79  handler.generate_function_body(
80  function_name, symbol_table, function, is_first_chance);
81  },
83  }
84 
85  void initialize(const cmdlinet &cmdline);
86 
88  void load_all_functions() const;
89 
90  void unload(const irep_idt &name) const { goto_functions.unload(name); }
91 
92  language_filet &add_language_file(const std::string &filename)
93  {
94  return language_files.add_file(filename);
95  }
96 
103  static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
104  lazy_goto_modelt &&model)
105  {
106  if(model.finalize())
107  return nullptr;
108  return std::move(model.goto_model);
109  }
110 
111  // Implement the abstract_goto_modelt interface:
112 
117  const goto_functionst &get_goto_functions() const override
118  {
119  return goto_model->goto_functions;
120  }
121 
122  const symbol_tablet &get_symbol_table() const override
123  {
124  return symbol_table;
125  }
126 
127  bool can_produce_function(const irep_idt &id) const override;
128 
130  override
131  {
132  return goto_functions.at(id);
133  }
134 
135 private:
136  std::unique_ptr<goto_modelt> goto_model;
137 
138 public:
141 
142 private:
145 
146  // Function/module processing functions
151 
154 
155  bool finalize();
156 };
157 
158 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
lazy_goto_functions_mapt::can_generate_function_bodyt can_generate_function_bodyt
Abstract interface to eager or lazy GOTO models.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
void unload(const irep_idt &name) const
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
const post_process_functionst post_process_functions
const lazy_goto_functions_mapt goto_functions
static lazy_goto_modelt from_handler_object(THandler &handler, const optionst &options, message_handlert &message_handler)
Create a lazy_goto_modelt from a object that defines function/module pass handlers.
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)
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function by name, or throw if no such function exists.
Model that holds partially loaded map of functions.
const generate_function_bodyt driver_program_generate_function_body
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> generate_function_bodyt
void unload(const key_type &name) const
Abstract interface to eager or lazy GOTO models.
message_handlert & message_handler
Logging helper field.
language_filest language_files
Symbol Table + CFG.
std::function< bool(goto_modelt &goto_model)> post_process_functionst
lazy_goto_functions_mapt::generate_function_bodyt generate_function_bodyt
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
void initialize(const cmdlinet &cmdline)
const goto_functionst & get_goto_functions() const override
Accessor to retrieve the internal goto_functionst.
The symbol table.
Definition: symbol_table.h:19
static std::unique_ptr< goto_modelt > process_whole_model_and_freeze(lazy_goto_modelt &&model)
The model returned here has access to the functions we&#39;ve already loaded but is frozen in the sense t...
::goto_functiont goto_functiont
Provides a wrapper for a map of lazily loaded goto_functiont.
std::function< void(goto_model_functiont &function, const abstract_goto_modelt &)> post_process_functiont
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Goto Programs with Functions.
The symbol table base class interface.
std::unique_ptr< goto_modelt > goto_model
const can_generate_function_bodyt driver_program_can_generate_function_body
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
language_filet & add_language_file(const std::string &filename)
Author: Diffblue Ltd.
lazy_goto_modelt & operator=(lazy_goto_modelt &&other)
const post_process_functiont post_process_function
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147