cprover
link_goto_model.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Link Goto Programs
4 
5 Author: 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 
19 #include <linking/linking_class.h>
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 
50 static 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 
135  if(link_functions(
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.