cprover
Loading...
Searching...
No Matches
link_goto_model.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Link Goto Programs
4
5Author: Michael Tautschnig, Daniel Kroening
6
7\*******************************************************************/
8
11
12#include "link_goto_model.h"
14
15#include <util/message.h>
16#include <util/rename_symbol.h>
17#include <util/symbol.h>
18
19#include "goto_model.h"
20
21#include <unordered_set>
22
26 const rename_symbolt &rename_symbol)
27{
28 for(auto &identifier : function.parameter_identifiers)
29 {
30 auto entry = rename_symbol.expr_map.find(identifier);
31 if(entry != rename_symbol.expr_map.end())
32 identifier = entry->second;
33 }
34
35 for(auto &instruction : function.body.instructions)
36 {
37 rename_symbol(instruction.code_nonconst());
38
39 if(instruction.has_condition())
40 rename_symbol(instruction.condition_nonconst());
41 }
42}
43
46static bool link_functions(
51 const rename_symbolt &rename_symbol,
52 const std::unordered_set<irep_idt> &weak_symbols)
53{
56
57 // merge functions
58 for(auto &gf_entry : src_functions.function_map)
59 {
60 // the function might have been renamed
61 rename_symbolt::expr_mapt::const_iterator e_it =
62 rename_symbol.expr_map.find(gf_entry.first);
63
65
66 if(e_it!=rename_symbol.expr_map.end())
67 final_id=e_it->second;
68
69 // already there?
70 goto_functionst::function_mapt::iterator dest_f_it=
71 dest_functions.function_map.find(final_id);
72
74 if(dest_f_it==dest_functions.function_map.end()) // not there yet
75 {
77 dest_functions.function_map.emplace(final_id, std::move(src_func));
78 }
79 else // collision!
80 {
82
83 if(in_dest_symbol_table.body.instructions.empty() ||
85 {
86 // the one with body wins!
88
89 in_dest_symbol_table.body.swap(src_func.body);
90 in_dest_symbol_table.parameter_identifiers.swap(
91 src_func.parameter_identifiers);
92 }
93 else if(
94 src_func.body.instructions.empty() ||
95 src_ns.lookup(gf_entry.first).is_weak)
96 {
97 // just keep the old one in dest
98 }
99 else if(to_code_type(ns.lookup(final_id).type).get_inlined())
100 {
101 // ok, we silently ignore
102 }
103 }
104 }
105
106 return false;
107}
108
110 goto_modelt &dest,
111 goto_modelt &&src,
112 message_handlert &message_handler)
113{
114 std::unordered_set<irep_idt> weak_symbols;
115
116 for(const auto &symbol_pair : dest.symbol_table.symbols)
117 {
118 if(symbol_pair.second.is_weak)
119 weak_symbols.insert(symbol_pair.first);
120 }
121
122 linkingt linking(dest.symbol_table, message_handler);
123
124 if(linking.link(src.symbol_table))
125 {
126 messaget log{message_handler};
127 log.error() << "typechecking main failed" << messaget::eom;
128 return {};
129 }
130
132 dest.symbol_table,
133 dest.goto_functions,
134 src.symbol_table,
135 src.goto_functions,
136 linking.rename_symbol,
138 {
139 messaget log{message_handler};
140 log.error() << "linking failed" << messaget::eom;
141 return {};
142 }
143
144 return linking.object_type_updates.get_expr_map();
145}
146
148 goto_modelt &dest,
150{
151 casting_replace_symbolt object_type_updates;
152 object_type_updates.get_expr_map().insert(
153 type_updates.begin(), type_updates.end());
154
157
158 // apply macros
160
161 for(const auto &symbol_pair : dest_symbol_table.symbols)
162 {
163 if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
164 {
165 const symbolt &symbol = symbol_pair.second;
166
167 INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
168 const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
169
170 #if 0
171 if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
172 {
173 std::cerr << symbol << '\n';
174 std::cerr << ns.lookup(id) << '\n';
175 }
176 INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
177 "type matches");
178 #endif
179
180 macro_application.insert_expr(symbol.name, id);
181 }
182 }
183
184 if(!macro_application.expr_map.empty())
185 {
186 for(auto &gf_entry : dest_functions.function_map)
187 {
188 irep_idt final_id = gf_entry.first;
190 }
191 }
192
193 if(!object_type_updates.empty())
194 {
195 for(auto &gf_entry : dest_functions.function_map)
196 {
197 for(auto &instruction : gf_entry.second.body.instructions)
198 {
199 if(instruction.is_function_call())
200 {
201 const bool changed =
202 !object_type_updates.replace(instruction.call_function());
203 if(changed && instruction.call_lhs().is_not_nil())
204 {
205 object_type_updates(instruction.call_lhs());
206 if(
207 instruction.call_lhs().type() !=
208 to_code_type(instruction.call_function().type()).return_type())
209 {
210 instruction.call_lhs() = typecast_exprt{
211 instruction.call_lhs(),
212 to_code_type(instruction.call_function().type()).return_type()};
213 }
214 }
215 }
216 else
217 {
218 instruction.transform([&object_type_updates](exprt expr) {
219 const bool changed = !object_type_updates.replace(expr);
220 return changed ? optionalt<exprt>{expr} : nullopt;
221 });
222 }
223 }
224 }
225 }
226}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
bool replace(exprt &dest) const override
Definition linking.cpp:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
const irep_idt & id() const
Definition irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
expr_mapt expr_map
bool empty() const
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
Semantic type conversion.
Definition std_expr.h:2017
Symbol Table + CFG.
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition linking.cpp:1565
ANSI-C Linking.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Symbol table entry.