From 9a2fd03d22993c9322c8c1a72b2c6090586ea8b4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 15 Nov 2017 16:58:29 +0000 Subject: [PATCH 1/2] Introduce the new data type representing specialised generic classes, and modify the concretisation process to use it. --- .../generate_java_generic_type.cpp | 195 ++++++++---------- src/java_bytecode/java_types.h | 25 +++ src/util/irep_ids.def | 1 + 3 files changed, 113 insertions(+), 108 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 7edcdf08bd1..d98b017e578 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -13,7 +13,7 @@ generate_java_generic_typet::generate_java_generic_typet( message_handlert &message_handler): - message_handler(message_handler) + message_handler(message_handler) {} /// Generate a concrete instantiation of a generic type. @@ -32,17 +32,13 @@ symbolt generate_java_generic_typet::operator()( INVARIANT( pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); - INVARIANT( - is_java_generic_class_type(pointer_subtype), - "Generic references type must be a generic class"); - - const java_generic_class_typet &generic_class_definition = - to_java_generic_class_type(to_java_class_type(pointer_subtype)); - const irep_idt new_tag = - build_generic_tag(existing_generic_type, generic_class_definition); - struct_union_typet::componentst replacement_components = - generic_class_definition.components(); + const java_class_typet &replacement_type= + to_java_class_type(pointer_subtype); + const irep_idt new_tag=build_generic_tag( + existing_generic_type, replacement_type); + struct_union_typet::componentst replacement_components= + replacement_type.components(); // Small auxiliary function, to perform the inplace // modification of the generic fields. @@ -50,7 +46,9 @@ symbolt generate_java_generic_typet::operator()( [&](struct_union_typet::componentt &component) { component.type() = substitute_type( - component.type(), generic_class_definition, existing_generic_type); + component.type(), + to_java_generic_class_type(replacement_type), + existing_generic_type); return component; }; @@ -63,27 +61,51 @@ symbolt generate_java_generic_typet::operator()( replacement_components.end(), replace_type_for_generic_field); - std::size_t after_modification_size = - generic_class_definition.components().size(); + std::size_t after_modification_size= + replacement_type.components().size(); INVARIANT( pre_modification_size==after_modification_size, "All components in the original class should be in the new class"); - 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) + const auto expected_symbol="java::"+id2string(new_tag); +// +// generate_class_stub( +// new_tag, +// symbol_table, +// message_handler, +// replacement_components); + + // inlined the generate_class_stub for now { - messaget message(message_handler); - message.warning() << "stub class symbol " << class_symbol.name - << " already exists" << messaget::eom; + java_specialised_generic_class_typet specialised_class; + specialised_class.set_tag(replacement_type.get_tag()); + // NOTE: the tag absolutely has to be BasicGeneric + specialised_class.set(ID_base_name, new_tag); + + // produce class symbol + symbolt new_symbol; + new_symbol.base_name = new_tag; + new_symbol.pretty_name = new_tag; + new_symbol.name = "java::" + id2string(new_tag); + specialised_class.set(ID_name, new_symbol.name); + new_symbol.type = specialised_class; + new_symbol.mode = ID_java; + new_symbol.is_type = true; + + std::pair res = symbol_table.insert(std::move(new_symbol)); + + if(!res.second) + { + messaget message(message_handler); + message.warning() << "stub class symbol " << new_symbol.name + << " already exists" << messaget::eom; + } + else + { + java_add_components_to_class(res.first, 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; @@ -109,16 +131,25 @@ typet generate_java_generic_typet::substitute_type( if(is_java_generic_parameter(parameter_type)) { auto component_identifier = to_java_generic_parameter(parameter_type) - .type_variable() - .get_identifier(); + .type_variable() + .get_identifier(); optionalt results = java_generics_get_index_for_subtype(generic_class, component_identifier); INVARIANT(results.has_value(), "generic component type not found"); - return generic_reference.generic_type_variables()[*results]; + + if(results) + { + return generic_reference.generic_type_variables()[*results]; + } + else + { + return parameter_type; + } } - else if(parameter_type.id() == ID_pointer) + else if( + parameter_type.id() == ID_pointer) { if(is_java_generic_type(parameter_type)) { @@ -134,27 +165,27 @@ typet generate_java_generic_typet::substitute_type( std::back_inserter(replaced_type_variables), [&](const java_generic_parametert &generic_param) -> java_generic_parametert { - const typet &replacement_type = - substitute_type(generic_param, generic_class, generic_reference); - - // This code will be simplified when references aren't considered to - // be generic parameters - if(is_java_generic_parameter(replacement_type)) - { - return to_java_generic_parameter(replacement_type); - } - else - { - INVARIANT( - is_reference(replacement_type), - "All generic parameters should be references"); - return java_generic_inst_parametert( - to_symbol_type(replacement_type.subtype())); - } - }); - - java_generic_typet new_type = generic_type; - new_type.generic_type_variables() = replaced_type_variables; + const typet &replacement_type = + substitute_type(generic_param, generic_class, generic_reference); + + // This code will be simplified when references aren't considered to + // be generic parameters + if(is_java_generic_parameter(replacement_type)) + { + return to_java_generic_parameter(replacement_type); + } + else + { + INVARIANT( + is_reference(replacement_type), + "All generic parameters should be references"); + return java_generic_inst_parametert( + to_symbol_type(replacement_type.subtype())); + } + }); + + java_generic_typet new_type=generic_type; + new_type.generic_type_variables()=replaced_type_variables; return new_type; } else if(parameter_type.subtype().id() == ID_symbol) @@ -163,14 +194,14 @@ typet generate_java_generic_typet::substitute_type( to_symbol_type(parameter_type.subtype()); if(is_java_array_tag(array_subtype.get_identifier())) { - const typet &array_element_type = - java_array_element_type(array_subtype); + const typet &array_element_type = java_array_element_type(array_subtype); const typet &new_array_type = substitute_type(array_element_type, generic_class, generic_reference); typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_C_element_type, new_array_type); + replacement_array_type.subtype().set( + ID_C_element_type, new_array_type); return replacement_array_type; } } @@ -199,62 +230,10 @@ irep_idt generate_java_generic_typet::build_generic_tag( INVARIANT( is_java_generic_inst_parameter(param), "Only create full concretized generic types"); - const irep_idt &id(id2string(param.subtype().get(ID_identifier))); - new_tag_buffer << id2string(id); - if(is_java_array_tag(id)) - { - const typet &element_type = - java_array_element_type(to_symbol_type(param.subtype())); - - // If this is an array of references then we will specialize its - // identifier using the type of the objects in the array. Else, there can - // be a problem with the same symbols for different instantiations using - // arrays with different types. - if(element_type.id() == ID_pointer) - { - const symbol_typet element_symbol = - to_symbol_type(element_type.subtype()); - new_tag_buffer << "of_" << id2string(element_symbol.get_identifier()); - } - } + new_tag_buffer << param.subtype().get(ID_identifier); } new_tag_buffer << ">"; 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; -} +} \ No newline at end of file diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index cd4aa45813d..9f98efa78c2 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -400,4 +400,29 @@ inline const optionalt java_generics_get_index_for_subtype( return std::distance(gen_types.cbegin(), iter); } +class java_specialised_generic_class_typet : public java_class_typet +{ + // note the constructor could take the components and construct it itself + // note vector of generic parameter of symbol type +public: + // TODO: to be defined more appropriately. + java_specialised_generic_class_typet() + { + set(ID_C_specialised_generic_java_class, true); + } +}; + +inline const bool java_is_specialised_generic_class_type(const typet &type) +{ + return type.get_bool(ID_C_specialised_generic_java_class); +} + +inline java_specialised_generic_class_typet +to_java_specialised_class_typet(const typet &type) +{ + INVARIANT(java_is_specialised_generic_class_type(type), + "Tried to convert a type that was not a specialised generic java class"); + return static_cast(type); +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 005124d0ea7..7b43b224177 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -833,6 +833,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(generic_types, #generic_types) IREP_ID_TWO(type_variables, #type_variables) +IREP_ID_TWO(C_specialised_generic_java_class, #specialised_class) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) From ff308ac6fa353bd73369103266ccbde99689601a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 15 Nov 2017 16:59:29 +0000 Subject: [PATCH 2/2] Extend the precondition to handle the case with the weird typecast expression for a concrete generic type. --- src/goto-programs/interpreter_evaluate.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 0a2a7ec6e72..9f2e3d19066 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include /// Reads a memory address and loads it into the `dest` variable. /// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written. @@ -1196,7 +1197,15 @@ mp_integer interpretert::evaluate_address( if(expr.operands().size()!=1) throw "typecast expects one operand"; - PRECONDITION(expr.type().id()==ID_pointer); + PRECONDITION(expr.type().id()==ID_pointer || + // with generics support, we get some weird typecast expressions, + // in the goto program, where the first operand is typecast into a + // struct that resembles the same type, and is of type "struct" instead + // "pointer" so the precondition above would fail. This makes sure to + // proceed the evaluation in the case where the operand is a generic + // instantiated type. + (expr.type().id()==ID_struct && + java_is_specialised_generic_class_type(expr.op0().type()))); return evaluate_address(expr.op0(), fail_quietly); }