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 "goto_inline_class.h"
23 
25  goto_modelt &goto_model,
26  message_handlert &message_handler,
27  bool adjust_function)
28 {
29  const namespacet ns(goto_model.symbol_table);
31  goto_model.goto_functions,
32  ns,
33  message_handler,
34  adjust_function);
35 }
36 
38  goto_functionst &goto_functions,
39  const namespacet &ns,
40  message_handlert &message_handler,
41  bool adjust_function)
42 {
44  goto_functions,
45  ns,
46  message_handler,
47  adjust_function);
48 
50 
51  // find entry point
52  goto_functionst::function_mapt::iterator it=
53  goto_functions.function_map.find(goto_functionst::entry_point());
54 
55  if(it==goto_functions.function_map.end())
56  return;
57 
58  goto_functiont &goto_function=it->second;
60  goto_function.body_available(),
61  "body of entry point function must be available");
62 
63  // gather all calls
64  // we use non-transitive inlining to avoid the goto program
65  // copying that goto_inlinet would do otherwise
66  goto_inlinet::inline_mapt inline_map;
67 
68  Forall_goto_functions(f_it, goto_functions)
69  {
70  goto_functiont &goto_function=f_it->second;
71 
72  if(!goto_function.body_available())
73  continue;
74 
75  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
76 
77  goto_programt &goto_program=goto_function.body;
78 
79  Forall_goto_program_instructions(i_it, goto_program)
80  {
81  if(!i_it->is_function_call())
82  continue;
83 
84  call_list.push_back(goto_inlinet::callt(i_it, false));
85  }
86  }
87 
88  goto_inline.goto_inline(
89  goto_functionst::entry_point(), goto_function, inline_map, true);
90 
91  // clean up
92  Forall_goto_functions(f_it, goto_functions)
93  {
94  if(f_it->first!=goto_functionst::entry_point())
95  {
96  goto_functiont &goto_function=f_it->second;
97  goto_function.body.clear();
98  }
99  }
100 }
101 
110  goto_modelt &goto_model,
111  message_handlert &message_handler,
112  unsigned smallfunc_limit,
113  bool adjust_function)
114 {
115  const namespacet ns(goto_model.symbol_table);
117  goto_model.goto_functions,
118  ns,
119  message_handler,
120  smallfunc_limit,
121  adjust_function);
122 }
123 
134  goto_functionst &goto_functions,
135  const namespacet &ns,
136  message_handlert &message_handler,
137  unsigned smallfunc_limit,
138  bool adjust_function)
139 {
141  goto_functions,
142  ns,
143  message_handler,
144  adjust_function);
145 
147 
148  // gather all calls
149  goto_inlinet::inline_mapt inline_map;
150 
151  Forall_goto_functions(f_it, goto_functions)
152  {
153  goto_functiont &goto_function=f_it->second;
154 
155  if(!goto_function.body_available())
156  continue;
157 
158  if(f_it->first==goto_functions.entry_point())
159  // Don't inline any function calls made from the _start function.
160  continue;
161 
162  goto_programt &goto_program=goto_function.body;
163 
164  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
165 
166  Forall_goto_program_instructions(i_it, goto_program)
167  {
168  if(!i_it->is_function_call())
169  continue;
170 
171  exprt lhs;
172  exprt function_expr;
173  exprt::operandst arguments;
174  goto_inlinet::get_call(i_it, lhs, function_expr, arguments);
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  PRECONDITION(i_it->is_function_call());
203 
204  call_list.push_back(goto_inlinet::callt(i_it, false));
205  }
206  }
207  }
208 
209  goto_inline.goto_inline(inline_map, false);
210 }
211 
219  goto_modelt &goto_model,
220  const irep_idt function,
221  message_handlert &message_handler,
222  bool adjust_function,
223  bool caching)
224 {
225  const namespacet ns(goto_model.symbol_table);
227  goto_model.goto_functions,
228  function,
229  ns,
230  message_handler,
231  adjust_function,
232  caching);
233 }
234 
243  goto_functionst &goto_functions,
244  const irep_idt function,
245  const namespacet &ns,
246  message_handlert &message_handler,
247  bool adjust_function,
248  bool caching)
249 {
251  goto_functions,
252  ns,
253  message_handler,
254  adjust_function,
255  caching);
256 
257  goto_functionst::function_mapt::iterator f_it=
258  goto_functions.function_map.find(function);
259 
260  if(f_it==goto_functions.function_map.end())
261  return;
262 
263  goto_functionst::goto_functiont &goto_function=f_it->second;
264 
265  if(!goto_function.body_available())
266  return;
267 
268  // gather all calls
269  goto_inlinet::inline_mapt inline_map;
270 
271  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
272 
273  goto_programt &goto_program=goto_function.body;
274 
275  Forall_goto_program_instructions(i_it, goto_program)
276  {
277  if(!i_it->is_function_call())
278  continue;
279 
280  call_list.push_back(goto_inlinet::callt(i_it, true));
281  }
282 
283  goto_inline.goto_inline(function, goto_function, inline_map, true);
284 }
285 
287  goto_modelt &goto_model,
288  const irep_idt function,
289  message_handlert &message_handler,
290  bool adjust_function,
291  bool caching)
292 {
293  const namespacet ns(goto_model.symbol_table);
294 
296  goto_model.goto_functions,
297  ns,
298  message_handler,
299  adjust_function,
300  caching);
301 
302  goto_functionst::function_mapt::iterator f_it=
303  goto_model.goto_functions.function_map.find(function);
304 
305  if(f_it==goto_model.goto_functions.function_map.end())
306  return jsont();
307 
308  goto_functionst::goto_functiont &goto_function=f_it->second;
309 
310  if(!goto_function.body_available())
311  return jsont();
312 
313  // gather all calls
314  goto_inlinet::inline_mapt inline_map;
315 
316  // create empty call list
317  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
318 
319  goto_programt &goto_program=goto_function.body;
320 
321  Forall_goto_program_instructions(i_it, goto_program)
322  {
323  if(!i_it->is_function_call())
324  continue;
325 
326  call_list.push_back(goto_inlinet::callt(i_it, true));
327  }
328 
329  goto_inline.goto_inline(function, goto_function, inline_map, true);
330  goto_model.goto_functions.update();
332 
333  return goto_inline.output_inline_log_json();
334 }
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
void compute_loop_numbers()
const irep_idt & get_identifier() const
Definition: std_expr.h:176
goto_programt body
Definition: goto_function.h:29
Definition: json.h:23
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.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
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...
void clear()
Clear the goto program.
Definition: goto_program.h:647
const irep_idt & id() const
Definition: irep.h:259
std::map< irep_idt, call_listt > inline_mapt
bool is_inlined() const
Definition: goto_function.h:49
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Function Inlining.
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
Definition: expr.h:57
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
bool body_available() const
Definition: goto_function.h:44
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Definition: goto_inline.cpp:24
Base class for all expressions.
Definition: expr.h:54
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32