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 #include <util/exception_utils.h>
21 
22 #include "goto_model.h"
23 
26  irep_idt &new_function_name,
27  const rename_symbolt &rename_symbol)
28 {
29  for(auto &identifier : function.parameter_identifiers)
30  {
31  auto entry = rename_symbol.expr_map.find(identifier);
32  if(entry != rename_symbol.expr_map.end())
33  identifier = entry->second;
34  }
35 
36  for(auto &instruction : function.body.instructions)
37  {
38  rename_symbol(instruction.code_nonconst());
39 
40  if(instruction.has_condition())
41  {
42  exprt c = instruction.get_condition();
43  rename_symbol(c);
44  instruction.set_condition(c);
45  }
46  }
47 }
48 
51 static bool link_functions(
52  symbol_tablet &dest_symbol_table,
53  goto_functionst &dest_functions,
54  const symbol_tablet &src_symbol_table,
55  goto_functionst &src_functions,
56  const rename_symbolt &rename_symbol,
57  const std::unordered_set<irep_idt> &weak_symbols,
58  const replace_symbolt &object_type_updates)
59 {
60  namespacet ns(dest_symbol_table);
61  namespacet src_ns(src_symbol_table);
62 
63  // merge functions
64  for(auto &gf_entry : src_functions.function_map)
65  {
66  // the function might have been renamed
67  rename_symbolt::expr_mapt::const_iterator e_it =
68  rename_symbol.expr_map.find(gf_entry.first);
69 
70  irep_idt final_id = gf_entry.first;
71 
72  if(e_it!=rename_symbol.expr_map.end())
73  final_id=e_it->second;
74 
75  // already there?
76  goto_functionst::function_mapt::iterator dest_f_it=
77  dest_functions.function_map.find(final_id);
78 
79  goto_functionst::goto_functiont &src_func = gf_entry.second;
80  if(dest_f_it==dest_functions.function_map.end()) // not there yet
81  {
82  rename_symbols_in_function(src_func, final_id, rename_symbol);
83  dest_functions.function_map.emplace(final_id, std::move(src_func));
84  }
85  else // collision!
86  {
87  goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
88 
89  if(in_dest_symbol_table.body.instructions.empty() ||
90  weak_symbols.find(final_id)!=weak_symbols.end())
91  {
92  // the one with body wins!
93  rename_symbols_in_function(src_func, final_id, rename_symbol);
94 
95  in_dest_symbol_table.body.swap(src_func.body);
96  in_dest_symbol_table.parameter_identifiers.swap(
97  src_func.parameter_identifiers);
98  }
99  else if(
100  src_func.body.instructions.empty() ||
101  src_ns.lookup(gf_entry.first).is_weak)
102  {
103  // just keep the old one in dest
104  }
105  else if(to_code_type(ns.lookup(final_id).type).get_inlined())
106  {
107  // ok, we silently ignore
108  }
109  }
110  }
111 
112  // apply macros
113  rename_symbolt macro_application;
114 
115  for(const auto &symbol_pair : dest_symbol_table.symbols)
116  {
117  if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
118  {
119  const symbolt &symbol = symbol_pair.second;
120 
121  INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
122  const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
123 
124  #if 0
125  if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
126  {
127  std::cerr << symbol << '\n';
128  std::cerr << ns.lookup(id) << '\n';
129  }
130  INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
131  "type matches");
132  #endif
133 
134  macro_application.insert_expr(symbol.name, id);
135  }
136  }
137 
138  if(!macro_application.expr_map.empty())
139  {
140  for(auto &gf_entry : dest_functions.function_map)
141  {
142  irep_idt final_id = gf_entry.first;
143  rename_symbols_in_function(gf_entry.second, final_id, macro_application);
144  }
145  }
146 
147  if(!object_type_updates.empty())
148  {
149  for(auto &gf_entry : dest_functions.function_map)
150  {
151  for(auto &instruction : gf_entry.second.body.instructions)
152  {
153  instruction.transform([&object_type_updates](exprt expr) {
154  object_type_updates(expr);
155  return expr;
156  });
157  }
158  }
159  }
160 
161  return false;
162 }
163 
165  goto_modelt &dest,
166  goto_modelt &src,
167  message_handlert &message_handler)
168 {
169  std::unordered_set<irep_idt> weak_symbols;
170 
171  for(const auto &symbol_pair : dest.symbol_table.symbols)
172  {
173  if(symbol_pair.second.is_weak)
174  weak_symbols.insert(symbol_pair.first);
175  }
176 
178  src.symbol_table,
179  message_handler);
180 
181  if(linking.typecheck_main())
182  {
183  throw invalid_source_file_exceptiont("typechecking main failed");
184  }
185  if(link_functions(
186  dest.symbol_table,
187  dest.goto_functions,
188  src.symbol_table,
189  src.goto_functions,
190  linking.rename_symbol,
191  weak_symbols,
192  linking.object_type_updates))
193  {
194  throw invalid_source_file_exceptiont("linking failed");
195  }
196 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
rename_symbolt::expr_map
expr_mapt expr_map
Definition: rename_symbol.h:63
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
rename_symbol.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
base_type_eq
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:290
linking
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1444
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
linkingt
Definition: linking_class.h:29
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
replace_symbolt::empty
bool empty() const
Definition: replace_symbol.h:56
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
linking_class.h
ANSI-C Linking.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
rename_symbolt::insert_expr
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
rename_symbolt
Definition: rename_symbol.h:26
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:665
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25