cprover
Loading...
Searching...
No Matches
goto_inline_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
14
15#ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
16#define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
17
18#include <unordered_set>
19
20#include <util/message.h>
21#include <util/json.h>
22
23#include "goto_functions.h"
24
26{
27public:
37 const namespacet &ns,
38 message_handlert &message_handler,
39 bool adjust_function,
40 bool caching = true)
41 : log(message_handler),
43 ns(ns),
46 {
47 }
48
50
51 // call that should be inlined
52 // false: inline non-transitively
53 // true: inline transitively
54 typedef std::pair<goto_programt::targett, bool> callt;
55
56 // list of calls that should be inlined
57 typedef std::list<callt> call_listt;
58
59 // list of calls per function that should be inlined
60 typedef std::map<irep_idt, call_listt> inline_mapt;
61
62 // handle given goto function
63 // force_full:
64 // - true: put skip on recursion and issue warning
65 // - false: leave call on recursion
66 void goto_inline(
67 const irep_idt identifier,
68 goto_functiont &goto_function,
70 const bool force_full=false);
71
72 // handle all functions
73 void goto_inline(
75 const bool force_full=false);
76
78 std::ostream &out,
79 const inline_mapt &inline_map);
80
81 void output_cache(std::ostream &out) const;
82
83 // call after goto_functions.update()!
89
90 // get call info of normal or bp call
91 static void get_call(
93 exprt &lhs,
94 exprt &function,
95 exprt::operandst &arguments);
96
98 {
99 public:
101 {
102 public:
103 // original segment location numbers
106 unsigned call_location_number; // original call location number
107 irep_idt function; // function from which segment was inlined
109 };
110
111 // remove segment that refer to the given goto program
112 void cleanup(const goto_programt &goto_program);
113
114 void cleanup(const goto_functionst::function_mapt &function_map);
115
116 void add_segment(
117 const goto_programt &goto_program,
118 const unsigned begin_location_number,
119 const unsigned end_location_number,
120 const unsigned call_location_number,
121 const irep_idt function);
122
123 void copy_from(const goto_programt &from, const goto_programt &to);
124
125 // call after goto_functions.update()!
127
128 // map from segment start to inline info
129 typedef std::map<
132
134 };
135
136protected:
140
141 const bool adjust_function;
142 const bool caching;
143
145
147 const irep_idt identifier,
148 goto_functiont &goto_function,
149 const inline_mapt &inline_map,
150 const bool force_full);
151
153 const irep_idt identifier,
154 const goto_functiont &goto_function,
155 const bool force_full);
156
157 bool check_inline_map(const inline_mapt &inline_map) const;
158 bool check_inline_map(
159 const irep_idt identifier,
160 const inline_mapt &inline_map) const;
161
162 bool is_ignored(const irep_idt id) const;
163
164 void clear()
165 {
166 cache.clear();
170 }
171
174 const inline_mapt &inline_map,
175 const bool transitive,
176 const bool force_full,
178
180 const goto_functiont &f,
183 const exprt &lhs,
184 const symbol_exprt &function,
185 const exprt::operandst &arguments);
186
187 void replace_return(
188 goto_programt &body,
189 const exprt &lhs);
190
192 const goto_programt::targett target,
193 const irep_idt &function_name,
194 const goto_functiont::parameter_identifierst &parameter_identifiers,
195 const exprt::operandst &arguments,
197
199 const goto_programt::targett target,
200 const goto_functiont::parameter_identifierst &parameter_identifiers,
202
203 // goto functions that were already inlined transitively
206
207 typedef std::unordered_set<irep_idt> finished_sett;
209
210 typedef std::unordered_set<irep_idt> recursion_sett;
212
213 typedef std::unordered_set<irep_idt> no_body_sett;
215};
216
217#endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
A collection of goto functions.
std::map< irep_idt, goto_functiont > function_mapt
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
std::vector< irep_idt > parameter_identifierst
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
void copy_from(const goto_programt &from, const goto_programt &to)
void cleanup(const goto_programt &goto_program)
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
bool is_ignored(const irep_idt id) const
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
std::list< callt > call_listt
goto_functionst & goto_functions
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
Sets up the class with the program to operate on.
jsont output_inline_log_json()
no_body_sett no_body_set
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
Inline all of the chosen calls in a given function.
recursion_sett recursion_set
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
bool check_inline_map(const inline_mapt &inline_map) const
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)
const bool adjust_function
goto_inline_logt inline_log
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
std::unordered_set< irep_idt > finished_sett
goto_functionst::goto_functiont goto_functiont
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst &parameter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
std::pair< goto_programt::targett, bool > callt
std::map< irep_idt, call_listt > inline_mapt
std::unordered_set< irep_idt > no_body_sett
void replace_return(goto_programt &body, const exprt &lhs)
finished_sett finished_set
std::unordered_set< irep_idt > recursion_sett
const namespacet & ns
goto_functionst::function_mapt cachet
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.
void output_cache(std::ostream &out) const
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
Definition json.h:27
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:80
Goto Programs with Functions.