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,
49  goto_programt &goto_program);
50 
51  bool restore_returns(
52  goto_functionst::function_mapt::iterator f_it);
53 
55  goto_programt &goto_program);
56 
58 };
59 
62 {
63  const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
64  const symbolt *existing_symbol = symbol_table.lookup(symbol_name);
65  if(existing_symbol != nullptr)
66  return existing_symbol->symbol_expr();
67 
68  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
69  const typet &return_type = to_code_type(function_symbol.type).return_type();
70 
71  if(return_type == empty_typet())
72  return symbol_exprt();
73 
74  auxiliary_symbolt new_symbol;
75  new_symbol.is_static_lifetime = true;
76  new_symbol.module = function_symbol.module;
77  new_symbol.base_name =
78  id2string(function_symbol.base_name) + RETURN_VALUE_SUFFIX;
79  new_symbol.name = symbol_name;
80  new_symbol.mode = function_symbol.mode;
81  // If we're creating this for the first time, the target function cannot have
82  // been remove_return'd yet, so this will still be the "true" return type:
83  new_symbol.type = return_type;
84  // Return-value symbols will always be written before they are read, so there
85  // is no need for __CPROVER_initialize to do anything:
86  new_symbol.type.set(ID_C_no_initialization_required, true);
87 
88  symbol_table.add(new_symbol);
89  return new_symbol.symbol_expr();
90 }
91 
96  const irep_idt &function_id,
98 {
99  typet return_type = function.type.return_type();
100 
101  // returns something but void?
102  if(return_type == empty_typet())
103  return;
104 
105  // add return_value symbol to symbol_table, if not already created:
106  symbol_exprt return_symbol = get_or_create_return_value_symbol(function_id);
107 
108  // look up the function symbol
109  symbolt &function_symbol = *symbol_table.get_writeable(function_id);
110 
111  // make the return type 'void'
112  function.type.return_type() = empty_typet();
113  function_symbol.type = function.type;
114 
115  goto_programt &goto_program = function.body;
116 
117  Forall_goto_program_instructions(i_it, goto_program)
118  {
119  if(i_it->is_return())
120  {
121  INVARIANT(
122  i_it->code.operands().size() == 1,
123  "return instructions should have one operand");
124 
125  // replace "return x;" by "fkt#return_value=x;"
126  code_assignt assignment(return_symbol, i_it->code.op0());
127 
128  // now turn the `return' into `assignment'
129  i_it->make_assignment(assignment);
130  }
131  }
132 }
133 
139  function_is_stubt function_is_stub,
140  goto_programt &goto_program)
141 {
142  Forall_goto_program_instructions(i_it, goto_program)
143  {
144  if(i_it->is_function_call())
145  {
146  code_function_callt &function_call=to_code_function_call(i_it->code);
147 
148  INVARIANT(
149  function_call.function().id() == ID_symbol,
150  "indirect function calls should have been removed prior to running "
151  "remove-returns");
152 
153  const irep_idt function_id =
154  to_symbol_expr(function_call.function()).get_identifier();
155 
156  symbol_exprt return_value;
157  typet old_return_type;
158  bool is_stub = function_is_stub(function_id);
159 
160  if(is_stub)
161  {
162  old_return_type =
163  to_code_type(function_call.function().type()).return_type();
164  }
165  else
166  {
167  // The callee may or may not already have been transformed by this pass,
168  // so its symbol-table entry may already have void return type.
169  // To simplify matters, create its return-value global now (if not
170  // already done), and use that to determine its true return type.
171  return_value = get_or_create_return_value_symbol(function_id);
172  if(return_value == symbol_exprt()) // really void-typed?
173  continue;
174  old_return_type = return_value.type();
175  }
176 
177  // Do we return anything?
178  if(old_return_type != empty_typet())
179  {
180  // replace "lhs=f(...)" by
181  // "f(...); lhs=f#return_value; DEAD f#return_value;"
182 
183  // fix the type
184  to_code_type(function_call.function().type()).return_type()=
185  empty_typet();
186 
187  if(function_call.lhs().is_not_nil())
188  {
189  exprt rhs;
190 
191  if(!is_stub)
192  {
193  // The return type in the definition of the function may differ
194  // from the return type in the declaration. We therefore do a
195  // cast.
197  return_value, function_call.lhs().type());
198  }
199  else
201  function_call.lhs().type(), i_it->source_location);
202 
203  goto_programt::targett t_a=goto_program.insert_after(i_it);
204  t_a->make_assignment();
205  t_a->source_location=i_it->source_location;
206  t_a->code=code_assignt(function_call.lhs(), rhs);
207  t_a->function=i_it->function;
208 
209  // fry the previous assignment
210  function_call.lhs().make_nil();
211 
212  if(!is_stub)
213  {
214  goto_programt::targett t_d=goto_program.insert_after(t_a);
215  t_d->make_dead();
216  t_d->source_location=i_it->source_location;
217  t_d->code = code_deadt(return_value);
218  t_d->function=i_it->function;
219  }
220  }
221  }
222  }
223  }
224 }
225 
227 {
228  Forall_goto_functions(it, goto_functions)
229  {
230  // NOLINTNEXTLINE
231  auto function_is_stub = [&goto_functions](const irep_idt &function_id) {
232  auto findit = goto_functions.function_map.find(function_id);
233  INVARIANT(
234  findit != goto_functions.function_map.end(),
235  "called function should have some entry in the function map");
236  return !findit->second.body_available();
237  };
238 
239  replace_returns(it->first, it->second);
240  do_function_calls(function_is_stub, it->second.body);
241  }
242 }
243 
245  goto_model_functiont &model_function,
246  function_is_stubt function_is_stub)
247 {
248  goto_functionst::goto_functiont &goto_function =
249  model_function.get_goto_function();
250 
251  // If this is a stub it doesn't have a corresponding #return_value,
252  // not any return instructions to alter:
253  if(goto_function.body.empty())
254  return;
255 
256  replace_returns(model_function.get_function_id(), goto_function);
257  do_function_calls(function_is_stub, goto_function.body);
258 }
259 
262  symbol_table_baset &symbol_table,
263  goto_functionst &goto_functions)
264 {
265  remove_returnst rr(symbol_table);
266  rr(goto_functions);
267 }
268 
281  goto_model_functiont &goto_model_function,
282  function_is_stubt function_is_stub)
283 {
284  remove_returnst rr(goto_model_function.get_symbol_table());
285  rr(goto_model_function, function_is_stub);
286 }
287 
289 void remove_returns(goto_modelt &goto_model)
290 {
291  remove_returnst rr(goto_model.symbol_table);
292  rr(goto_model.goto_functions);
293 }
294 
301  const symbol_table_baset &symbol_table,
302  const irep_idt &function_id)
303 {
304  // look up the function symbol
305  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
306  code_typet type = to_code_type(function_symbol.type);
307 
308  // do we have X#return_value?
309  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
310 
311  symbol_tablet::symbolst::const_iterator rv_it=
312  symbol_table.symbols.find(rv_name);
313 
314  if(rv_it != symbol_table.symbols.end())
315  type.return_type() = rv_it->second.type;
316 
317  return type;
318 }
319 
322  goto_functionst::function_mapt::iterator f_it)
323 {
324  const irep_idt function_id=f_it->first;
325 
326  // do we have X#return_value?
327  std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
328 
329  symbol_tablet::symbolst::const_iterator rv_it=
330  symbol_table.symbols.find(rv_name);
331 
332  if(rv_it==symbol_table.symbols.end())
333  return true;
334 
335  // look up the function symbol
336  symbolt &function_symbol=*symbol_table.get_writeable(function_id);
337 
338  // restore the return type
339  f_it->second.type=original_return_type(symbol_table, function_id);
340  function_symbol.type=f_it->second.type;
341 
342  // remove the return_value symbol from the symbol_table
343  irep_idt rv_name_id=rv_it->second.name;
344  symbol_table.erase(rv_it);
345 
346  goto_programt &goto_program=f_it->second.body;
347 
348  bool did_something = false;
349 
350  Forall_goto_program_instructions(i_it, goto_program)
351  {
352  if(i_it->is_assign())
353  {
354  code_assignt &assign=to_code_assign(i_it->code);
355  if(assign.lhs().id()!=ID_symbol ||
356  to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
357  continue;
358 
359  // replace "fkt#return_value=x;" by "return x;"
360  const exprt rhs = assign.rhs();
361  i_it->make_return();
362  i_it->code = code_returnt(rhs);
363  did_something = true;
364  }
365  }
366 
367  if(did_something)
368  remove_skip(goto_program);
369 
370  return false;
371 }
372 
375  goto_programt &goto_program)
376 {
378 
379  Forall_goto_program_instructions(i_it, goto_program)
380  {
381  if(i_it->is_function_call())
382  {
383  code_function_callt &function_call=to_code_function_call(i_it->code);
384 
385  // ignore function pointers
386  if(function_call.function().id()!=ID_symbol)
387  continue;
388 
389  const irep_idt function_id=
390  to_symbol_expr(function_call.function()).get_identifier();
391 
392  const symbolt &function_symbol=ns.lookup(function_id);
393 
394  // fix the type
395  to_code_type(function_call.function().type()).return_type()=
396  to_code_type(function_symbol.type).return_type();
397 
398  // find "f(...); lhs=f#return_value; DEAD f#return_value;"
399  // and revert to "lhs=f(...);"
400  goto_programt::instructionst::iterator next=i_it;
401  ++next;
402  INVARIANT(
403  next!=goto_program.instructions.end(),
404  "non-void function call must be followed by #return_value read");
405 
406  if(!next->is_assign())
407  continue;
408 
409  const code_assignt &assign=to_code_assign(next->code);
410 
411  if(assign.rhs().id()!=ID_symbol)
412  continue;
413 
414  irep_idt rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;
415  const symbol_exprt &rhs=to_symbol_expr(assign.rhs());
416  if(rhs.get_identifier()!=rv_name)
417  continue;
418 
419  // restore the previous assignment
420  function_call.lhs()=assign.lhs();
421 
422  // remove the assignment and subsequent dead
423  // i_it remains valid
424  next=goto_program.instructions.erase(next);
425  INVARIANT(
426  next!=goto_program.instructions.end() && next->is_dead(),
427  "read from #return_value should be followed by DEAD #return_value");
428  // i_it remains valid
429  goto_program.instructions.erase(next);
430  }
431  }
432 }
433 
435 {
436  // restore all types first
437  bool unmodified=true;
438  Forall_goto_functions(it, goto_functions)
439  unmodified=restore_returns(it) && unmodified;
440 
441  if(!unmodified)
442  {
443  Forall_goto_functions(it, goto_functions)
444  undo_function_calls(it->second.body);
445  }
446 }
447 
449 void restore_returns(goto_modelt &goto_model)
450 {
451  remove_returnst rr(goto_model.symbol_table);
452  rr.restore(goto_model.goto_functions);
453 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:96
remove_returnst::restore
void restore(goto_functionst &goto_functions)
Definition: remove_returns.cpp:434
symbol_table_baset::get_writeable
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
irept::make_nil
void make_nil()
Definition: irep.h:315
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
goto_model_functiont::get_function_id
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:210
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
symbol_table_baset::erase
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
function_is_stubt
std::function< bool(const irep_idt &)> function_is_stubt
Definition: remove_returns.h:34
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:148
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
remove_returnst::undo_function_calls
void undo_function_calls(goto_programt &goto_program)
turns f(...); lhs=f::return_value; into lhs=f(...)
Definition: remove_returns.cpp:374
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:48
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
remove_returnst::remove_returnst
remove_returnst(symbol_table_baset &_symbol_table)
Definition: remove_returns.cpp:25
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
remove_returnst::restore_returns
bool restore_returns(goto_functionst::function_mapt::iterator f_it)
turns an assignment to fkt::return_value back into 'return x'
Definition: remove_returns.cpp:321
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
goto_model_functiont::get_symbol_table
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:196
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
RETURN_VALUE_SUFFIX
#define RETURN_VALUE_SUFFIX
Definition: remove_returns.h:21
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
nullary_exprt::op0
const exprt & op0() const =delete
remove_returns.h
remove_returnst::symbol_table
symbol_table_baset & symbol_table
Definition: remove_returns.cpp:41
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
original_return_type
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.
Definition: remove_returns.cpp:300
remove_returnst::get_or_create_return_value_symbol
symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id)
Definition: remove_returns.cpp:61
remove_returnst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_returns.cpp:226
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:261
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
remove_returnst::do_function_calls
void do_function_calls(function_is_stubt function_is_stub, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
Definition: remove_returns.cpp:138
remove_returnst
Definition: remove_returns.cpp:22
goto_model_functiont::get_goto_function
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:203
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
remove_returnst::replace_returns
void replace_returns(const irep_idt &function_id, goto_functionst::goto_functiont &function)
turns 'return x' into an assignment to fkt::return_value
Definition: remove_returns.cpp:95
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
restore_returns
void restore_returns(goto_modelt &goto_model)
restores return statements
Definition: remove_returns.cpp:449
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
validation_modet::INVARIANT
@ INVARIANT