CBMC
lazy_goto_functions_map.h
Go to the documentation of this file.
1 
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 
14 #include <langapi/language_file.h>
16 #include <util/message.h>
18 
30 {
31 public:
32  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
33  typedef irep_idt key_type;
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
44  typedef const value_type &const_reference;
45  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
46  typedef value_type *pointer;
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 
65 private:
66  typedef std::map<key_type, goto_functiont> underlying_mapt;
71  mutable std::unordered_set<irep_idt> processed_functions;
72 
79 
80 public:
99  {
100  }
101 
105  const_mapped_type at(const key_type &name) const
106  {
107  return ensure_function_loaded_internal(name).second;
108  }
109 
113  mapped_type at(const key_type &name)
114  {
115  return ensure_function_loaded_internal(name).second;
116  }
117 
123  bool can_produce_function(const key_type &name) const
124  {
127  }
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 
142 private:
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  {
148  symbol_table_buildert symbol_table_builder =
150 
151  journalling_symbol_tablet journalling_table =
152  journalling_symbol_tablet::wrap(symbol_table_builder);
153  reference named_function = ensure_entry_converted(name, journalling_table);
154  mapped_type function = named_function.second;
155  if(processed_functions.count(name) == 0)
156  {
157  // Run function-pass conversions
158  post_process_function(name, function, journalling_table);
159  // Assign procedure-local location numbers for now
160  function.body.compute_location_numbers();
161  processed_functions.insert(name);
162  }
163  return named_function;
164  }
165 
175  const key_type &name,
176  symbol_table_baset &function_symbol_table) const
177  {
178  // Fill in symbol table entry body if not already done
180  name, function_symbol_table, message_handler);
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:
189  bool body_provided = driver_program_generate_function_body(
190  name,
191  function_symbol_table,
192  function,
194 
195  // Second chance: see if language_filest can provide a body:
196  if(!body_provided)
197  {
198  // Create goto_functiont
199  goto_convert_functionst convert_functions(
200  function_symbol_table, message_handler);
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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
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.
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...
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.
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.