cprover
remove_returns.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove function return values
4 
5 Author: Daniel Kroening
6 
7 Date: September 2009
8 
9 \*******************************************************************/
10 
13 
14 #include "remove_returns.h"
15 
16 #include <util/std_expr.h>
17 #include <util/symbol_table.h>
18 
20 {
21 public:
22  explicit remove_returnst(symbol_tablet &_symbol_table):
23  symbol_table(_symbol_table)
24  {
25  }
26 
27  void operator()(
28  goto_functionst &goto_functions);
29 
30  void restore(
31  goto_functionst &goto_functions);
32 
33 protected:
35 
36  void replace_returns(
37  goto_functionst::function_mapt::iterator f_it);
38 
39  void do_function_calls(
40  goto_functionst &goto_functions,
41  goto_programt &goto_program);
42 
43  bool restore_returns(
44  goto_functionst::function_mapt::iterator f_it);
45 
47  goto_functionst &goto_functions,
48  goto_programt &goto_program);
49 };
50 
53  goto_functionst::function_mapt::iterator f_it)
54 {
55  typet return_type=f_it->second.type.return_type();
56 
57  const irep_idt function_id=f_it->first;
58 
59  // returns something but void?
60  bool has_return_value=return_type!=empty_typet();
61 
62  if(has_return_value)
63  {
64  // look up the function symbol
65  symbol_tablet::symbolst::iterator s_it=
66  symbol_table.symbols.find(function_id);
67 
68  assert(s_it!=symbol_table.symbols.end());
69  symbolt &function_symbol=s_it->second;
70 
71  // make the return type 'void'
72  f_it->second.type.return_type()=empty_typet();
73  function_symbol.type=f_it->second.type;
74 
75  // add return_value symbol to symbol_table
76  auxiliary_symbolt new_symbol;
77  new_symbol.is_static_lifetime=true;
78  new_symbol.module=function_symbol.module;
79  new_symbol.base_name=
80  id2string(function_symbol.base_name)+RETURN_VALUE_SUFFIX;
81  new_symbol.name=id2string(function_symbol.name)+RETURN_VALUE_SUFFIX;
82  new_symbol.mode=function_symbol.mode;
83  new_symbol.type=return_type;
84 
85  symbol_table.add(new_symbol);
86  }
87 
88  goto_programt &goto_program=f_it->second.body;
89 
90  if(goto_program.empty())
91  return;
92 
93  if(has_return_value)
94  {
95  Forall_goto_program_instructions(i_it, goto_program)
96  {
97  if(i_it->is_return())
98  {
99  assert(i_it->code.operands().size()==1);
100 
101  // replace "return x;" by "fkt#return_value=x;"
102  symbol_exprt lhs_expr;
103  lhs_expr.set_identifier(id2string(function_id)+RETURN_VALUE_SUFFIX);
104  lhs_expr.type()=return_type;
105 
106  code_assignt assignment(lhs_expr, i_it->code.op0());
107 
108  // now turn the `return' into `assignment'
109  i_it->type=ASSIGN;
110  i_it->code=assignment;
111  }
112  }
113  }
114 }
115 
118  goto_functionst &goto_functions,
119  goto_programt &goto_program)
120 {
121  Forall_goto_program_instructions(i_it, goto_program)
122  {
123  if(i_it->is_function_call())
124  {
125  code_function_callt &function_call=to_code_function_call(i_it->code);
126 
127  code_typet old_type=to_code_type(function_call.function().type());
128 
129  // Do we return anything?
130  if(old_type.return_type()!=empty_typet())
131  {
132  // replace "lhs=f(...)" by
133  // "f(...); lhs=f#return_value; DEAD f#return_value;"
134  assert(function_call.function().id()==ID_symbol);
135 
136  const irep_idt function_id=
137  to_symbol_expr(function_call.function()).get_identifier();
138 
139  // see if we have a body
140  goto_functionst::function_mapt::const_iterator
141  f_it=goto_functions.function_map.find(function_id);
142 
143  if(f_it==goto_functions.function_map.end())
144  throw
145  "failed to find function `"+id2string(function_id)+
146  "' in function map";
147 
148  // fix the type
149  to_code_type(function_call.function().type()).return_type()=
150  empty_typet();
151 
152  if(function_call.lhs().is_not_nil())
153  {
154  exprt rhs;
155 
156  if(f_it->second.body_available())
157  {
158  symbol_exprt return_value;
159  return_value.type()=function_call.lhs().type();
160  return_value.set_identifier(
161  id2string(function_id)+RETURN_VALUE_SUFFIX);
162  rhs=return_value;
163  }
164  else
165  {
166  rhs=side_effect_expr_nondett(function_call.lhs().type());
167  }
168 
169  goto_programt::targett t_a=goto_program.insert_after(i_it);
170  t_a->make_assignment();
171  t_a->source_location=i_it->source_location;
172  t_a->code=code_assignt(function_call.lhs(), rhs);
173  t_a->function=i_it->function;
174 
175  // fry the previous assignment
176  function_call.lhs().make_nil();
177 
178  if(f_it->second.body_available())
179  {
180  goto_programt::targett t_d=goto_program.insert_after(t_a);
181  t_d->make_dead();
182  t_d->source_location=i_it->source_location;
183  t_d->code=code_deadt(rhs);
184  t_d->function=i_it->function;
185  }
186  }
187  }
188  }
189  }
190 }
191 
193 {
194  Forall_goto_functions(it, goto_functions)
195  {
196  replace_returns(it);
197  do_function_calls(goto_functions, it->second.body);
198  }
199 }
200 
204  goto_functionst &goto_functions)
205 {
206  remove_returnst rr(symbol_table);
207  rr(goto_functions);
208 }
209 
211 void remove_returns(goto_modelt &goto_model)
212 {
213  remove_returnst rr(goto_model.symbol_table);
214  rr(goto_model.goto_functions);
215 }
216 
219  const irep_idt &function_id)
220 {
221  code_typet type;
222  type.make_nil();
223 
224  // do we have X#return_value?
225  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
226 
227  symbol_tablet::symbolst::const_iterator rv_it=
228  symbol_table.symbols.find(rv_name);
229 
230  if(rv_it!=symbol_table.symbols.end())
231  {
232  // look up the function symbol
233  symbol_tablet::symbolst::const_iterator s_it=
234  symbol_table.symbols.find(function_id);
235 
236  assert(s_it!=symbol_table.symbols.end());
237 
238  type=to_code_type(s_it->second.type);
239  type.return_type()=rv_it->second.type;
240  }
241 
242  return type;
243 }
244 
247  goto_functionst::function_mapt::iterator f_it)
248 {
249  const irep_idt function_id=f_it->first;
250 
251  // do we have X#return_value?
252  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
253 
254  symbol_tablet::symbolst::iterator rv_it=
255  symbol_table.symbols.find(rv_name);
256 
257  if(rv_it==symbol_table.symbols.end())
258  return true;
259 
260  // look up the function symbol
261  symbol_tablet::symbolst::iterator s_it=
262  symbol_table.symbols.find(function_id);
263 
264  assert(s_it!=symbol_table.symbols.end());
265  symbolt &function_symbol=s_it->second;
266 
267  // restore the return type
268  f_it->second.type=original_return_type(symbol_table, function_id);
269  function_symbol.type=f_it->second.type;
270 
271  // remove the return_value symbol from the symbol_table
272  irep_idt rv_name_id=rv_it->second.name;
273  symbol_table.symbols.erase(rv_it);
274 
275  goto_programt &goto_program=f_it->second.body;
276 
277  Forall_goto_program_instructions(i_it, goto_program)
278  {
279  if(i_it->is_assign())
280  {
281  code_assignt &assign=to_code_assign(i_it->code);
282  if(assign.lhs().id()!=ID_symbol ||
283  to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
284  continue;
285 
286  // replace "fkt#return_value=x;" by "return x;"
287  code_returnt return_code(assign.rhs());
288 
289  // the assignment might be a goto target
290  i_it->make_skip();
291  i_it++;
292 
293  while(!i_it->is_goto() && !i_it->is_end_function())
294  {
295  assert(i_it->is_dead());
296  i_it++;
297  }
298 
299  if(i_it->is_goto())
300  {
301  goto_programt::const_targett target=i_it->get_target();
302  assert(target->is_end_function());
303  }
304  else
305  {
306  assert(i_it->is_end_function());
307  i_it=goto_program.instructions.insert(i_it, *i_it);
308  }
309 
310  i_it->make_return();
311  i_it->code=return_code;
312  }
313  }
314 
315  return false;
316 }
317 
320  goto_functionst &goto_functions,
321  goto_programt &goto_program)
322 {
324 
325  Forall_goto_program_instructions(i_it, goto_program)
326  {
327  if(i_it->is_function_call())
328  {
329  code_function_callt &function_call=to_code_function_call(i_it->code);
330 
331  // ignore function pointers
332  if(function_call.function().id()!=ID_symbol)
333  continue;
334 
335  const irep_idt function_id=
336  to_symbol_expr(function_call.function()).get_identifier();
337 
338  const symbolt &function_symbol=ns.lookup(function_id);
339 
340  // fix the type
341  to_code_type(function_call.function().type()).return_type()=
342  to_code_type(function_symbol.type).return_type();
343 
344  // find "f(...); lhs=f#return_value; DEAD f#return_value;"
345  // and revert to "lhs=f(...);"
346  goto_programt::instructionst::iterator next=i_it;
347  ++next;
348  assert(next!=goto_program.instructions.end());
349 
350  if(!next->is_assign())
351  continue;
352 
353  const code_assignt &assign=to_code_assign(next->code);
354 
355  if(assign.rhs().id()!=ID_symbol)
356  continue;
357 
358  irep_idt rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
359  const symbol_exprt &rhs=to_symbol_expr(assign.rhs());
360  if(rhs.get_identifier()!=rv_name)
361  continue;
362 
363  // restore the previous assignment
364  function_call.lhs()=assign.lhs();
365 
366  // remove the assignment and subsequent dead
367  // i_it remains valid
368  next=goto_program.instructions.erase(next);
369  assert(next!=goto_program.instructions.end());
370  assert(next->is_dead());
371  // i_it remains valid
372  goto_program.instructions.erase(next);
373  }
374  }
375 }
376 
378 {
379  // restore all types first
380  bool unmodified=true;
381  Forall_goto_functions(it, goto_functions)
382  unmodified=restore_returns(it) && unmodified;
383 
384  if(!unmodified)
385  {
386  Forall_goto_functions(it, goto_functions)
387  undo_function_calls(goto_functions, it->second.body);
388  }
389 }
390 
394  goto_functionst &goto_functions)
395 {
396  remove_returnst rr(symbol_table);
397  rr.restore(goto_functions);
398 }
void restore(goto_functionst &goto_functions)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
irep_idt mode
Language mode.
Definition: symbol.h:55
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
remove_returnst(symbol_tablet &_symbol_table)
symbol_tablet & symbol_table
bool empty() const
Is the program empty?
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
typet & type()
Definition: expr.h:60
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
instructionst::const_iterator const_targett
symbolst symbols
Definition: symbol_table.h:57
void undo_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns f(...); lhs=f::return_value; into x=f(...)
exprt & rhs()
Definition: std_code.h:162
The empty type.
Definition: std_types.h:53
API to expression classes.
code_typet original_return_type(const symbol_tablet &symbol_table, const irep_idt &function_id)
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void do_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
bool restore_returns(goto_functionst::function_mapt::iterator f_it)
turns &#39;return x&#39; into an assignment to fkt::return_value
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
A function call.
Definition: std_code.h:657
Remove function returns.
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
#define Forall_goto_functions(it, functions)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
A removal of a local variable.
Definition: std_code.h:234
void make_nil()
Definition: irep.h:243
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
void remove_returns(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void operator()(goto_functionst &goto_functions)
#define RETURN_VALUE_SUFFIX
Return from a function.
Definition: std_code.h:714
void replace_returns(goto_functionst::function_mapt::iterator f_it)
turns &#39;return x&#39; into an assignment to fkt::return_value
goto_functionst goto_functions
Definition: goto_model.h:26
const typet & return_type() const
Definition: std_types.h:831
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700