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  goto_programt &program=function.body;
31  rename_symbol(function.type);
32 
34  {
35  rename_symbol(iit->code);
36  rename_symbol(iit->guard);
37  // we need to update the instruction's function field as
38  // well, with the new symbol for the function
39  iit->function=new_function_name;
40  }
41 }
42 
45 static bool link_functions(
46  symbol_tablet &dest_symbol_table,
47  goto_functionst &dest_functions,
48  const symbol_tablet &src_symbol_table,
49  goto_functionst &src_functions,
50  const rename_symbolt &rename_symbol,
51  const std::unordered_set<irep_idt> &weak_symbols,
52  const replace_symbolt &object_type_updates)
53 {
54  namespacet ns(dest_symbol_table);
55  namespacet src_ns(src_symbol_table);
56 
57  // merge functions
58  Forall_goto_functions(src_it, src_functions)
59  {
60  // the function might have been renamed
61  rename_symbolt::expr_mapt::const_iterator e_it=
62  rename_symbol.expr_map.find(src_it->first);
63 
64  irep_idt final_id=src_it->first;
65 
66  if(e_it!=rename_symbol.expr_map.end())
67  final_id=e_it->second;
68 
69  // already there?
70  goto_functionst::function_mapt::iterator dest_f_it=
71  dest_functions.function_map.find(final_id);
72 
73  goto_functionst::goto_functiont &src_func = src_it->second;
74  if(dest_f_it==dest_functions.function_map.end()) // not there yet
75  {
76  rename_symbols_in_function(src_func, final_id, rename_symbol);
77  dest_functions.function_map.emplace(final_id, std::move(src_func));
78  }
79  else // collision!
80  {
81  goto_functionst::goto_functiont &in_dest_symbol_table = dest_f_it->second;
82 
83  if(in_dest_symbol_table.body.instructions.empty() ||
84  weak_symbols.find(final_id)!=weak_symbols.end())
85  {
86  // the one with body wins!
87  rename_symbols_in_function(src_func, final_id, rename_symbol);
88 
89  in_dest_symbol_table.body.swap(src_func.body);
90  in_dest_symbol_table.type=src_func.type;
91  }
92  else if(src_func.body.instructions.empty() ||
93  src_ns.lookup(src_it->first).is_weak)
94  {
95  // just keep the old one in dest
96  }
97  else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
98  {
99  // ok, we silently ignore
100  }
101  else
102  {
103  // the linking code will have ensured that types match
104  rename_symbol(src_func.type);
105  INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns),
106  "linking ensures that types match");
107  }
108  }
109  }
110 
111  // apply macros
112  rename_symbolt macro_application;
113 
114  for(const auto &symbol_pair : dest_symbol_table.symbols)
115  {
116  if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
117  {
118  const symbolt &symbol = symbol_pair.second;
119 
120  INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
121  const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
122 
123  #if 0
124  if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
125  {
126  std::cerr << symbol << '\n';
127  std::cerr << ns.lookup(id) << '\n';
128  }
129  INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns),
130  "type matches");
131  #endif
132 
133  macro_application.insert_expr(symbol.name, id);
134  }
135  }
136 
137  if(!macro_application.expr_map.empty())
138  Forall_goto_functions(dest_it, dest_functions)
139  {
140  irep_idt final_id=dest_it->first;
141  rename_symbols_in_function(dest_it->second, final_id, macro_application);
142  }
143 
144  if(!object_type_updates.empty())
145  {
146  Forall_goto_functions(dest_it, dest_functions)
147  Forall_goto_program_instructions(iit, dest_it->second.body)
148  {
149  object_type_updates(iit->code);
150  object_type_updates(iit->guard);
151  }
152  }
153 
154  return false;
155 }
156 
158  goto_modelt &dest,
159  goto_modelt &src,
160  message_handlert &message_handler)
161 {
162  std::unordered_set<irep_idt> weak_symbols;
163 
164  for(const auto &symbol_pair : dest.symbol_table.symbols)
165  {
166  if(symbol_pair.second.is_weak)
167  weak_symbols.insert(symbol_pair.first);
168  }
169 
171  src.symbol_table,
172  message_handler);
173 
174  if(linking.typecheck_main())
175  {
176  throw invalid_source_file_exceptiont("typechecking main failed");
177  }
178  if(link_functions(
179  dest.symbol_table,
180  dest.goto_functions,
181  src.symbol_table,
182  src.goto_functions,
183  linking.rename_symbol,
184  weak_symbols,
185  linking.object_type_updates))
186  {
187  throw invalid_source_file_exceptiont("linking failed");
188  }
189 }
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool empty() const
Symbol table entry.
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:332
const irep_idt & get_identifier() const
Definition: std_expr.h:176
exprt value
Initial value of symbol.
Definition: symbol.h:34
Thrown when we can&#39;t handle something in an input source file.
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1391
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
expr_mapt expr_map
Definition: rename_symbol.h:59
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
Replace expression or type symbols by an expression or type, respectively.
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const symbolst & symbols
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
typet type
Type of symbol.
Definition: symbol.h:31
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
ANSI-C Linking.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Base Type Computation.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166