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,
55 journalling_symbol_tablet &function_symbols)>
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:
99 {
100 }
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
123 bool can_produce_function(const key_type &name) const
124 {
127 }
128
129 void unload(const key_type &name) const
130 {
131 goto_functions.erase(name);
132 }
133
134 void ensure_function_loaded(const key_type &name) const
135 {
137 }
138
139private:
140 // This returns a non-const reference, but if you use this method from a
141 // const method then you should not return such a reference without making it
142 // const first
144 {
145 symbol_table_buildert symbol_table_builder =
147
148 journalling_symbol_tablet journalling_table =
149 journalling_symbol_tablet::wrap(symbol_table_builder);
150 reference named_function = ensure_entry_converted(name, journalling_table);
151 mapped_type function = named_function.second;
152 if(processed_functions.count(name) == 0)
153 {
154 // Run function-pass conversions
155 post_process_function(name, function, journalling_table);
156 // Assign procedure-local location numbers for now
158 processed_functions.insert(name);
159 }
160 return named_function;
161 }
162
172 const key_type &name,
173 symbol_table_baset &function_symbol_table) const
174 {
175 // Fill in symbol table entry body if not already done
176 language_files.convert_lazy_method(name, function_symbol_table);
177
178 underlying_mapt::iterator it = goto_functions.find(name);
179 if(it != goto_functions.end())
180 return *it;
181
182 goto_functiont function;
183
184 // First chance: see if the driver program wants to provide a replacement:
185 bool body_provided = driver_program_generate_function_body(
186 name,
187 function_symbol_table,
188 function,
190
191 // Second chance: see if language_filest can provide a body:
192 if(!body_provided)
193 {
194 // Create goto_functiont
195 goto_convert_functionst convert_functions(
196 function_symbol_table, message_handler);
197 convert_functions.convert_function(name, function);
198 }
199
200 // Add to map
201 return *goto_functions.emplace(name, std::move(function)).first;
202 }
203};
204
205#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:755
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)
bool can_convert_lazy_method(const irep_idt &id) const
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
Provides a wrapper for a map of lazily loaded goto_functiont.
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.
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...
void ensure_function_loaded(const key_type &name) const
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.
std::function< bool(const irep_idt &function_name, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available)> generate_function_bodyt
const goto_functiont & const_mapped_type
The type of elements returned by const members.
void unload(const key_type &name) const
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
std::pair< const key_type, goto_functiont > value_type
std::map< key_type, goto_functiont > underlying_mapt
const value_type & const_reference
const can_generate_function_bodyt driver_program_can_generate_function_body
std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> post_process_functiont
message_handlert & message_handler
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.
Definition: symbol_table.h:14
Goto Programs with Functions.
Goto Programs with Functions.
Author: Diffblue Ltd.