Skip to content

Commit 1b5b169

Browse files
author
Daniel Kroening
committed
clean up lower_java_new
This cleanup avoids direct access to expression internals, and avoids two copies.
1 parent 142ae78 commit 1b5b169

File tree

1 file changed

+30
-23
lines changed

1 file changed

+30
-23
lines changed

jbmc/src/java_bytecode/remove_java_new.cpp

Lines changed: 30 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -47,15 +47,15 @@ class remove_java_newt : public messaget
4747

4848
goto_programt::targett lower_java_new(
4949
const irep_idt &function_identifier,
50-
exprt lhs,
51-
side_effect_exprt rhs,
50+
const exprt &lhs,
51+
const side_effect_exprt &rhs,
5252
goto_programt &,
5353
goto_programt::targett);
5454

5555
goto_programt::targett lower_java_new_array(
5656
const irep_idt &function_identifier,
57-
exprt lhs,
58-
side_effect_exprt rhs,
57+
const exprt &lhs,
58+
const side_effect_exprt &rhs,
5959
goto_programt &,
6060
goto_programt::targett);
6161
};
@@ -74,8 +74,8 @@ class remove_java_newt : public messaget
7474
/// destruction when replacing the instruction.
7575
goto_programt::targett remove_java_newt::lower_java_new(
7676
const irep_idt &function_identifier,
77-
exprt lhs,
78-
side_effect_exprt rhs,
77+
const exprt &lhs,
78+
const side_effect_exprt &rhs,
7979
goto_programt &dest,
8080
goto_programt::targett target)
8181
{
@@ -123,8 +123,8 @@ goto_programt::targett remove_java_newt::lower_java_new(
123123
/// destruction when replacing the instruction.
124124
goto_programt::targett remove_java_newt::lower_java_new_array(
125125
const irep_idt &function_identifier,
126-
exprt lhs,
127-
side_effect_exprt rhs,
126+
const exprt &lhs,
127+
const side_effect_exprt &rhs,
128128
goto_programt &dest,
129129
goto_programt::targett target)
130130
{
@@ -325,24 +325,31 @@ goto_programt::targett remove_java_newt::lower_java_new(
325325
goto_programt &goto_program,
326326
goto_programt::targett target)
327327
{
328-
const auto maybe_code_assign =
329-
expr_try_dynamic_cast<code_assignt>(target->code);
330-
if(!maybe_code_assign)
328+
if(!target->is_assign())
331329
return target;
332330

333-
const exprt &lhs = maybe_code_assign->lhs();
334-
const exprt &rhs = maybe_code_assign->rhs();
335-
336-
if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_java_new)
337-
{
338-
return lower_java_new(
339-
function_identifier, lhs, to_side_effect_expr(rhs), goto_program, target);
340-
}
341-
342-
if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_java_new_array)
331+
if(as_const(*target).get_assign().rhs().id() == ID_side_effect)
343332
{
344-
return lower_java_new_array(
345-
function_identifier, lhs, to_side_effect_expr(rhs), goto_program, target);
333+
// we make a copy, as we intend to destroy the assignment
334+
// inside lower_java_new and lower_java_new_array
335+
const auto code_assign = target->get_assign();
336+
337+
const exprt &lhs = code_assign.lhs();
338+
const exprt &rhs = code_assign.rhs();
339+
340+
const auto &side_effect_expr = to_side_effect_expr(rhs);
341+
const auto &statement = side_effect_expr.get_statement();
342+
343+
if(statement == ID_java_new)
344+
{
345+
return lower_java_new(
346+
function_identifier, lhs, side_effect_expr, goto_program, target);
347+
}
348+
else if(statement == ID_java_new_array)
349+
{
350+
return lower_java_new_array(
351+
function_identifier, lhs, side_effect_expr, goto_program, target);
352+
}
346353
}
347354

348355
return target;

0 commit comments

Comments
 (0)