diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 668a3b2cc72..599190feced 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -249,9 +249,11 @@ void java_object_factoryt::gen_pointer_target_init( PRECONDITION(expr.type().id() == ID_pointer); PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); - if(target_type.id() == ID_struct) + const typet &followed_target_type = ns.follow(target_type); + + if(followed_target_type.id() == ID_struct) { - const auto &target_class_type = to_java_class_type(target_type); + const auto &target_class_type = to_java_class_type(followed_target_type); if(has_prefix(id2string(target_class_type.get_tag()), "java::array[")) { gen_nondet_array_init( @@ -565,10 +567,11 @@ void java_object_factoryt::gen_nondet_pointer_init( // When we visit for 2nd time a type AND the maximum depth is exceeded, we set // the pointer to NULL instead of recursively initializing the struct to which // it points. - const typet &subtype=ns.follow(pointer_type.subtype()); - if(subtype.id()==ID_struct) + const typet &subtype = pointer_type.subtype(); + const typet &followed_subtype = ns.follow(subtype); + if(followed_subtype.id() == ID_struct) { - const struct_typet &struct_type=to_struct_type(subtype); + const struct_typet &struct_type = to_struct_type(followed_subtype); const irep_idt &struct_tag=struct_type.get_tag(); // If this is a recursive type of some kind AND the depth is exceeded, set @@ -604,7 +607,9 @@ void java_object_factoryt::gen_nondet_pointer_init( // decide to do this for all types, we should do it here. // Note also that this logic is mirrored in // ci_lazy_methodst::initialize_instantiated_classes. - if(const auto class_type = type_try_dynamic_cast(subtype)) + if( + const auto class_type = + type_try_dynamic_cast(followed_subtype)) { if(class_type->get_base("java::java.lang.Enum") && !must_be_null) { @@ -1024,8 +1029,8 @@ void java_object_factoryt::gen_nondet_init( update_in_placet update_in_place, const source_locationt &location) { - const typet &type = override_type.has_value() ? ns.follow(*override_type) - : ns.follow(expr.type()); + const typet &type = override_type.has_value() ? *override_type : expr.type(); + const typet &followed_type = ns.follow(type); if(type.id()==ID_pointer) { @@ -1049,9 +1054,9 @@ void java_object_factoryt::gen_nondet_init( update_in_place, location); } - else if(type.id()==ID_struct) + else if(followed_type.id() == ID_struct) { - const struct_typet struct_type=to_struct_type(type); + const struct_typet struct_type = to_struct_type(followed_type); // If we are about to initialize a generic class (as a superclass object // for a different object), add its concrete types to the map and delete diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 6c60e82cb23..a9d0d5ad840 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -44,6 +44,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ java_bytecode/java_bytecode_parser/parse_java_field.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ + java_bytecode/java_object_factory/struct_tag_types.cpp \ java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 4e2ef931915..7b1f24fb4f5 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -315,6 +315,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( const std::vector &entry_point_instructions, const symbol_tablet &symbol_table) { + namespacet ns(symbol_table); + // First we need to find the assignments to the component belonging to // the structure_name object const auto &component_assignments = @@ -361,14 +363,13 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( // After we have found the declaration of the final assignment's // right hand side, then we want to identify that the type // is the one we expect, e.g.: - // struct java.lang.Integer { __CPROVER_string @class_identifier; } - // tmp_object_factory$2; + // struct java.lang.Integer tmp_object_factory$2; const auto &component_declaration = require_goto_statements::require_declaration_of_name( component_tmp_name, entry_point_instructions); - REQUIRE(component_declaration.symbol().type().id() == ID_struct); + REQUIRE(component_declaration.symbol().type().id() == ID_struct_tag); const auto &component_struct = - to_struct_type(component_declaration.symbol().type()); + ns.follow_tag(to_struct_tag_type(component_declaration.symbol().type())); REQUIRE(component_struct.get(ID_name) == component_type_name); return component_tmp_name; diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 5d803a770d8..6ea76302000 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -316,9 +316,9 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper"); THEN("Object 'v' has field 'field' of type IWrapper") { @@ -366,9 +366,9 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper"); THEN( "Object 'v' has field 'field' of type Object (upper bound of the " @@ -416,11 +416,11 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); REQUIRE( - tmp_object_struct.get_tag() == - "GenericFields$GenericInnerOuter$Outer"); + tmp_object_struct_tag.get_identifier() == + "java::GenericFields$GenericInnerOuter$Outer"); THEN("Object 'v' has field 'field' of type InnerClass") { @@ -481,11 +481,11 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); REQUIRE( - tmp_object_struct.get_tag() == - "GenericFields$GenericRewriteParameter$A"); + tmp_object_struct_tag.get_identifier() == + "java::GenericFields$GenericRewriteParameter$A"); THEN("Object 'v' has field 'value' of type Integer") { diff --git a/jbmc/unit/java_bytecode/java_object_factory/A.class b/jbmc/unit/java_bytecode/java_object_factory/A.class new file mode 100644 index 00000000000..e0f4c1848c9 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/A.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/A.java b/jbmc/unit/java_bytecode/java_object_factory/A.java new file mode 100644 index 00000000000..b0118eb94f5 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/A.java @@ -0,0 +1,11 @@ + +public class A { + + public B b; + public C c; + +} + +class B { } + +class C { } diff --git a/jbmc/unit/java_bytecode/java_object_factory/B.class b/jbmc/unit/java_bytecode/java_object_factory/B.class new file mode 100644 index 00000000000..e5654ceb07b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/B.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/C.class b/jbmc/unit/java_bytecode/java_object_factory/C.class new file mode 100644 index 00000000000..fda468de8d2 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/C.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/D.class b/jbmc/unit/java_bytecode/java_object_factory/D.class new file mode 100644 index 00000000000..06526bbfa08 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/D.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/E.class b/jbmc/unit/java_bytecode/java_object_factory/E.class new file mode 100644 index 00000000000..4c34c057652 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/E.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/Generic.class b/jbmc/unit/java_bytecode/java_object_factory/Generic.class new file mode 100644 index 00000000000..ea5c92e890c Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/Generic.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasArray.class b/jbmc/unit/java_bytecode/java_object_factory/HasArray.class new file mode 100644 index 00000000000..8b3a1c25c60 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/HasArray.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasArray.java b/jbmc/unit/java_bytecode/java_object_factory/HasArray.java new file mode 100644 index 00000000000..6e5f5f8d215 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasArray.java @@ -0,0 +1,8 @@ + +public class HasArray { + + public D[] ds; + +} + +class D { } diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasEnum.class b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.class new file mode 100644 index 00000000000..1b87ff41d4a Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java new file mode 100644 index 00000000000..5e2c97ab74b --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java @@ -0,0 +1,8 @@ + +public class HasEnum { + + public E e; + +} + +enum E { x, y, z } diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class new file mode 100644 index 00000000000..dfae98673cc Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java new file mode 100644 index 00000000000..894c7cd04f2 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java @@ -0,0 +1,16 @@ + +public class HasGeneric { + + public Generic s; + public Generic t; + public OtherGeneric u; + +} + +class Generic { + T t; +} + +class OtherGeneric { + Generic gen; +} diff --git a/jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class b/jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class new file mode 100644 index 00000000000..a46150cab26 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/Root.class b/jbmc/unit/java_bytecode/java_object_factory/Root.class new file mode 100644 index 00000000000..6115bcba8c1 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_object_factory/Root.class differ diff --git a/jbmc/unit/java_bytecode/java_object_factory/Root.java b/jbmc/unit/java_bytecode/java_object_factory/Root.java new file mode 100644 index 00000000000..b1db5c85737 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/Root.java @@ -0,0 +1,12 @@ + +public class Root { + + // This one isn't used in the tests; it just references other classes + // to get them loaded. + + A a; + HasArray ha; + HasEnum he; + HasGeneric hg; + +} diff --git a/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt b/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt index c4380fa26bd..cbdc5447cf2 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt @@ -1,5 +1,6 @@ java_bytecode java_object_factory +java-testing-utils langapi # should go away testing-utils util diff --git a/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp b/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp new file mode 100644 index 00000000000..3e20cccac6e --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp @@ -0,0 +1,214 @@ +/*******************************************************************\ + +Module: Unit tests for Java-object-factory's treatment of tag types + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +#include + +static bool is_decl_with_struct_tag(const codet &code, const irep_idt &id) +{ + if(code.get_statement() != ID_decl) + return false; + + const typet &decl_type = to_code_decl(code).symbol().type(); + return decl_type.id() == ID_struct_tag && + to_struct_tag_type(decl_type).get_identifier() == id; +} + +static bool is_decl_of_type(const codet &code, const typet &type) +{ + return code.get_statement() == ID_decl && + to_code_decl(code).symbol().type() == type; +} + +static bool +contains(const exprt &expr, std::function predicate) +{ + return std::any_of(expr.depth_begin(), expr.depth_end(), predicate); +} + +static bool +contains(const codet &code, std::function predicate) +{ + std::vector statements = + require_goto_statements::get_all_statements(code); + return std::any_of(statements.begin(), statements.end(), predicate); +} + +static bool +contains(const typet &type, std::function predicate) +{ + if(predicate(type)) + return true; + + if(type.has_subtypes()) + { + for(const auto &subtype : to_type_with_subtypes(type).subtypes()) + { + if(contains(subtype, predicate)) + return true; + } + } + + return false; +} + +static bool contains_decl_of_type(const codet &code, const typet &type) +{ + return contains(code, [&type](const codet &subcode) { + return is_decl_of_type(subcode, type); + }); +} + +static bool contains_decl_with_struct_tag(const codet &code, const irep_idt &id) +{ + return contains(code, [&id](const codet &subcode) { + return is_decl_with_struct_tag(subcode, id); + }); +} + +static bool uses_raw_struct_types(const typet &type) +{ + return contains( + type, [](const typet &subtype) { return subtype.id() == ID_struct; }); +} + +static bool uses_raw_struct_types(const exprt &expr) +{ + return contains(expr, [](const exprt &subexpr) { + return uses_raw_struct_types(subexpr.type()); + }); +} + +code_blockt +initialise_nondet_object_of_type(const typet &type, symbol_tablet &symbol_table) +{ + code_blockt created_code; + java_object_factory_parameterst parameters; + select_pointer_typet pointer_selector; + + object_factory( + type, + "root", + created_code, + symbol_table, + parameters, + lifetimet::AUTOMATIC_LOCAL, + source_locationt(), + pointer_selector); + + return created_code; +} + +SCENARIO( + "java_object_factory_tag_types", + "[core][java_bytecode][java_object_factory]") +{ + GIVEN("Some classes with fields") + { + register_language(new_java_bytecode_language); + symbol_tablet symbol_table = + load_java_class("Root", "./java_bytecode/java_object_factory"); + + WHEN("Creating a nondet 'A' object") + { + struct_tag_typet A_type("java::A"); + struct_tag_typet B_type("java::B"); + struct_tag_typet C_type("java::C"); + + const auto a_pointer = java_reference_type(A_type); + code_blockt created_code = + initialise_nondet_object_of_type(a_pointer, symbol_table); + + THEN("An A, a B and a C object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, A_type)); + REQUIRE(contains_decl_of_type(created_code, B_type)); + REQUIRE(contains_decl_of_type(created_code, C_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasArray' object") + { + struct_tag_typet HasArray_type("java::HasArray"); + struct_tag_typet D_type("java::D"); + + const auto HasArray_pointer = java_reference_type(HasArray_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasArray_pointer, symbol_table); + + THEN("A HasArray object should be created") + { + REQUIRE(contains_decl_of_type(created_code, HasArray_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasEnum' object") + { + struct_tag_typet HasEnum_type("java::HasEnum"); + struct_tag_typet E_type("java::E"); + + const auto HasEnum_pointer = java_reference_type(HasEnum_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasEnum_pointer, symbol_table); + + THEN("A HasEnum object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, HasEnum_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasGeneric' object") + { + struct_tag_typet HasGeneric_type("java::HasGeneric"); + irep_idt generic_id = "java::Generic"; + irep_idt other_generic_id = "java::OtherGeneric"; + + const auto HasGeneric_pointer = java_reference_type(HasGeneric_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasGeneric_pointer, symbol_table); + + THEN("An HasGeneric, Generic and OtherGeneric object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, HasGeneric_type)); + // These ones are just checked for a tag rather than a full type because + // the tags are decorated with generic information, and I just want to + // check they (a) are created and (b) don't use expanded types, rather + // than verifying their full structure. + REQUIRE(contains_decl_with_struct_tag(created_code, generic_id)); + REQUIRE(contains_decl_with_struct_tag(created_code, other_generic_id)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + } +}