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/suffix.h>
18 
19 #include "goto_model.h"
20 
21 #include "remove_skip.h"
22 
23 #define RETURN_VALUE_SUFFIX "#return_value"
24 
26 {
27 public:
28  explicit remove_returnst(symbol_table_baset &_symbol_table):
29  symbol_table(_symbol_table)
30  {
31  }
32 
33  void operator()(
34  goto_functionst &goto_functions);
35 
36  void operator()(
37  goto_model_functiont &model_function,
38  function_is_stubt function_is_stub);
39 
40  void restore(
41  goto_functionst &goto_functions);
42 
43 protected:
45 
46  void replace_returns(
47  const irep_idt &function_id,
49 
50  bool do_function_calls(
51  function_is_stubt function_is_stub,
52  goto_programt &goto_program);
53 
54  bool restore_returns(
55  goto_functionst::function_mapt::iterator f_it);
56 
58  goto_programt &goto_program);
59 
61  get_or_create_return_value_symbol(const irep_idt &function_id);
62 };
63 
66 {
67  const namespacet ns(symbol_table);
68  const auto symbol_expr = return_value_symbol(function_id, ns);
69  const auto symbol_name = symbol_expr.get_identifier();
70  if(symbol_table.has_symbol(symbol_name))
71  return symbol_expr;
72 
73  const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
74  const typet &return_type = to_code_type(function_symbol.type).return_type();
75 
76  if(return_type == empty_typet())
77  return {};
78 
79  auxiliary_symbolt new_symbol;
80  new_symbol.is_static_lifetime = true;
81  new_symbol.module = function_symbol.module;
82  new_symbol.base_name =
83  id2string(function_symbol.base_name) + RETURN_VALUE_SUFFIX;
84  new_symbol.name = symbol_name;
85  new_symbol.mode = function_symbol.mode;
86  // If we're creating this for the first time, the target function cannot have
87  // been remove_return'd yet, so this will still be the "true" return type:
88  new_symbol.type = return_type;
89  // Return-value symbols will always be written before they are read, so there
90  // is no need for __CPROVER_initialize to do anything:
91  new_symbol.type.set(ID_C_no_initialization_required, true);
92 
93  symbol_table.add(new_symbol);
94  return new_symbol.symbol_expr();
95 }
96 
101  const irep_idt &function_id,
103 {
104  typet return_type = function.type.return_type();
105 
106  // returns something but void?
107  if(return_type == empty_typet())
108  return;
109 
110  // add return_value symbol to symbol_table, if not already created:
111  const auto return_symbol = get_or_create_return_value_symbol(function_id);
112 
113  goto_programt &goto_program = function.body;
114 
115  Forall_goto_program_instructions(i_it, goto_program)
116  {
117  if(i_it->is_return())
118  {
119  INVARIANT(
120  i_it->code.operands().size() == 1,
121  "return instructions should have one operand");
122 
123  if(return_symbol.has_value())
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 =
131  }
132  else
133  i_it->turn_into_skip();
134  }
135  }
136 }
137 
145  function_is_stubt function_is_stub,
146  goto_programt &goto_program)
147 {
148  bool requires_update = false;
149 
150  Forall_goto_program_instructions(i_it, goto_program)
151  {
152  if(i_it->is_function_call())
153  {
154  code_function_callt function_call = i_it->get_function_call();
155 
156  INVARIANT(
157  function_call.function().id() == ID_symbol,
158  "indirect function calls should have been removed prior to running "
159  "remove-returns");
160 
161  const irep_idt function_id =
162  to_symbol_expr(function_call.function()).get_identifier();
163 
164  // Do we return anything?
165  if(does_function_call_return(function_call))
166  {
167  // replace "lhs=f(...)" by
168  // "f(...); lhs=f#return_value; DEAD f#return_value;"
169 
170  exprt rhs;
171 
172  bool is_stub = function_is_stub(function_id);
173  optionalt<symbol_exprt> return_value;
174 
175  if(!is_stub)
176  {
177  return_value = get_or_create_return_value_symbol(function_id);
178  CHECK_RETURN(return_value.has_value());
179 
180  // The return type in the definition of the function may differ
181  // from the return type in the declaration. We therefore do a
182  // cast.
184  *return_value, function_call.lhs().type());
185  }
186  else
187  {
189  function_call.lhs().type(), i_it->source_location);
190  }
191 
192  goto_programt::targett t_a = goto_program.insert_after(
193  i_it,
195  code_assignt(function_call.lhs(), rhs), i_it->source_location));
196 
197  // fry the previous assignment
198  function_call.lhs().make_nil();
199 
200  if(!is_stub)
201  {
202  goto_program.insert_after(
203  t_a,
204  goto_programt::make_dead(*return_value, i_it->source_location));
205  }
206 
207  // update the call
208  i_it->set_function_call(function_call);
209 
210  requires_update = true;
211  }
212  }
213  }
214 
215  return requires_update;
216 }
217 
219 {
220  Forall_goto_functions(it, goto_functions)
221  {
222  // NOLINTNEXTLINE
223  auto function_is_stub = [&goto_functions](const irep_idt &function_id) {
224  auto findit = goto_functions.function_map.find(function_id);
225  INVARIANT(
226  findit != goto_functions.function_map.end(),
227  "called function `" + id2string(function_id) +
228  "' should have an entry in the function map");
229  return !findit->second.body_available();
230  };
231 
232  replace_returns(it->first, it->second);
233  if(do_function_calls(function_is_stub, it->second.body))
234  goto_functions.compute_location_numbers(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  if(do_function_calls(function_is_stub, goto_function.body))
252  model_function.compute_location_numbers();
253 }
254 
257  symbol_table_baset &symbol_table,
258  goto_functionst &goto_functions)
259 {
260  remove_returnst rr(symbol_table);
261  rr(goto_functions);
262 }
263 
276  goto_model_functiont &goto_model_function,
277  function_is_stubt function_is_stub)
278 {
279  remove_returnst rr(goto_model_function.get_symbol_table());
280  rr(goto_model_function, function_is_stub);
281 }
282 
284 void remove_returns(goto_modelt &goto_model)
285 {
286  remove_returnst rr(goto_model.symbol_table);
287  rr(goto_model.goto_functions);
288 }
289 
292  goto_functionst::function_mapt::iterator f_it)
293 {
294  const irep_idt function_id=f_it->first;
295 
296  // do we have X#return_value?
297  auto rv_name = return_value_identifier(function_id);
298  symbol_tablet::symbolst::const_iterator rv_it=
299  symbol_table.symbols.find(rv_name);
300  if(rv_it==symbol_table.symbols.end())
301  return true;
302 
303  // remove the return_value symbol from the symbol_table
304  irep_idt rv_name_id=rv_it->second.name;
305  symbol_table.erase(rv_it);
306 
307  goto_programt &goto_program=f_it->second.body;
308 
309  bool did_something = false;
310 
311  Forall_goto_program_instructions(i_it, goto_program)
312  {
313  if(i_it->is_assign())
314  {
315  const auto &assign = i_it->get_assign();
316 
317  if(assign.lhs().id()!=ID_symbol ||
318  to_symbol_expr(assign.lhs()).get_identifier()!=rv_name_id)
319  continue;
320 
321  // replace "fkt#return_value=x;" by "return x;"
322  const exprt rhs = assign.rhs();
323  *i_it =
325  did_something = true;
326  }
327  }
328 
329  if(did_something)
330  remove_skip(goto_program);
331 
332  return false;
333 }
334 
337  goto_programt &goto_program)
338 {
340 
341  Forall_goto_program_instructions(i_it, goto_program)
342  {
343  if(i_it->is_function_call())
344  {
345  code_function_callt function_call = i_it->get_function_call();
346 
347  // ignore function pointers
348  if(function_call.function().id()!=ID_symbol)
349  continue;
350 
351  const irep_idt function_id=
352  to_symbol_expr(function_call.function()).get_identifier();
353 
354  // find "f(...); lhs=f#return_value; DEAD f#return_value;"
355  // and revert to "lhs=f(...);"
356  goto_programt::instructionst::iterator next = std::next(i_it);
357 
358  INVARIANT(
359  next!=goto_program.instructions.end(),
360  "non-void function call must be followed by #return_value read");
361 
362  if(!next->is_assign())
363  continue;
364 
365  const code_assignt &assign = next->get_assign();
366 
367  const auto rv_symbol = return_value_symbol(function_id, ns);
368  if(assign.rhs() != rv_symbol)
369  continue;
370 
371  // restore the previous assignment
372  function_call.lhs()=assign.lhs();
373 
374  i_it->set_function_call(function_call);
375 
376  // remove the assignment and subsequent dead
377  // i_it remains valid
378  next=goto_program.instructions.erase(next);
379  INVARIANT(
380  next!=goto_program.instructions.end() && next->is_dead(),
381  "read from #return_value should be followed by DEAD #return_value");
382  // i_it remains valid
383  goto_program.instructions.erase(next);
384  }
385  }
386 }
387 
389 {
390  // restore all types first
391  bool unmodified=true;
392  Forall_goto_functions(it, goto_functions)
393  unmodified=restore_returns(it) && unmodified;
394 
395  if(!unmodified)
396  {
397  Forall_goto_functions(it, goto_functions)
398  undo_function_calls(it->second.body);
399  }
400 }
401 
403 void restore_returns(goto_modelt &goto_model)
404 {
405  remove_returnst rr(goto_model.symbol_table);
406  rr.restore(goto_model.goto_functions);
407 }
408 
410 {
411  return id2string(identifier) + RETURN_VALUE_SUFFIX;
412 }
413 
415 return_value_symbol(const irep_idt &identifier, const namespacet &ns)
416 {
417  const symbolt &function_symbol = ns.lookup(identifier);
418  const typet &return_type = to_code_type(function_symbol.type).return_type();
419  return symbol_exprt(return_value_identifier(identifier), return_type);
420 }
421 
423 {
425 }
426 
427 bool is_return_value_symbol(const symbol_exprt &symbol_expr)
428 {
429  return is_return_value_identifier(symbol_expr.get_identifier());
430 }
431 
433 {
434  return to_code_type(function_call.function().type()).return_type() !=
435  empty_typet() &&
436  function_call.lhs().is_not_nil();
437 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
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:104
remove_returnst::restore
void restore(goto_functionst &goto_functions)
Definition: remove_returns.cpp:388
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
irept::make_nil
void make_nil()
Definition: irep.h:475
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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:85
goto_model_functiont::get_function_id
const irep_idt & get_function_id()
Get function id.
Definition: goto_model.h:232
goto_model.h
Symbol Table + CFG.
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
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:88
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
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:82
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
is_return_value_identifier
bool is_return_value_identifier(const irep_idt &id)
Returns true if id is a special return-value symbol produced by return_value_identifier.
Definition: remove_returns.cpp:422
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:336
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
RETURN_VALUE_SUFFIX
#define RETURN_VALUE_SUFFIX
Definition: remove_returns.cpp:23
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
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:28
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
does_function_call_return
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
Definition: remove_returns.cpp:432
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
is_return_value_symbol
bool is_return_value_symbol(const symbol_exprt &symbol_expr)
Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol.
Definition: remove_returns.cpp:427
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:291
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
goto_model_functiont::get_symbol_table
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition: goto_model.h:218
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_model_functiont::compute_location_numbers
void compute_location_numbers()
Re-number our goto_function.
Definition: goto_model.h:209
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
remove_returns.h
Replace function returns by assignments to global variables.
remove_returnst::symbol_table
symbol_table_baset & symbol_table
Definition: remove_returns.cpp:44
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:838
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
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:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
return_value_identifier
irep_idt return_value_identifier(const irep_idt &identifier)
produces the identifier that is used to store the return value of the function with the given identif...
Definition: remove_returns.cpp:409
remove_returnst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_returns.cpp:218
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
suffix.h
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
remove_returns
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: remove_returns.cpp:256
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:73
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:655
return_value_symbol
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
Definition: remove_returns.cpp:415
remove_returnst::get_or_create_return_value_symbol
optionalt< symbol_exprt > get_or_create_return_value_symbol(const irep_idt &function_id)
Definition: remove_returns.cpp:65
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
remove_returnst
Definition: remove_returns.cpp:26
goto_model_functiont::get_goto_function
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition: goto_model.h:225
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
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:100
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:183
restore_returns
void restore_returns(goto_modelt &goto_model)
restores return statements
Definition: remove_returns.cpp:403
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
validation_modet::INVARIANT
@ INVARIANT
remove_returnst::do_function_calls
bool 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:144