cprover
remove_returns.h File Reference

Replace function returns by assignments to global variables. More...

#include <functional>
#include <util/std_types.h>
+ Include dependency graph for remove_returns.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define RETURN_VALUE_SUFFIX   "#return_value"
 The functions remove_returns() remove return instructions from a goto program. More...
 

Typedefs

typedef std::function< bool(const irep_idt &)> function_is_stubt
 

Functions

void remove_returns (symbol_table_baset &, goto_functionst &)
 removes returns More...
 
void remove_returns (goto_model_functiont &, function_is_stubt)
 Removes returns from a single function. More...
 
void remove_returns (goto_modelt &)
 removes returns More...
 
void restore_returns (symbol_table_baset &, goto_functionst &)
 
void restore_returns (goto_modelt &)
 restores return statements More...
 
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. More...
 

Detailed Description

Replace function returns by assignments to global variables.

Definition in file remove_returns.h.

Macro Definition Documentation

◆ RETURN_VALUE_SUFFIX

#define RETURN_VALUE_SUFFIX   "#return_value"

The functions remove_returns() remove return instructions from a goto program.

The restore_returns() functions restore the returns in a goto program in which they have been removed previously.

In a goto program in which returns have not been removed, functions return values via the return instruction, which is followed by a GOTO to the end of the function. Unlike in C, in a goto program the return instruction does not cause control-flow to return to the call site. Instead, it simply sets the return value that will be returned once the function returns to the call site when the END_FUNCTION instruction is encountered.

Consider the following C code (with ... indicating further code):

int func()
{
...
return 1;
...
}
r = func();

This code would appear in a goto program as follows:

func
...
return 1;
GOTO 1
...
r = func();

The return removal pass introduces a thread-local global variable func::return_value (one for each non-void function) to which the return value is assigned, and this variable is then assigned to the lhs expression that takes the function return value:

func
...
func#return_value = 1;
GOTO 1
...
func();
r = func#return_value;

As return instructions are removed, the return types of the function types are set to void as well (represented by the type empty_typet). This applies both to the functions (i.e., the member type of goto_functiont) and to the call sites (i.e., the type to_code_function_call(code).function().type() with code being the code member of the instructiont instance that represents the function call).

The types of function pointer expressions in the goto program are however not changed. For example, in an assignment where func is assigned to a function pointer, such as int (*f)(void) = func, the function types appearing in the lhs and rhs both retain the integer return type.

Definition at line 89 of file remove_returns.h.

Typedef Documentation

◆ function_is_stubt

typedef std::function<bool(const irep_idt &)> function_is_stubt

Definition at line 98 of file remove_returns.h.

Function Documentation

◆ 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.

Parameters
symbol_tableglobal symbol table
function_idfunction to get the type of
Returns
the function's type with its return_type() restored to its original value

Definition at line 307 of file remove_returns.cpp.

◆ remove_returns() [1/3]

void remove_returns ( symbol_table_baset ,
goto_functionst  
)

removes returns

Definition at line 268 of file remove_returns.cpp.

◆ remove_returns() [2/3]

void remove_returns ( goto_model_functiont goto_model_function,
function_is_stubt  function_is_stub 
)

Removes returns from a single function.

Only usable with Java programs at the moment; to use it with other languages, they must annotate their stub functions with ID_C_incomplete as currently done in java_bytecode_convert_method.cpp.

This will generate #return_value variables, if not already present, for both the function being altered and any callees.

Parameters
goto_model_functionfunction to transform
function_is_stubfunction that will be used to test whether a given callee has been or will be given a body. It should return true if so, or false if the function will remain a bodyless stub.

Definition at line 287 of file remove_returns.cpp.

◆ remove_returns() [3/3]

void remove_returns ( goto_modelt )

removes returns

Definition at line 296 of file remove_returns.cpp.

◆ restore_returns() [1/2]

void restore_returns ( symbol_table_baset ,
goto_functionst  
)

◆ restore_returns() [2/2]

void restore_returns ( goto_modelt )

restores return statements

Definition at line 459 of file remove_returns.cpp.