remove uses of typet::subtype() const

Author: kroening

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -174,7 +174,7 @@ void ci_lazy_methods_neededt::gather_field_types(
         gather_field_types(field.type(), ns);
       else if(field.type().id() == ID_pointer)
       {
-        if(field.type().subtype().id() == ID_struct_tag)
+        if(to_pointer_type(field.type()).base_type().id() == ID_struct_tag)
         {
           add_all_needed_classes(to_pointer_type(field.type()));
         }
@@ -186,7 +186,7 @@ void ci_lazy_methods_neededt::gather_field_types(
           // We should therefore only be skipping pointers such as the uint16t*
           // in our internal String representation.
           INVARIANT(
-            field.type().subtype().id() != ID_struct,
+            to_pointer_type(field.type()).base_type().id() != ID_struct,
             "struct types should be referred to by symbol at this stage");
         }
       }

jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -27,9 +27,10 @@ static bool is_nondet_pointer(exprt expr)
   // and we do not want to convert it. If the type is a ptr-to-void or a
   // function pointer then we also do not want to convert it.
   const typet &type = expr.type();
-  const bool non_void_non_function_pointer = type.id() == ID_pointer &&
-                                             type.subtype().id() != ID_empty &&
-                                             type.subtype().id() != ID_code;
+  const bool non_void_non_function_pointer =
+    type.id() == ID_pointer &&
+    to_pointer_type(type).base_type().id() != ID_empty &&
+    to_pointer_type(type).base_type().id() != ID_code;
   return can_cast_expr<side_effect_expr_nondett>(expr) &&
          non_void_non_function_pointer;
 }

jbmc/src/java_bytecode/expr2java.cpp

@@ -340,13 +340,13 @@ std::string expr2javat::convert_java_new(const exprt &src)
       convert(static_cast<const exprt &>(src.find(ID_size)));
 
     dest+=' ';
-    dest+=convert(src.type().subtype());
+    dest += convert(to_pointer_type(src.type()).base_type());
     dest+='[';
     dest+=tmp_size;
     dest+=']';
   }
   else
-    dest="new "+convert(src.type().subtype());
+    dest = "new " + convert(to_pointer_type(src.type()).base_type());
 
   return dest;
 }

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -102,7 +102,7 @@ java_bytecode_parse_treet::find_annotation(
     [&annotation_type_name](const annotationt &annotation) {
       if(annotation.type.id() != ID_pointer)
         return false;
-      const typet &type = annotation.type.subtype();
+      const typet &type = to_pointer_type(annotation.type).base_type();
       return type.id() == ID_struct_tag &&
              to_struct_tag_type(type).get_identifier() == annotation_type_name;
     });

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -600,7 +600,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
       get_class_refs_rec(c.type());
   }
   else if(src.id()==ID_pointer)
-    get_class_refs_rec(src.subtype());
+    get_class_refs_rec(to_pointer_type(src).base_type());
 }
 
 /// For each of the given annotations, get a reference to its class and

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1381,16 +1381,16 @@ code_blockt gen_nondet_array_init(
   const size_t max_nondet_array_length)
 {
   PRECONDITION(expr.type().id() == ID_pointer);
-  PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
+  PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_struct_tag);
   PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
   code_blockt statements;
 
   const namespacet ns(symbol_table);
-  const typet &type = ns.follow(expr.type().subtype());
+  const typet &type = ns.follow(to_pointer_type(expr.type()).base_type());
   const struct_typet &struct_type = to_struct_type(type);
-  const typet &element_type =
-    static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
+  const typet &element_type = static_cast<const typet &>(
+    to_pointer_type(expr.type()).base_type().find(ID_element_type));
 
   auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
 

jbmc/src/java_bytecode/java_qualifiers.cpp

@@ -97,7 +97,9 @@ std::string java_qualifierst::as_string() const
   for(const java_annotationt &annotation : annotations)
   {
     out << '@';
-    out << annotation.get_type().subtype().get(ID_identifier);
+    out << to_reference_type(annotation.get_type())
+             .base_type()
+             .get(ID_identifier);
 
     if(!annotation.get_values().empty())
     {

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -556,7 +556,8 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
   code_blockt tmp;
-  allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
+  allocate_objects.allocate_dynamic_object(
+    tmp, str, to_reference_type(str.type()).base_type());
   allocate_objects.declare_created_symbols(code);
   code.append(tmp);
 

jbmc/src/java_bytecode/lambda_synthesis.cpp

@@ -586,7 +586,8 @@ static symbol_exprt instantiate_new_object(
     "REF_NewInvokeSpecial lambda must refer to a constructor");
   const auto &created_type = method_type.parameters().at(0).type();
   irep_idt created_class =
-    to_struct_tag_type(created_type.subtype()).get_identifier();
+    to_struct_tag_type(to_reference_type(created_type).base_type())
+      .get_identifier();
 
   // Call static init if it exists:
   irep_idt static_init_name = clinit_wrapper_name(created_class);
@@ -612,10 +613,11 @@ static symbol_exprt instantiate_new_object(
 
 /// If \p maybe_boxed_type is a boxed primitive return its unboxing method;
 /// otherwise return empty.
-static optionalt<irep_idt> get_unboxing_method(const typet &maybe_boxed_type)
+static optionalt<irep_idt>
+get_unboxing_method(const pointer_typet &maybe_boxed_type)
 {
   const irep_idt &boxed_type_id =
-    to_struct_tag_type(maybe_boxed_type.subtype()).get_identifier();
+    to_struct_tag_type(maybe_boxed_type.base_type()).get_identifier();
   const java_boxed_type_infot *boxed_type_info =
     get_boxed_type_info_by_name(boxed_type_id);
   return boxed_type_info ? boxed_type_info->unboxing_function_name
@@ -633,7 +635,8 @@ exprt make_function_expr(
   if(!method_type.has_this())
     return function_symbol.symbol_expr();
   const irep_idt &declared_on_class_id =
-    to_struct_tag_type(method_type.get_this()->type().subtype())
+    to_struct_tag_type(
+      to_pointer_type(method_type.get_this()->type()).base_type())
       .get_identifier();
   const auto &this_symbol = symbol_table.lookup_ref(declared_on_class_id);
   if(to_java_class_type(this_symbol.type).get_final())
@@ -717,7 +720,8 @@ exprt box_or_unbox_type_if_necessary(
 
   const irep_idt transform_function_id =
     original_is_pointer
-      ? get_unboxing_method(original_type) // Use static type if known
+      ? get_unboxing_method(
+          to_pointer_type(original_type)) // Use static type if known
           .value_or(primitive_type_info->unboxing_function_name)
       : primitive_type_info->boxed_type_factory_method;
 

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -99,7 +99,8 @@ void java_simple_method_stubst::create_method_stub_at(
 
   namespacet ns(symbol_table);
 
-  const auto &expected_base = ns.follow(expected_type.subtype());
+  const auto &expected_base =
+    ns.follow(to_pointer_type(expected_type).base_type());
   if(expected_base.id() != ID_struct)
     return;
 

src/cpp/expr2cpp.cpp

@@ -258,7 +258,9 @@ std::string expr2cppt::convert_rec(
     dest += "> " + convert(to_template_type(src).subtype());
     return dest;
   }
-  else if(src.id()==ID_pointer && src.subtype().id()==ID_nullptr)
+  else if(
+    src.id() == ID_pointer &&
+    to_pointer_type(src).base_type().id() == ID_nullptr)
   {
     return "std::nullptr_t";
   }
@@ -270,9 +272,11 @@ std::string expr2cppt::convert_rec(
 
     std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
 
-    if(src.subtype().id()==ID_code)
+    const auto &base_type = to_pointer_type(src).base_type();
+
+    if(base_type.id() == ID_code)
     {
-      const code_typet &code_type = to_code_type(src.subtype());
+      const code_typet &code_type = to_code_type(base_type);
       const typet &return_type = code_type.return_type();
       dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
 
@@ -292,7 +296,7 @@ std::string expr2cppt::convert_rec(
       dest+=d;
     }
     else
-      dest=convert_rec(src.subtype(), c_qualifierst(), "")+" "+dest+d;
+      dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
 
     return dest;
   }
@@ -375,13 +379,13 @@ std::string expr2cppt::convert_cpp_new(const exprt &src)
       convert(static_cast<const exprt &>(src.find(ID_size)));
 
     dest+=' ';
-    dest+=convert(src.type().subtype());
+    dest += convert(to_pointer_type(src.type()).base_type());
     dest+='[';
     dest+=tmp_size;
     dest+=']';
   }
   else
-    dest="new "+convert(src.type().subtype());
+    dest = "new " + convert(to_pointer_type(src.type()).base_type());
 
   return dest;
 }

src/goto-programs/string_abstraction.cpp

@@ -46,7 +46,8 @@ bool string_abstractiont::build_wrap(
   if(
     dest.type() != a_t &&
     !(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
-      dest.type().subtype() == a_t.subtype()))
+      to_array_type(dest.type()).element_type() ==
+        to_pointer_type(a_t).base_type()))
   {
     messaget log{message_handler};
     log.warning() << "warning: inconsistent abstract type for "
@@ -59,7 +60,8 @@ bool string_abstractiont::build_wrap(
 
 bool string_abstractiont::is_ptr_string_struct(const typet &type) const
 {
-  return type.id() == ID_pointer && type.subtype() == string_struct;
+  return type.id() == ID_pointer &&
+         to_pointer_type(type).base_type() == string_struct;
 }
 
 static inline bool is_ptr_argument(const typet &type)
@@ -340,10 +342,16 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
 {
   if(symbol.type.id() == ID_array || symbol.type.id() == ID_pointer)
   {
-    const typet &source_subt =
-      is_ptr_string_struct(symbol.type) ? source_type : source_type.subtype();
+    const typet &source_subt = is_ptr_string_struct(symbol.type)
+                                 ? source_type
+                                 : to_type_with_subtype(source_type).subtype();
     symbol_exprt sym_expr = add_dummy_symbol_and_value(
-      dest, ref_instr, symbol, irep_idt(), symbol.type.subtype(), source_subt);
+      dest,
+      ref_instr,
+      symbol,
+      irep_idt(),
+      to_type_with_subtype(symbol.type).subtype(),
+      source_subt);
 
     if(symbol.type.id() == ID_array)
       return array_of_exprt(sym_expr, to_array_type(symbol.type));
@@ -435,7 +443,8 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
 
   // set the value - may be nil
   if(
-    source_type.id() == ID_array && is_char_type(source_type.subtype()) &&
+    source_type.id() == ID_array &&
+    is_char_type(to_array_type(source_type).element_type()) &&
     type == string_struct)
   {
     new_symbol.value = struct_exprt(
@@ -570,7 +579,8 @@ void string_abstractiont::abstract_function_call(
         abstract_type.id()==ID_pointer)
     {
       INVARIANT(
-        str_args.back().type().subtype() == abstract_type.subtype(),
+        to_array_type(str_args.back().type()).element_type() ==
+          to_pointer_type(abstract_type).base_type(),
         "argument array type differs from formal parameter pointer type");
 
       index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
@@ -712,11 +722,13 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
   if(type.id() == ID_array || type.id() == ID_pointer)
   {
     // char* or void* or char[]
-    if(is_char_type(type.subtype()) || type.subtype().id() == ID_empty)
+    const auto &subtype = to_type_with_subtype(type);
+
+    if(is_char_type(subtype) || subtype.id() == ID_empty)
       map_entry.first->second=pointer_type(string_struct);
     else
     {
-      const typet &subt = build_abstraction_type_rec(type.subtype(), known);
+      const typet &subt = build_abstraction_type_rec(subtype, known);
       if(!subt.is_nil())
       {
         if(type.id() == ID_array)
@@ -793,7 +805,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
 
     return dest.type() != abstract_type ||
            (dest.type().id() == ID_array && abstract_type.id() == ID_pointer &&
-            dest.type().subtype() == abstract_type.subtype());
+            to_array_type(dest.type()).element_type() ==
+              to_pointer_type(abstract_type).base_type());
   }
 
   if(object.id()==ID_string_constant)
@@ -807,7 +820,9 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
     return build_symbol_constant(str_len, str_len+1, dest);
   }
 
-  if(object.id()==ID_array && is_char_type(object.type().subtype()))
+  if(
+    object.id() == ID_array &&
+    is_char_type(to_array_type(object.type()).element_type()))
     return build_array(to_array_expr(object), dest, write);
 
   // other constants aren't useful
@@ -926,8 +941,9 @@ bool string_abstractiont::build_pointer(const exprt &object,
     dest=address_of_exprt(dest);
     return false;
   }
-  else if(ptr.pointer.id()==ID_symbol &&
-      is_char_type(object.type().subtype()))
+  else if(
+    ptr.pointer.id() == ID_symbol &&
+    is_char_type(to_pointer_type(object.type()).base_type()))
     // recursive call; offset will be handled by pointer_offset in SIZE/LENGTH
     // checks
     return build_wrap(ptr.pointer, dest, write);

src/goto-programs/string_instrumentation.cpp

@@ -882,10 +882,11 @@ void string_instrumentationt::invalidate_buffer(
   check->complete_goto(exit);
 
   const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
-  const dereference_exprt deref(b_plus_i, buf_type.subtype());
+  const dereference_exprt deref(
+    b_plus_i, to_type_with_subtype(buf_type).subtype());
 
   const side_effect_expr_nondett nondet(
-    buf_type.subtype(), target->source_location());
+    to_type_with_subtype(buf_type).subtype(), target->source_location());
 
   invalidate->code_nonconst() = code_assignt(deref, nondet);
 }

src/util/type.h

@@ -45,13 +45,15 @@ class typet:public irept
   }
 #endif
 
+protected:
   const typet &subtype() const
   {
     if(get_sub().empty())
       return static_cast<const typet &>(get_nil_irep());
     return static_cast<const typet &>(get_sub().front());
   }
 
+public:
   typet &subtype()
   {
     subt &sub=get_sub();