introduce pointer_typet::base_type()

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -66,8 +66,8 @@ static java_class_typet
 followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
 {
   const pointer_typet &pointer_type = to_pointer_type(expr.type());
-  const java_class_typet &java_class_type =
-    to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype()));
+  const java_class_typet &java_class_type = to_java_class_type(
+    namespacet{symbol_table}.follow(pointer_type.base_type()));
   return java_class_type;
 }
 
@@ -602,7 +602,7 @@ static code_with_references_listt assign_non_enum_pointer_from_json(
   code_blockt output_code;
   exprt dereferenced_symbol_expr =
     info.allocate_objects.allocate_dynamic_object(
-      output_code, expr, to_pointer_type(expr.type()).subtype());
+      output_code, expr, to_pointer_type(expr.type()).base_type());
   for(codet &code : output_code.statements())
     result.add(std::move(code));
   result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
@@ -754,7 +754,7 @@ static get_or_create_reference_resultt get_or_create_reference(
     {
       code_blockt block;
       reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
-        block, expr, pointer_type.subtype());
+        block, expr, pointer_type.base_type());
       code.add(block);
     }
     auto iterator_inserted_pair = info.references.insert({id, reference});

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -117,14 +117,14 @@ void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(
   const pointer_typet &pointer_type,
   const namespacet &ns)
 {
-  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
+  const auto &class_type = to_struct_tag_type(pointer_type.base_type());
   const auto &param_classid = class_type.get_identifier();
 
   // Note here: different arrays may have different element types, so we should
   // explore again even if we've seen this classid before in the array case.
   if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
   {
-    gather_field_types(pointer_type.subtype(), ns);
+    gather_field_types(pointer_type.base_type(), ns);
   }
 
   if(is_java_generic_type(pointer_type))
@@ -159,7 +159,7 @@ void ci_lazy_methods_neededt::gather_field_types(
         java_array_element_type(to_struct_tag_type(class_type));
       if(
         element_type.id() == ID_pointer &&
-        element_type.subtype().id() != ID_empty)
+        to_pointer_type(element_type).base_type().id() != ID_empty)
       {
         // This is a reference array -- mark its element type available.
         add_all_needed_classes(to_pointer_type(element_type));

jbmc/src/java_bytecode/code_with_references.cpp

@@ -20,8 +20,8 @@ codet allocate_array(
 {
   pointer_typet pointer_type = to_pointer_type(expr.type());
   const auto &element_type =
-    java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
-  pointer_type.subtype().set(ID_element_type, element_type);
+    java_array_element_type(to_struct_tag_type(pointer_type.base_type()));
+  pointer_type.base_type().set(ID_element_type, element_type);
   side_effect_exprt java_new_array{
     ID_java_new_array, {array_length_expr}, pointer_type, loc};
   return code_frontend_assignt{expr, java_new_array, loc};

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp

@@ -18,7 +18,7 @@ void generic_parameter_specialization_map_keyst::insert(
     return;
   // The supplied type must be the full type of the pointer's subtype
   PRECONDITION(
-    pointer_type.subtype().get(ID_identifier) ==
+    pointer_type.base_type().get(ID_identifier) ==
     pointer_subtype_struct.get(ID_name));
 
   // If the pointer points to:

jbmc/src/java_bytecode/goto_check_java.cpp

@@ -1148,7 +1148,7 @@ bool goto_check_javat::check_rec_member(const member_exprt &member)
   if(member_offset_opt.has_value())
   {
     pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-    new_pointer_type.subtype() = member.type();
+    new_pointer_type.base_type() = member.type();
 
     const exprt char_pointer = typecast_exprt::conditional_cast(
       deref.pointer(), pointer_type(char_type()));

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -412,7 +412,7 @@ static void instrument_get_monitor_count(
 
   const namespacet ns(symbol_table);
   const auto &followed_type =
-    ns.follow(to_pointer_type(f_code.arguments()[0].type()).subtype());
+    ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type());
   const auto &object_type = to_struct_type(followed_type);
   code_assignt code_assign(
     f_code.lhs(),

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1235,7 +1235,7 @@ void mark_java_implicitly_generic_class_type(
                                 id2string(strip_java_namespace_prefix(
                                   outer_generic_type_parameter.get_name()));
           java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
-            outer_generic_type_parameter.subtype());
+            outer_generic_type_parameter.base_type());
           bound.type_variable_ref().set_identifier(identifier);
           implicit_generic_type_parameters.emplace_back(identifier, bound);
         }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2711,10 +2711,10 @@ void java_bytecode_convert_methodt::convert_getstatic(
     else if(arg0.type().id() == ID_pointer)
     {
       const auto &pointer_type = to_pointer_type(arg0.type());
-      if(pointer_type.subtype().id() == ID_struct_tag)
+      if(pointer_type.base_type().id() == ID_struct_tag)
       {
         needed_lazy_methods->add_needed_class(
-          to_struct_tag_type(pointer_type.subtype()).get_identifier());
+          to_struct_tag_type(pointer_type.base_type()).get_identifier());
       }
     }
     else if(is_assertions_disabled_field)

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1486,7 +1486,7 @@ bool java_bytecode_languaget::convert_single_method_code(
       // TODO(tkiley): investigation
       namespacet ns{symbol_table};
       const java_class_typet &underlying_type =
-        to_java_class_type(ns.follow(pointer_return_type->subtype()));
+        to_java_class_type(ns.follow(pointer_return_type->base_type()));
 
       if(!underlying_type.is_abstract())
         needed_lazy_methods->add_all_needed_classes(*pointer_return_type);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -480,7 +480,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   const namespacet ns(symbol_table);
-  const typet &subtype = pointer_type.subtype();
+  const typet &subtype = pointer_type.base_type();
   const typet &followed_subtype = ns.follow(subtype);
   PRECONDITION(followed_subtype.id() == ID_struct);
   const pointer_typet &replacement_pointer_type =
@@ -499,7 +499,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
-      replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
+      replacement_pointer_type,
+      ns.follow(replacement_pointer_type.base_type()));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
       assignments, lifetime, replacement_pointer_type, depth, location);
@@ -1019,7 +1020,7 @@ void java_object_factoryt::gen_nondet_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
-      pointer_type, ns.follow(pointer_type.subtype()));
+      pointer_type, ns.follow(pointer_type.base_type()));
 
     gen_nondet_pointer_init(
       assignments,

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -82,19 +82,21 @@ exprt make_clean_pointer_cast(
     return ptr;
 
   if(
-    ptr.type().subtype() == java_void_type() ||
-    target_type.subtype() == java_void_type())
+    to_pointer_type(ptr.type()).base_type() == java_void_type() ||
+    target_type.base_type() == java_void_type())
+  {
     return typecast_exprt(ptr, target_type);
+  }
 
-  const typet &target_base=ns.follow(target_type.subtype());
+  const typet &target_base = ns.follow(target_type.base_type());
 
   exprt bare_ptr=ptr;
   while(bare_ptr.id()==ID_typecast)
   {
     assert(
       bare_ptr.type().id()==ID_pointer &&
       "Non-pointer in make_clean_pointer_cast?");
-    if(bare_ptr.type().subtype() == java_void_type())
+    if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
       bare_ptr = to_typecast_expr(bare_ptr).op();
   }
 

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -64,8 +64,8 @@ bool java_string_library_preprocesst::is_java_string_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_type(base_type);
   }
   return false;
 }
@@ -95,8 +95,8 @@ bool java_string_library_preprocesst::is_java_string_builder_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_builder_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_builder_type(base_type);
   }
   return false;
 }
@@ -118,8 +118,8 @@ bool java_string_library_preprocesst::is_java_string_buffer_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_buffer_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_buffer_type(base_type);
   }
   return false;
 }
@@ -141,8 +141,8 @@ bool java_string_library_preprocesst::is_java_char_sequence_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_char_sequence_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_char_sequence_type(base_type);
   }
   return false;
 }
@@ -164,8 +164,8 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_char_array_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_char_array_type(base_type);
   }
   return false;
 }

jbmc/src/java_bytecode/java_types.cpp

@@ -1049,9 +1049,9 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
   const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
   INVARIANT(
     type.get_identifier() ==
-      to_struct_tag_type(gen_base_type.subtype()).get_identifier(),
+      to_struct_tag_type(gen_base_type.base_type()).get_identifier(),
     "identifier of " + type.pretty() + "\n and identifier of type " +
-      gen_base_type.subtype().pretty() +
+      gen_base_type.base_type().pretty() +
       "\ncreated by java_type_from_string for " + base_ref +
       " should be equal");
   generic_types().insert(

jbmc/src/java_bytecode/java_types.h

@@ -1056,7 +1056,7 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
   PRECONDITION(index<gen_types.size());
   const java_generic_parametert &gen_type=gen_types[index];
 
-  return gen_type.subtype();
+  return gen_type.base_type();
 }
 
 /// Type to hold a Java class that is implicitly generic, e.g., an inner

jbmc/src/java_bytecode/java_utils.cpp

@@ -273,7 +273,7 @@ pointer_typet pointer_to_replacement_type(
   const pointer_typet &given_pointer_type,
   const java_class_typet &replacement_class_type)
 {
-  if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
+  if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
   {
     struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
     return pointer_type(struct_tag_subtype);

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -59,21 +59,21 @@ pointer_typet select_pointer_typet::specialize_generics(
     }
   }
 
-  auto subtype =
-    type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
-  if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
+  auto base_type =
+    type_try_dynamic_cast<struct_tag_typet>(pointer_type.base_type());
+  if(base_type != nullptr && is_java_array_tag(base_type->get_identifier()))
   {
     // if the pointer is an array, recursively specialize its element type
     const auto *array_element_type =
-      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
+      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*base_type));
     if(array_element_type == nullptr)
       return pointer_type;
 
     const pointer_typet &new_array_type = specialize_generics(
       *array_element_type, generic_parameter_specialization_map);
 
     pointer_typet replacement_array_type = java_array_type('a');
-    replacement_array_type.subtype().set(ID_element_type, new_array_type);
+    replacement_array_type.base_type().set(ID_element_type, new_array_type);
     return replacement_array_type;
   }
 

jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp

@@ -319,7 +319,7 @@ 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_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
 
         THEN("Object 'v' has field 'field' of type IWrapper")
@@ -369,7 +369,7 @@ 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_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
 
         THEN(
@@ -419,7 +419,7 @@ 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_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(
           tmp_object_struct_tag.get_identifier() ==
           "java::GenericFields$GenericInnerOuter$Outer");
@@ -484,7 +484,7 @@ 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_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(
           tmp_object_struct_tag.get_identifier() ==
           "java::GenericFields$GenericRewriteParameter$A");

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

@@ -48,7 +48,7 @@ SCENARIO(
          {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
 
     // ... which is of type `KeyValue` ...
-    const auto &subtype = gen_type.subtype();
+    const auto &subtype = gen_type.base_type();
     const auto &key_value =
       symbol_table.lookup_ref(to_struct_tag_type(subtype).get_identifier());
     REQUIRE(key_value.type.id() == ID_struct);
@@ -66,9 +66,9 @@ SCENARIO(
         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_struct_tag);
+    REQUIRE(next_type.base_type().id() == ID_struct_tag);
     const struct_tag_typet &next_symbol =
-      to_struct_tag_type(next_type.subtype());
+      to_struct_tag_type(next_type.base_type());
     REQUIRE(
       symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
       "java::KeyValue");
@@ -79,9 +79,9 @@ SCENARIO(
         reverse.type(),
         {{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
          {require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
-    REQUIRE(reverse_type.subtype().id() == ID_struct_tag);
+    REQUIRE(reverse_type.base_type().id() == ID_struct_tag);
     const struct_tag_typet &reverse_symbol =
-      to_struct_tag_type(reverse_type.subtype());
+      to_struct_tag_type(reverse_type.base_type());
     REQUIRE(
       symbol_table.lookup_ref(reverse_symbol.get_identifier()).name ==
       "java::KeyValue");

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp

@@ -72,7 +72,7 @@ void validate_lambda_assignment(
     require_type::require_pointer(side_effect_expr.type(), {});
 
   const struct_tag_typet &lambda_implementor_type =
-    require_type::require_struct_tag(lambda_temp_type.subtype());
+    require_type::require_struct_tag(lambda_temp_type.base_type());
 
   const irep_idt &tmp_class_identifier =
     lambda_implementor_type.get_identifier();

jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp

@@ -37,7 +37,7 @@ SCENARIO(
           field_t.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t_subtype =
-        to_struct_tag_type(field_t_pointer.subtype());
+        to_struct_tag_type(field_t_pointer.base_type());
       const struct_typet &subtype_type = to_struct_type(
         new_symbol_table.lookup_ref(field_t_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_type));
@@ -63,7 +63,7 @@ SCENARIO(
           field_t2.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t2_subtype =
-        to_struct_tag_type(field_t2_pointer.subtype());
+        to_struct_tag_type(field_t2_pointer.base_type());
       const struct_typet &subtype_struct = to_struct_type(
         new_symbol_table.lookup_ref(field_t2_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_struct));
@@ -91,7 +91,7 @@ SCENARIO(
           field_t3.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t3_subtype =
-        to_struct_tag_type(field_t3_pointer.subtype());
+        to_struct_tag_type(field_t3_pointer.base_type());
       const struct_typet &subtype_struct = to_struct_type(
         new_symbol_table.lookup_ref(field_t3_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_struct));