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  goto_programt &program=function.body;
38  rename_symbol(function.type);
39 
41  {
42  rename_symbol(iit->code);
43 
44  if(iit->has_condition())
45  {
46  exprt c = iit->get_condition();
47  rename_symbol(c);
48  iit->set_condition(c);
49  }
50  }
51 }
52 
55 static bool link_functions(
56  symbol_tablet &dest_symbol_table,
57  goto_functionst &dest_functions,
58  const symbol_tablet &src_symbol_table,
59  goto_functionst &src_functions,
60  const rename_symbolt &rename_symbol,
61  const std::unordered_set<irep_idt> &weak_symbols,
62  const replace_symbolt &object_type_updates)
63 {
64  namespacet ns(dest_symbol_table);
65  namespacet src_ns(src_symbol_table);
66 
67  // merge functions
68  Forall_goto_functions(src_it, src_functions)
69  {
70  // the function might have been renamed
71  rename_symbolt::expr_mapt::const_iterator e_it=
72  rename_symbol.expr_map.find(src_it->first);
73 
74  irep_idt final_id=src_it->first;
75 
76  if(e_it!=rename_symbol.expr_map.end())
77  final_id=e_it->second;
78 
79  // already there?
80  goto_functionst::function_mapt::iterator dest_f_it=
81  dest_functions.function_map.find(final_id);
82 
83  goto_functionst::goto_functiont &src_func = src_it->second;
84  if(dest_f_it==dest_functions.function_map.end()) // not there yet
85  {
86  rename_symbols_in_function(src_func, final_id, rename_symbol);
87  dest_functions.function_map.emplace(final_id, std::move(src_func));
88  }
89  else // collision!
90  {
91  goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
92 
93  if(in_dest_symbol_table.body.instructions.empty() ||
94  weak_symbols.find(final_id)!=weak_symbols.end())
95  {
96  // the one with body wins!
97  rename_symbols_in_function(src_func, final_id, rename_symbol);
98 
99  in_dest_symbol_table.body.swap(src_func.body);
100  in_dest_symbol_table.parameter_identifiers.swap(
101  src_func.parameter_identifiers);
102  in_dest_symbol_table.type=src_func.type;
103  }
104  else if(src_func.body.instructions.empty() ||
105  src_ns.lookup(src_it->first).is_weak)
106  {
107  // just keep the old one in dest
108  }
109  else if(to_code_type(ns.lookup(final_id).type).get_inlined())
110  {
111  // ok, we silently ignore
112  }
113  else
114  {
115  // the linking code will have ensured that types match
116  rename_symbol(src_func.type);
117  INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns),
118  "linking ensures that types match");
119  }
120  }
121  }
122 
123  // apply macros
124  rename_symbolt macro_application;
125 
126  for(const auto &symbol_pair : dest_symbol_table.symbols)
127  {
128  if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
129  {
130  const symbolt &symbol = symbol_pair.second;
131 
132  INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
133  const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
134 
135  #if 0
136  if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
137  {
138  std::cerr << symbol << '\n';
139  std::cerr << ns.lookup(id) << '\n';
140  }
141  INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
142  "type matches");
143  #endif
144 
145  macro_application.insert_expr(symbol.name, id);
146  }
147  }
148 
149  if(!macro_application.expr_map.empty())
150  Forall_goto_functions(dest_it, dest_functions)
151  {
152  irep_idt final_id=dest_it->first;
153  rename_symbols_in_function(dest_it->second, final_id, macro_application);
154  }
155 
156  if(!object_type_updates.empty())
157  {
158  Forall_goto_functions(dest_it, dest_functions)
159  Forall_goto_program_instructions(iit, dest_it->second.body)
160  {
161  iit->transform([&object_type_updates](exprt expr) {
162  object_type_updates(expr);
163  return expr;
164  });
165  }
166  }
167 
168  return false;
169 }
170 
172  goto_modelt &dest,
173  goto_modelt &src,
174  message_handlert &message_handler)
175 {
176  std::unordered_set<irep_idt> weak_symbols;
177 
178  for(const auto &symbol_pair : dest.symbol_table.symbols)
179  {
180  if(symbol_pair.second.is_weak)
181  weak_symbols.insert(symbol_pair.first);
182  }
183 
185  src.symbol_table,
186  message_handler);
187 
188  if(linking.typecheck_main())
189  {
190  throw invalid_source_file_exceptiont("typechecking main failed");
191  }
192  if(link_functions(
193  dest.symbol_table,
194  dest.goto_functions,
195  src.symbol_table,
196  src.goto_functions,
197  linking.rename_symbol,
198  weak_symbols,
199  linking.object_type_updates))
200  {
201  throw invalid_source_file_exceptiont("linking failed");
202  }
203 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
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:53
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:946
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:1441
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:177
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
replace_symbolt::empty
bool empty() const
Definition: replace_symbol.h:56
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
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
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:867
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