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 
14 
16 
17 class optionst;
18 
43 {
44 public:
52  typedef std::function<
53  void(goto_model_functiont &function, const abstract_goto_modelt &model)>
55 
61  typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
62 
71 
94 
128 
130 
132  {
133  goto_model = std::move(other.goto_model);
134  language_files = std::move(other.language_files);
135  return *this;
136  }
137 
152  template <typename THandler>
154  THandler &handler,
155  const optionst &options,
157  {
158  return lazy_goto_modelt(
159  [&handler,
160  &options](goto_model_functiont &fun, const abstract_goto_modelt &model) {
161  handler.process_goto_function(fun, model, options);
162  },
163  [&handler, &options](goto_modelt &goto_model) -> bool {
164  return handler.process_goto_functions(goto_model, options);
165  },
166  [&handler](const irep_idt &name) -> bool {
167  return handler.can_generate_function_body(name);
168  },
169  [&handler](
170  const irep_idt &function_name,
172  goto_functiont &function,
173  bool is_first_chance) {
174  return handler.generate_function_body(
175  function_name, symbol_table, function, is_first_chance);
176  },
178  }
179 
180  void
181  initialize(const std::vector<std::string> &files, const optionst &options);
182 
184  void load_all_functions() const;
185 
186  void unload(const irep_idt &name) const
187  {
188  goto_functions.unload(name);
189  }
190 
191  language_filet &add_language_file(const std::string &filename)
192  {
193  return language_files.add_file(filename);
194  }
195 
202  static std::unique_ptr<goto_modelt>
204  {
205  if(model.finalize())
206  return nullptr;
207  return std::move(model.goto_model);
208  }
209 
210  // Implement the abstract_goto_modelt interface:
211 
216  const goto_functionst &get_goto_functions() const override
217  {
218  return goto_model->goto_functions;
219  }
220 
221  const symbol_tablet &get_symbol_table() const override
222  {
223  return symbol_table;
224  }
225 
226  bool can_produce_function(const irep_idt &id) const override;
227 
243  get_goto_function(const irep_idt &id) override
244  {
245  return goto_functions.at(id);
246  }
247 
252  void validate(
254  const goto_model_validation_optionst &goto_model_validation_options =
255  goto_model_validation_optionst{}) const override
256  {
257  goto_model->validate(vm, goto_model_validation_options);
258  }
259 
260 private:
261  std::unique_ptr<goto_modelt> goto_model;
262 
263 public:
266 
267 private:
270 
271  // Function/module processing functions
276 
279 
280  bool finalize();
281 };
282 
283 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
Abstract interface to eager or lazy GOTO models.
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
Provides a wrapper for a map of lazily loaded goto_functiont.
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
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
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
std::unique_ptr< goto_modelt > goto_model
lazy_goto_modelt(lazy_goto_modelt &&other)
const can_generate_function_bodyt driver_program_can_generate_function_body
const post_process_functiont post_process_function
const generate_function_bodyt driver_program_generate_function_body
lazy_goto_modelt & operator=(lazy_goto_modelt &&other)
const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function body.
const goto_functionst & get_goto_functions() const override
Accessor to retrieve the internal goto_functionst.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
const lazy_goto_functions_mapt goto_functions
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...
language_filest language_files
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.
const post_process_functionst post_process_functions
void unload(const irep_idt &name) const
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...
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.
message_handlert & message_handler
Logging helper field.
std::function< bool(goto_modelt &goto_model)> post_process_functionst
Callback function that post-processes a whole GOTO model.
language_filet & add_language_file(const std::string &filename)
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 ...
std::function< void(goto_model_functiont &function, const abstract_goto_modelt &model)> post_process_functiont
Callback function that post-processes a GOTO function.
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
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...
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:20
Goto Programs with Functions.
Symbol Table + CFG.
Author: Diffblue Ltd.
validation_modet