cprover
Loading...
Searching...
No Matches
lazy_goto_functions_map.h
Go to the documentation of this file.
1
2
5
6#ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
7#define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
8
9#include <unordered_set>
10
13
16#include <util/message.h>
18
30{
31public:
32 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
34 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
37 // NOLINTNEXTLINE(readability/identifiers) - name matches mapped_type
39 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
40 typedef std::pair<const key_type, goto_functiont> value_type;
41 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
43 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
45 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
47 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
48 typedef const value_type *const_pointer;
49 // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
50 typedef std::size_t size_type;
51
52 typedef std::function<void(
53 const irep_idt &name,
57 typedef std::function<bool(const irep_idt &name)> can_generate_function_bodyt;
58 typedef std::function<bool(
59 const irep_idt &function_name,
61 goto_functiont &function,
62 bool body_available)>
64
65private:
66 typedef std::map<key_type, goto_functiont> underlying_mapt;
71 mutable std::unordered_set<irep_idt> processed_functions;
72
79
80public:
101
105 const_mapped_type at(const key_type &name) const
106 {
107 return ensure_function_loaded_internal(name).second;
108 }
109
114 {
115 return ensure_function_loaded_internal(name).second;
116 }
117
128
132 std::size_t unload(const key_type &name) const
133 {
134 return goto_functions.erase(name);
135 }
136
137 void ensure_function_loaded(const key_type &name) const
138 {
140 }
141
142private:
143 // This returns a non-const reference, but if you use this method from a
144 // const method then you should not return such a reference without making it
145 // const first
147 {
150
154 mapped_type function = named_function.second;
155 if(processed_functions.count(name) == 0)
156 {
157 // Run function-pass conversions
159 // Assign procedure-local location numbers for now
161 processed_functions.insert(name);
162 }
163 return named_function;
164 }
165
175 const key_type &name,
177 {
178 // Fill in symbol table entry body if not already done
181
182 underlying_mapt::iterator it = goto_functions.find(name);
183 if(it != goto_functions.end())
184 return *it;
185
186 goto_functiont function;
187
188 // First chance: see if the driver program wants to provide a replacement:
190 name,
192 function,
194
195 // Second chance: see if language_filest can provide a body:
196 if(!body_provided)
197 {
198 // Create goto_functiont
201 convert_functions.convert_function(name, function);
202 }
203
204 // Add to map
205 return *goto_functions.emplace(name, std::move(function)).first;
206 }
207};
208
209#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
void compute_location_numbers(unsigned &nr)
Compute location numbers.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table, message_handlert &message_handler)
bool can_convert_lazy_method(const irep_idt &id) const
Provides a wrapper for a map of lazily loaded goto_functiont.
std::function< bool(const irep_idt &name) can_generate_function_bodyt)
lazy_goto_functions_mapt(underlying_mapt &goto_functions, language_filest &language_files, symbol_tablet &symbol_table, post_process_functiont post_process_function, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler)
Creates a lazy_goto_functions_mapt.
std::size_t unload(const key_type &name) const
Remove the function named name from the function map, if it exists.
const post_process_functiont post_process_function
reference ensure_entry_converted(const key_type &name, symbol_table_baset &function_symbol_table) const
Convert a function if not already converted, then return a reference to its goto_functionst map entry...
std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols) post_process_functiont)
void ensure_function_loaded(const key_type &name) const
std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) generate_function_bodyt)
const_mapped_type at(const key_type &name) const
Gets the body for a given function.
std::unordered_set< irep_idt > processed_functions
Names of functions that are already fully available in the programt state.
mapped_type at(const key_type &name)
Gets the body for a given function.
const goto_functiont & const_mapped_type
The type of elements returned by const members.
std::pair< const key_type, goto_functiont > value_type
std::map< key_type, goto_functiont > underlying_mapt
const can_generate_function_bodyt driver_program_can_generate_function_body
const generate_function_bodyt driver_program_generate_function_body
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
reference ensure_function_loaded_internal(const key_type &name) const
The symbol table base class interface.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
The symbol table.
Goto Programs with Functions.
Goto Programs with Functions.
Author: Diffblue Ltd.