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 <util/prefix.h>
15 #include <util/cprover_prefix.h>
16 #include <util/std_code.h>
17 #include <util/std_expr.h>
18 
19 #include "goto_inline_class.h"
20 
22  goto_modelt &goto_model,
23  message_handlert &message_handler,
24  bool adjust_function)
25 {
26  const namespacet ns(goto_model.symbol_table);
28  goto_model.goto_functions,
29  ns,
30  message_handler,
31  adjust_function);
32 }
33 
35  goto_functionst &goto_functions,
36  const namespacet &ns,
37  message_handlert &message_handler,
38  bool adjust_function)
39 {
41  goto_functions,
42  ns,
43  message_handler,
44  adjust_function);
45 
47 
48  // find entry point
49  goto_functionst::function_mapt::iterator it=
50  goto_functions.function_map.find(goto_functionst::entry_point());
51 
52  if(it==goto_functions.function_map.end())
53  return;
54 
55  goto_functiont &entry_function = it->second;
57  entry_function.body_available(),
58  "body of entry point function must be available");
59 
60  // gather all calls
61  // we use non-transitive inlining to avoid the goto program
62  // copying that goto_inlinet would do otherwise
63  goto_inlinet::inline_mapt inline_map;
64 
65  for(auto &gf_entry : goto_functions.function_map)
66  {
67  goto_functiont &goto_function = gf_entry.second;
68 
69  if(!goto_function.body_available())
70  continue;
71 
72  goto_inlinet::call_listt &call_list = inline_map[gf_entry.first];
73 
74  goto_programt &goto_program=goto_function.body;
75 
76  Forall_goto_program_instructions(i_it, goto_program)
77  {
78  if(!i_it->is_function_call())
79  continue;
80 
81  call_list.push_back(goto_inlinet::callt(i_it, false));
82  }
83  }
84 
85  goto_inline.goto_inline(
86  goto_functionst::entry_point(), entry_function, inline_map, true);
87 
88  // clean up
89  for(auto &gf_entry : goto_functions.function_map)
90  {
91  if(gf_entry.first != goto_functionst::entry_point())
92  {
93  goto_functiont &goto_function = gf_entry.second;
94  goto_function.body.clear();
95  }
96  }
97 }
98 
107  goto_modelt &goto_model,
108  message_handlert &message_handler,
109  unsigned smallfunc_limit,
110  bool adjust_function)
111 {
112  const namespacet ns(goto_model.symbol_table);
114  goto_model.goto_functions,
115  ns,
116  message_handler,
117  smallfunc_limit,
118  adjust_function);
119 }
120 
131  goto_functionst &goto_functions,
132  const namespacet &ns,
133  message_handlert &message_handler,
134  unsigned smallfunc_limit,
135  bool adjust_function)
136 {
138  goto_functions,
139  ns,
140  message_handler,
141  adjust_function);
142 
144 
145  // gather all calls
146  goto_inlinet::inline_mapt inline_map;
147 
148  for(auto &gf_entry : goto_functions.function_map)
149  {
150  goto_functiont &goto_function = gf_entry.second;
151 
152  if(!goto_function.body_available())
153  continue;
154 
155  if(gf_entry.first == goto_functions.entry_point())
156  {
157  // Don't inline any function calls made from the _start function.
158  continue;
159  }
160 
161  goto_programt &goto_program=goto_function.body;
162 
163  goto_inlinet::call_listt &call_list = inline_map[gf_entry.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:1185
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:29
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:440
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:106
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:54
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:80
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:141
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:38
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
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:109
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
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
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:767
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:569
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:74
code_typet::get_inlined
bool get_inlined() const
Definition: std_types.h:659
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:21