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/base_type.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
22 #include "remove_skip.h"
23 #include "goto_inline_class.h"
24 
26  goto_modelt &goto_model,
27  message_handlert &message_handler,
28  bool adjust_function)
29 {
30  const namespacet ns(goto_model.symbol_table);
32  goto_model.goto_functions,
33  ns,
34  message_handler,
35  adjust_function);
36 }
37 
39  goto_functionst &goto_functions,
40  const namespacet &ns,
41  message_handlert &message_handler,
42  bool adjust_function)
43 {
45  goto_functions,
46  ns,
47  message_handler,
48  adjust_function);
49 
50  typedef goto_functionst::goto_functiont goto_functiont;
51 
52  // find entry point
53  goto_functionst::function_mapt::iterator it=
54  goto_functions.function_map.find(goto_functionst::entry_point());
55 
56  if(it==goto_functions.function_map.end())
57  return;
58 
59  goto_functiont &goto_function=it->second;
60  assert(goto_function.body_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(!goto_inlinet::is_call(i_it))
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(), goto_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 
145  typedef goto_functionst::goto_functiont goto_functiont;
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(!goto_inlinet::is_call(i_it))
168  continue;
169 
170  exprt lhs;
171  exprt function_expr;
172  exprt::operandst arguments;
173  exprt constrain;
174  goto_inlinet::get_call(i_it, lhs, function_expr, arguments, constrain);
175 
176  if(function_expr.id()!=ID_symbol)
177  // Can't handle pointers to functions
178  continue;
179 
180  const symbol_exprt &symbol_expr=to_symbol_expr(function_expr);
181  const irep_idt id=symbol_expr.get_identifier();
182 
183  goto_functionst::function_mapt::const_iterator f_it=
184  goto_functions.function_map.find(id);
185 
186  if(f_it==goto_functions.function_map.end())
187  // Function not loaded, can't check size
188  continue;
189 
190  // called function
191  const goto_functiont &goto_function=f_it->second;
192 
193  if(!goto_function.body_available())
194  // The bodies of functions that don't have bodies can't be inlined.
195  continue;
196 
197  const goto_programt &goto_program=goto_function.body;
198 
199  if(goto_function.is_inlined() ||
200  goto_program.instructions.size()<=smallfunc_limit)
201  {
202  assert(goto_inlinet::is_call(i_it));
203  call_list.push_back(goto_inlinet::callt(i_it, false));
204  }
205  }
206  }
207 
208  goto_inline.goto_inline(inline_map, false);
209 }
210 
218  goto_modelt &goto_model,
219  const irep_idt function,
220  message_handlert &message_handler,
221  bool adjust_function,
222  bool caching)
223 {
224  const namespacet ns(goto_model.symbol_table);
226  goto_model.goto_functions,
227  function,
228  ns,
229  message_handler,
230  adjust_function,
231  caching);
232 }
233 
242  goto_functionst &goto_functions,
243  const irep_idt function,
244  const namespacet &ns,
245  message_handlert &message_handler,
246  bool adjust_function,
247  bool caching)
248 {
250  goto_functions,
251  ns,
252  message_handler,
253  adjust_function,
254  caching);
255 
256  goto_functionst::function_mapt::iterator f_it=
257  goto_functions.function_map.find(function);
258 
259  if(f_it==goto_functions.function_map.end())
260  return;
261 
262  goto_functionst::goto_functiont &goto_function=f_it->second;
263 
264  if(!goto_function.body_available())
265  return;
266 
267  // gather all calls
268  goto_inlinet::inline_mapt inline_map;
269 
270  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
271 
272  goto_programt &goto_program=goto_function.body;
273 
274  Forall_goto_program_instructions(i_it, goto_program)
275  {
276  if(!goto_inlinet::is_call(i_it))
277  continue;
278 
279  call_list.push_back(goto_inlinet::callt(i_it, true));
280  }
281 
282  goto_inline.goto_inline(function, goto_function, inline_map, true);
283 }
284 
286  goto_functionst &goto_functions,
287  const irep_idt function,
288  const namespacet &ns,
289  message_handlert &message_handler,
290  bool adjust_function,
291  bool caching)
292 {
294  goto_functions,
295  ns,
296  message_handler,
297  adjust_function,
298  caching);
299 
300  goto_functionst::function_mapt::iterator f_it=
301  goto_functions.function_map.find(function);
302 
303  if(f_it==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(!goto_inlinet::is_call(i_it))
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_functions.update();
329  goto_functions.compute_loop_numbers();
330 
331  return goto_inline.output_inline_log_json();
332 }
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Definition: json.h:21
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.
symbol_tablet symbol_table
Definition: goto_model.h:25
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
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...
const irep_idt & id() const
Definition: irep.h:189
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::map< irep_idt, call_listt > inline_mapt
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Function Inlining.
goto_function_templatet< goto_programt > goto_functiont
jsont goto_function_inline_and_log(goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
std::vector< exprt > operandst
Definition: expr.h:49
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:25
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Base Type Computation.
Program Transformation.
static bool is_call(goto_programt::const_targett target)
goto_functionst goto_functions
Definition: goto_model.h:26
jsont output_inline_log_json()