cprover
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 
11 #include "goto_functions.h"
12 #include "goto_convert_functions.h"
13 
14 #include <util/message.h>
15 #include <langapi/language_file.h>
17 
29 {
30 public:
31  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
32  typedef irep_idt key_type;
33  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
36  // NOLINTNEXTLINE(readability/identifiers) - name matches mapped_type
38  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
39  typedef std::pair<const key_type, goto_functiont> value_type;
40  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
42  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
43  typedef const value_type &const_reference;
44  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
45  typedef value_type *pointer;
46  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
47  typedef const value_type *const_pointer;
48  // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL
49  typedef std::size_t size_type;
50 
51  typedef
52  std::function<void(
53  const irep_idt &name,
55  journalling_symbol_tablet &function_symbols)>
57  typedef std::function<bool(const irep_idt &name)>
59  typedef std::function<
60  bool(
61  const irep_idt &function_name,
63  goto_functiont &function,
64  bool body_available)>
66 
67 private:
68  typedef std::map<key_type, goto_functiont> underlying_mapt;
73  mutable std::unordered_set<irep_idt> processed_functions;
74 
81 
82 public:
101  {
102  }
103 
107  const_mapped_type at(const key_type &name) const
108  {
109  return ensure_function_loaded_internal(name).second;
110  }
111 
115  mapped_type at(const key_type &name)
116  {
117  return ensure_function_loaded_internal(name).second;
118  }
119 
125  bool can_produce_function(const key_type &name) const
126  {
127  return
130  }
131 
132  void unload(const key_type &name) const { goto_functions.erase(name); }
133 
134  void ensure_function_loaded(const key_type &name) const
135  {
137  }
138 
139 private:
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  journalling_symbol_tablet journalling_table =
146  journalling_symbol_tablet::wrap(symbol_table);
147  reference named_function=ensure_entry_converted(name, journalling_table);
148  mapped_type function=named_function.second;
149  if(processed_functions.count(name)==0)
150  {
151  // Run function-pass conversions
152  post_process_function(name, function, journalling_table);
153  // Assign procedure-local location numbers for now
154  function.body.compute_location_numbers();
155  processed_functions.insert(name);
156  }
157  return named_function;
158  }
159 
169  const key_type &name,
170  symbol_table_baset &function_symbol_table) const
171  {
172  underlying_mapt::iterator it=goto_functions.find(name);
173  if(it!=goto_functions.end())
174  return *it;
175 
176  goto_functiont function;
177 
178  // First chance: see if the driver program wants to provide a replacement:
179  bool body_provided =
181  name,
182  function_symbol_table,
183  function,
185 
186  // Second chance: see if language_filest can provide a body:
187  if(!body_provided)
188  {
189  // Fill in symbol table entry body if not already done
190  language_files.convert_lazy_method(name, function_symbol_table);
191  body_provided = function_symbol_table.lookup_ref(name).value.is_not_nil();
192 
193  // Create goto_functiont
194  goto_convert_functionst convert_functions(
195  function_symbol_table, message_handler);
196  convert_functions.convert_function(name, function);
197  }
198 
199  // Add to map
200  return *goto_functions.emplace(name, std::move(function)).first;
201  }
202 };
203 
204 #endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
std::unordered_set< irep_idt > processed_functions
Names of functions that are already fully available in the programt state.
bool is_not_nil() const
Definition: irep.h:103
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::function< bool(const irep_idt &name)> can_generate_function_bodyt
mapped_type at(const key_type &name)
Gets the body for a given function.
Goto Programs with Functions.
exprt value
Initial value of symbol.
Definition: symbol.h:37
std::pair< const key_type, goto_functiont > value_type
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
std::map< key_type, goto_functiont > underlying_mapt
const goto_functiont & const_mapped_type
The type of elements returned by const members.
bool can_convert_lazy_method(const irep_idt &id) const
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
const value_type & const_reference
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_mapped_type at(const key_type &name) const
Gets the body for a given function.
The symbol table.
Definition: symbol_table.h:19
::goto_functiont goto_functiont
Provides a wrapper for a map of lazily loaded goto_functiont.
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
void ensure_function_loaded(const key_type &name) const
Goto Programs with Functions.
message_handlert & message_handler
The symbol table base class interface.
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...
const post_process_functiont post_process_function
Author: Diffblue Ltd.
const can_generate_function_bodyt driver_program_can_generate_function_body
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
const generate_function_bodyt driver_program_generate_function_body
std::function< void(const irep_idt &name, goto_functionst::goto_functiont &function, journalling_symbol_tablet &function_symbols)> post_process_functiont
reference ensure_function_loaded_internal(const key_type &name) const