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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
lazy_goto_functions_mapt::can_generate_function_bodyt
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
Definition: lazy_goto_functions_map.h:59
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:251
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
lazy_goto_modelt::driver_program_generate_function_body
const generate_function_bodyt driver_program_generate_function_body
Definition: lazy_goto_model.h:261
optionst
Definition: options.h:22
lazy_goto_modelt::goto_functions
const lazy_goto_functions_mapt goto_functions
Definition: lazy_goto_model.h:254
lazy_goto_modelt::process_whole_model_and_freeze
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...
Definition: lazy_goto_model.h:200
lazy_goto_modelt::add_language_file
language_filet & add_language_file(const std::string &filename)
Definition: lazy_goto_model.h:189
lazy_goto_modelt::language_files
language_filest language_files
Definition: lazy_goto_model.h:255
language_filet
Definition: language_file.h:40
goto_model.h
lazy_goto_functions_mapt
Provides a wrapper for a map of lazily loaded goto_functiont.
Definition: lazy_goto_functions_map.h:29
goto_modelt
Definition: goto_model.h:24
lazy_goto_functions_mapt::unload
void unload(const key_type &name) const
Definition: lazy_goto_functions_map.h:133
lazy_goto_modelt::operator=
lazy_goto_modelt & operator=(lazy_goto_modelt &&other)
Definition: lazy_goto_model.h:130
lazy_goto_modelt::can_produce_function
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: lazy_goto_model.cpp:281
lazy_goto_modelt::message_handler
message_handlert & message_handler
Logging helper field.
Definition: lazy_goto_model.h:264
lazy_goto_modelt::can_generate_function_bodyt
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...
Definition: lazy_goto_model.h:69
lazy_goto_modelt::driver_program_can_generate_function_body
const can_generate_function_bodyt driver_program_can_generate_function_body
Definition: lazy_goto_model.h:260
lazy_goto_modelt::finalize
bool finalize()
Definition: lazy_goto_model.cpp:256
lazy_goto_modelt::from_handler_object
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.
Definition: lazy_goto_model.h:152
lazy_goto_modelt::get_goto_function
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function body.
Definition: lazy_goto_model.h:240
lazy_goto_functions_mapt::at
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
Definition: lazy_goto_functions_map.h:108
abstract_goto_model.h
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:41
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
lazy_goto_modelt::generate_function_bodyt
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...
Definition: lazy_goto_model.h:92
lazy_goto_functions_map.h
Author: Diffblue Ltd.
lazy_goto_modelt::goto_model
std::unique_ptr< goto_modelt > goto_model
Definition: lazy_goto_model.h:247
lazy_goto_modelt::unload
void unload(const irep_idt &name) const
Definition: lazy_goto_model.h:187
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
message_handlert
Definition: message.h:24
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
lazy_goto_modelt::initialize
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 ...
Definition: lazy_goto_model.cpp:110
lazy_goto_modelt::post_process_functions
const post_process_functionst post_process_functions
Definition: lazy_goto_model.h:259
lazy_goto_modelt::post_process_function
const post_process_functiont post_process_function
Definition: lazy_goto_model.h:258
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
lazy_goto_functions_mapt::generate_function_bodyt
std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> generate_function_bodyt
Definition: lazy_goto_functions_map.h:66
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:19
lazy_goto_modelt::load_all_functions
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Definition: lazy_goto_model.cpp:228
lazy_goto_modelt::post_process_functiont
std::function< void(goto_model_functiont &function, const abstract_goto_modelt &model)> post_process_functiont
Callback function that post-processes a GOTO function.
Definition: lazy_goto_model.h:53
goto_convert_functions.h
lazy_goto_modelt::get_goto_functions
const goto_functionst & get_goto_functions() const override
Accessor to retrieve the internal goto_functionst.
Definition: lazy_goto_model.h:214
lazy_goto_modelt::post_process_functionst
std::function< bool(goto_modelt &goto_model)> post_process_functionst
Callback function that post-processes a whole GOTO model.
Definition: lazy_goto_model.h:60
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
lazy_goto_modelt::lazy_goto_modelt
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.
lazy_goto_modelt::get_symbol_table
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
Definition: lazy_goto_model.h:219
language_file.h
language_filest
Definition: language_file.h:61