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