diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index bcbc97e4ae7..f7f64e3fe94 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -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 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, diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp index fd14f98ada4..e8db1b91788 100644 --- a/src/goto-checker/symex_coverage.cpp +++ b/src/goto-checker/symex_coverage.cpp @@ -160,9 +160,8 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( // 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)); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 491954821f9..0416af0bb25 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -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); } } diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 5eaef4d52e2..803295a33d3 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -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) @@ -164,73 +157,56 @@ bool remove_returnst::do_function_calls( const irep_idt function_id = to_symbol_expr(function_call.function()).get_identifier(); - optionalt 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 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; } } } @@ -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) @@ -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); @@ -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); diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index 2cf5a486ecc..a1c9636ce71 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -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 @@ -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 diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp index 2f3d42480e6..c5530182bcc 100644 --- a/src/goto-programs/validate_goto_model.cpp +++ b/src/goto-programs/validate_goto_model.cpp @@ -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"); } } }