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 optionst;
17 
42 {
43 public:
51  typedef std::function<
52  void(goto_model_functiont &function, const abstract_goto_modelt &model)>
54 
60  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
61 
70 
93 
121  explicit lazy_goto_modelt(
127 
129 
131  {
132  goto_model = std::move(other.goto_model);
133  language_files = std::move(other.language_files);
134  return *this;
135  }
136 
151  template<typename THandler>
153  THandler &handler,
154  const optionst &options,
156  {
157  return lazy_goto_modelt(
158  [&handler,
159  &options](goto_model_functiont &fun, const abstract_goto_modelt &model) {
160  handler.process_goto_function(fun, model, options);
161  },
162  [&handler, &options](goto_modelt &goto_model) -> bool {
163  return handler.process_goto_functions(goto_model, options);
164  },
165  [&handler](const irep_idt &name) -> bool {
166  return handler.can_generate_function_body(name);
167  },
168  [&handler]
169  (const irep_idt &function_name,
171  goto_functiont &function,
172  bool is_first_chance)
173  {
174  return
175  handler.generate_function_body(
176  function_name, symbol_table, function, is_first_chance);
177  },
179  }
180 
181  void
182  initialize(const std::vector<std::string> &files, const optionst &options);
183 
185  void load_all_functions() const;
186 
187  void unload(const irep_idt &name) const { goto_functions.unload(name); }
188 
189  language_filet &add_language_file(const std::string &filename)
190  {
191  return language_files.add_file(filename);
192  }
193 
200  static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
201  lazy_goto_modelt &&model)
202  {
203  if(model.finalize())
204  return nullptr;
205  return std::move(model.goto_model);
206  }
207 
208  // Implement the abstract_goto_modelt interface:
209 
214  const goto_functionst &get_goto_functions() const override
215  {
216  return goto_model->goto_functions;
217  }
218 
219  const symbol_tablet &get_symbol_table() const override
220  {
221  return symbol_table;
222  }
223 
224  bool can_produce_function(const irep_idt &id) const override;
225 
241  override
242  {
243  return goto_functions.at(id);
244  }
245 
246 private:
247  std::unique_ptr<goto_modelt> goto_model;
248 
249 public:
252 
253 private:
256 
257  // Function/module processing functions
262 
265 
266  bool finalize();
267 };
268 
269 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
lazy_goto_functions_mapt::can_generate_function_bodyt can_generate_function_bodyt
Callback function that determines whether the creator of a lazy_goto_modelt can itself supply a funct...
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)
Construct a lazy GOTO model, supplying callbacks that customise its behaviour.
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 body.
A GOTO model that produces function bodies on demand.
const generate_function_bodyt driver_program_generate_function_body
std::function< void(goto_model_functiont &function, const abstract_goto_modelt &model)> post_process_functiont
Callback function that post-processes a GOTO function.
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
Callback function that post-processes a whole GOTO model.
lazy_goto_functions_mapt::generate_function_bodyt generate_function_bodyt
Callback function that may provide a body for a GOTO function, either as a fallback (when we don't ha...
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
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'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.
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
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
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153