Skip to content

Java bytecode conversion: inline or move temporaries #4532

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 15, 2019
Merged

Java bytecode conversion: inline or move temporaries #4532

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cec0869
Do not take a reference to a temporary
tautschnig Apr 13, 2019
cc7eff6
Java bytecode conversion: inline or move temporaries
tautschnig Apr 13, 2019
1e9d135
Use code_blockt::add(code, source_location)
tautschnig Apr 13, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -859,7 +859,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
local_symbol.type = java_reference_type(struct_tag_type);
local_symbol.mode=ID_java;
symbol_table.add(local_symbol);
const auto &local_symexpr=local_symbol.symbol_expr();
const auto local_symexpr = local_symbol.symbol_expr();

code_declt declare_cloned(local_symexpr);

Expand Down
63 changes: 24 additions & 39 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1621,15 +1621,12 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
{
PRECONDITION(op.size() == 1 && results.size() == 1);

const typecast_exprt pointer(op[0], java_array_type(statement[0]));

dereference_exprt array{pointer};
PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
dereference_exprt array{
typecast_exprt{op[0], java_array_type(statement[0])}};
PRECONDITION(array.type().id() == ID_struct_tag);
array.set(ID_java_member_access, true);

const member_exprt length(array, "length", java_int_type());

results[0]=length;
results[0] = member_exprt{std::move(array), "length", java_int_type()};
}
else if(statement=="tableswitch" ||
statement=="lookupswitch")
Expand Down Expand Up @@ -1823,8 +1820,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(

if(start_new_block)
{
code_labelt newlabel(label(std::to_string(address)), code_blockt());
root_block.add(newlabel);
root_block.add(
code_labelt{label(std::to_string(address)), code_blockt{}});
root.branch.push_back(block_tree_nodet::get_leaf());
assert((root.branch_addresses.empty() ||
root.branch_addresses.back()<address) &&
Expand Down Expand Up @@ -1952,10 +1949,9 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
if(a_it == args.begin())
{
code_switch_caset code_case(nil_exprt(), std::move(code));
code_case.add_source_location() = location;
code_case.set_default();

code_block.add(std::move(code_case));
code_block.add(std::move(code_case), location);
}
else
{
Expand All @@ -1964,9 +1960,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
case_op.add_source_location() = location;

code_switch_caset code_case(std::move(case_op), std::move(code));
code_case.add_source_location() = location;

code_block.add(std::move(code_case));
code_block.add(std::move(code_case), location);
}
}
}
Expand Down Expand Up @@ -2490,7 +2484,7 @@ code_blockt java_bytecode_convert_methodt::convert_newarray(
constant_exprt size_limit = from_integer(max_array_length, java_int_type());
binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
code_assumet assume_le_max_size(le_max_size);
block.add(assume_le_max_size);
block.add(std::move(assume_le_max_size));
}
const exprt tmp = tmp_variable("newarray", ref_type);
block.add(code_assignt(tmp, java_new_array));
Expand Down Expand Up @@ -2693,10 +2687,10 @@ code_blockt java_bytecode_convert_methodt::convert_iinc(

const exprt arg1_int_type =
typecast_exprt::conditional_cast(arg1, java_int_type());
const code_assignt code_assign(
code_assignt code_assign(
variable(arg0, 'i', address, NO_CAST),
plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
block.add(code_assign);
block.add(std::move(code_assign));

return block;
}
Expand Down Expand Up @@ -2829,20 +2823,16 @@ exprt java_bytecode_convert_methodt::convert_aload(
const irep_idt &statement,
const exprt::operandst &op) const
{
const char &type_char = statement[0];
const typecast_exprt pointer(op[0], java_array_type(type_char));

dereference_exprt deref{pointer};
const char type_char = statement[0];
dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
deref.set(ID_java_member_access, true);

const member_exprt data_ptr(
member_exprt data_ptr(
deref, "data", pointer_type(java_type_from_char(type_char)));

plus_exprt data_plus_offset{data_ptr, op[1]};
plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
// tag it so it's easy to identify during instrumentation
data_plus_offset.set(ID_java_array_access, true);
const dereference_exprt element{data_plus_offset};
return java_bytecode_promotion(element);
return java_bytecode_promotion(dereference_exprt{data_plus_offset});
}

code_blockt java_bytecode_convert_methodt::convert_store(
Expand All @@ -2860,15 +2850,15 @@ code_blockt java_bytecode_convert_methodt::convert_store(
toassign = typecast_exprt::conditional_cast(toassign, var.type());

code_blockt block;
block.add_source_location() = location;

save_stack_entries(
"stack_store",
block,
bytecode_write_typet::VARIABLE,
var_name);
code_assignt assign(var, toassign);
assign.add_source_location() = location;
block.add(assign);

block.add(code_assignt{var, toassign}, location);
return block;
}

Expand All @@ -2878,28 +2868,23 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
const source_locationt &location)
{
const char type_char = statement[0];
const typecast_exprt pointer(op[0], java_array_type(type_char));

dereference_exprt deref{pointer};
dereference_exprt deref{typecast_exprt{op[0], java_array_type(type_char)}};
deref.set(ID_java_member_access, true);

const member_exprt data_ptr(
member_exprt data_ptr(
deref, "data", pointer_type(java_type_from_char(type_char)));

plus_exprt data_plus_offset{data_ptr, op[1]};
plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
// tag it so it's easy to identify during instrumentation
data_plus_offset.set(ID_java_array_access, true);
const dereference_exprt element{data_plus_offset};

code_blockt block;
block.add_source_location() = location;

save_stack_entries(
"stack_astore", block, bytecode_write_typet::ARRAY_REF, "");

code_assignt array_put(element, op[2]);
array_put.add_source_location() = location;
block.add(array_put);
code_assignt array_put{dereference_exprt{data_plus_offset}, op[2]};
block.add(std::move(array_put), location);
return block;
}

Expand Down
25 changes: 13 additions & 12 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -468,10 +468,8 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
array_type, "cprover_string_content", loc, function_id, symbol_table);
const symbol_exprt content_field = sym_content.symbol_expr();
code.add(code_declt(content_field), loc);
const refined_string_exprt str{
length_field, content_field, refined_string_type};
code.add(code_declt(length_field), loc);
return str;
code.add(code_declt{length_field}, loc);
return refined_string_exprt{length_field, content_field, refined_string_type};
}

/// add symbols with prefix cprover_string_length and cprover_string_data and
Expand Down Expand Up @@ -601,10 +599,10 @@ exprt make_nondet_infinite_char_array(
const symbol_exprt data_pointer = data_sym.symbol_expr();
code.add(code_declt(data_pointer));
code.add(make_allocate_code(data_pointer, array_type.size()));
const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
const exprt data = dereference_exprt{data_pointer};
code.add(code_assignt(data, nondet_data), loc);
return data;
side_effect_expr_nondett nondet_data{array_type, loc};
dereference_exprt data{data_pointer};
code.add(code_assignt{data, std::move(nondet_data)}, loc);
return std::move(data);
}

/// Add a call to a primitive of the string solver, letting it know that
Expand Down Expand Up @@ -847,8 +845,8 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(

// Assignments
code.add(code_assignt(lhs.length(), rhs_length), loc);
const exprt data_as_array = get_data(deref, symbol_table);
code.add(code_assignt(lhs.content(), data_as_array), loc);
exprt data_as_array = get_data(deref, symbol_table);
code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc);
}

/// Create a string expression whose value is given by a literal
Expand All @@ -868,9 +866,12 @@ java_string_library_preprocesst::string_literal_to_string_expr(
symbol_table_baset &symbol_table,
code_blockt &code)
{
const constant_exprt expr(s, string_typet());
return string_expr_of_function(
ID_cprover_string_literal_func, {expr}, loc, symbol_table, code);
ID_cprover_string_literal_func,
{constant_exprt{s, string_typet{}}},
loc,
symbol_table,
code);
}

/// Provide code for the String.valueOf(F) function.
Expand Down