From ffd089f2080899299ae08297072c55974e14bfa9 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 8 Nov 2017 12:52:46 +0000 Subject: [PATCH] Constructed class to mimic the original class in all but name of symbol When the tag was wrong it causes issues in calling methods and meant the real time type information would not be handled correctly. As the components on the new class have been moved, accessing the components by index no longer works. Instead access the components by name (and made use of other helper functions) --- .../generate_java_generic_type.cpp | 54 ++++++++++++++++--- .../generate_java_generic_type.h | 8 +++ .../generate_java_generic_type.cpp | 24 ++++----- 3 files changed, 68 insertions(+), 18 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 2b5badb381b..7edcdf08bd1 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -70,13 +70,20 @@ symbolt generate_java_generic_typet::operator()( pre_modification_size==after_modification_size, "All components in the original class should be in the new class"); - const auto expected_symbol="java::"+id2string(new_tag); + const java_class_typet &new_java_class = construct_specialised_generic_type( + generic_class_definition, new_tag, replacement_components); + const type_symbolt &class_symbol = + build_symbol_from_specialised_class(new_java_class); + + std::pair res = symbol_table.insert(std::move(class_symbol)); + if(!res.second) + { + messaget message(message_handler); + message.warning() << "stub class symbol " << class_symbol.name + << " already exists" << messaget::eom; + } - generate_class_stub( - new_tag, - symbol_table, - message_handler, - replacement_components); + const auto expected_symbol="java::"+id2string(new_tag); auto symbol=symbol_table.lookup(expected_symbol); INVARIANT(symbol, "New class not created"); return *symbol; @@ -216,3 +223,38 @@ irep_idt generate_java_generic_typet::build_generic_tag( return new_tag_buffer.str(); } + +/// Build the specalised version of the specific class, with the specified +/// parameters and name. +/// \param generic_class_definition: The generic class we are specialising +/// \param new_tag: The new name for the class (like Generic) +/// \param new_components: The specialised components +/// \return The newly constructed class. +java_class_typet +generate_java_generic_typet::construct_specialised_generic_type( + const java_generic_class_typet &generic_class_definition, + const irep_idt &new_tag, + const struct_typet::componentst &new_components) const +{ + java_class_typet specialised_class = generic_class_definition; + // We are specialising the logic - so we don't want to be marked as generic + specialised_class.set(ID_C_java_generics_class_type, false); + specialised_class.set(ID_name, "java::" + id2string(new_tag)); + specialised_class.set(ID_base_name, new_tag); + specialised_class.components() = new_components; + return specialised_class; +} + +/// Construct the symbol to be moved into the symbol table +/// \param specialised_class: The newly constructed specialised class +/// \return The symbol to add to the symbol table +type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class( + const java_class_typet &specialised_class) const +{ + type_symbolt new_symbol(specialised_class); + new_symbol.base_name = specialised_class.get(ID_base_name); + new_symbol.pretty_name = specialised_class.get(ID_base_name); + new_symbol.name = specialised_class.get(ID_name); + new_symbol.mode = ID_java; + return new_symbol; +} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 601c32ca7a6..f7e7656abc7 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -33,6 +33,14 @@ class generate_java_generic_typet const java_generic_class_typet &replacement_type, const java_generic_typet &generic_reference) const; + java_class_typet construct_specialised_generic_type( + const java_generic_class_typet &generic_class_definition, + const irep_idt &new_tag, + const struct_typet::componentst &new_components) const; + + type_symbolt build_symbol_from_specialised_class( + const java_class_typet &specialised_class) const; + message_handlert &message_handler; }; diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index 1e7d52981a2..81be01d6c2b 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -153,22 +153,22 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); auto first_symbol=new_symbol_table.lookup(first_expected_symbol); REQUIRE(first_symbol->type.id()==ID_struct); - auto first_symbol_type= - to_struct_type(first_symbol->type).components()[3].type(); - REQUIRE(first_symbol_type.id()==ID_pointer); - REQUIRE(first_symbol_type.subtype().id()==ID_symbol); - REQUIRE(to_symbol_type(first_symbol_type.subtype()).get_identifier()== - "java::java.lang.Boolean"); + const struct_union_typet::componentt &component = + require_type::require_component( + to_struct_type(first_symbol->type), "elem"); + auto first_symbol_type=component.type(); + require_type::require_pointer( + first_symbol_type, symbol_typet("java::java.lang.Boolean")); REQUIRE(new_symbol_table.has_symbol(second_expected_symbol)); auto second_symbol=new_symbol_table.lookup(second_expected_symbol); REQUIRE(second_symbol->type.id()==ID_struct); - auto second_symbol_type= - to_struct_type(second_symbol->type).components()[3].type(); - REQUIRE(second_symbol_type.id()==ID_pointer); - REQUIRE(second_symbol_type.subtype().id()==ID_symbol); - REQUIRE(to_symbol_type(second_symbol_type.subtype()).get_identifier()== - "java::java.lang.Integer"); + const struct_union_typet::componentt &second_component = + require_type::require_component( + to_struct_type(second_symbol->type), "elem"); + auto second_symbol_type=second_component.type(); + require_type::require_pointer( + second_symbol_type, symbol_typet("java::java.lang.Integer")); } }