remove usage of typet::subtype()

This commit replaces invocations of typet::subtype() by the appropriate
methods offered by the more specific types, e.g., pointer_typet,
array_typet, and so on.

Author: kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2431,8 +2431,8 @@ void java_bytecode_convert_methodt::convert_athrow(
 {
   if(
     assert_no_exceptions_thrown ||
-    ((uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
-      "java::java.lang.AssertionError") &&
+    ((uncaught_exceptions_domaint::get_exception_type(
+        to_reference_type(op[0].type())) == "java::java.lang.AssertionError") &&
      !throw_assertion_error))
   {
     // we translate athrow into

jbmc/src/java_bytecode/java_types.h

@@ -809,7 +809,8 @@ class java_generic_parametert : public reference_typet
 template <>
 inline bool can_cast_type<java_generic_parametert>(const typet &base)
 {
-  return is_reference(base) && is_java_generic_parameter_tag(base.subtype());
+  return is_reference(base) &&
+         is_java_generic_parameter_tag(to_reference_type(base).base_type());
 }
 
 /// Checks whether the type is a java generic parameter/variable, e.g., `T` in
@@ -937,7 +938,8 @@ class java_generic_typet:public reference_typet
 template <>
 inline bool can_cast_type<java_generic_typet>(const typet &type)
 {
-  return is_reference(type) && is_java_generic_struct_tag_type(type.subtype());
+  return is_reference(type) &&
+         is_java_generic_struct_tag_type(to_reference_type(type).base_type());
 }
 
 /// \param type: the type to check

jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp

@@ -37,7 +37,8 @@ SCENARIO(
         REQUIRE(annotations.size() == 1);
         const auto &annotation = annotations.front();
         const auto &identifier =
-          to_struct_tag_type(annotation.type.subtype()).get_identifier();
+          to_struct_tag_type(to_reference_type(annotation.type).base_type())
+            .get_identifier();
         REQUIRE(id2string(identifier) == "java::MyClassAnnotation");
         const auto &element_value_pair = annotation.element_value_pairs.front();
         const auto &element_name = element_value_pair.element_name;
@@ -64,7 +65,8 @@ SCENARIO(
         REQUIRE(annotations.size() == 1);
         const auto &annotation = annotations.front();
         const auto &identifier =
-          to_struct_tag_type(annotation.type.subtype()).get_identifier();
+          to_struct_tag_type(to_reference_type(annotation.type).base_type())
+            .get_identifier();
         REQUIRE(id2string(identifier) == "java::MyMethodAnnotation");
         const auto &element_value_pair = annotation.element_value_pairs.front();
         const auto &element_name = element_value_pair.element_name;

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

@@ -93,8 +93,9 @@ SCENARIO(
         const auto &id =
           to_symbol_expr(element_value_pair.value).get_identifier();
         const auto &java_type = java_type_from_string(id2string(id));
-        const std::string &class_name =
-          id2string(to_struct_tag_type(java_type->subtype()).get_identifier());
+        const std::string &class_name = id2string(
+          to_struct_tag_type(to_reference_type(*java_type).base_type())
+            .get_identifier());
         REQUIRE(id2string(class_name) == "java::java.lang.String");
       }
     }

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -30,9 +30,10 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
     member_exprt(plain_expr, "member", java_int_type());
   const constant_exprt invalid_constant = constant_exprt("", java_int_type());
   const constant_exprt valid_constant = constant_exprt("0", java_int_type());
-  const index_exprt valid_index =
-    index_exprt(valid_symbol_expr, valid_constant);
-  const index_exprt index_plain = index_exprt(exprt(), exprt());
+  const index_exprt valid_index = index_exprt(
+    symbol_exprt("id", array_typet(typet(), nil_exprt())), valid_constant);
+  const index_exprt index_plain =
+    index_exprt(exprt(ID_nil, array_typet(typet(), nil_exprt())), exprt());
   const byte_extract_exprt byte_little_endian = byte_extract_exprt(
     ID_byte_extract_little_endian, exprt(), exprt(), typet());
   const byte_extract_exprt byte_big_endian =

src/analyses/does_remove_const.cpp

@@ -12,9 +12,10 @@ Author: Diffblue Ltd.
 #include "does_remove_const.h"
 
 #include <goto-programs/goto_program.h>
-#include <util/type.h>
-#include <util/std_code.h>
+
 #include <util/base_type.h>
+#include <util/pointer_expr.h>
+#include <util/std_code.h>
 
 /// A naive analysis to look for casts that remove const-ness from pointers.
 /// \param goto_program: the goto program to check
@@ -122,16 +123,20 @@ bool does_remove_constt::does_type_preserve_const_correctness(
 {
   while(target_type->id()==ID_pointer)
   {
-    bool direct_subtypes_at_least_as_const=
-      is_type_at_least_as_const_as(
-        target_type->subtype(), source_type->subtype());
+    PRECONDITION(source_type->id() == ID_pointer);
+
+    const auto &target_pointer_type = to_pointer_type(*target_type);
+    const auto &source_pointer_type = to_pointer_type(*source_type);
+
+    bool direct_subtypes_at_least_as_const = is_type_at_least_as_const_as(
+      target_pointer_type.base_type(), source_pointer_type.base_type());
     // We have a pointer to something, but the thing it is pointing to can't be
     // modified normally, but can through this pointer
     if(!direct_subtypes_at_least_as_const)
       return false;
     // Check the subtypes if they are pointers
-    target_type=&target_type->subtype();
-    source_type=&source_type->subtype();
+    target_type = &target_pointer_type.base_type();
+    source_type = &source_pointer_type.base_type();
   }
   return true;
 }

src/analyses/goto_check_c.cpp

@@ -1352,7 +1352,8 @@ void goto_check_ct::pointer_primitive_check(
       return;
   }
 
-  const auto size_of_expr_opt = size_of_expr(pointer.type().subtype(), ns);
+  const auto size_of_expr_opt =
+    size_of_expr(to_pointer_type(pointer.type()).base_type(), ns);
 
   const exprt size = !size_of_expr_opt.has_value()
                        ? from_integer(1, size_type())

src/analyses/goto_rw.cpp

@@ -98,7 +98,8 @@ void rw_range_sett::get_objects_complex_imag(
 {
   const exprt &op = expr.op();
 
-  auto subtype_bits = pointer_offset_bits(op.type().subtype(), ns);
+  auto subtype_bits =
+    pointer_offset_bits(to_complex_type(op.type()).subtype(), ns);
   CHECK_RETURN(subtype_bits.has_value());
 
   range_spect sub_size = to_range_spect(*subtype_bits);

src/analyses/uncaught_exceptions_analysis.cpp

@@ -15,17 +15,17 @@ Author: Cristina David
 #include "uncaught_exceptions_analysis.h"
 
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/symbol_table.h>
 
 #include <goto-programs/goto_functions.h>
 
 /// Returns the compile type of an exception
-irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
+irep_idt
+uncaught_exceptions_domaint::get_exception_type(const pointer_typet &type)
 {
-  PRECONDITION(type.id()==ID_pointer);
-
-  if(type.subtype().id() == ID_struct_tag)
-    return to_struct_tag_type(type.subtype()).get_identifier();
+  if(type.base_type().id() == ID_struct_tag)
+    return to_struct_tag_type(type.base_type()).get_identifier();
   else
     return ID_empty;
 }
@@ -73,7 +73,8 @@ void uncaught_exceptions_domaint::transform(
   {
     const exprt &exc_symbol = get_exception_symbol(instruction.get_code());
     // retrieve the static type of the thrown exception
-    const irep_idt &type_id=get_exception_type(exc_symbol.type());
+    const irep_idt &type_id =
+      get_exception_type(to_pointer_type(exc_symbol.type()));
     join(type_id);
     // we must consider all the subtypes given that
     // the runtime type is a subtype of the static type

src/analyses/uncaught_exceptions_analysis.h

@@ -20,6 +20,7 @@ Author: Cristina David
 
 class goto_functionst;
 class namespacet;
+class pointer_typet;
 
 /// defines the domain used by the uncaught  exceptions analysis
 class uncaught_exceptions_analysist;
@@ -41,7 +42,7 @@ class uncaught_exceptions_domaint
     stack_caught.clear();
   }
 
-  static irep_idt get_exception_type(const typet &type);
+  static irep_idt get_exception_type(const pointer_typet &);
 
   static exprt get_exception_symbol(const exprt &exor);
 

src/ansi-c/ansi_c_convert_type.cpp

@@ -53,11 +53,12 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       c_storage_spec.asm_label =
         to_string_constant(type_with_subtypes.subtypes()[0]).get_value();
   }
-  else if(type.id()==ID_section &&
-          type.has_subtype() &&
-          type.subtype().id()==ID_string_constant)
+  else if(
+    type.id() == ID_section && type.has_subtype() &&
+    to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    c_storage_spec.section = to_string_constant(type.subtype()).get_value();
+    c_storage_spec.section =
+      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
   }
   else if(type.id()==ID_const)
     c_qualifiers.is_constant=true;
@@ -69,7 +70,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     // this gets turned into the qualifier, uh
     c_qualifiers.is_atomic=true;
-    read_rec(type.subtype());
+    read_rec(to_type_with_subtype(type).subtype());
   }
   else if(type.id()==ID_char)
     char_cnt++;
@@ -228,18 +229,20 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     constructor=true;
   else if(type.id()==ID_destructor)
     destructor=true;
-  else if(type.id()==ID_alias &&
-          type.has_subtype() &&
-          type.subtype().id()==ID_string_constant)
+  else if(
+    type.id() == ID_alias && type.has_subtype() &&
+    to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    c_storage_spec.alias = to_string_constant(type.subtype()).get_value();
+    c_storage_spec.alias =
+      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
   }
   else if(type.id()==ID_frontend_pointer)
   {
     // We turn ID_frontend_pointer to ID_pointer
     // Pointers have a width, much like integers,
     // which is added here.
-    pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
+    pointer_typet tmp(
+      to_type_with_subtype(type).subtype(), config.ansi_c.pointer_width);
     tmp.add_source_location()=type.source_location();
     const irep_idt typedef_identifier=type.get(ID_C_typedef);
     if(!typedef_identifier.empty())

src/ansi-c/ansi_c_entry_point.cpp

@@ -405,7 +405,7 @@ bool generate_ansi_c_start_function(
       {
         // assign argv[argc] to NULL
         const null_pointer_exprt null(
-          to_pointer_type(argv_symbol.type.subtype()));
+          to_pointer_type(to_array_type(argv_symbol.type).element_type()));
 
         index_exprt index_expr(
           argv_symbol.symbol_expr(), argc_symbol.symbol_expr());
@@ -422,7 +422,8 @@ bool generate_ansi_c_start_function(
         const symbolt &envp_size_symbol=ns.lookup("envp_size'");
 
         // assume envp[envp_size] is NULL
-        null_pointer_exprt null(to_pointer_type(envp_symbol.type.subtype()));
+        null_pointer_exprt null(
+          to_pointer_type(to_array_type(envp_symbol.type).element_type()));
 
         index_exprt index_expr(
           envp_symbol.symbol_expr(), envp_size_symbol.symbol_expr());

src/ansi-c/ansi_c_parser.cpp

@@ -171,7 +171,7 @@ ansi_c_id_classt ansi_c_parsert::get_class(const typet &type)
     }
   }
   else if(type.has_subtype())
-    return get_class(type.subtype());
+    return get_class(to_type_with_subtype(type).subtype());
 
   return ansi_c_id_classt::ANSI_C_SYMBOL;
 }

src/ansi-c/c_storage_spec.cpp

@@ -46,11 +46,12 @@ void c_storage_spect::read(const typet &type)
       if(it->id()==ID_thread)
         is_thread_local=true;
   }
-  else if(type.id()==ID_alias &&
-          type.has_subtype() &&
-          type.subtype().id()==ID_string_constant)
+  else if(
+    type.id() == ID_alias && type.has_subtype() &&
+    to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    alias = to_string_constant(type.subtype()).get_value();
+    alias =
+      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
   }
   else if(
     type.id() == ID_asm && !to_type_with_subtypes(type).subtypes().empty() &&
@@ -59,10 +60,11 @@ void c_storage_spect::read(const typet &type)
     asm_label =
       to_string_constant(to_type_with_subtypes(type).subtypes()[0]).get_value();
   }
-  else if(type.id()==ID_section &&
-          type.has_subtype() &&
-          type.subtype().id()==ID_string_constant)
+  else if(
+    type.id() == ID_section && type.has_subtype() &&
+    to_type_with_subtype(type).subtype().id() == ID_string_constant)
   {
-    section = to_string_constant(type.subtype()).get_value();
+    section =
+      to_string_constant(to_type_with_subtype(type).subtype()).get_value();
   }
 }