cprover
Loading...
Searching...
No Matches
link_to_library.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Library Linking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "link_to_library.h"
13
15
18#include "goto_model.h"
19#include "link_goto_model.h"
20
22static std::pair<optionalt<replace_symbolt::expr_mapt>, bool> add_one_function(
23 goto_modelt &goto_model,
24 message_handlert &message_handler,
25 const std::function<void(
26 const std::set<irep_idt> &,
27 const symbol_tablet &,
29 message_handlert &)> &library,
30 const irep_idt &missing_function)
31{
32 goto_modelt library_model;
33 library(
34 {missing_function},
35 goto_model.symbol_table,
36 library_model.symbol_table,
37 message_handler);
38
39 // convert to CFG
40 if(
41 library_model.symbol_table.symbols.find(missing_function) !=
42 library_model.symbol_table.symbols.end())
43 {
45 missing_function,
46 library_model.symbol_table,
47 library_model.goto_functions,
48 message_handler);
49 }
50 // We might need a function that's outside our own library, but brought in via
51 // some header file included by the library. Those functions already exist in
52 // goto_model.symbol_table, but haven't been converted just yet.
53 else if(
54 goto_model.symbol_table.symbols.find(missing_function) !=
55 goto_model.symbol_table.symbols.end())
56 {
58 missing_function,
59 goto_model.symbol_table,
60 library_model.goto_functions,
61 message_handler);
62 }
63
64 // check whether additional initialization may be required
65 bool init_required = false;
66 if(
68 goto_model.goto_functions.function_map.end())
69 {
70 for(const auto &entry : library_model.symbol_table)
71 {
72 if(
73 entry.second.is_static_lifetime && !entry.second.is_type &&
74 !entry.second.is_macro && entry.second.type.id() != ID_code &&
75 !goto_model.symbol_table.has_symbol(entry.first))
76 {
77 init_required = true;
78 break;
79 }
80 }
81 }
82
83 return {
84 link_goto_model(goto_model, std::move(library_model), message_handler),
85 init_required};
86}
87
98 goto_modelt &goto_model,
99 message_handlert &message_handler,
100 const std::function<void(
101 const std::set<irep_idt> &,
102 const symbol_tablet &,
104 message_handlert &)> &library)
105{
106 // this needs a fixedpoint, as library functions
107 // may depend on other library functions
108
109 std::set<irep_idt> added_functions;
110 // Linking in library functions (now seeing full definitions rather than
111 // forward declarations, or perhaps even cases of missing forward
112 // declarations) may result in type changes to objects.
113 replace_symbolt::expr_mapt object_type_updates;
114 bool need_reinit = false;
115
116 while(true)
117 {
118 std::unordered_set<irep_idt> called_functions =
120
121 bool changed = false;
122 for(const auto &id : called_functions)
123 {
124 goto_functionst::function_mapt::const_iterator f_it =
125 goto_model.goto_functions.function_map.find(id);
126
127 if(
128 f_it != goto_model.goto_functions.function_map.end() &&
129 f_it->second.body_available())
130 {
131 // it's overridden!
132 }
133 else if(added_functions.find(id) != added_functions.end())
134 {
135 // already added
136 }
137 else
138 {
139 changed = true;
140 added_functions.insert(id);
141
142 auto one_result =
143 add_one_function(goto_model, message_handler, library, id);
144 auto updates_opt = one_result.first;
145 need_reinit |= one_result.second;
146 if(!updates_opt.has_value())
147 {
148 messaget log{message_handler};
149 log.warning() << "Linking library function '" << id << "' failed"
150 << messaget::eom;
151 continue;
152 }
153 object_type_updates.insert(updates_opt->begin(), updates_opt->end());
154 }
155 }
156
157 // done?
158 if(!changed)
159 break;
160 }
161
162 if(need_reinit && goto_model.can_produce_function(INITIALIZE_FUNCTION))
163 recreate_initialize_function(goto_model, message_handler);
164
165 if(!object_type_updates.empty())
166 finalize_linking(goto_model, object_type_updates);
167}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
std::unordered_map< irep_idt, exprt > expr_mapt
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
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.
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