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"
13
14#include <unordered_set>
15
16#include <util/symbol.h>
17#include <util/rename_symbol.h>
18
20
21#include "goto_model.h"
22
25 irep_idt &new_function_name,
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 {
41 exprt c = instruction.get_condition();
42 rename_symbol(c);
43 instruction.set_condition(c);
44 }
45 }
46}
47
50static bool link_functions(
51 symbol_tablet &dest_symbol_table,
52 goto_functionst &dest_functions,
53 const symbol_tablet &src_symbol_table,
54 goto_functionst &src_functions,
55 const rename_symbolt &rename_symbol,
56 const std::unordered_set<irep_idt> &weak_symbols)
57{
58 namespacet ns(dest_symbol_table);
59 namespacet src_ns(src_symbol_table);
60
61 // merge functions
62 for(auto &gf_entry : src_functions.function_map)
63 {
64 // the function might have been renamed
65 rename_symbolt::expr_mapt::const_iterator e_it =
66 rename_symbol.expr_map.find(gf_entry.first);
67
68 irep_idt final_id = gf_entry.first;
69
70 if(e_it!=rename_symbol.expr_map.end())
71 final_id=e_it->second;
72
73 // already there?
74 goto_functionst::function_mapt::iterator dest_f_it=
75 dest_functions.function_map.find(final_id);
76
77 goto_functionst::goto_functiont &src_func = gf_entry.second;
78 if(dest_f_it==dest_functions.function_map.end()) // not there yet
79 {
80 rename_symbols_in_function(src_func, final_id, rename_symbol);
81 dest_functions.function_map.emplace(final_id, std::move(src_func));
82 }
83 else // collision!
84 {
85 goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
86
87 if(in_dest_symbol_table.body.instructions.empty() ||
88 weak_symbols.find(final_id)!=weak_symbols.end())
89 {
90 // the one with body wins!
91 rename_symbols_in_function(src_func, final_id, rename_symbol);
92
93 in_dest_symbol_table.body.swap(src_func.body);
94 in_dest_symbol_table.parameter_identifiers.swap(
95 src_func.parameter_identifiers);
96 }
97 else if(
98 src_func.body.instructions.empty() ||
99 src_ns.lookup(gf_entry.first).is_weak)
100 {
101 // just keep the old one in dest
102 }
103 else if(to_code_type(ns.lookup(final_id).type).get_inlined())
104 {
105 // ok, we silently ignore
106 }
107 }
108 }
109
110 return false;
111}
112
114 goto_modelt &dest,
115 goto_modelt &&src,
116 message_handlert &message_handler)
117{
118 std::unordered_set<irep_idt> weak_symbols;
119
120 for(const auto &symbol_pair : dest.symbol_table.symbols)
121 {
122 if(symbol_pair.second.is_weak)
123 weak_symbols.insert(symbol_pair.first);
124 }
125
126 linkingt linking(dest.symbol_table, src.symbol_table, message_handler);
127
128 if(linking.typecheck_main())
129 {
130 messaget log{message_handler};
131 log.error() << "typechecking main failed" << messaget::eom;
132 return {};
133 }
134
136 dest.symbol_table,
137 dest.goto_functions,
138 src.symbol_table,
139 src.goto_functions,
140 linking.rename_symbol,
141 weak_symbols))
142 {
143 messaget log{message_handler};
144 log.error() << "linking failed" << messaget::eom;
145 return {};
146 }
147
148 return linking.object_type_updates.get_expr_map();
149}
150
152 goto_modelt &dest,
153 const replace_symbolt::expr_mapt &type_updates)
154{
155 unchecked_replace_symbolt object_type_updates;
156 object_type_updates.get_expr_map().insert(
157 type_updates.begin(), type_updates.end());
158
159 goto_functionst &dest_functions = dest.goto_functions;
160 symbol_tablet &dest_symbol_table = dest.symbol_table;
161
162 // apply macros
163 rename_symbolt macro_application;
164
165 for(const auto &symbol_pair : dest_symbol_table.symbols)
166 {
167 if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
168 {
169 const symbolt &symbol = symbol_pair.second;
170
171 INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
172 const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
173
174 #if 0
175 if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
176 {
177 std::cerr << symbol << '\n';
178 std::cerr << ns.lookup(id) << '\n';
179 }
180 INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
181 "type matches");
182 #endif
183
184 macro_application.insert_expr(symbol.name, id);
185 }
186 }
187
188 if(!macro_application.expr_map.empty())
189 {
190 for(auto &gf_entry : dest_functions.function_map)
191 {
192 irep_idt final_id = gf_entry.first;
193 rename_symbols_in_function(gf_entry.second, final_id, macro_application);
194 }
195 }
196
197 if(!object_type_updates.empty())
198 {
199 for(auto &gf_entry : dest_functions.function_map)
200 {
201 for(auto &instruction : gf_entry.second.body.instructions)
202 {
203 instruction.transform([&object_type_updates](exprt expr) {
204 object_type_updates(expr);
205 return expr;
206 });
207 }
208 }
209 }
210}
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:291
bool get_inlined() const
Definition: std_types.h:665
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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().
Definition: namespace.cpp:138
expr_mapt expr_map
Definition: rename_symbol.h:63
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
bool empty() const
const expr_mapt & get_expr_map() const
std::unordered_map< irep_idt, exprt > expr_mapt
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
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
Symbol Table + CFG.
bool linking(symbol_tablet &dest_symbol_table, const symbol_tablet &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:1470
ANSI-C Linking.
nonstd::optional< T > optionalt
Definition: optional.h:35
#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:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Symbol table entry.