Merge pull request #6580 from diffblue/pointer_base_type

introduce pointer_typet::base_type()

Author: tautschnig

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

@@ -481,7 +481,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 =
@@ -500,7 +500,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);
@@ -1020,7 +1021,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,