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 #include <util/json_expr.h>
18 
19 #include "goto_functions.h"
20 
21 class goto_inlinet:public messaget
22 {
23 public:
26  const namespacet &ns,
28  bool adjust_function,
29  bool caching=true):
30  messaget(message_handler),
31  goto_functions(goto_functions),
32  ns(ns),
33  adjust_function(adjust_function),
35  {
36  }
37 
39 
40  // call that should be inlined
41  // false: inline non-transitively
42  // true: inline transitively
43  typedef std::pair<goto_programt::targett, bool> callt;
44 
45  // list of calls that should be inlined
46  typedef std::list<callt> call_listt;
47 
48  // list of calls per function that should be inlined
49  typedef std::map<irep_idt, call_listt> inline_mapt;
50 
51  // handle given goto function
52  // force_full:
53  // - true: put skip on recursion and issue warning
54  // - false: leave call on recursion
55  void goto_inline(
56  const irep_idt identifier,
57  goto_functiont &goto_function,
58  const inline_mapt &inline_map,
59  const bool force_full=false);
60 
61  // handle all functions
62  void goto_inline(
63  const inline_mapt &inline_map,
64  const bool force_full=false);
65 
66  void output_inline_map(
67  std::ostream &out,
68  const inline_mapt &inline_map);
69 
70  void output_cache(std::ostream &out) const;
71 
72  // call after goto_functions.update()!
74  {
77  }
78 
79  // is bp call
80  static bool is_bp_call(goto_programt::const_targett target);
81  // is normal or bp call
82  static bool is_call(goto_programt::const_targett target);
83  // get call info of normal or bp call
84  static void get_call(
86  exprt &lhs,
87  exprt &function,
88  exprt::operandst &arguments,
89  exprt &constrain);
90 
92  {
93  public:
95  {
96  public:
97  // original segment location numbers
100  unsigned call_location_number; // original call location number
101  irep_idt function; // function from which segment was inlined
103  };
104 
105  // remove segment that refer to the given goto program
106  void cleanup(const goto_programt &goto_program);
107 
108  void cleanup(const goto_functionst::function_mapt &function_map);
109 
110  void add_segment(
111  const goto_programt &goto_program,
112  const unsigned begin_location_number,
113  const unsigned end_location_number,
114  const unsigned call_location_number,
115  const irep_idt function);
116 
117  void copy_from(const goto_programt &from, const goto_programt &to);
118 
119  // call after goto_functions.update()!
121 
122  // map from segment start to inline info
123  typedef std::map<
126 
127  log_mapt log_map;
128  };
129 
130 protected:
132  const namespacet &ns;
133 
134  const bool adjust_function;
135  const bool caching;
136 
138 
140  const irep_idt identifier,
141  goto_functiont &goto_function,
142  const inline_mapt &inline_map,
143  const bool force_full);
144 
145  const goto_functiont &goto_inline_transitive(
146  const irep_idt identifier,
147  const goto_functiont &goto_function,
148  const bool force_full);
149 
150  bool check_inline_map(const inline_mapt &inline_map) const;
151  bool check_inline_map(
152  const irep_idt identifier,
153  const inline_mapt &inline_map) const;
154 
155  bool is_ignored(const irep_idt id) const;
156 
157  void clear()
158  {
159  cache.clear();
160  finished_set.clear();
161  recursion_set.clear();
162  no_body_set.clear();
163  }
164 
166  goto_programt &dest,
167  const inline_mapt &inline_map,
168  const bool transitive,
169  const bool force_full,
170  goto_programt::targett target);
171 
173  const goto_functiont &f,
174  goto_programt &dest,
175  goto_programt::targett target,
176  const exprt &lhs,
177  const symbol_exprt &function,
178  const exprt::operandst &arguments,
179  const exprt &constrain);
180 
182  goto_programt &dest,
183  const exprt &lhs,
184  goto_programt::targett target,
185  const symbol_exprt &function,
186  const exprt::operandst &arguments);
187 
188  void replace_return(
189  goto_programt &body,
190  const exprt &lhs,
191  const exprt &constrain);
192 
194  const goto_programt::targett target,
195  const irep_idt &function_name,
196  const code_typet &code_type,
197  const exprt::operandst &arguments,
198  goto_programt &dest);
199 
201  const goto_programt::targett target,
202  const irep_idt &function_name,
203  const code_typet &code_type,
204  goto_programt &dest);
205 
206  // goto functions that were already inlined transitively
208  cachet cache;
209 
210  typedef std::unordered_set<irep_idt, irep_id_hash> finished_sett;
211  finished_sett finished_set;
212 
213  typedef std::unordered_set<irep_idt, irep_id_hash> recursion_sett;
214  recursion_sett recursion_set;
215 
216  typedef std::unordered_set<irep_idt, irep_id_hash> no_body_sett;
217  no_body_sett no_body_set;
218 };
219 
220 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
std::map< irep_idt, goto_functiont > function_mapt
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
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)
Base type of functions.
Definition: std_types.h:734
goto_inline_logt inline_log
bool is_ignored(const irep_idt id) const
static bool is_bp_call(goto_programt::const_targett target)
Goto Programs with Functions.
Definition: json.h:21
void cleanup(const goto_programt &goto_program)
const bool caching
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
std::unordered_set< irep_idt, irep_id_hash > recursion_sett
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::map< irep_idt, call_listt > inline_mapt
instructionst::const_iterator const_targett
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, const exprt &constrain)
recursion_sett recursion_set
Expressions in JSON.
std::unordered_set< irep_idt, irep_id_hash > no_body_sett
void replace_return(goto_programt &body, const exprt &lhs, const exprt &constrain)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
bool check_inline_map(const inline_mapt &inline_map) const
goto_function_templatet< goto_programt > goto_functiont
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
std::vector< exprt > operandst
Definition: expr.h:49
const bool adjust_function
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
goto_functionst & goto_functions
const namespacet & ns
finished_sett finished_set
no_body_sett no_body_set
void output_cache(std::ostream &out) const
goto_functionst::function_mapt cachet
std::unordered_set< irep_idt, irep_id_hash > finished_sett
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
Base class for all expressions.
Definition: expr.h:46
void copy_from(const goto_programt &from, const goto_programt &to)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
goto_functionst::goto_functiont goto_functiont
static bool is_call(goto_programt::const_targett target)
message_handlert * message_handler
Definition: message.h:259
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
void insert_function_nobody(goto_programt &dest, const exprt &lhs, goto_programt::targett target, const symbol_exprt &function, const exprt::operandst &arguments)
jsont output_inline_log_json()