Java object factory: retain tagged types

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<java_class_typet>(subtype))
+  if(
+    const auto class_type =
+      type_try_dynamic_cast<java_class_typet>(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

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 \

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<codet> &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;

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")
         {

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 { }

jbmc/unit/java_bytecode/java_object_factory/HasArray.java

@@ -0,0 +1,8 @@
+
+public class HasArray {
+
+  public D[] ds;
+
+}
+
+class D { }

jbmc/unit/java_bytecode/java_object_factory/HasEnum.java

@@ -0,0 +1,8 @@
+
+public class HasEnum {
+
+  public E e;
+
+}
+
+enum E { x, y, z }

jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java

@@ -0,0 +1,16 @@
+
+public class HasGeneric {
+
+  public Generic<String> s;
+  public Generic<Integer> t;
+  public OtherGeneric<String> u;
+
+}
+
+class Generic<T> {
+  T t;
+}
+
+class OtherGeneric<T> {
+  Generic<T> gen;
+}

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;
+
+}

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