CBMC
link_to_library.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Library Linking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "link_to_library.h"
13 
17 
19 
20 #include "goto_convert_functions.h"
21 
23 static std::pair<std::optional<replace_symbolt::expr_mapt>, bool>
25  goto_modelt &goto_model,
26  message_handlert &message_handler,
27  const std::function<void(
28  const std::set<irep_idt> &,
29  const symbol_tablet &,
30  symbol_tablet &,
31  message_handlert &)> &library,
32  const irep_idt &missing_function)
33 {
34  goto_modelt library_model;
35  library(
36  {missing_function},
37  goto_model.symbol_table,
38  library_model.symbol_table,
39  message_handler);
40 
41  // convert to CFG
42  if(
43  library_model.symbol_table.symbols.find(missing_function) !=
44  library_model.symbol_table.symbols.end() &&
45  library_model.symbol_table.lookup_ref(missing_function).value.is_not_nil())
46  {
48  missing_function,
49  library_model.symbol_table,
50  library_model.goto_functions,
51  message_handler);
52  // this function is now included in goto_functions, no need to re-convert
53  // should the goto binary be reloaded
54  library_model.symbol_table.get_writeable_ref(missing_function)
55  .set_compiled();
56  }
57  // We might need a function that's outside our own library, but brought in via
58  // some header file included by the library. Those functions already exist in
59  // goto_model.symbol_table, but haven't been converted just yet.
60  else if(
61  goto_model.symbol_table.symbols.find(missing_function) !=
62  goto_model.symbol_table.symbols.end() &&
63  goto_model.symbol_table.lookup_ref(missing_function).value.is_not_nil() &&
64  !goto_model.symbol_table.lookup_ref(missing_function).is_compiled())
65  {
67  missing_function,
68  goto_model.symbol_table,
69  library_model.goto_functions,
70  message_handler);
71  // this function is now included in goto_functions, no need to re-convert
72  // should the goto binary be reloaded
73  goto_model.symbol_table.get_writeable_ref(missing_function).set_compiled();
74  }
75 
76  // check whether additional initialization may be required
77  bool init_required = false;
78  if(
80  goto_model.goto_functions.function_map.end())
81  {
82  for(const auto &entry : library_model.symbol_table)
83  {
84  if(
85  entry.second.is_static_lifetime && !entry.second.is_type &&
86  !entry.second.is_macro && entry.second.type.id() != ID_code &&
87  !goto_model.symbol_table.has_symbol(entry.first))
88  {
89  init_required = true;
90  break;
91  }
92  }
93  }
94 
95  return {
96  link_goto_model(goto_model, std::move(library_model), message_handler),
97  init_required};
98 }
99 
110  goto_modelt &goto_model,
111  message_handlert &message_handler,
112  const std::function<void(
113  const std::set<irep_idt> &,
114  const symbol_tablet &,
115  symbol_tablet &,
116  message_handlert &)> &library)
117 {
118  // this needs a fixedpoint, as library functions
119  // may depend on other library functions
120 
121  std::set<irep_idt> added_functions;
122  // Linking in library functions (now seeing full definitions rather than
123  // forward declarations, or perhaps even cases of missing forward
124  // declarations) may result in type changes to objects.
125  replace_symbolt::expr_mapt object_type_updates;
126  bool need_reinit = false;
127 
128  while(true)
129  {
130  std::unordered_set<irep_idt> called_functions =
132 
133  bool changed = false;
134  for(const auto &id : called_functions)
135  {
136  goto_functionst::function_mapt::const_iterator f_it =
137  goto_model.goto_functions.function_map.find(id);
138 
139  if(
140  f_it != goto_model.goto_functions.function_map.end() &&
141  f_it->second.body_available())
142  {
143  // it's overridden!
144  }
145  else if(added_functions.find(id) != added_functions.end())
146  {
147  // already added
148  }
149  else
150  {
151  changed = true;
152  added_functions.insert(id);
153 
154  auto one_result =
155  add_one_function(goto_model, message_handler, library, id);
156  auto updates_opt = one_result.first;
157  need_reinit |= one_result.second;
158  if(!updates_opt.has_value())
159  {
160  messaget log{message_handler};
161  log.warning() << "Linking library function '" << id << "' failed"
162  << messaget::eom;
163  continue;
164  }
165  object_type_updates.insert(updates_opt->begin(), updates_opt->end());
166  }
167  }
168 
169  // done?
170  if(!changed)
171  break;
172  }
173 
174  if(need_reinit && goto_model.can_produce_function(INITIALIZE_FUNCTION))
175  recreate_initialize_function(goto_model, message_handler);
176 
177  if(!object_type_updates.empty())
178  finalize_linking(goto_model, object_type_updates);
179 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
function_mapt function_map
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: goto_model.h:95
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
bool is_not_nil() const
Definition: irep.h:372
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static eomt eom
Definition: message.h:289
std::unordered_map< irep_idt, exprt > expr_mapt
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:120
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:113
exprt value
Initial value of symbol.
Definition: symbol.h:34
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Query Called Functions.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Symbol Table + CFG.
double log(double x)
Definition: math.c:2776
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION