cprover
Loading...
Searching...
No Matches
remove_returns.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove function return values
4
5Author: Daniel Kroening
6
7Date: September 2009
8
9\*******************************************************************/
10
13
14#include "remove_returns.h"
15
16#include <util/std_code.h>
17#include <util/std_expr.h>
18#include <util/suffix.h>
19
20#include "goto_model.h"
21
22#include "remove_skip.h"
23
24#define RETURN_VALUE_SUFFIX "#return_value"
25
27{
28public:
29 explicit remove_returnst(symbol_table_baset &_symbol_table):
30 symbol_table(_symbol_table)
31 {
32 }
33
34 void operator()(
35 goto_functionst &goto_functions);
36
37 void operator()(
38 goto_model_functiont &model_function,
39 function_is_stubt function_is_stub);
40
41 void restore(
42 goto_functionst &goto_functions);
43
44protected:
46
47 void replace_returns(
48 const irep_idt &function_id,
50
52 function_is_stubt function_is_stub,
53 goto_programt &goto_program);
54
55 bool
56 restore_returns(const irep_idt &function_id, goto_programt &goto_program);
57
59 goto_programt &goto_program);
60
63};
64
67{
68 const namespacet ns(symbol_table);
69 const auto symbol_expr = return_value_symbol(function_id, ns);
70 const auto symbol_name = symbol_expr.get_identifier();
71 if(symbol_table.has_symbol(symbol_name))
72 return symbol_expr;
73
74 const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
75 const typet &return_type = to_code_type(function_symbol.type).return_type();
76
77 if(return_type == empty_typet())
78 return {};
79
80 auxiliary_symbolt new_symbol;
81 new_symbol.is_static_lifetime = true;
82 new_symbol.module = function_symbol.module;
83 new_symbol.base_name =
84 id2string(function_symbol.base_name) + RETURN_VALUE_SUFFIX;
85 new_symbol.name = symbol_name;
86 new_symbol.mode = function_symbol.mode;
87 // If we're creating this for the first time, the target function cannot have
88 // been remove_return'd yet, so this will still be the "true" return type:
89 new_symbol.type = return_type;
90 // Return-value symbols will always be written before they are read, so there
91 // is no need for __CPROVER_initialize to do anything:
92 new_symbol.type.set(ID_C_no_initialization_required, true);
93
94 symbol_table.add(new_symbol);
95 return new_symbol.symbol_expr();
96}
97
102 const irep_idt &function_id,
104{
105 // look up the function symbol
106 symbolt &function_symbol = *symbol_table.get_writeable(function_id);
107
108 // returns something but void?
109 if(to_code_type(function_symbol.type).return_type() == empty_typet())
110 return;
111
112 // add return_value symbol to symbol_table, if not already created:
113 const auto return_symbol = get_or_create_return_value_symbol(function_id);
114
115 goto_programt &goto_program = function.body;
116
117 for(auto &instruction : goto_program.instructions)
118 {
119 if(instruction.is_set_return_value())
120 {
121 INVARIANT(
122 instruction.get_code().operands().size() == 1,
123 "return instructions should have one operand");
124
125 if(return_symbol.has_value())
126 {
127 // replace "return x;" by "fkt#return_value=x;"
128 code_assignt assignment(*return_symbol, instruction.return_value());
129
130 // now turn the `return' into `assignment'
131 auto labels = std::move(instruction.labels);
132 instruction = goto_programt::make_assignment(
133 assignment, instruction.source_location());
134 instruction.labels = std::move(labels);
135 }
136 else
137 instruction.turn_into_skip();
138 }
139 }
140}
141
149 function_is_stubt function_is_stub,
150 goto_programt &goto_program)
151{
152 bool requires_update = false;
153
154 Forall_goto_program_instructions(i_it, goto_program)
155 {
156 if(i_it->is_function_call())
157 {
158 INVARIANT(
159 i_it->call_function().id() == ID_symbol,
160 "indirect function calls should have been removed prior to running "
161 "remove-returns");
162
163 const irep_idt function_id =
164 to_symbol_expr(i_it->call_function()).get_identifier();
165
166 // Do we return anything?
168 {
169 // replace "lhs=f(...)" by
170 // "f(...); lhs=f#return_value; DEAD f#return_value;"
171
172 exprt rhs;
173
174 bool is_stub = function_is_stub(function_id);
175 optionalt<symbol_exprt> return_value;
176
177 if(!is_stub)
178 {
179 return_value = get_or_create_return_value_symbol(function_id);
180 CHECK_RETURN(return_value.has_value());
181
182 // The return type in the definition of the function may differ
183 // from the return type in the declaration. We therefore do a
184 // cast.
186 *return_value, i_it->call_lhs().type());
187 }
188 else
189 {
191 i_it->call_lhs().type(), i_it->source_location());
192 }
193
194 goto_programt::targett t_a = goto_program.insert_after(
195 i_it,
197 code_assignt(i_it->call_lhs(), rhs), i_it->source_location()));
198
199 // fry the previous assignment
200 i_it->call_lhs().make_nil();
201
202 if(!is_stub)
203 {
204 goto_program.insert_after(
205 t_a,
206 goto_programt::make_dead(*return_value, i_it->source_location()));
207 }
208
209 requires_update = true;
210 }
211 }
212 }
213
214 return requires_update;
215}
216
218{
219 for(auto &gf_entry : goto_functions.function_map)
220 {
221 // NOLINTNEXTLINE
222 auto function_is_stub = [&goto_functions](const irep_idt &function_id) {
223 auto findit = goto_functions.function_map.find(function_id);
224 INVARIANT(
225 findit != goto_functions.function_map.end(),
226 "called function `" + id2string(function_id) +
227 "' should have an entry in the function map");
228 return !findit->second.body_available();
229 };
230
231 replace_returns(gf_entry.first, gf_entry.second);
232 if(do_function_calls(function_is_stub, gf_entry.second.body))
233 goto_functions.compute_location_numbers(gf_entry.second.body);
234 }
235}
236
238 goto_model_functiont &model_function,
239 function_is_stubt function_is_stub)
240{
241 goto_functionst::goto_functiont &goto_function =
242 model_function.get_goto_function();
243
244 // If this is a stub it doesn't have a corresponding #return_value,
245 // not any return instructions to alter:
246 if(goto_function.body.empty())
247 return;
248
249 replace_returns(model_function.get_function_id(), goto_function);
250 if(do_function_calls(function_is_stub, goto_function.body))
251 model_function.compute_location_numbers();
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
284{
285 remove_returnst rr(goto_model.symbol_table);
286 rr(goto_model.goto_functions);
287}
288
291 const irep_idt &function_id,
292 goto_programt &goto_program)
293{
294 // do we have X#return_value?
295 auto rv_name = return_value_identifier(function_id);
296 symbol_tablet::symbolst::const_iterator rv_it=
297 symbol_table.symbols.find(rv_name);
298 if(rv_it==symbol_table.symbols.end())
299 return true;
300
301 // remove the return_value symbol from the symbol_table
302 irep_idt rv_name_id=rv_it->second.name;
303 symbol_table.erase(rv_it);
304
305 bool did_something = false;
306
307 for(auto &instruction : goto_program.instructions)
308 {
309 if(instruction.is_assign())
310 {
311 if(
312 instruction.assign_lhs().id() != ID_symbol ||
313 to_symbol_expr(instruction.assign_lhs()).get_identifier() != rv_name_id)
314 {
315 continue;
316 }
317
318 // replace "fkt#return_value=x;" by "return x;"
319 const exprt rhs = instruction.assign_rhs();
321 rhs, instruction.source_location());
322 did_something = true;
323 }
324 }
325
326 if(did_something)
327 remove_skip(goto_program);
328
329 return false;
330}
331
334 goto_programt &goto_program)
335{
337
338 Forall_goto_program_instructions(i_it, goto_program)
339 {
340 if(i_it->is_function_call())
341 {
342 // ignore function pointers
343 if(i_it->call_function().id() != ID_symbol)
344 continue;
345
346 const irep_idt function_id =
347 to_symbol_expr(i_it->call_function()).get_identifier();
348
349 // find "f(...); lhs=f#return_value; DEAD f#return_value;"
350 // and revert to "lhs=f(...);"
351 goto_programt::instructionst::iterator next = std::next(i_it);
352
353 INVARIANT(
354 next!=goto_program.instructions.end(),
355 "non-void function call must be followed by #return_value read");
356
357 if(!next->is_assign())
358 continue;
359
360 const auto rv_symbol = return_value_symbol(function_id, ns);
361 if(next->assign_rhs() != rv_symbol)
362 continue;
363
364 // restore the previous assignment
365 i_it->call_lhs() = next->assign_lhs();
366
367 // remove the assignment and subsequent dead
368 // i_it remains valid
369 next=goto_program.instructions.erase(next);
370 INVARIANT(
371 next!=goto_program.instructions.end() && next->is_dead(),
372 "read from #return_value should be followed by DEAD #return_value");
373 // i_it remains valid
374 goto_program.instructions.erase(next);
375 }
376 }
377}
378
380{
381 // restore all types first
382 bool unmodified=true;
383 for(auto &gf_entry : goto_functions.function_map)
384 {
385 unmodified =
386 restore_returns(gf_entry.first, gf_entry.second.body) && unmodified;
387 }
388
389 if(!unmodified)
390 {
391 for(auto &gf_entry : goto_functions.function_map)
392 undo_function_calls(gf_entry.second.body);
393 }
394}
395
398{
399 remove_returnst rr(goto_model.symbol_table);
400 rr.restore(goto_model.goto_functions);
401}
402
404{
405 return id2string(identifier) + RETURN_VALUE_SUFFIX;
406}
407
409return_value_symbol(const irep_idt &identifier, const namespacet &ns)
410{
411 const symbolt &function_symbol = ns.lookup(identifier);
412 const typet &return_type = to_code_type(function_symbol.type).return_type();
413 return symbol_exprt(return_value_identifier(identifier), return_type);
414}
415
417{
419}
420
421bool is_return_value_symbol(const symbol_exprt &symbol_expr)
422{
423 return is_return_value_identifier(symbol_expr.get_identifier());
424}
425
427{
428 return to_code_type(function_call.call_function().type()).return_type() !=
429 empty_typet() &&
430 function_call.call_lhs().is_not_nil();
431}
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:147
A codet representing an assignment in the program.
const typet & return_type() const
Definition std_types.h:645
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
void compute_location_numbers()
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:183
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:232
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:225
void compute_location_numbers()
Re-number our goto_function.
Definition goto_model.h:209
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:218
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool restore_returns(const irep_idt &function_id, goto_programt &goto_program)
turns an assignment to fkt::return_value back into 'return x'
void operator()(goto_functionst &goto_functions)
symbol_table_baset & symbol_table
optionalt< symbol_exprt > get_or_create_return_value_symbol(const irep_idt &function_id)
remove_returnst(symbol_table_baset &_symbol_table)
void undo_function_calls(goto_programt &goto_program)
turns f(...); lhs=f::return_value; into lhs=f(...)
void replace_returns(const irep_idt &function_id, goto_functionst::goto_functiont &function)
turns 'return x' into an assignment to fkt::return_value
void restore(goto_functionst &goto_functions)
bool do_function_calls(function_is_stubt function_is_stub, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The symbol table base class interface.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_static_lifetime
Definition symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt mode
Language mode.
Definition symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
nonstd::optional< T > optionalt
Definition optional.h:35
void restore_returns(goto_modelt &goto_model)
restores return statements
#define RETURN_VALUE_SUFFIX
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
bool is_return_value_identifier(const irep_idt &id)
Returns true if id is a special return-value symbol produced by return_value_identifier.
bool does_function_call_return(const goto_programt::instructiont &function_call)
Check if the function_call returns anything.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
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.
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...
Replace function returns by assignments to global variables.
std::function< bool(const irep_idt &)> function_is_stubt
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17