cprover
goto_inline_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
11 #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
12 
13 #include <unordered_set>
14 
15 #include <util/message.h>
16 #include <util/json.h>
17 
18 #include "goto_functions.h"
19 
20 class goto_inlinet:public messaget
21 {
22 public:
25  const namespacet &ns,
27  bool adjust_function,
28  bool caching=true):
31  ns(ns),
34  {
35  }
36 
38 
39  // call that should be inlined
40  // false: inline non-transitively
41  // true: inline transitively
42  typedef std::pair<goto_programt::targett, bool> callt;
43 
44  // list of calls that should be inlined
45  typedef std::list<callt> call_listt;
46 
47  // list of calls per function that should be inlined
48  typedef std::map<irep_idt, call_listt> inline_mapt;
49 
50  // handle given goto function
51  // force_full:
52  // - true: put skip on recursion and issue warning
53  // - false: leave call on recursion
54  void goto_inline(
55  const irep_idt identifier,
56  goto_functiont &goto_function,
57  const inline_mapt &inline_map,
58  const bool force_full=false);
59 
60  // handle all functions
61  void goto_inline(
62  const inline_mapt &inline_map,
63  const bool force_full=false);
64 
65  void output_inline_map(
66  std::ostream &out,
67  const inline_mapt &inline_map);
68 
69  void output_cache(std::ostream &out) const;
70 
71  // call after goto_functions.update()!
73  {
76  }
77 
78  // get call info of normal or bp call
79  static void get_call(
81  exprt &lhs,
82  exprt &function,
83  exprt::operandst &arguments);
84 
86  {
87  public:
89  {
90  public:
91  // original segment location numbers
94  unsigned call_location_number; // original call location number
95  irep_idt function; // function from which segment was inlined
97  };
98 
99  // remove segment that refer to the given goto program
100  void cleanup(const goto_programt &goto_program);
101 
102  void cleanup(const goto_functionst::function_mapt &function_map);
103 
104  void add_segment(
105  const goto_programt &goto_program,
106  const unsigned begin_location_number,
107  const unsigned end_location_number,
108  const unsigned call_location_number,
109  const irep_idt function);
110 
111  void copy_from(const goto_programt &from, const goto_programt &to);
112 
113  // call after goto_functions.update()!
115 
116  // map from segment start to inline info
117  typedef std::map<
120 
122  };
123 
124 protected:
126  const namespacet &ns;
127 
128  const bool adjust_function;
129  const bool caching;
130 
132 
134  const irep_idt identifier,
135  goto_functiont &goto_function,
136  const inline_mapt &inline_map,
137  const bool force_full);
138 
140  const irep_idt identifier,
141  const goto_functiont &goto_function,
142  const bool force_full);
143 
144  bool check_inline_map(const inline_mapt &inline_map) const;
145  bool check_inline_map(
146  const irep_idt identifier,
147  const inline_mapt &inline_map) const;
148 
149  bool is_ignored(const irep_idt id) const;
150 
151  void clear()
152  {
153  cache.clear();
154  finished_set.clear();
155  recursion_set.clear();
156  no_body_set.clear();
157  }
158 
160  goto_programt &dest,
161  const inline_mapt &inline_map,
162  const bool transitive,
163  const bool force_full,
164  goto_programt::targett target);
165 
167  const goto_functiont &f,
168  goto_programt &dest,
169  goto_programt::targett target,
170  const exprt &lhs,
171  const symbol_exprt &function,
172  const exprt::operandst &arguments);
173 
174  void replace_return(
175  goto_programt &body,
176  const exprt &lhs);
177 
179  const goto_programt::targett target,
180  const irep_idt &function_name,
181  const goto_functiont::parameter_identifierst &parameter_identifiers,
182  const exprt::operandst &arguments,
183  goto_programt &dest);
184 
186  const goto_programt::targett target,
187  const goto_functiont::parameter_identifierst &parameter_identifiers,
188  goto_programt &dest);
189 
190  // goto functions that were already inlined transitively
193 
194  typedef std::unordered_set<irep_idt> finished_sett;
196 
197  typedef std::unordered_set<irep_idt> recursion_sett;
199 
200  typedef std::unordered_set<irep_idt> no_body_sett;
202 };
203 
204 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number
unsigned begin_location_number
Definition: goto_inline_class.h:92
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_inlinet::insert_function_body
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)
Definition: goto_inline_class.cpp:234
goto_inlinet::output_inline_log_json
jsont output_inline_log_json()
Definition: goto_inline_class.h:72
goto_inlinet::call_listt
std::list< callt > call_listt
Definition: goto_inline_class.h:45
goto_inlinet::goto_inline_logt::add_segment
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)
Definition: goto_inline_class.cpp:752
goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number
unsigned call_location_number
Definition: goto_inline_class.h:94
goto_inlinet::replace_return
void replace_return(goto_programt &body, const exprt &lhs)
Definition: goto_inline_class.cpp:157
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:447
goto_inlinet::recursion_sett
std::unordered_set< irep_idt > recursion_sett
Definition: goto_inline_class.h:197
exprt
Base class for all expressions.
Definition: expr.h:53
goto_inlinet::goto_inline
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
Definition: goto_inline_class.cpp:481
goto_inlinet::goto_inline_logt::cleanup
void cleanup(const goto_programt &goto_program)
Definition: goto_inline_class.cpp:731
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number
unsigned end_location_number
Definition: goto_inline_class.h:93
jsont
Definition: json.h:27
goto_inlinet::callt
std::pair< goto_programt::targett, bool > callt
Definition: goto_inline_class.h:42
goto_inlinet::goto_inline_logt
Definition: goto_inline_class.h:86
goto_inlinet::adjust_function
const bool adjust_function
Definition: goto_inline_class.h:128
goto_inlinet::no_body_set
no_body_sett no_body_set
Definition: goto_inline_class.h:201
goto_inlinet::goto_inline_nontransitive
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
Definition: goto_inline_class.cpp:496
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_inlinet::recursion_set
recursion_sett recursion_set
Definition: goto_inline_class.h:198
goto_inlinet::cachet
goto_functionst::function_mapt cachet
Definition: goto_inline_class.h:191
goto_inlinet::clear
void clear()
Definition: goto_inline_class.h:151
goto_functionst::function_mapt
std::map< irep_idt, goto_functiont > function_mapt
Definition: goto_functions.h:26
goto_inlinet::goto_inline_logt::log_mapt
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
Definition: goto_inline_class.h:119
goto_inlinet::goto_inline_logt::output_inline_log_json
jsont output_inline_log_json() const
Definition: goto_inline_class.cpp:827
goto_inlinet::caching
const bool caching
Definition: goto_inline_class.h:129
goto_inlinet::no_body_sett
std::unordered_set< irep_idt > no_body_sett
Definition: goto_inline_class.h:200
goto_inlinet::goto_inline_logt::log_map
log_mapt log_map
Definition: goto_inline_class.h:121
goto_inlinet::goto_inlinet
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
Definition: goto_inline_class.h:23
goto_inlinet::cache
cachet cache
Definition: goto_inline_class.h:192
goto_inlinet::parameter_destruction
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)
Definition: goto_inline_class.cpp:131
goto_inlinet::goto_inline_logt::goto_inline_log_infot::end
goto_programt::const_targett end
Definition: goto_inline_class.h:96
message_handlert
Definition: message.h:28
goto_inlinet::goto_functions
goto_functionst & goto_functions
Definition: goto_inline_class.h:125
goto_inlinet::ns
const namespacet & ns
Definition: goto_inline_class.h:126
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
goto_inlinet::finished_sett
std::unordered_set< irep_idt > finished_sett
Definition: goto_inline_class.h:194
goto_inlinet::goto_inline_logt::goto_inline_log_infot
Definition: goto_inline_class.h:89
goto_inlinet::output_inline_map
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
Definition: goto_inline_class.cpp:676
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_inlinet::parameter_assignments
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)
Definition: goto_inline_class.cpp:30
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
goto_inlinet::finished_set
finished_sett finished_set
Definition: goto_inline_class.h:195
goto_inlinet::goto_inline_transitive
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
Definition: goto_inline_class.cpp:548
goto_inlinet::expand_function_call
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
Definition: goto_inline_class.cpp:321
json.h
goto_inlinet::check_inline_map
bool check_inline_map(const inline_mapt &inline_map) const
Definition: goto_inline_class.cpp:665
goto_functions.h
Goto Programs with Functions.
goto_inlinet::inline_log
goto_inline_logt inline_log
Definition: goto_inline_class.h:131
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:36
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_inlinet::is_ignored
bool is_ignored(const irep_idt id) const
Definition: goto_inline_class.cpp:610
message.h
goto_inlinet::goto_inline_logt::copy_from
void copy_from(const goto_programt &from, const goto_programt &to)
Definition: goto_inline_class.cpp:781
goto_inlinet::output_cache
void output_cache(std::ostream &out) const
Definition: goto_inline_class.cpp:719
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
goto_inlinet
Definition: goto_inline_class.h:21
goto_inlinet::goto_functiont
goto_functionst::goto_functiont goto_functiont
Definition: goto_inline_class.h:37