Skip to content

Commit 0716bfd

Browse files
committed
introduce instructiont::return_value()
This mirrors the change in #5861 by replacing the use of code_returnt by directly returning the return value expression. The client code is simplified considerably.
1 parent a4c81ef commit 0716bfd

File tree

9 files changed

+47
-68
lines changed

9 files changed

+47
-68
lines changed

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,11 +54,10 @@ void validate_nondet_method_removed(
5454

5555
if(inst.is_return())
5656
{
57-
const code_returnt &ret_expr = to_code_return(inst.code);
58-
if(ret_expr.return_value().id() == ID_side_effect)
57+
const auto &return_value = inst.return_value();
58+
if(return_value.id() == ID_side_effect)
5959
{
60-
const side_effect_exprt &see =
61-
to_side_effect_expr(ret_expr.return_value());
60+
const side_effect_exprt &see = to_side_effect_expr(return_value);
6261
if(see.get_statement() == ID_nondet)
6362
{
6463
replacement_nondet_exists = true;

src/analyses/goto_check.cpp

Lines changed: 11 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2013,22 +2013,18 @@ void goto_checkt::goto_check(
20132013
}
20142014
else if(i.is_return())
20152015
{
2016-
if(i.code.operands().size()==1)
2016+
check(i.return_value());
2017+
// the return value invalidate any assertion
2018+
invalidate(i.return_value());
2019+
2020+
if(has_subexpr(i.return_value(), [](const exprt &expr) {
2021+
return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2022+
}))
20172023
{
2018-
const code_returnt &code_return = to_code_return(i.code);
2019-
check(code_return.return_value());
2020-
// the return value invalidate any assertion
2021-
invalidate(code_return.return_value());
2022-
2023-
if(has_subexpr(code_return.return_value(), [](const exprt &expr) {
2024-
return expr.id() == ID_r_ok || expr.id() == ID_w_ok;
2025-
}))
2026-
{
2027-
exprt &return_value = to_code_return(i.code).return_value();
2028-
auto rw_ok_cond = rw_ok_check(return_value);
2029-
if(rw_ok_cond.has_value())
2030-
return_value = *rw_ok_cond;
2031-
}
2024+
exprt &return_value = i.return_value();
2025+
auto rw_ok_cond = rw_ok_check(return_value);
2026+
if(rw_ok_cond.has_value())
2027+
return_value = *rw_ok_cond;
20322028
}
20332029
}
20342030
else if(i.is_throw())

src/analyses/goto_rw.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -775,16 +775,8 @@ void goto_rw(
775775
break;
776776

777777
case RETURN:
778-
{
779-
const code_returnt &code_return=
780-
to_code_return(target->code);
781-
if(code_return.has_return_value())
782-
rw_set.get_objects_rec(
783-
function,
784-
target,
785-
rw_range_sett::get_modet::READ,
786-
code_return.return_value());
787-
}
778+
rw_set.get_objects_rec(
779+
function, target, rw_range_sett::get_modet::READ, target->return_value());
788780
break;
789781

790782
case OTHER:

src/goto-instrument/goto_program2code.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -418,14 +418,12 @@ goto_programt::const_targett goto_program2codet::convert_return(
418418
goto_programt::const_targett upper_bound,
419419
code_blockt &dest)
420420
{
421-
const code_returnt &ret = target->get_return();
422-
423421
// add return instruction unless original code was missing a return
424-
if(!ret.has_return_value() ||
425-
ret.return_value().id()!=ID_side_effect ||
426-
to_side_effect_expr(ret.return_value()).get_statement()!=ID_nondet)
422+
if(
423+
target->return_value().id() != ID_side_effect ||
424+
to_side_effect_expr(target->return_value()).get_statement() != ID_nondet)
427425
{
428-
dest.add(ret);
426+
dest.add(code_returnt{target->return_value()});
429427
}
430428

431429
// all v3 (or later) goto programs have an explicit GOTO after return

src/goto-programs/goto_inline_class.cpp

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -165,31 +165,20 @@ void goto_inlinet::replace_return(
165165
{
166166
if(it->is_return())
167167
{
168-
const auto &code_return = it->get_return();
169-
170168
if(lhs.is_not_nil())
171169
{
172-
if(!code_return.has_return_value())
173-
{
174-
log.warning().source_location = it->code.find_source_location();
175-
log.warning() << "return expects one operand!\n"
176-
<< it->code.pretty() << messaget::eom;
177-
continue;
178-
}
179-
180170
// a typecast may be necessary if the declared return type at the call
181171
// site differs from the defined return type
182172
it->code = code_assignt(
183173
lhs,
184-
typecast_exprt::conditional_cast(
185-
code_return.return_value(), lhs.type()));
174+
typecast_exprt::conditional_cast(it->return_value(), lhs.type()));
186175
it->type=ASSIGN;
187176

188177
it++;
189178
}
190-
else if(code_return.has_return_value())
179+
else
191180
{
192-
it->code = code_expressiont(code_return.return_value());
181+
it->code = code_expressiont(it->return_value());
193182
it->type=OTHER;
194183
it++;
195184
}

src/goto-programs/goto_program.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -285,8 +285,7 @@ std::list<exprt> expressions_read(
285285
break;
286286

287287
case RETURN:
288-
if(instruction.get_return().return_value().is_not_nil())
289-
dest.push_back(instruction.get_return().return_value());
288+
dest.push_back(instruction.return_value());
290289
break;
291290

292291
case FUNCTION_CALL:
@@ -928,13 +927,9 @@ void goto_programt::instructiont::transform(
928927

929928
case RETURN:
930929
{
931-
auto new_return_value = f(get_return().return_value());
930+
auto new_return_value = f(return_value());
932931
if(new_return_value.has_value())
933-
{
934-
auto new_return = get_return();
935-
new_return.return_value() = *new_return_value;
936-
set_return(new_return);
937-
}
932+
return_value() = *new_return_value;
938933
}
939934
break;
940935

@@ -1037,7 +1032,7 @@ void goto_programt::instructiont::apply(
10371032
break;
10381033

10391034
case RETURN:
1040-
f(get_return().return_value());
1035+
f(return_value());
10411036
break;
10421037

10431038
case ASSIGN:

src/goto-programs/goto_program.h

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include <sstream>
1919
#include <string>
2020

21+
#include <util/deprecate.h>
2122
#include <util/invariant.h>
2223
#include <util/namespace.h>
2324
#include <util/source_location.h>
@@ -232,13 +233,29 @@ class goto_programt
232233
}
233234

234235
/// Get the return statement for READ
236+
DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
235237
const code_returnt &get_return() const
236238
{
237239
PRECONDITION(is_return());
238240
return to_code_return(code);
239241
}
240242

243+
/// Get the return value of a RETURN instruction
244+
const exprt &return_value() const
245+
{
246+
PRECONDITION(is_return());
247+
return to_code_return(code).return_value();
248+
}
249+
250+
/// Get the return value of a RETURN instruction
251+
exprt &return_value()
252+
{
253+
PRECONDITION(is_return());
254+
return to_code_return(code).return_value();
255+
}
256+
241257
/// Set the return statement for READ
258+
DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
242259
void set_return(code_returnt c)
243260
{
244261
PRECONDITION(is_return());

src/goto-programs/interpreter.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -300,11 +300,10 @@ void interpretert::step()
300300
if(call_stack.empty())
301301
throw "RETURN without call"; // NOLINT(readability/throw)
302302

303-
if(pc->code.operands().size()==1 &&
304-
call_stack.top().return_value_address!=0)
303+
if(call_stack.top().return_value_address != 0)
305304
{
306305
mp_vectort rhs;
307-
evaluate(pc->code.op0(), rhs);
306+
evaluate(pc->return_value(), rhs);
308307
assign(call_stack.top().return_value_address, rhs);
309308
}
310309

src/pointer-analysis/goto_program_dereference.cpp

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -228,13 +228,7 @@ void goto_program_dereferencet::dereference_instruction(
228228
}
229229
else if(i.is_return())
230230
{
231-
auto r = i.get_return();
232-
233-
if(r.return_value().is_not_nil())
234-
{
235-
dereference_expr(r.return_value(), checks_only);
236-
i.set_return(r);
237-
}
231+
dereference_expr(i.return_value(), checks_only);
238232
}
239233
else if(i.is_other())
240234
{

0 commit comments

Comments
 (0)