replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4873 from romainbrenguier/bugfix/java-convert-variable 

Avoid unnecessary typecast in java_bytecode_convert_methodt::variable
This commit is contained in:
Romain Brenguier 2019-07-11 13:04:11 +01:00 committed by GitHub
parent cbef420de7 1c93adbab2
commit 1e5fd65072
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 411 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

77
jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View File

@ -164,21 +164,18 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
/// from a bytecode at address `address` a value of type `type_char` stored in
/// the JVM's slot `arg`.
/// \param arg: The local variable slot
/// \param type_char: The type of the value stored in the slot pointed by `arg`
/// \param type_char: The type of the value stored in the slot pointed to by
/// `arg`, this is only used in the case where a new unnamed local variable
/// is created
/// \param address: Bytecode address used to find a variable that the LVT
/// declares to be live and living in the slot pointed by `arg` for this
/// bytecode
/// \param do_cast: Indicates whether we should return the original symbol_exprt
/// or a typecast_exprt if the type of the symbol_exprt does not equal that
/// represented by `type_char`
/// \return symbol_exprt or type-cast symbol_exprt
exprt java_bytecode_convert_methodt::variable(
const exprt &arg,
char type_char,
size_t address,
java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
size_t address)
{
typet t=java_type_from_char(type_char);
const std::size_t number_int =
numeric_cast_v<std::size_t>(to_constant_expr(arg));
variablest &var_list=variables[number_int];
@ -187,24 +184,17 @@ exprt java_bytecode_convert_methodt::variable(
const variablet &var=
find_variable_for_slot(address, var_list);
if(var.symbol_expr.get_identifier().empty())
{
// an unnamed local variable
irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
if(!var.symbol_expr.get_identifier().empty())
return var.symbol_expr;
symbol_exprt result(identifier, t);
// an unnamed local variable
irep_idt base_name = "anonlocal::" + std::to_string(number_int) + type_char;
irep_idt identifier = id2string(current_method) + "::" + id2string(base_name);
symbol_exprt result(identifier, java_type_from_char(type_char));
result.set(ID_C_base_name, base_name);
used_local_names.insert(result);
return std::move(result);
}
else
{
exprt result=var.symbol_expr;
if(do_cast == CAST_AS_NEEDED)
result = typecast_exprt::conditional_cast(result, t);
return result;
}
}
/// Returns the member type for a method, based on signature or descriptor
@ -1346,8 +1336,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
else if(bytecode == patternt("?load") || bytecode == patternt("?load_?"))
{
// load a value from a local variable
results[0]=
variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED);
results[0] = convert_load(arg0, statement[0], i_it->address);
}
else if(bytecode == BC_ldc || bytecode == BC_ldc_w || bytecode == BC_ldc2_w)
{
@ -2710,7 +2699,7 @@ code_blockt java_bytecode_convert_methodt::convert_iinc(
code_blockt block;
block.add_source_location() = location;
// search variable on stack
const exprt &locvar = variable(arg0, 'i', address, NO_CAST);
const exprt &locvar = variable(arg0, 'i', address);
save_stack_entries(
"stack_iinc",
block,
@ -2720,8 +2709,11 @@ code_blockt java_bytecode_convert_methodt::convert_iinc(
const exprt arg1_int_type =
typecast_exprt::conditional_cast(arg1, java_int_type());
code_assignt code_assign(
variable(arg0, 'i', address, NO_CAST),
plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type));
variable(arg0, 'i', address),
plus_exprt(
typecast_exprt::conditional_cast(
variable(arg0, 'i', address), java_int_type()),
arg1_int_type));
block.add(std::move(code_assign));
return block;
@ -2826,7 +2818,7 @@ code_blockt java_bytecode_convert_methodt::convert_ret(
const method_offsett address)
{
code_blockt c;
auto retvar = variable(arg0, 'a', address, NO_CAST);
auto retvar = variable(arg0, 'a', address);
for(size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
{
irep_idt number = std::to_string(jsr_ret_targets[idx]);
@ -2888,6 +2880,27 @@ exprt java_bytecode_convert_methodt::convert_aload(
return java_bytecode_promotion(dereference_exprt{data_plus_offset});
}
exprt java_bytecode_convert_methodt::convert_load(
const exprt &index,
char type_char,
size_t address)
{
const exprt var = variable(index, type_char, address);
if(type_char == 'i')
{
INVARIANT(
can_cast_type<bitvector_typet>(var.type()) &&
type_try_dynamic_cast<bitvector_typet>(var.type())->get_width() <= 32,
"iload can be used for boolean, byte, short, int and char");
return typecast_exprt::conditional_cast(var, java_int_type());
}
INVARIANT(
(type_char == 'a' && can_cast_type<reference_typet>(var.type())) ||
var.type() == java_type_from_char(type_char),
"Variable type must match [adflv]load return type");
return var;
}
code_blockt java_bytecode_convert_methodt::convert_store(
const irep_idt &statement,
const exprt &arg0,
@ -2895,13 +2908,9 @@ code_blockt java_bytecode_convert_methodt::convert_store(
const method_offsett address,
const source_locationt &location)
{
const exprt var = variable(arg0, statement[0], address, NO_CAST);
const exprt var = variable(arg0, statement[0], address);
const irep_idt &var_name = to_symbol_expr(var).get_identifier();
exprt toassign = op[0];
if('a' == statement[0])
toassign = typecast_exprt::conditional_cast(toassign, var.type());
code_blockt block;
block.add_source_location() = location;
@ -2911,7 +2920,9 @@ code_blockt java_bytecode_convert_methodt::convert_store(
bytecode_write_typet::VARIABLE,
var_name);
block.add(code_assignt{var, toassign}, location);
block.add(
code_assignt{var, typecast_exprt::conditional_cast(op[0], var.type())},
location);
return block;
}

17
jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
View File

@ -183,11 +183,7 @@ protected:
NO_CAST
};
exprt variable(
const exprt &arg,
char type_char,
size_t address,
variable_cast_argumentt do_cast);
exprt variable(const exprt &arg, char type_char, size_t address);
// temporary variables
std::list<symbol_exprt> tmp_vars;
@ -369,6 +365,17 @@ protected:
static exprt
convert_aload(const irep_idt &statement, const exprt::operandst &op);
/// Load reference from local variable.
/// \p index must be an unsigned byte and an index in the local variable array
/// of the current frame. The type of the local variable at index \p index
/// must:
/// - be a reference type if \p type_char is 'a'
/// - be either boolean, byte, short, int, or char if \p type_char is 'i', a
/// typecast to `int` is added if needed
/// - match \c java_type_of_char(type_char) otherwise
/// \return the local variable at \p index
exprt convert_load(const exprt &index, char type_char, size_t address);
code_blockt convert_ret(
const std::vector<method_offsett> &jsr_ret_targets,
const exprt &arg0,

352
jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp
View File

@ -308,6 +308,48 @@ public:
{
return converter.convert_astore(statement, op, location);
}
static exprt variable(
java_bytecode_convert_methodt &converter,
const exprt &arg,
char type_char,
size_t address)
{
return converter.variable(arg, type_char, address);
}
static void add_variable(
java_bytecode_convert_methodt &converter,
std::size_t index,
symbol_exprt symbol_expr,
std::size_t start_pc,
std::size_t length,
bool is_parameter,
std::vector<java_bytecode_convert_methodt::holet> holes)
{
converter.variables[index].emplace_back(
std::move(symbol_expr), start_pc, length, is_parameter, std::move(holes));
}
static exprt convert_load(
java_bytecode_convert_methodt &converter,
const exprt &index,
char type_char,
size_t address)
{
return converter.convert_load(index, type_char, address);
}
static code_blockt convert_store(
java_bytecode_convert_methodt &converter,
const irep_idt &statement,
const exprt &arg0,
const exprt::operandst &op,
const java_bytecode_convert_methodt::method_offsett address,
const source_locationt &location)
{
return converter.convert_store(statement, arg0, op, address, location);
}
};
SCENARIO(
@ -518,3 +560,313 @@ SCENARIO(
}
}
}
SCENARIO(
"java convert method variable",
"[core][java_bytecode][java_bytecode_convert_method][variable]")
{
symbol_tablet symbol_table;
java_string_library_preprocesst string_preprocess;
const class_hierarchyt class_hierarchy{};
const std::size_t max_array_length = 10;
const bool throw_assertion_error = true;
const bool threading_support = false;
java_bytecode_convert_methodt converter{symbol_table,
null_message_handler,
max_array_length,
throw_assertion_error,
{},
string_preprocess,
class_hierarchy,
threading_support};
GIVEN("An int_array variable")
{
const source_locationt location;
const typet int_array_type = java_array_type('i');
const symbol_exprt int_array{"int_array", int_array_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, int_array, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is retrieved via its index with type_char a")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result = java_bytecode_convert_method_unit_testt::variable(
converter, index_expr, 'a', address);
THEN("the result is int_array")
{
REQUIRE(result == int_array);
}
}
WHEN("There is no variable at the given index")
{
const constant_exprt index_expr =
from_integer(variable_index + 1, java_int_type());
const exprt result = java_bytecode_convert_method_unit_testt::variable(
converter, index_expr, 'a', address);
THEN("A new reference variable is created")
{
REQUIRE(result != int_array);
REQUIRE(can_cast_expr<symbol_exprt>(result));
REQUIRE(result.type() == java_type_from_char('a'));
}
}
}
GIVEN("An Object variable")
{
const source_locationt location;
const typet object_type = java_lang_object_type();
const symbol_exprt obj{"obj", object_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, obj, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is retrieved via its index with type_char a")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result = java_bytecode_convert_method_unit_testt::variable(
converter, index_expr, 'a', address);
THEN("the result is obj")
{
REQUIRE(result == obj);
}
}
}
GIVEN("An long variable")
{
const source_locationt location;
const typet long_type = java_long_type();
const symbol_exprt long_var{"long_var", long_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, long_var, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is retrieved via its index with type_char l")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result = java_bytecode_convert_method_unit_testt::variable(
converter, index_expr, 'l', address);
THEN("the result is long_var")
{
REQUIRE(result == long_var);
}
}
}
}
SCENARIO(
"java convert load",
"[core][java_bytecode][java_bytecode_convert_method][convert_load]")
{
symbol_tablet symbol_table;
java_string_library_preprocesst string_preprocess;
const class_hierarchyt class_hierarchy{};
const std::size_t max_array_length = 10;
const bool throw_assertion_error = true;
const bool threading_support = false;
java_bytecode_convert_methodt converter{symbol_table,
null_message_handler,
max_array_length,
throw_assertion_error,
{},
string_preprocess,
class_hierarchy,
threading_support};
GIVEN("An int_array variable")
{
const source_locationt location;
const typet int_array_type = java_array_type('i');
const symbol_exprt int_array{"int_array", int_array_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, int_array, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is loaded with aload")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result =
java_bytecode_convert_method_unit_testt::convert_load(
converter, index_expr, 'a', address);
THEN("the result is int_array")
{
REQUIRE(result == int_array);
}
}
WHEN("There is no variable at the given index")
{
const constant_exprt index_expr =
from_integer(variable_index + 1, java_int_type());
const exprt result = java_bytecode_convert_method_unit_testt::variable(
converter, index_expr, 'a', address);
THEN("A new reference variable is created")
{
REQUIRE(result != int_array);
REQUIRE(can_cast_expr<symbol_exprt>(result));
REQUIRE(result.type() == java_type_from_char('a'));
}
}
}
GIVEN("An Object variable")
{
const source_locationt location;
const typet object_type = java_lang_object_type();
const symbol_exprt obj{"obj", object_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, obj, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is loaded with aload")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result =
java_bytecode_convert_method_unit_testt::convert_load(
converter, index_expr, 'a', address);
THEN("the result is obj")
{
REQUIRE(result == obj);
}
}
}
GIVEN("A long variable")
{
const source_locationt location;
const typet long_type = java_long_type();
const symbol_exprt long_var{"long_var", long_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter, variable_index, long_var, start_pc, length, is_parameter, {});
const std::size_t address = 0;
WHEN("The variable is loaded with lload")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result =
java_bytecode_convert_method_unit_testt::convert_load(
converter, index_expr, 'l', address);
THEN("the result is long_var")
{
REQUIRE(result == long_var);
}
}
}
GIVEN("A boolean variable")
{
const source_locationt location;
const symbol_exprt boolean_var{"boolean_var", java_boolean_type()};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter,
variable_index,
boolean_var,
start_pc,
length,
is_parameter,
{});
const std::size_t address = 0;
WHEN("The variable is loaded with iload")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const exprt result =
java_bytecode_convert_method_unit_testt::convert_load(
converter, index_expr, 'i', address);
THEN("the result is (int)boolean_var")
{
REQUIRE(result.type() == java_int_type());
REQUIRE(
make_query(result).as<typecast_exprt>()[0].get() == boolean_var);
}
}
}
}
SCENARIO(
"convert store",
"[core][java_bytecode][java_bytecode_convert_method][convert_store]")
{
symbol_tablet symbol_table;
java_string_library_preprocesst string_preprocess;
const class_hierarchyt class_hierarchy{};
const std::size_t max_array_length = 10;
const bool throw_assertion_error = true;
const bool threading_support = false;
java_bytecode_convert_methodt converter{symbol_table,
null_message_handler,
max_array_length,
throw_assertion_error,
{},
string_preprocess,
class_hierarchy,
threading_support};
GIVEN("An int_array variable")
{
const source_locationt location;
const typet int_array_type = java_array_type('i');
const symbol_exprt int_array{"int_array", int_array_type};
const symbol_exprt int_array_copy{"int_array_copy", int_array_type};
const std::size_t variable_index = 0;
const std::size_t start_pc = 0;
const std::size_t length = 1;
const bool is_parameter = false;
java_bytecode_convert_method_unit_testt::add_variable(
converter,
variable_index,
int_array_copy,
start_pc,
length,
is_parameter,
{});
WHEN("astore is called on the int array")
{
const constant_exprt index_expr =
from_integer(variable_index, java_int_type());
const code_blockt result_code =
java_bytecode_convert_method_unit_testt::convert_store(
converter, "astore", index_expr, {int_array}, 0, location);
THEN(
"The result is one assignment of the form "
"`int_array_copy = int_array`")
{
REQUIRE(result_code.statements().size() == 1);
auto assign_query =
make_query(result_code.statements()[0]).as<code_assignt>();
REQUIRE(can_cast_expr<symbol_exprt>(assign_query[0].get()));
REQUIRE(assign_query[1].get() == int_array);
THEN("Left-hand-side has type int array")
{
REQUIRE(assign_query[0].get().type() == int_array_type);
}
}
}
}
}