Skip to content
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

Java arrays are instanceof Object #1778

Merged
merged 4 commits into from
Mar 8, 2018
Merged

Java arrays are instanceof Object #1778

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
881b127
Refactor: use class_typet instead of struct_typet for java class
peterschrammel Jan 30, 2018
8995fce
Java arrays are instanceof Object
peterschrammel Jan 30, 2018
ae276ef
Activate two instanceof regression tests
peterschrammel Jan 29, 2018
5fa3a1a
Refactor: improve variable naming
peterschrammel Mar 6, 2018
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 regression/cbmc-java/instanceof1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
instanceof1.class

^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/instanceof3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
instanceof3.class

^EXIT=0$
Expand Down
61 changes: 33 additions & 28 deletions 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 @@ -478,39 +478,41 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
if(symbol_table.has_symbol(symbol_type_identifier))
return;

struct_typet struct_type;
class_typet class_type;
// we have the base class, java.lang.Object, length and data
// of appropriate type
struct_type.set_tag(symbol_type_identifier);

struct_type.components().reserve(3);
struct_typet::componentt
comp0("@java.lang.Object", symbol_typet("java::java.lang.Object"));
comp0.set_pretty_name("@java.lang.Object");
comp0.set_base_name("@java.lang.Object");
struct_type.components().push_back(comp0);

struct_typet::componentt comp1("length", java_int_type());
comp1.set_pretty_name("length");
comp1.set_base_name("length");
struct_type.components().push_back(comp1);

struct_typet::componentt
comp2("data", java_reference_type(java_type_from_char(l)));
comp2.set_pretty_name("data");
comp2.set_base_name("data");
struct_type.components().push_back(comp2);
class_type.set_tag(symbol_type_identifier);

class_type.components().reserve(3);
class_typet::componentt base_class_component(
"@java.lang.Object", symbol_typet("java::java.lang.Object"));
base_class_component.set_pretty_name("@java.lang.Object");
base_class_component.set_base_name("@java.lang.Object");
class_type.components().push_back(base_class_component);

class_typet::componentt length_component("length", java_int_type());
length_component.set_pretty_name("length");
length_component.set_base_name("length");
class_type.components().push_back(length_component);

class_typet::componentt data_component(
"data", java_reference_type(java_type_from_char(l)));
data_component.set_pretty_name("data");
data_component.set_base_name("data");
class_type.components().push_back(data_component);

class_type.add_base(symbol_typet("java::java.lang.Object"));

INVARIANT(
is_valid_java_array(struct_type),
is_valid_java_array(class_type),
"Constructed a new type representing a Java Array "
"object that doesn't match expectations");

symbolt symbol;
symbol.name=symbol_type_identifier;
symbol.base_name=symbol_type.get(ID_C_base_name);
symbol.is_type=true;
symbol.type=struct_type;
symbol.type = class_type;
symbol_table.add(symbol);

// Also provide a clone method:
Expand Down Expand Up @@ -557,14 +559,16 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
java_reference_type(symbol_type));
dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
dereference_exprt new_array(local_symexpr, symbol_type);
member_exprt old_length(old_array, comp1.get_name(), comp1.type());
member_exprt old_length(
old_array, length_component.get_name(), length_component.type());
java_new_array.copy_to_operands(old_length);
code_assignt create_blank(local_symexpr, java_new_array);
clone_body.move_to_operands(create_blank);


member_exprt old_data(old_array, comp2.get_name(), comp2.type());
member_exprt new_data(new_array, comp2.get_name(), comp2.type());
member_exprt old_data(
old_array, data_component.get_name(), data_component.type());
member_exprt new_data(
new_array, data_component.get_name(), data_component.type());

/*
// TODO use this instead of a loop.
Expand All @@ -583,7 +587,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
index_symbol.name=index_name;
index_symbol.base_name="index";
index_symbol.pretty_name=index_symbol.base_name;
index_symbol.type=comp1.type();
index_symbol.type = length_component.type();
index_symbol.mode=ID_java;
symbol_table.add(index_symbol);
const auto &index_symexpr=index_symbol.symbol_expr();
Expand Down Expand Up @@ -614,7 +618,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
// End for-loop
clone_body.move_to_operands(copy_loop);

member_exprt new_base_class(new_array, comp0.get_name(), comp0.type());
member_exprt new_base_class(
new_array, base_class_component.get_name(), base_class_component.type());
address_of_exprt retval(new_base_class);
code_returnt return_inst(retval);
clone_body.move_to_operands(return_inst);
Expand Down