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,
27  bool adjust_function)
28 {
29  const namespacet ns(goto_model.symbol_table);
31  goto_model.goto_functions,
32  ns,
34  adjust_function);
35 }
36 
38  goto_functionst &goto_functions,
39  const namespacet &ns,
41  bool adjust_function)
42 {
44  goto_functions,
45  ns,
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 
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,
112  unsigned smallfunc_limit,
113  bool adjust_function)
114 {
115  const namespacet ns(goto_model.symbol_table);
117  goto_model.goto_functions,
118  ns,
120  smallfunc_limit,
121  adjust_function);
122 }
123 
134  goto_functionst &goto_functions,
135  const namespacet &ns,
137  unsigned smallfunc_limit,
138  bool adjust_function)
139 {
141  goto_functions,
142  ns,
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 
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  INVARIANT(i_it->is_function_call(), "is a call");
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,
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,
230  adjust_function,
231  caching);
232 }
233 
242  goto_functionst &goto_functions,
243  const irep_idt function,
244  const namespacet &ns,
246  bool adjust_function,
247  bool caching)
248 {
250  goto_functions,
251  ns,
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 
275  {
276  if(!i_it->is_function_call())
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_modelt &goto_model,
287  const irep_idt function,
289  bool adjust_function,
290  bool caching)
291 {
292  const namespacet ns(goto_model.symbol_table);
293 
295  goto_model.goto_functions,
296  ns,
298  adjust_function,
299  caching);
300 
301  goto_functionst::function_mapt::iterator f_it=
302  goto_model.goto_functions.function_map.find(function);
303 
304  if(f_it==goto_model.goto_functions.function_map.end())
305  return jsont();
306 
307  goto_functionst::goto_functiont &goto_function=f_it->second;
308 
309  if(!goto_function.body_available())
310  return jsont();
311 
312  // gather all calls
313  goto_inlinet::inline_mapt inline_map;
314 
315  // create empty call list
316  goto_inlinet::call_listt &call_list=inline_map[f_it->first];
317 
318  goto_programt &goto_program=goto_function.body;
319 
321  {
322  if(!i_it->is_function_call())
323  continue;
324 
325  call_list.push_back(goto_inlinet::callt(i_it, true));
326  }
327 
328  goto_inline.goto_inline(function, goto_function, inline_map, true);
329  goto_model.goto_functions.update();
331 
332  return goto_inline.output_inline_log_json();
333 }
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:128
goto_programt body
Definition: goto_function.h:23
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)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
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:611
const irep_idt & id() const
Definition: irep.h:189
std::map< irep_idt, call_listt > inline_mapt
bool is_inlined() const
Definition: goto_function.h:34
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Function Inlining.
::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
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
bool body_available() const
Definition: goto_function.h:29
static irep_idt entry_point()
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:42
#define Forall_goto_functions(it, functions)
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Base Type Computation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32