CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/link_to_library.cpp Source File

CBMC
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
14#include <goto-programs/compute_called_functions.h>
15#include <goto-programs/goto_model.h>
16#include <goto-programs/link_goto_model.h>
17
18#include <linking/static_lifetime_init.h>
19
20#include "goto_convert_functions.h"
21
23static 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 &,
31 message_handlert &)> &library,
33{
35 library(
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 {
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 {
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
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),
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 &,
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
175 recreate_initialize_function(goto_model, message_handler);
176
177 if(!object_type_updates.empty())
178 finalize_linking(goto_model, object_type_updates);
179}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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
Definition goto_model.h:27
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
Definition message.h:27
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.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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
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.
std::optional< replace_symbolt::expr_mapt > link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &message_handler)
Link goto model src into goto model dest, invalidating src in this process.
void finalize_linking(goto_modelt &dest, const replace_symbolt::expr_mapt &type_updates)
Apply type_updates to dest, where type_updates were constructed from one or more calls to link_goto_m...
Read Goto Programs.
static std::pair< std::optional< replace_symbolt::expr_mapt >, bool > add_one_function(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library, const irep_idt &missing_function)
Try to add missing_function from library to goto_model.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
Library Linking.
double log(double x)
Definition math.c:2416
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

AltStyle によって変換されたページ (->オリジナル) /