Skip to content

Commit b6cae86

Browse files
author
Daniel Kroening
committed
remove_java_new can now follow one typecast
statements such as var = (type) java_new(....) can now be lowered. This removes the requirement to introduce a temporary just to do the typecast.
1 parent d8598f8 commit b6cae86

File tree

1 file changed

+24
-13
lines changed

1 file changed

+24
-13
lines changed

jbmc/src/java_bytecode/remove_java_new.cpp

Lines changed: 24 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -94,11 +94,17 @@ goto_programt::targett remove_java_newt::lower_java_new(
9494
malloc_expr.copy_to_operands(*object_size);
9595
// could use true and get rid of the code below
9696
malloc_expr.copy_to_operands(false_exprt());
97-
*target =
98-
goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location);
97+
98+
auto malloc_expr_casted =
99+
typecast_exprt::conditional_cast(malloc_expr, lhs.type());
100+
101+
*target = goto_programt::make_assignment(
102+
code_assignt(lhs, malloc_expr_casted), location);
99103

100104
// zero-initialize the object
101-
dereference_exprt deref(lhs, object_type);
105+
auto lhs_casted = typecast_exprt::conditional_cast(lhs, rhs.type());
106+
107+
dereference_exprt deref(lhs_casted, object_type);
102108
auto zero_object = zero_initializer(object_type, location, ns);
103109
CHECK_RETURN(zero_object.has_value());
104110
set_class_identifier(
@@ -147,8 +153,11 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
147153
// code use true and get rid of the code below
148154
malloc_expr.copy_to_operands(false_exprt());
149155

150-
*target =
151-
goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location);
156+
auto lhs_casted = typecast_exprt::conditional_cast(lhs, malloc_expr.type());
157+
158+
*target = goto_programt::make_assignment(
159+
code_assignt(lhs_casted, malloc_expr), location);
160+
152161
goto_programt::targett next = std::next(target);
153162

154163
const struct_typet &struct_type = to_struct_type(ns.follow(object_type));
@@ -159,7 +168,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
159168
PRECONDITION(struct_type.components().size() == 3);
160169

161170
// Init base class:
162-
dereference_exprt deref(lhs, object_type);
171+
dereference_exprt deref(lhs_casted, object_type);
163172
auto zero_object = zero_initializer(object_type, location, ns);
164173
CHECK_RETURN(zero_object.has_value());
165174
set_class_identifier(
@@ -328,15 +337,17 @@ goto_programt::targett remove_java_newt::lower_java_new(
328337
if(!target->is_assign())
329338
return target;
330339

331-
if(as_const(*target).get_assign().rhs().id() == ID_side_effect)
332-
{
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();
340+
// we make a copy of lhs/rhs, as we intend to destroy the assignment
341+
// inside lower_java_new and lower_java_new_array
342+
const auto &code_assign = target->get_assign();
343+
auto rhs = code_assign.rhs();
344+
auto lhs = code_assign.lhs();
336345

337-
const exprt &lhs = code_assign.lhs();
338-
const exprt &rhs = code_assign.rhs();
346+
if(rhs.id() == ID_typecast) // follow one typecast
347+
rhs = to_typecast_expr(rhs).op();
339348

349+
if(rhs.id() == ID_side_effect)
350+
{
340351
const auto &side_effect_expr = to_side_effect_expr(rhs);
341352
const auto &statement = side_effect_expr.get_statement();
342353

0 commit comments

Comments
 (0)