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 
18 #include "goto_model.h"
19 
20 #include "remove_skip.h"
21 
23 {
24 public:
25  explicit remove_returnst(symbol_table_baset &_symbol_table):
26  symbol_table(_symbol_table)
27  {
28  }
29 
30  void operator()(
31  goto_functionst &goto_functions);
32 
33  void operator()(
34  goto_model_functiont &model_function,
35  function_is_stubt function_is_stub);
36 
37  void restore(
38  goto_functionst &goto_functions);
39 
40 protected:
42 
43  void replace_returns(
44  const irep_idt &function_id,
46 
47  void do_function_calls(
48  function_is_stubt function_is_stub,
50 
51  bool restore_returns(
52  goto_functionst::function_mapt::iterator f_it);
53 
55  goto_functionst &goto_functions,
57 
59 };
60 
63 {
64  const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
65  const symbolt *existing_symbol = symbol_table.lookup(symbol_name);
66  if(existing_symbol != nullptr)
67  return existing_symbol->symbol_expr();
68 
69  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
70  const typet &return_type = to_code_type(function_symbol.type).return_type();
71 
72  if(return_type == empty_typet())
73  return symbol_exprt();
74 
75  auxiliary_symbolt new_symbol;
76  new_symbol.is_static_lifetime = true;
77  new_symbol.module = function_symbol.module;
78  new_symbol.base_name =
79  id2string(function_symbol.base_name) + RETURN_VALUE_SUFFIX;
80  new_symbol.name = symbol_name;
81  new_symbol.mode = function_symbol.mode;
82  // If we're creating this for the first time, the target function cannot have
83  // been remove_return'd yet, so this will still be the "true" return type:
84  new_symbol.type = return_type;
85  // Return-value symbols will always be written before they are read, so there
86  // is no need for __CPROVER_initialize to do anything:
87  new_symbol.type.set(ID_C_no_initialization_required, true);
88 
89  symbol_table.add(new_symbol);
90  return new_symbol.symbol_expr();
91 }
92 
97  const irep_idt &function_id,
99 {
100  typet return_type = function.type.return_type();
101 
102  // returns something but void?
103  if(return_type == empty_typet())
104  return;
105 
106  // add return_value symbol to symbol_table, if not already created:
107  symbol_exprt return_symbol = get_or_create_return_value_symbol(function_id);
108 
109  // look up the function symbol
110  symbolt &function_symbol = *symbol_table.get_writeable(function_id);
111 
112  // make the return type 'void'
113  function.type.return_type() = empty_typet();
114  function_symbol.type = function.type;
115 
116  goto_programt &goto_program = function.body;
117 
119  {
120  if(i_it->is_return())
121  {
122  INVARIANT(
123  i_it->code.operands().size() == 1,
124  "return instructions should have one operand");
125 
126  // replace "return x;" by "fkt#return_value=x;"
127  code_assignt assignment(return_symbol, i_it->code.op0());
128 
129  // now turn the `return' into `assignment'
130  i_it->make_assignment(assignment);
131  }
132  }
133 }
134 
140  function_is_stubt function_is_stub,
142 {
144  {
145  if(i_it->is_function_call())
146  {
147  code_function_callt &function_call=to_code_function_call(i_it->code);
148 
149  INVARIANT(
150  function_call.function().id() == ID_symbol,
151  "indirect function calls should have been removed prior to running "
152  "remove-returns");
153 
154  const irep_idt function_id =
155  to_symbol_expr(function_call.function()).get_identifier();
156 
157  symbol_exprt return_value;
158  typet old_return_type;
159  bool is_stub = function_is_stub(function_id);
160 
161  if(is_stub)
162  {
163  old_return_type =
164  to_code_type(function_call.function().type()).return_type();
165  }
166  else
167  {
168  // The callee may or may not already have been transformed by this pass,
169  // so its symbol-table entry may already have void return type.
170  // To simplify matters, create its return-value global now (if not
171  // already done), and use that to determine its true return type.
172  return_value = get_or_create_return_value_symbol(function_id);
173  if(return_value == symbol_exprt()) // really void-typed?
174  continue;
175  old_return_type = return_value.type();
176  }
177 
178  // Do we return anything?
179  if(old_return_type != empty_typet())
180  {
181  // replace "lhs=f(...)" by
182  // "f(...); lhs=f#return_value; DEAD f#return_value;"
183 
184  // fix the type
185  to_code_type(function_call.function().type()).return_type()=
186  empty_typet();
187 
188  if(function_call.lhs().is_not_nil())
189  {
190  exprt rhs;
191 
192  if(!is_stub)
193  rhs=return_value;
194  else
195  rhs=side_effect_expr_nondett(function_call.lhs().type());
196 
198  t_a->make_assignment();
199  t_a->source_location=i_it->source_location;
200  t_a->code=code_assignt(function_call.lhs(), rhs);
201  t_a->function=i_it->function;
202 
203  // fry the previous assignment
204  function_call.lhs().make_nil();
205 
206  if(!is_stub)
207  {
209  t_d->make_dead();
210  t_d->source_location=i_it->source_location;
211  t_d->code=code_deadt(rhs);
212  t_d->function=i_it->function;
213  }
214  }
215  }
216  }
217  }
218 }
219 
221 {
222  Forall_goto_functions(it, goto_functions)
223  {
224  // NOLINTNEXTLINE
225  auto function_is_stub = [&goto_functions](const irep_idt &function_id) {
226  auto findit = goto_functions.function_map.find(function_id);
227  INVARIANT(
228  findit != goto_functions.function_map.end(),
229  "called function should have some entry in the function map");
230  return !findit->second.body_available();
231  };
232 
233  replace_returns(it->first, it->second);
234  do_function_calls(function_is_stub, it->second.body);
235  }
236 }
237 
239  goto_model_functiont &model_function,
240  function_is_stubt function_is_stub)
241 {
242  goto_functionst::goto_functiont &goto_function =
243  model_function.get_goto_function();
244 
245  // If this is a stub it doesn't have a corresponding #return_value,
246  // not any return instructions to alter:
247  if(goto_function.body.empty())
248  return;
249 
250  replace_returns(model_function.get_function_id(), goto_function);
251  do_function_calls(function_is_stub, goto_function.body);
252 }
253 
256  symbol_table_baset &symbol_table,
257  goto_functionst &goto_functions)
258 {
259  remove_returnst rr(symbol_table);
260  rr(goto_functions);
261 }
262 
275  goto_model_functiont &goto_model_function,
276  function_is_stubt function_is_stub)
277 {
278  remove_returnst rr(goto_model_function.get_symbol_table());
279  rr(goto_model_function, function_is_stub);
280 }
281 
283 void remove_returns(goto_modelt &goto_model)
284 {
285  remove_returnst rr(goto_model.symbol_table);
286  rr(goto_model.goto_functions);
287 }
288 
295  const symbol_table_baset &symbol_table,
296  const irep_idt &function_id)
297 {
298  // look up the function symbol
299  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
300  code_typet type = to_code_type(function_symbol.type);
301 
302  // do we have X#return_value?
303  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
304 
305  symbol_tablet::symbolst::const_iterator rv_it=
306  symbol_table.symbols.find(rv_name);
307 
308  if(rv_it != symbol_table.symbols.end())
309  type.return_type() = rv_it->second.type;
310 
311  return type;
312 }
313 
316  goto_functionst::function_mapt::iterator f_it)
317 {
318  const irep_idt function_id=f_it->first;
319 
320  // do we have X#return_value?
321  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
322 
323  symbol_tablet::symbolst::const_iterator rv_it=
324  symbol_table.symbols.find(rv_name);
325 
326  if(rv_it==symbol_table.symbols.end())
327  return true;
328 
329  // look up the function symbol
330  symbolt &function_symbol=*symbol_table.get_writeable(function_id);
331 
332  // restore the return type
333  f_it->second.type=original_return_type(symbol_table, function_id);
334  function_symbol.type=f_it->second.type;
335 
336  // remove the return_value symbol from the symbol_table
337  irep_idt rv_name_id=rv_it->second.name;
338  symbol_table.erase(rv_it);
339 
340  goto_programt &goto_program=f_it->second.body;
341 
342  bool did_something = false;
343 
345  {
346  if(i_it->is_assign())
347  {
348  code_assignt &assign=to_code_assign(i_it->code);
349  if(assign.lhs().id()!=ID_symbol ||
350  to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
351  continue;
352 
353  // replace "fkt#return_value=x;" by "return x;"
354  const exprt rhs = assign.rhs();
355  i_it->make_return();
356  i_it->code = code_returnt(rhs);
357  did_something = true;
358  }
359  }
360 
361  if(did_something)
363 
364  return false;
365 }
366 
369  goto_functionst &goto_functions,
371 {
373 
375  {
376  if(i_it->is_function_call())
377  {
378  code_function_callt &function_call=to_code_function_call(i_it->code);
379 
380  // ignore function pointers
381  if(function_call.function().id()!=ID_symbol)
382  continue;
383 
384  const irep_idt function_id=
385  to_symbol_expr(function_call.function()).get_identifier();
386 
387  const symbolt &function_symbol=ns.lookup(function_id);
388 
389  // fix the type
390  to_code_type(function_call.function().type()).return_type()=
391  to_code_type(function_symbol.type).return_type();
392 
393  // find "f(...); lhs=f#return_value; DEAD f#return_value;"
394  // and revert to "lhs=f(...);"
395  goto_programt::instructionst::iterator next=i_it;
396  ++next;
397  INVARIANT(
398  next!=goto_program.instructions.end(),
399  "non-void function call must be followed by #return_value read");
400 
401  if(!next->is_assign())
402  continue;
403 
404  const code_assignt &assign=to_code_assign(next->code);
405 
406  if(assign.rhs().id()!=ID_symbol)
407  continue;
408 
409  irep_idt rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
410  const symbol_exprt &rhs=to_symbol_expr(assign.rhs());
411  if(rhs.get_identifier()!=rv_name)
412  continue;
413 
414  // restore the previous assignment
415  function_call.lhs()=assign.lhs();
416 
417  // remove the assignment and subsequent dead
418  // i_it remains valid
419  next=goto_program.instructions.erase(next);
420  INVARIANT(
421  next!=goto_program.instructions.end() && next->is_dead(),
422  "read from #return_value should be followed by DEAD #return_value");
423  // i_it remains valid
424  goto_program.instructions.erase(next);
425  }
426  }
427 }
428 
430 {
431  // restore all types first
432  bool unmodified=true;
433  Forall_goto_functions(it, goto_functions)
434  unmodified=restore_returns(it) && unmodified;
435 
436  if(!unmodified)
437  {
438  Forall_goto_functions(it, goto_functions)
439  undo_function_calls(goto_functions, it->second.body);
440  }
441 }
442 
444 void restore_returns(goto_modelt &goto_model)
445 {
446  remove_returnst rr(goto_model.symbol_table);
447  rr.restore(goto_model.goto_functions);
448 }
void restore(goto_functionst &goto_functions)
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
std::function< bool(const irep_idt &)> function_is_stubt
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:200
exprt & op0()
Definition: expr.h:72
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_identifier() const
Definition: std_expr.h:128
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
code_typet original_return_type(const symbol_table_baset &symbol_table, const irep_idt &function_id)
Get code type of a function that has had remove_returns run upon it.
bool is_static_lifetime
Definition: symbol.h:67
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:193
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:186
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
Symbol Table + CFG.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
instructionst::iterator targett
Definition: goto_program.h:397
void undo_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns f(...); lhs=f::return_value; into lhs=f(...)
exprt & rhs()
Definition: std_code.h:213
The empty type.
Definition: std_types.h:54
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
bool restore_returns(goto_functionst::function_mapt::iterator f_it)
turns an assignment to fkt::return_value back into &#39;return x&#39;
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
A function call.
Definition: std_code.h:828
void restore_returns(goto_modelt &goto_model)
restores return statements
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
remove_returnst(symbol_table_baset &_symbol_table)
Remove function returns.
const symbolst & symbols
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
symbol_table_baset & symbol_table
typet type
Type of symbol.
Definition: symbol.h:34
void replace_returns(const irep_idt &function_id, goto_functionst::goto_functiont &function)
turns &#39;return x&#39; into an assignment to fkt::return_value
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_functions(it, functions)
symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id)
A removal of a local variable.
Definition: std_code.h:305
void make_nil()
Definition: irep.h:243
void do_function_calls(function_is_stubt function_is_stub, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void operator()(goto_functionst &goto_functions)
#define RETURN_VALUE_SUFFIX
Return from a function.
Definition: std_code.h:893
Program Transformation.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147