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 <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
53  std::function<void(
54  const irep_idt &name,
56  journalling_symbol_tablet &function_symbols)>
58  typedef std::function<bool(const irep_idt &name)>
60  typedef std::function<
61  bool(
62  const irep_idt &function_name,
64  goto_functiont &function,
65  bool body_available)>
67 
68 private:
69  typedef std::map<key_type, goto_functiont> underlying_mapt;
74  mutable std::unordered_set<irep_idt> processed_functions;
75 
82 
83 public:
102  {
103  }
104 
108  const_mapped_type at(const key_type &name) const
109  {
110  return ensure_function_loaded_internal(name).second;
111  }
112 
116  mapped_type at(const key_type &name)
117  {
118  return ensure_function_loaded_internal(name).second;
119  }
120 
126  bool can_produce_function(const key_type &name) const
127  {
128  return
131  }
132 
133  void unload(const key_type &name) const { goto_functions.erase(name); }
134 
135  void ensure_function_loaded(const key_type &name) const
136  {
138  }
139 
140 private:
141  // This returns a non-const reference, but if you use this method from a
142  // const method then you should not return such a reference without making it
143  // const first
145  {
146  symbol_table_buildert symbol_table_builder =
148 
149  journalling_symbol_tablet journalling_table =
150  journalling_symbol_tablet::wrap(symbol_table_builder);
151  reference named_function=ensure_entry_converted(name, journalling_table);
152  mapped_type function=named_function.second;
153  if(processed_functions.count(name)==0)
154  {
155  // Run function-pass conversions
156  post_process_function(name, function, journalling_table);
157  // Assign procedure-local location numbers for now
158  function.body.compute_location_numbers();
159  processed_functions.insert(name);
160  }
161  return named_function;
162  }
163 
173  const key_type &name,
174  symbol_table_baset &function_symbol_table) const
175  {
176  underlying_mapt::iterator it=goto_functions.find(name);
177  if(it!=goto_functions.end())
178  return *it;
179 
180  goto_functiont function;
181 
182  // First chance: see if the driver program wants to provide a replacement:
183  bool body_provided =
185  name,
186  function_symbol_table,
187  function,
189 
190  // Second chance: see if language_filest can provide a body:
191  if(!body_provided)
192  {
193  // Fill in symbol table entry body if not already done
194  language_files.convert_lazy_method(name, function_symbol_table);
195  body_provided = function_symbol_table.lookup_ref(name).value.is_not_nil();
196 
197  // Create goto_functiont
198  goto_convert_functionst convert_functions(
199  function_symbol_table, message_handler);
200  convert_functions.convert_function(name, function);
201  }
202 
203  // Add to map
204  return *goto_functions.emplace(name, std::move(function)).first;
205  }
206 };
207 
208 #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:173
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:34
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
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
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.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
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.
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