Skip to content

remove_returns now preserves signature #4266

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 14, 2019
Merged

remove_returns now preserves signature #4266

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2089,16 +2089,14 @@ void java_bytecode_convert_methodt::convert_invoke(
// less accurate.
if(method_symbol != symbol_table.symbols.end())
{
const auto &restored_type =
original_return_type(symbol_table, invoked_method_id);
// Note the number of parameters might change here due to constructors using
// invokespecial will have zero arguments (the `this` is added below)
// but the symbol for the <init> will have the this parameter.
INVARIANT(
to_java_method_type(arg0.type()).return_type().id() ==
restored_type.return_type().id(),
to_code_type(method_symbol->second.type).return_type().id(),
"Function return type must not change in kind");
arg0.type() = restored_type;
arg0.type() = method_symbol->second.type;
}

// Note arg0 and arg0.type() are subject to many side-effects in this method,
Expand Down
5 changes: 2 additions & 3 deletions src/goto-checker/symex_coverage.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,9 +160,8 @@ goto_program_coverage_recordt::goto_program_coverage_recordt(
// </method>
xml.set_attribute("name", id2string(gf_it->first));

code_typet sig_type =
original_return_type(ns.get_symbol_table(), gf_it->first);
xml.set_attribute("signature", from_type(ns, gf_it->first, sig_type));
xml.set_attribute(
"signature", from_type(ns, gf_it->first, gf_it->second.type));

xml.set_attribute("line-rate", rate_detailed(lines_covered, lines_total));
xml.set_attribute("branch-rate", rate(branches_covered, branches_total));
Expand Down
45 changes: 16 additions & 29 deletions src/goto-programs/goto_program.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -713,37 +713,24 @@ void goto_programt::instructiont::validate(
!symbol_expr_type_matches_symbol_table &&
table_symbol->type.id() == ID_code)
{
// Return removal sets the return type of a function symbol table
// entry to 'void', but some callsites still expect the original
// type (e.g. if a function is passed as a parameter)
symbol_expr_type_matches_symbol_table =
goto_symbol_expr.type() ==
original_return_type(ns.get_symbol_table(), goto_id);

// If a function declaration and its definition are in different
// translation units they may have different return types.
// Thus, the return type in the symbol table may differ
// from the return type in the symbol expr.
if(
!symbol_expr_type_matches_symbol_table &&
goto_symbol_expr.type().id() == ID_code)
goto_symbol_expr.type().source_location().get_file() !=
table_symbol->type.source_location().get_file())
{
// If a function declaration and its definition are in different
// translation units they may have different return types,
// which remove_returns patches up with a typecast. If thats
// the case, then the return type in the symbol table may differ
// from the return type in the symbol expr
if(
goto_symbol_expr.type().source_location().get_file() !=
table_symbol->type.source_location().get_file())
{
// temporarily fixup the return types
auto goto_symbol_expr_type =
to_code_type(goto_symbol_expr.type());
auto table_symbol_type = to_code_type(table_symbol->type);

goto_symbol_expr_type.return_type() =
table_symbol_type.return_type();

symbol_expr_type_matches_symbol_table =
base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
}
// temporarily fixup the return types
auto goto_symbol_expr_type =
to_code_type(goto_symbol_expr.type());
auto table_symbol_type = to_code_type(table_symbol->type);

goto_symbol_expr_type.return_type() =
table_symbol_type.return_type();

symbol_expr_type_matches_symbol_table =
base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
}
}

Expand Down
140 changes: 39 additions & 101 deletions src/goto-programs/remove_returns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,13 +106,6 @@ void remove_returnst::replace_returns(
// add return_value symbol to symbol_table, if not already created:
const auto return_symbol = get_or_create_return_value_symbol(function_id);

// look up the function symbol
symbolt &function_symbol = *symbol_table.get_writeable(function_id);

// make the return type 'void'
function.type.return_type() = empty_typet();
function_symbol.type = function.type;

goto_programt &goto_program = function.body;

Forall_goto_program_instructions(i_it, goto_program)
Expand Down Expand Up @@ -164,73 +157,56 @@ bool remove_returnst::do_function_calls(
const irep_idt function_id =
to_symbol_expr(function_call.function()).get_identifier();

optionalt<symbol_exprt> return_value;
typet old_return_type;
bool is_stub = function_is_stub(function_id);

if(is_stub)
{
old_return_type =
to_code_type(function_call.function().type()).return_type();
}
else
{
// The callee may or may not already have been transformed by this pass,
// so its symbol-table entry may already have void return type.
// To simplify matters, create its return-value global now (if not
// already done), and use that to determine its true return type.
return_value = get_or_create_return_value_symbol(function_id);
if(!return_value.has_value()) // really void-typed?
continue;
old_return_type = return_value->type();
}

// Do we return anything?
if(old_return_type != empty_typet())
if(
to_code_type(function_call.function().type()).return_type() !=
empty_typet() &&
function_call.lhs().is_not_nil())
{
// replace "lhs=f(...)" by
// "f(...); lhs=f#return_value; DEAD f#return_value;"

// fix the type
to_code_type(function_call.function().type()).return_type()=
empty_typet();
exprt rhs;

bool is_stub = function_is_stub(function_id);
optionalt<symbol_exprt> return_value;

if(!is_stub)
{
return_value = get_or_create_return_value_symbol(function_id);
CHECK_RETURN(return_value.has_value());

// The return type in the definition of the function may differ
// from the return type in the declaration. We therefore do a
// cast.
rhs = typecast_exprt::conditional_cast(
*return_value, function_call.lhs().type());
}
else
{
rhs = side_effect_expr_nondett(
function_call.lhs().type(), i_it->source_location);
}

goto_programt::targett t_a = goto_program.insert_after(
i_it,
goto_programt::make_assignment(
code_assignt(function_call.lhs(), rhs), i_it->source_location));

// fry the previous assignment
function_call.lhs().make_nil();

if(function_call.lhs().is_not_nil())
if(!is_stub)
{
exprt rhs;

if(!is_stub)
{
// The return type in the definition of the function may differ
// from the return type in the declaration. We therefore do a
// cast.
rhs = typecast_exprt::conditional_cast(
*return_value, function_call.lhs().type());
}
else
rhs = side_effect_expr_nondett(
function_call.lhs().type(), i_it->source_location);

goto_programt::targett t_a = goto_program.insert_after(
i_it,
goto_programt::make_assignment(
code_assignt(function_call.lhs(), rhs), i_it->source_location));

// fry the previous assignment
function_call.lhs().make_nil();

if(!is_stub)
{
goto_program.insert_after(
t_a,
goto_programt::make_dead(*return_value, i_it->source_location));
}

requires_update = true;
goto_program.insert_after(
t_a,
goto_programt::make_dead(*return_value, i_it->source_location));
}

// update the call
i_it->set_function_call(function_call);

requires_update = true;
}
}
}
Expand Down Expand Up @@ -309,31 +285,6 @@ void remove_returns(goto_modelt &goto_model)
rr(goto_model.goto_functions);
}

/// Get code type of a function that has had remove_returns run upon it
/// \param symbol_table: global symbol table
/// \param function_id: function to get the type of
/// \return the function's type with its `return_type()` restored to its
/// original value
code_typet original_return_type(
const symbol_table_baset &symbol_table,
const irep_idt &function_id)
{
// look up the function symbol
const symbolt &function_symbol = symbol_table.lookup_ref(function_id);
code_typet type = to_code_type(function_symbol.type);

// do we have X#return_value?
std::string rv_name=id2string(function_id)+RETURN_VALUE_SUFFIX;

symbol_tablet::symbolst::const_iterator rv_it=
symbol_table.symbols.find(rv_name);

if(rv_it != symbol_table.symbols.end())
type.return_type() = rv_it->second.type;

return type;
}

/// turns an assignment to fkt#return_value back into 'return x'
bool remove_returnst::restore_returns(
goto_functionst::function_mapt::iterator f_it)
Expand All @@ -349,13 +300,6 @@ bool remove_returnst::restore_returns(
if(rv_it==symbol_table.symbols.end())
return true;

// look up the function symbol
symbolt &function_symbol=*symbol_table.get_writeable(function_id);

// restore the return type
f_it->second.type=original_return_type(symbol_table, function_id);
function_symbol.type=f_it->second.type;

// remove the return_value symbol from the symbol_table
irep_idt rv_name_id=rv_it->second.name;
symbol_table.erase(rv_it);
Expand Down Expand Up @@ -407,12 +351,6 @@ void remove_returnst::undo_function_calls(
const irep_idt function_id=
to_symbol_expr(function_call.function()).get_identifier();

const symbolt &function_symbol=ns.lookup(function_id);

// fix the type
to_code_type(function_call.function().type()).return_type()=
to_code_type(function_symbol.type).return_type();

// find "f(...); lhs=f#return_value; DEAD f#return_value;"
// and revert to "lhs=f(...);"
goto_programt::instructionst::iterator next = std::next(i_it);
Expand Down
17 changes: 1 addition & 16 deletions src/goto-programs/remove_returns.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,18 +66,7 @@ Date: September 2009
/// 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.
/// `remove_returns()` does not change the signature of the function.

#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
#define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
Expand Down Expand Up @@ -106,8 +95,4 @@ void restore_returns(symbol_table_baset &, goto_functionst &);

void restore_returns(goto_modelt &);

code_typet original_return_type(
const symbol_table_baset &symbol_table,
const irep_idt &function_id);

#endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
8 changes: 1 addition & 7 deletions src/goto-programs/validate_goto_model.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,13 +133,7 @@ void validate_goto_modelt::check_returns_removed()
DATA_CHECK(
vm,
function_call.lhs().is_nil(),
"function call return should be nil");

const auto &callee = to_code_type(function_call.function().type());
DATA_CHECK(
vm,
callee.return_type().id() == ID_empty,
"called function must have empty return type");
"function call lhs return should be nil");
}
}
}
Expand Down