diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp index bdb2ca18c60..2f32ad92991 100644 --- a/jbmc/src/java_bytecode/replace_java_nondet.cpp +++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp @@ -165,7 +165,7 @@ static bool is_return_with_variable( { return false; } - const auto &rhs = to_code_return(instr.code).return_value(); + const auto &rhs = instr.return_value(); return is_symbol_with_id(rhs, identifier) || is_typecast_with_id(rhs, identifier); } @@ -276,8 +276,7 @@ static goto_programt::targett check_and_replace_target( if(target_instruction->is_return()) { - const auto &nondet_var = - to_code_return(target_instruction->code).return_value(); + const auto &nondet_var = target_instruction->return_value(); side_effect_expr_nondett inserted_expr( nondet_var.type(), target_instruction->source_location); diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp index 872066ded25..5bbd9054246 100644 --- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp +++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp @@ -54,11 +54,10 @@ void validate_nondet_method_removed( if(inst.is_return()) { - const code_returnt &ret_expr = to_code_return(inst.code); - if(ret_expr.return_value().id() == ID_side_effect) + const auto &return_value = inst.return_value(); + if(return_value.id() == ID_side_effect) { - const side_effect_exprt &see = - to_side_effect_expr(ret_expr.return_value()); + const side_effect_exprt &see = to_side_effect_expr(return_value); if(see.get_statement() == ID_nondet) { replacement_nondet_exists = true; diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 28b89fbc6ef..22b0b58d573 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -2013,22 +2013,18 @@ void goto_checkt::goto_check( } else if(i.is_return()) { - if(i.code.operands().size()==1) + check(i.return_value()); + // the return value invalidate any assertion + invalidate(i.return_value()); + + if(has_subexpr(i.return_value(), [](const exprt &expr) { + return expr.id() == ID_r_ok || expr.id() == ID_w_ok; + })) { - const code_returnt &code_return = to_code_return(i.code); - check(code_return.return_value()); - // the return value invalidate any assertion - invalidate(code_return.return_value()); - - if(has_subexpr(code_return.return_value(), [](const exprt &expr) { - return expr.id() == ID_r_ok || expr.id() == ID_w_ok; - })) - { - exprt &return_value = to_code_return(i.code).return_value(); - auto rw_ok_cond = rw_ok_check(return_value); - if(rw_ok_cond.has_value()) - return_value = *rw_ok_cond; - } + exprt &return_value = i.return_value(); + auto rw_ok_cond = rw_ok_check(return_value); + if(rw_ok_cond.has_value()) + return_value = *rw_ok_cond; } } else if(i.is_throw()) diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 056564e221e..88ea9b54137 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -775,16 +775,8 @@ void goto_rw( break; case RETURN: - { - const code_returnt &code_return= - to_code_return(target->code); - if(code_return.has_return_value()) - rw_set.get_objects_rec( - function, - target, - rw_range_sett::get_modet::READ, - code_return.return_value()); - } + rw_set.get_objects_rec( + function, target, rw_range_sett::get_modet::READ, target->return_value()); break; case OTHER: diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 379414c0bb3..52b85923982 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -418,14 +418,12 @@ goto_programt::const_targett goto_program2codet::convert_return( goto_programt::const_targett upper_bound, code_blockt &dest) { - const code_returnt &ret = target->get_return(); - // add return instruction unless original code was missing a return - if(!ret.has_return_value() || - ret.return_value().id()!=ID_side_effect || - to_side_effect_expr(ret.return_value()).get_statement()!=ID_nondet) + if( + target->return_value().id() != ID_side_effect || + to_side_effect_expr(target->return_value()).get_statement() != ID_nondet) { - dest.add(ret); + dest.add(code_returnt{target->return_value()}); } // all v3 (or later) goto programs have an explicit GOTO after return diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 6bce8790bdc..e559c887861 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -165,31 +165,20 @@ void goto_inlinet::replace_return( { if(it->is_return()) { - const auto &code_return = it->get_return(); - if(lhs.is_not_nil()) { - if(!code_return.has_return_value()) - { - log.warning().source_location = it->code.find_source_location(); - log.warning() << "return expects one operand!\n" - << it->code.pretty() << messaget::eom; - continue; - } - // a typecast may be necessary if the declared return type at the call // site differs from the defined return type it->code = code_assignt( lhs, - typecast_exprt::conditional_cast( - code_return.return_value(), lhs.type())); + typecast_exprt::conditional_cast(it->return_value(), lhs.type())); it->type=ASSIGN; it++; } - else if(code_return.has_return_value()) + else { - it->code = code_expressiont(code_return.return_value()); + it->code = code_expressiont(it->return_value()); it->type=OTHER; it++; } diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index c74bad5cd0b..13954fa927d 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -285,8 +285,7 @@ std::list expressions_read( break; case RETURN: - if(instruction.get_return().return_value().is_not_nil()) - dest.push_back(instruction.get_return().return_value()); + dest.push_back(instruction.return_value()); break; case FUNCTION_CALL: @@ -928,13 +927,9 @@ void goto_programt::instructiont::transform( case RETURN: { - auto new_return_value = f(get_return().return_value()); + auto new_return_value = f(return_value()); if(new_return_value.has_value()) - { - auto new_return = get_return(); - new_return.return_value() = *new_return_value; - set_return(new_return); - } + return_value() = *new_return_value; } break; @@ -1037,7 +1032,7 @@ void goto_programt::instructiont::apply( break; case RETURN: - f(get_return().return_value()); + f(return_value()); break; case ASSIGN: diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b461b7f0c6f..566fc7c554e 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -232,13 +233,29 @@ class goto_programt } /// Get the return statement for READ + DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead")) const code_returnt &get_return() const { PRECONDITION(is_return()); return to_code_return(code); } + /// Get the return value of a RETURN instruction + const exprt &return_value() const + { + PRECONDITION(is_return()); + return to_code_return(code).return_value(); + } + + /// Get the return value of a RETURN instruction + exprt &return_value() + { + PRECONDITION(is_return()); + return to_code_return(code).return_value(); + } + /// Set the return statement for READ + DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead")) void set_return(code_returnt c) { PRECONDITION(is_return()); diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 2a2ebacf83b..606b35803f4 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -300,11 +300,10 @@ void interpretert::step() if(call_stack.empty()) throw "RETURN without call"; // NOLINT(readability/throw) - if(pc->code.operands().size()==1 && - call_stack.top().return_value_address!=0) + if(call_stack.top().return_value_address != 0) { mp_vectort rhs; - evaluate(pc->code.op0(), rhs); + evaluate(pc->return_value(), rhs); assign(call_stack.top().return_value_address, rhs); } diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 5470e41bc47..ce68db56696 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -228,13 +228,7 @@ void goto_program_dereferencet::dereference_instruction( } else if(i.is_return()) { - auto r = i.get_return(); - - if(r.return_value().is_not_nil()) - { - dereference_expr(r.return_value(), checks_only); - i.set_return(r); - } + dereference_expr(i.return_value(), checks_only); } else if(i.is_other()) {