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/base_type.h>
17 #include <util/symbol.h>
18 #include <util/rename_symbol.h>
19 
20 #include <linking/linking_class.h>
21 #include <util/exception_utils.h>
22 
23 #include "goto_model.h"
24 
27  irep_idt &new_function_name,
28  const rename_symbolt &rename_symbol)
29 {
30  for(auto &identifier : function.parameter_identifiers)
31  {
32  auto entry = rename_symbol.expr_map.find(identifier);
33  if(entry != rename_symbol.expr_map.end())
34  identifier = entry->second;
35  }
36 
37  for(auto &instruction : function.body.instructions)
38  {
39  rename_symbol(instruction.code);
40 
41  if(instruction.has_condition())
42  {
43  exprt c = instruction.get_condition();
44  rename_symbol(c);
45  instruction.set_condition(c);
46  }
47  }
48 }
49 
52 static bool link_functions(
53  symbol_tablet &dest_symbol_table,
54  goto_functionst &dest_functions,
55  const symbol_tablet &src_symbol_table,
56  goto_functionst &src_functions,
57  const rename_symbolt &rename_symbol,
58  const std::unordered_set<irep_idt> &weak_symbols,
59  const replace_symbolt &object_type_updates)
60 {
61  namespacet ns(dest_symbol_table);
62  namespacet src_ns(src_symbol_table);
63 
64  // merge functions
65  for(auto &gf_entry : src_functions.function_map)
66  {
67  // the function might have been renamed
68  rename_symbolt::expr_mapt::const_iterator e_it =
69  rename_symbol.expr_map.find(gf_entry.first);
70 
71  irep_idt final_id = gf_entry.first;
72 
73  if(e_it!=rename_symbol.expr_map.end())
74  final_id=e_it->second;
75 
76  // already there?
77  goto_functionst::function_mapt::iterator dest_f_it=
78  dest_functions.function_map.find(final_id);
79 
80  goto_functionst::goto_functiont &src_func = gf_entry.second;
81  if(dest_f_it==dest_functions.function_map.end()) // not there yet
82  {
83  rename_symbols_in_function(src_func, final_id, rename_symbol);
84  dest_functions.function_map.emplace(final_id, std::move(src_func));
85  }
86  else // collision!
87  {
88  goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
89 
90  if(in_dest_symbol_table.body.instructions.empty() ||
91  weak_symbols.find(final_id)!=weak_symbols.end())
92  {
93  // the one with body wins!
94  rename_symbols_in_function(src_func, final_id, rename_symbol);
95 
96  in_dest_symbol_table.body.swap(src_func.body);
97  in_dest_symbol_table.parameter_identifiers.swap(
98  src_func.parameter_identifiers);
99  }
100  else if(
101  src_func.body.instructions.empty() ||
102  src_ns.lookup(gf_entry.first).is_weak)
103  {
104  // just keep the old one in dest
105  }
106  else if(to_code_type(ns.lookup(final_id).type).get_inlined())
107  {
108  // ok, we silently ignore
109  }
110  }
111  }
112 
113  // apply macros
114  rename_symbolt macro_application;
115 
116  for(const auto &symbol_pair : dest_symbol_table.symbols)
117  {
118  if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
119  {
120  const symbolt &symbol = symbol_pair.second;
121 
122  INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
123  const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
124 
125  #if 0
126  if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
127  {
128  std::cerr << symbol << '\n';
129  std::cerr << ns.lookup(id) << '\n';
130  }
131  INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
132  "type matches");
133  #endif
134 
135  macro_application.insert_expr(symbol.name, id);
136  }
137  }
138 
139  if(!macro_application.expr_map.empty())
140  {
141  for(auto &gf_entry : dest_functions.function_map)
142  {
143  irep_idt final_id = gf_entry.first;
144  rename_symbols_in_function(gf_entry.second, final_id, macro_application);
145  }
146  }
147 
148  if(!object_type_updates.empty())
149  {
150  for(auto &gf_entry : dest_functions.function_map)
151  {
152  for(auto &instruction : gf_entry.second.body.instructions)
153  {
154  instruction.transform([&object_type_updates](exprt expr) {
155  object_type_updates(expr);
156  return expr;
157  });
158  }
159  }
160  }
161 
162  return false;
163 }
164 
166  goto_modelt &dest,
167  goto_modelt &src,
168  message_handlert &message_handler)
169 {
170  std::unordered_set<irep_idt> weak_symbols;
171 
172  for(const auto &symbol_pair : dest.symbol_table.symbols)
173  {
174  if(symbol_pair.second.is_weak)
175  weak_symbols.insert(symbol_pair.first);
176  }
177 
179  src.symbol_table,
180  message_handler);
181 
182  if(linking.typecheck_main())
183  {
184  throw invalid_source_file_exceptiont("typechecking main failed");
185  }
186  if(link_functions(
187  dest.symbol_table,
188  dest.goto_functions,
189  src.symbol_table,
190  src.goto_functions,
191  linking.rename_symbol,
192  weak_symbols,
193  linking.object_type_updates))
194  {
195  throw invalid_source_file_exceptiont("linking failed");
196  }
197 }
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:20
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:27
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:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
base_type.h
Base Type Computation.
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:1437
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
linkingt
Definition: linking_class.h:28
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
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:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:870
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
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