diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class new file mode 100644 index 00000000000..a7920d988fc Binary files /dev/null and b/jbmc/regression/jbmc/generics_recursive_parameters/KeyValue.class differ diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class new file mode 100644 index 00000000000..58e7cc0256a Binary files /dev/null and b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.class differ diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java new file mode 100644 index 00000000000..1fbdeb644d2 --- /dev/null +++ b/jbmc/regression/jbmc/generics_recursive_parameters/MutuallyRecursiveGenerics.java @@ -0,0 +1,11 @@ +class KeyValue { + KeyValue next; + KeyValue reverse; + K key; + V value; +} +class MutuallyRecursiveGenerics { + void f() { + KeyValue example1; + } +} diff --git a/jbmc/regression/jbmc/generics_recursive_parameters/test.desc b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc new file mode 100644 index 00000000000..859670558b4 --- /dev/null +++ b/jbmc/regression/jbmc/generics_recursive_parameters/test.desc @@ -0,0 +1,9 @@ +CORE +MutuallyRecursiveGenerics.class +--cover location --function MutuallyRecursiveGenerics.f +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This failed before due to infinite recursion in the way how the instantiated +generic parameters were used. cf. TG-3067 diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index 18cc04a0918..8666806e040 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -72,9 +72,9 @@ const void generic_parameter_specialization_map_keyst::insert_pairs( const irep_idt &key = pair.first.get_name(); if(generic_parameter_specialization_map.count(key) == 0) generic_parameter_specialization_map.emplace( - key, std::stack()); + key, std::vector()); (*generic_parameter_specialization_map.find(key)) - .second.push(pair.second); + .second.push_back(pair.second); // We added something, so pop it when this is destroyed: erase_keys.push_back(key); diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h index 9a68dd73d87..36f0efb2afb 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -33,11 +33,10 @@ class generic_parameter_specialization_map_keyst for(const auto key : erase_keys) { PRECONDITION(generic_parameter_specialization_map.count(key) != 0); - (*generic_parameter_specialization_map.find(key)).second.pop(); - if((*generic_parameter_specialization_map.find(key)).second.empty()) - { + auto &val = generic_parameter_specialization_map.find(key)->second; + val.pop_back(); + if(val.empty()) generic_parameter_specialization_map.erase(key); - } } } diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index b8ed2371242..5ec5909620b 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -41,7 +41,7 @@ class java_object_factoryt /// Every time the non-det generator visits a type and the type is generic /// (either a struct or a pointer), the following map is used to store and - /// look up the concrete types of the generic paramaters in the current + /// look up the concrete types of the generic parameters in the current /// scope. Note that not all generic parameters need to have a concrete /// type, e.g., the method under test is generic. The types are removed /// from the map when the scope changes. Note that in different depths diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index cd0c99505e5..ed657af0384 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -32,8 +32,11 @@ pointer_typet select_pointer_typet::convert_pointer_type( // a generic parameter, specialize it with concrete types if(!generic_parameter_specialization_map.empty()) { - return specialize_generics( - pointer_type, generic_parameter_specialization_map); + generic_parameter_recursion_trackingt visited; + const auto &type = specialize_generics( + pointer_type, generic_parameter_specialization_map, visited); + INVARIANT(visited.empty(), "recursion stack must be empty here"); + return type; } else { @@ -62,13 +65,24 @@ pointer_typet select_pointer_typet::convert_pointer_type( pointer_typet select_pointer_typet::specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt - &generic_parameter_specialization_map) const + &generic_parameter_specialization_map, + generic_parameter_recursion_trackingt &visited_nodes) const { if(is_java_generic_parameter(pointer_type)) { const java_generic_parametert ¶meter = to_java_generic_parameter(pointer_type); const irep_idt ¶meter_name = parameter.get_name(); + + // avoid infinite recursion by looking at each generic argument from + // previous assignments + if(visited_nodes.find(parameter_name) != visited_nodes.end()) + { + const optionalt result = get_recursively_instantiated_type( + parameter_name, generic_parameter_specialization_map); + return result.has_value() ? result.value() : pointer_type; + } + if(generic_parameter_specialization_map.count(parameter_name) == 0) { // this means that the generic pointer_type has not been specialized @@ -78,15 +92,20 @@ pointer_typet select_pointer_typet::specialize_generics( return pointer_type; } const pointer_typet &type = - generic_parameter_specialization_map.find(parameter_name)->second.top(); + generic_parameter_specialization_map.find(parameter_name)->second.back(); // generic parameters can be adopted from outer classes or superclasses so // we may need to search for the concrete type recursively - return is_java_generic_parameter(type) - ? specialize_generics( - to_java_generic_parameter(type), - generic_parameter_specialization_map) - : type; + if(!is_java_generic_parameter(type)) + return type; + + visited_nodes.insert(parameter_name); + const auto returned_type = specialize_generics( + to_java_generic_parameter(type), + generic_parameter_specialization_map, + visited_nodes); + visited_nodes.erase(parameter_name); + return returned_type; } else if(pointer_type.subtype().id() == ID_symbol) { @@ -99,7 +118,8 @@ pointer_typet select_pointer_typet::specialize_generics( { const pointer_typet &new_array_type = specialize_generics( to_pointer_type(array_element_type), - generic_parameter_specialization_map); + generic_parameter_specialization_map, + visited_nodes); pointer_typet replacement_array_type = java_array_type('a'); replacement_array_type.subtype().set(ID_C_element_type, new_array_type); @@ -109,3 +129,96 @@ pointer_typet select_pointer_typet::specialize_generics( } return pointer_type; } + +/// Return the first concrete type instantiation if any such exists. This method +/// is only to be called when the `specialize_generics` cannot find an +/// instantiation due to a loop in its recursion. +/// \param parameter_name The name of the generic parameter type we want to have +/// instantiated +/// \param generic_parameter_specialization_map Map of type names to +/// specialization stack +/// \return The first instantiated type for the generic type or nothing if no +/// such instantiation exists. +optionalt +select_pointer_typet::get_recursively_instantiated_type( + const irep_idt ¶meter_name, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map) const +{ + generic_parameter_recursion_trackingt visited; + const size_t max_depth = + generic_parameter_specialization_map.find(parameter_name)->second.size(); + + irep_idt current_parameter = parameter_name; + for(size_t depth = 0; depth < max_depth; depth++) + { + const auto retval = get_recursively_instantiated_type( + current_parameter, generic_parameter_specialization_map, visited, depth); + if(retval.has_value()) + { + CHECK_RETURN(!is_java_generic_parameter(*retval)); + return retval; + } + CHECK_RETURN(visited.empty()); + + const auto &entry = + generic_parameter_specialization_map.find(current_parameter) + ->second.back(); + current_parameter = to_java_generic_parameter(entry).get_name(); + } + return {}; +} + +/// See get_recursively instantiated_type, the additional parameters just track +/// the recursion to prevent visiting the same depth again and specify which +/// stack depth is analyzed. +/// \param parameter_name The name of the generic parameter type we want to have +/// instantiated +/// \param generic_parameter_specialization_map Map of type names to +/// specialization stack +/// \param visited Tracks the visited parameter names +/// \param depth Stack depth to analyze +/// \return if this type is not a generic type, it is returned as a valid +/// instantiation, if nothing can be found at the given depth, en empty +/// optional is returned +optionalt +select_pointer_typet::get_recursively_instantiated_type( + const irep_idt ¶meter_name, + const generic_parameter_specialization_mapt + &generic_parameter_specialization_map, + generic_parameter_recursion_trackingt &visited, + const size_t depth) const +{ + const auto &val = generic_parameter_specialization_map.find(parameter_name); + INVARIANT( + val != generic_parameter_specialization_map.end(), + "generic parameter must be a key in map"); + + const auto &replacements = val->second; + + INVARIANT( + depth < replacements.size(), "cannot access elements outside stack"); + + // Check if there is a recursion loop, if yes return with nothing found + if(visited.find(parameter_name) != visited.end()) + { + return {}; + } + + const size_t index = (replacements.size() - 1) - depth; + const auto &type = replacements[index]; + + if(!is_java_generic_parameter(type)) + { + return type; + } + + visited.insert(parameter_name); + const auto inst_val = get_recursively_instantiated_type( + to_java_generic_parameter(type).get_name(), + generic_parameter_specialization_map, + visited, + depth); + visited.erase(parameter_name); + return inst_val; +} diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index 2f2af2792f1..64c1127f6c1 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -11,18 +11,29 @@ /// \file /// Handle selection of correct pointer type (for example changing abstract /// classes to concrete versions). +#include -#include -#include #include "java_types.h" +#include +#include -typedef std::unordered_map> +typedef std::unordered_map> generic_parameter_specialization_mapt; +typedef std::set generic_parameter_recursion_trackingt; class namespacet; class select_pointer_typet { + optionalt get_recursively_instantiated_type( + const irep_idt &, + const generic_parameter_specialization_mapt &, + generic_parameter_recursion_trackingt &, + const size_t) const; + optionalt get_recursively_instantiated_type( + const irep_idt ¶meter_name, + const generic_parameter_specialization_mapt &visited) const; + public: virtual ~select_pointer_typet() = default; virtual pointer_typet convert_pointer_type( @@ -34,7 +45,8 @@ class select_pointer_typet pointer_typet specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt - &generic_parameter_specialization_map) const; + &generic_parameter_specialization_map, + generic_parameter_recursion_trackingt &visited) const; }; #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 16da78dcda2..0b6df177183 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -32,6 +32,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ util/simplify_expr.cpp \ java_bytecode/java_virtual_functions/virtual_functions.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ + java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ # Empty last line INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit diff --git a/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class new file mode 100644 index 00000000000..d093b949329 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class new file mode 100644 index 00000000000..ed2b3621526 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java new file mode 100644 index 00000000000..55dea15389b --- /dev/null +++ b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java @@ -0,0 +1,29 @@ +class Outer { + class Inner { + Outer o; + U u; + } + Inner inner; + K key; + V value; +} +class Three { + Three rotate; + Three normal; + X x; + E e; + U u; +} +class KeyValue { + KeyValue next; + KeyValue reverse; + K key; + V value; +} +class MutuallyRecursiveGenerics { + KeyValue example1; + Three example2; + Outer example3; + void f() { + } +} diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class new file mode 100644 index 00000000000..136c195e97d Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class new file mode 100644 index 00000000000..06ce8540988 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Three.class b/jbmc/unit/java_bytecode/goto_program_generics/Three.class new file mode 100644 index 00000000000..3921f569040 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/Three.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp new file mode 100644 index 00000000000..98dc10b63ed --- /dev/null +++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp @@ -0,0 +1,278 @@ +/*******************************************************************\ + + Module: Unit tests for parsing mutually generic classes + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include + +SCENARIO( + "Generics class with mutually recursive_generic parameters", + "[core][java_bytecode][goto_programs_generics]") +{ + const symbol_tablet &symbol_table = load_java_class( + "MutuallyRecursiveGenerics", + "./java_bytecode/goto_program_generics", + "MutuallyRecursiveGenerics.f"); + + const std::string class_prefix = "java::MutuallyRecursiveGenerics"; + + REQUIRE(symbol_table.has_symbol(class_prefix)); + + WHEN( + "parsing class which has generic type parameters and two field with those" + "parameters in use") + { + const auto &root = symbol_table.lookup_ref(class_prefix); + const typet &type = root.type; + REQUIRE(type.id() == ID_struct); + + // needs an `example1` local variable ... + const struct_union_typet::componentt &example1 = + require_type::require_component(to_struct_type(type), "example1"); + + // ... which is generic and has two explicit generic parameter + // instantiations, String and Integer ... + const java_generic_typet &gen_type = + require_type::require_java_generic_type( + example1.type(), + {{require_type::type_argument_kindt::Inst, "java::java.lang.String"}, + {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + + // ... which is of type `KeyValue` ... + const auto &subtype = gen_type.subtype(); + const auto &key_value = + symbol_table.lookup_ref(to_symbol_type(subtype).get_identifier()); + REQUIRE(key_value.type.id() == ID_struct); + REQUIRE(key_value.name == "java::KeyValue"); + + // ... and contains two local variables of type `KeyValue` ... + const auto &next = + require_type::require_component(to_struct_type(key_value.type), "next"); + const auto &reverse = require_type::require_component( + to_struct_type(key_value.type), "reverse"); + + // ... where `next` has the same generic parameter instantiations ... + const java_generic_typet &next_type = + require_type::require_java_generic_type( + next.type(), + {{require_type::type_argument_kindt::Var, "java::KeyValue::K"}, + {require_type::type_argument_kindt::Var, "java::KeyValue::V"}}); + REQUIRE(next_type.subtype().id() == ID_symbol); + const symbol_typet &next_symbol = to_symbol_type(next_type.subtype()); + REQUIRE( + symbol_table.lookup_ref(next_symbol.get_identifier()).name == + "java::KeyValue"); + + // ... and `reverse` has the same but in reversed order + const java_generic_typet &reverse_type = + require_type::require_java_generic_type( + reverse.type(), + {{require_type::type_argument_kindt::Var, "java::KeyValue::V"}, + {require_type::type_argument_kindt::Var, "java::KeyValue::K"}}); + REQUIRE(next_type.subtype().id() == ID_symbol); + const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype()); + REQUIRE( + symbol_table.lookup_ref(next_symbol.get_identifier()).name == + "java::KeyValue"); + } + WHEN("The class of type `MutuallyRecursiveGenerics` is created") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + const auto has_key_and_value_field = [&]( + const irep_idt &field, + const irep_idt &key_type, + const irep_idt &val_type) { + require_goto_statements::require_struct_component_assignment( + field, {}, "key", key_type, {}, entry_point_code); + require_goto_statements::require_struct_component_assignment( + field, {}, "value", val_type, {}, entry_point_code); + }; + + const irep_idt &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN( + "The Object has a field `example1` of type `KeyValue`") + { + const auto &example1_field = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "example1", + "java::KeyValue", + {}, + entry_point_code); + + THEN( + "Object 'example1' has field 'key' of type `String` and field `value` " + "of type `Integer`") + { + has_key_and_value_field( + example1_field, "java::java.lang.String", "java::java.lang.Integer"); + } + + THEN("`example1` has field next") + { + const auto &next_field = + require_goto_statements::require_struct_component_assignment( + example1_field, {}, "next", "java::KeyValue", {}, entry_point_code); + has_key_and_value_field( + next_field, "java::java.lang.String", "java::java.lang.Integer"); + } + THEN("`example1` has field `reverse`") + { + const auto &reverse_field = + require_goto_statements::require_struct_component_assignment( + example1_field, + {}, + "reverse", + "java::KeyValue", + {}, + entry_point_code); + has_key_and_value_field( + reverse_field, "java::java.lang.Integer", "java::java.lang.String"); + } + } + THEN( + "The Object has a field `example2` of type `Three`") + { + const auto &example2_field = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code); + + const auto has_x_e_u_fields = [&]( + const irep_idt &field, + const irep_idt &x_type, + const irep_idt &e_type, + const irep_idt &u_type) { + require_goto_statements::require_struct_component_assignment( + field, {}, "x", x_type, {}, entry_point_code); + require_goto_statements::require_struct_component_assignment( + field, {}, "e", e_type, {}, entry_point_code); + require_goto_statements::require_struct_component_assignment( + field, {}, "u", u_type, {}, entry_point_code); + }; + + THEN( + "Object 'example2' has field 'x' of type `Byte`, field `u` of type " + "`Character` and a field `e` of type `Integer`.") + { + has_x_e_u_fields( + example2_field, + "java::java.lang.Byte", + "java::java.lang.Character", + "java::java.lang.Integer"); + + THEN("`example2` has field `rotate`") + { + const auto &rotate_field = + require_goto_statements::require_struct_component_assignment( + example2_field, + {}, + "rotate", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + rotate_field, + "java::java.lang.Integer", + "java::java.lang.Byte", + "java::java.lang.Character"); + + THEN("`rotate` has itself a field `rotate` ... ") + { + const auto &rotate_rec_field = + require_goto_statements::require_struct_component_assignment( + rotate_field, + {}, + "rotate", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + rotate_rec_field, + "java::java.lang.Character", + "java::java.lang.Integer", + "java::java.lang.Byte"); + } + THEN("`rotate` has also a field `normal` ... ") + { + const auto &rotate_normal_field = + require_goto_statements::require_struct_component_assignment( + rotate_field, + {}, + "normal", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + rotate_normal_field, + "java::java.lang.Integer", + "java::java.lang.Byte", + "java::java.lang.Character"); + } + } + THEN("`example2` has field `normal`") + { + const auto &normal_field = + require_goto_statements::require_struct_component_assignment( + example2_field, + {}, + "normal", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + normal_field, + "java::java.lang.Byte", + "java::java.lang.Character", + "java::java.lang.Integer"); + THEN("`normal` has itself a field `normal`") + { + const auto &normal_rec_field = + require_goto_statements::require_struct_component_assignment( + example2_field, + {}, + "normal", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + normal_rec_field, + "java::java.lang.Byte", + "java::java.lang.Character", + "java::java.lang.Integer"); + } + THEN("`normal` has also a field `rotate`") + { + const auto &normal_rotate_field = + require_goto_statements::require_struct_component_assignment( + example2_field, + {}, + "rotate", + "java::Three", + {}, + entry_point_code); + has_x_e_u_fields( + normal_rotate_field, + "java::java.lang.Integer", + "java::java.lang.Byte", + "java::java.lang.Character"); + } + } + } + } + } + + // TODO: add test for TG-3828 +}