Merge pull request #6599 from diffblue/typet_subtype_const

remove usage of typet::subtype()

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);