cprover
Loading...
Searching...
No Matches
lazy_goto_model.h
Go to the documentation of this file.
1
2
5
6#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
7#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H
8
10
14
16
17class optionst;
18
43{
44public:
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 {
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
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
260private:
261 std::unique_ptr<goto_modelt> goto_model;
262
263public:
266
267private:
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...
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)
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.
language_filet & add_language_file(const std::string &filename)
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 goto_functionst::goto_functiont & get_goto_function(const irep_idt &id) override
Get a GOTO function body.
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
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...
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.
lazy_goto_modelt & operator=(lazy_goto_modelt &&other)
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...
const goto_functionst & get_goto_functions() const override
Accessor to retrieve the internal goto_functionst.
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.
const symbol_tablet & get_symbol_table() const override
Accessor to get the symbol table.
std::function< bool(goto_modelt &goto_model)> post_process_functionst
Callback function that post-processes a whole GOTO model.
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.
The symbol table base class interface.
The symbol table.
Goto Programs with Functions.
Symbol Table + CFG.
Author: Diffblue Ltd.
validation_modet