cprover
goto_inline.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Function Inlining
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_inline.h"
13 
14 #include <cassert>
15 
16 #include <util/prefix.h>
17 #include <util/cprover_prefix.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 
21 #include "goto_inline_class.h"
22 
24  goto_modelt &goto_model,
25  message_handlert &message_handler,
26  bool adjust_function)
27 {
28  const namespacet ns(goto_model.symbol_table);
30  goto_model.goto_functions,
31  ns,
32  message_handler,
33  adjust_function);
34 }
35 
37  goto_functionst &goto_functions,
38  const namespacet &ns,
39  message_handlert &message_handler,
40  bool adjust_function)
41 {
43  goto_functions,
44  ns,
45  message_handler,
46  adjust_function);
47 
49 
50  // find entry point
51  goto_functionst::function_mapt::iterator it=
52  goto_functions.function_map.find(goto_functionst::entry_point());
53 
54  if(it==goto_functions.function_map.end())
55  return;
56 
57  goto_functiont &entry_function = it->second;
59  entry_function.body_available(),
60  "body of entry point function must be available");
61 
62  // gather all calls
63  // we use non-transitive inlining to avoid the goto program
64  // copying that goto_inlinet would do otherwise
65  goto_inlinet::inline_mapt inline_map;
66 
67  Forall_goto_functions(f_it, goto_functions)
68  {
69  goto_functiont &goto_function=f_it->second;
70 
71  if(!goto_function.body_available())
72  continue;
73 
74  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
75 
76  goto_programt &goto_program=goto_function.body;
77 
78  Forall_goto_program_instructions(i_it, goto_program)
79  {
80  if(!i_it->is_function_call())
81  continue;
82 
83  call_list.push_back(goto_inlinet::callt(i_it, false));
84  }
85  }
86 
87  goto_inline.goto_inline(
88  goto_functionst::entry_point(), entry_function, inline_map, true);
89 
90  // clean up
91  Forall_goto_functions(f_it, goto_functions)
92  {
93  if(f_it->first!=goto_functionst::entry_point())
94  {
95  goto_functiont &goto_function=f_it->second;
96  goto_function.body.clear();
97  }
98  }
99 }
100 
109  goto_modelt &goto_model,
110  message_handlert &message_handler,
111  unsigned smallfunc_limit,
112  bool adjust_function)
113 {
114  const namespacet ns(goto_model.symbol_table);
116  goto_model.goto_functions,
117  ns,
118  message_handler,
119  smallfunc_limit,
120  adjust_function);
121 }
122 
133  goto_functionst &goto_functions,
134  const namespacet &ns,
135  message_handlert &message_handler,
136  unsigned smallfunc_limit,
137  bool adjust_function)
138 {
140  goto_functions,
141  ns,
142  message_handler,
143  adjust_function);
144 
146 
147  // gather all calls
148  goto_inlinet::inline_mapt inline_map;
149 
150  Forall_goto_functions(f_it, goto_functions)
151  {
152  goto_functiont &goto_function=f_it->second;
153 
154  if(!goto_function.body_available())
155  continue;
156 
157  if(f_it->first==goto_functions.entry_point())
158  // Don't inline any function calls made from the _start function.
159  continue;
160 
161  goto_programt &goto_program=goto_function.body;
162 
163  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
164 
165  Forall_goto_program_instructions(i_it, goto_program)
166  {
167  if(!i_it->is_function_call())
168  continue;
169 
170  exprt lhs;
171  exprt function_expr;
172  exprt::operandst arguments;
173  goto_inlinet::get_call(i_it, lhs, function_expr, arguments);
174 
175  if(function_expr.id()!=ID_symbol)
176  // Can't handle pointers to functions
177  continue;
178 
179  const symbol_exprt &symbol_expr=to_symbol_expr(function_expr);
180  const irep_idt id=symbol_expr.get_identifier();
181 
182  goto_functionst::function_mapt::const_iterator called_it =
183  goto_functions.function_map.find(id);
184 
185  if(called_it == goto_functions.function_map.end())
186  // Function not loaded, can't check size
187  continue;
188 
189  // called function
190  const goto_functiont &called_function = called_it->second;
191 
192  if(!called_function.body_available())
193  // The bodies of functions that don't have bodies can't be inlined.
194  continue;
195 
196  if(
197  to_code_type(ns.lookup(id).type).get_inlined() ||
198  called_function.body.instructions.size() <= smallfunc_limit)
199  {
200  PRECONDITION(i_it->is_function_call());
201 
202  call_list.push_back(goto_inlinet::callt(i_it, false));
203  }
204  }
205  }
206 
207  goto_inline.goto_inline(inline_map, false);
208 }
209 
217  goto_modelt &goto_model,
218  const irep_idt function,
219  message_handlert &message_handler,
220  bool adjust_function,
221  bool caching)
222 {
223  const namespacet ns(goto_model.symbol_table);
225  goto_model.goto_functions,
226  function,
227  ns,
228  message_handler,
229  adjust_function,
230  caching);
231 }
232 
241  goto_functionst &goto_functions,
242  const irep_idt function,
243  const namespacet &ns,
244  message_handlert &message_handler,
245  bool adjust_function,
246  bool caching)
247 {
249  goto_functions,
250  ns,
251  message_handler,
252  adjust_function,
253  caching);
254 
255  goto_functionst::function_mapt::iterator f_it=
256  goto_functions.function_map.find(function);
257 
258  if(f_it==goto_functions.function_map.end())
259  return;
260 
261  goto_functionst::goto_functiont &goto_function=f_it->second;
262 
263  if(!goto_function.body_available())
264  return;
265 
266  // gather all calls
267  goto_inlinet::inline_mapt inline_map;
268 
269  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
270 
271  goto_programt &goto_program=goto_function.body;
272 
273  Forall_goto_program_instructions(i_it, goto_program)
274  {
275  if(!i_it->is_function_call())
276  continue;
277 
278  call_list.push_back(goto_inlinet::callt(i_it, true));
279  }
280 
281  goto_inline.goto_inline(function, goto_function, inline_map, true);
282 }
283 
285  goto_modelt &goto_model,
286  const irep_idt function,
287  message_handlert &message_handler,
288  bool adjust_function,
289  bool caching)
290 {
291  const namespacet ns(goto_model.symbol_table);
292 
294  goto_model.goto_functions,
295  ns,
296  message_handler,
297  adjust_function,
298  caching);
299 
300  goto_functionst::function_mapt::iterator f_it=
301  goto_model.goto_functions.function_map.find(function);
302 
303  if(f_it==goto_model.goto_functions.function_map.end())
304  return jsont();
305 
306  goto_functionst::goto_functiont &goto_function=f_it->second;
307 
308  if(!goto_function.body_available())
309  return jsont();
310 
311  // gather all calls
312  goto_inlinet::inline_mapt inline_map;
313 
314  // create empty call list
315  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
316 
317  goto_programt &goto_program=goto_function.body;
318 
319  Forall_goto_program_instructions(i_it, goto_program)
320  {
321  if(!i_it->is_function_call())
322  continue;
323 
324  call_list.push_back(goto_inlinet::callt(i_it, true));
325  }
326 
327  goto_inline.goto_inline(function, goto_function, inline_map, true);
328  goto_model.goto_functions.update();
330 
331  return goto_inline.output_inline_log_json();
332 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
goto_inline.h
Function Inlining.
goto_inlinet::call_listt
std::list< callt > call_listt
Definition: goto_inline_class.h:45
goto_inlinet::get_call
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
Definition: goto_inline_class.cpp:447
goto_function_inline_and_log
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Definition: goto_inline.cpp:284
goto_partial_inline
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
Definition: goto_inline.cpp:108
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
jsont
Definition: json.h:27
goto_inlinet::callt
std::pair< goto_programt::targett, bool > callt
Definition: goto_inline_class.h:42
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
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:44
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
goto_inline_class.h
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
goto_function_inline
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
Definition: goto_inline.cpp:216
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
cprover_prefix.h
std_code.h
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:783
goto_inlinet::inline_mapt
std::map< irep_idt, call_listt > inline_mapt
Definition: goto_inline_class.h:48
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
goto_functionst::update
void update()
Definition: goto_functions.h:81
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
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
std_expr.h
API to expression classes.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_inlinet
Definition: goto_inline_class.h:21
goto_inline
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:23