Merge pull request #6878 from diffblue/typet_subtype_const3

remove uses of typet::subtype() const

Author: tautschnig

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -397,8 +397,8 @@ static code_with_references_listt assign_array_data_component_from_json(
 {
   const auto &java_class_type = followed_class_type(expr, info.symbol_table);
   const auto &data_component = java_class_type.components()[2];
-  const auto &element_type =
-    java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+  const auto &element_type = java_array_element_type(
+    to_struct_tag_type(to_pointer_type(expr.type()).base_type()));
   const exprt data_member_expr = typecast_exprt::conditional_cast(
     member_exprt{dereference_exprt{expr}, "data", data_component.type()},
     pointer_type(element_type));
@@ -461,8 +461,8 @@ assign_det_length_array_from_json(
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(expr.type()));
-  const auto &element_type =
-    java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+  const auto &element_type = java_array_element_type(
+    to_struct_tag_type(to_java_reference_type(expr.type()).base_type()));
   const json_arrayt json_array = get_untyped_array(json, element_type);
   const auto number_of_elements =
     from_integer(json_array.size(), java_int_type());
@@ -490,8 +490,8 @@ static code_with_references_listt assign_nondet_length_array_from_json(
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(array.type()));
-  const auto &element_type =
-    java_array_element_type(to_struct_tag_type(array.type().subtype()));
+  const auto &element_type = java_array_element_type(
+    to_struct_tag_type(to_java_reference_type(array.type()).base_type()));
   const json_arrayt json_array = get_untyped_array(json, element_type);
   code_with_references_listt result;
   exprt number_of_elements = from_integer(json_array.size(), java_int_type());
@@ -884,8 +884,8 @@ code_with_references_listt assign_from_json_rec(
       else
       {
         PRECONDITION(is_java_array_type(expr.type()));
-        const auto &element_type =
-          java_array_element_type(to_struct_tag_type(expr.type().subtype()));
+        const auto &element_type = java_array_element_type(
+          to_struct_tag_type(to_java_reference_type(expr.type()).base_type()));
         const std::size_t length = get_untyped_array(json, element_type).size();
         result.add(allocate_array(
           expr, from_integer(length, java_int_type()), info.loc));

jbmc/src/java_bytecode/java_types.cpp

@@ -164,11 +164,12 @@ bool is_java_array_type(const typet &type)
 {
   if(
     !can_cast_type<pointer_typet>(type) ||
-    !can_cast_type<struct_tag_typet>(type.subtype()))
+    !can_cast_type<struct_tag_typet>(to_pointer_type(type).base_type()))
   {
     return false;
   }
-  const auto &subtype_struct_tag = to_struct_tag_type(type.subtype());
+  const auto &subtype_struct_tag =
+    to_struct_tag_type(to_pointer_type(type).base_type());
   return is_java_array_tag(subtype_struct_tag.get_identifier());
 }
 
@@ -177,8 +178,9 @@ bool is_java_array_type(const typet &type)
 /// an array type.
 bool is_multidim_java_array_type(const typet &type)
 {
-  return is_java_array_type(type) && is_java_array_type(java_array_element_type(
-                                       to_struct_tag_type(type.subtype())));
+  return is_java_array_type(type) &&
+         is_java_array_type(java_array_element_type(
+           to_struct_tag_type(to_pointer_type(type).base_type())));
 }
 
 /// Returns the underlying element type and array dimensionality of Java struct
@@ -190,8 +192,8 @@ java_array_dimension_and_element_type(const struct_tag_typet &type)
   typet underlying_type;
   for(underlying_type = java_reference_type(type);
       is_java_array_type(underlying_type);
-      underlying_type =
-        java_array_element_type(to_struct_tag_type(underlying_type.subtype())))
+      underlying_type = java_array_element_type(to_struct_tag_type(
+        to_java_reference_type(underlying_type).base_type())))
   {
     ++array_dimensions;
   }
@@ -539,7 +541,7 @@ size_t find_closing_semi_colon_for_reference_type(
 java_reference_typet java_reference_array_type(const struct_tag_typet &subtype)
 {
   java_reference_typet result = java_array_type('a');
-  result.subtype().set(ID_element_type, java_reference_type(subtype));
+  result.base_type().set(ID_element_type, java_reference_type(subtype));
   return result;
 }
 
@@ -892,11 +894,13 @@ bool equal_java_types(const typet &type1, const typet &type2)
   bool arrays_with_same_element_type = true;
   if(
     type1.id() == ID_pointer && type2.id() == ID_pointer &&
-    type1.subtype().id() == ID_struct_tag &&
-    type2.subtype().id() == ID_struct_tag)
+    to_pointer_type(type1).base_type().id() == ID_struct_tag &&
+    to_pointer_type(type2).base_type().id() == ID_struct_tag)
   {
-    const auto &subtype_symbol1 = to_struct_tag_type(type1.subtype());
-    const auto &subtype_symbol2 = to_struct_tag_type(type2.subtype());
+    const auto &subtype_symbol1 =
+      to_struct_tag_type(to_pointer_type(type1).base_type());
+    const auto &subtype_symbol2 =
+      to_struct_tag_type(to_pointer_type(type2).base_type());
     if(
       subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
       is_java_array_tag(subtype_symbol1.get_identifier()))
@@ -952,7 +956,8 @@ void get_dependencies_from_generic_parameters_rec(
   // Java reference type
   else if(t.id() == ID_pointer)
   {
-    get_dependencies_from_generic_parameters_rec(t.subtype(), refs);
+    get_dependencies_from_generic_parameters_rec(
+      to_pointer_type(t).base_type(), refs);
   }
 
   // method type with parameters and return value
@@ -1102,9 +1107,10 @@ std::string pretty_java_type(const typet &type)
     return "byte";
   else if(is_reference(type))
   {
-    if(type.subtype().id() == ID_struct_tag)
+    if(to_reference_type(type).base_type().id() == ID_struct_tag)
     {
-      const auto &struct_tag_type = to_struct_tag_type(type.subtype());
+      const auto &struct_tag_type =
+        to_struct_tag_type(to_reference_type(type).base_type());
       const irep_idt &id = struct_tag_type.get_identifier();
       if(is_java_array_tag(id))
         return pretty_java_type(java_array_element_type(struct_tag_type)) +

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -176,8 +176,8 @@ bool remove_instanceoft::lower_instanceof(
 
   if(target_type_is_reference_array)
   {
-    const auto &underlying_type =
-      to_struct_tag_type(underlying_type_and_dimension.first.subtype());
+    const auto &underlying_type = to_struct_tag_type(
+      to_pointer_type(underlying_type_and_dimension.first).base_type());
 
     test_conjuncts.push_back(equal_exprt(
       object_class_identifier_field,

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -88,7 +88,7 @@ goto_programt::targett remove_java_newt::lower_java_new(
   PRECONDITION(rhs.operands().empty());
   PRECONDITION(rhs.type().id() == ID_pointer);
   source_locationt location = rhs.source_location();
-  typet object_type = rhs.type().subtype();
+  typet object_type = to_pointer_type(rhs.type()).base_type();
 
   // build size expression
   const auto object_size = size_of_expr(object_type, ns);
@@ -141,7 +141,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   PRECONDITION(rhs.type().id() == ID_pointer);
 
   source_locationt location = rhs.source_location();
-  struct_tag_typet object_type = to_struct_tag_type(rhs.type().subtype());
+  struct_tag_typet object_type =
+    to_struct_tag_type(to_pointer_type(rhs.type()).base_type());
   PRECONDITION(ns.follow(object_type).id() == ID_struct);
 
   // build size expression
@@ -201,7 +202,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
       goto_programt::make_assignment(code_assignt(
         object_array_element_type,
         constant_exprt(
-          to_struct_tag_type(underlying_type_and_dimension.first.subtype())
+          to_struct_tag_type(
+            to_pointer_type(underlying_type_and_dimension.first).base_type())
             .get_identifier(),
           string_typet()),
         location)));
@@ -307,8 +309,8 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     sub_java_new.operands().erase(sub_java_new.operands().begin());
 
     // we already know that rhs has pointer type
-    typet sub_type =
-      static_cast<const typet &>(rhs.type().subtype().find(ID_element_type));
+    typet sub_type = static_cast<const typet &>(
+      to_pointer_type(rhs.type()).base_type().find(ID_element_type));
     CHECK_RETURN(sub_type.id() == ID_pointer);
     sub_java_new.type() = sub_type;
 

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -201,7 +201,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
     // Return top if dereferencing a null pointer or we are top
     bool is_value_top = is_top() || value_stack.is_top_value();
     return env.abstract_object_factory(
-      type().subtype(), ns, is_value_top, !is_value_top);
+      to_pointer_type(type()).base_type(), ns, is_value_top, !is_value_top);
   }
   else
   {
@@ -230,7 +230,8 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
   if(stack.empty())
   {
     // We should not be changing the type of an abstract object
-    PRECONDITION(new_value->type() == ns.follow(type().subtype()));
+    PRECONDITION(
+      new_value->type() == ns.follow(to_pointer_type(type()).base_type()));
 
     // Get an expression that we can assign to
     exprt value = to_address_of_expr(value_stack.to_expression()).object();
@@ -273,7 +274,8 @@ abstract_object_pointert constant_pointer_abstract_objectt::typecast(
   {
     auto &env = const_cast<abstract_environmentt &>(environment);
 
-    auto heap_array_type = array_typet(new_type.subtype(), nil_exprt());
+    auto heap_array_type =
+      array_typet(to_pointer_type(new_type).base_type(), nil_exprt());
     auto array_object =
       environment.abstract_object_factory(heap_array_type, ns, true, false);
     auto heap_symbol = symbol_exprt(value.get(ID_identifier), heap_array_type);

src/analyses/variable-sensitivity/full_array_abstract_object.cpp

@@ -394,7 +394,8 @@ abstract_object_pointert full_array_abstract_objectt::get_top_entry(
   const abstract_environmentt &env,
   const namespacet &ns) const
 {
-  return env.abstract_object_factory(type().subtype(), ns, true, false);
+  return env.abstract_object_factory(
+    to_type_with_subtype(type()).subtype(), ns, true, false);
 }
 
 abstract_object_pointert full_array_abstract_objectt::write_location_context(

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -70,7 +70,7 @@ abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference(
   if(is_top() || is_bottom())
   {
     return env.abstract_object_factory(
-      type().subtype(), ns, is_top(), !is_top());
+      to_pointer_type(type()).base_type(), ns, is_top(), !is_top());
   }
 
   abstract_object_sett results;

src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp

@@ -11,6 +11,7 @@ Date: April 2016
 #include "variable_sensitivity_domain.h"
 
 #include <util/cprover_prefix.h>
+#include <util/pointer_expr.h>
 #include <util/symbol_table.h>
 
 #include <algorithm>
@@ -325,7 +326,9 @@ void variable_sensitivity_domaint::transform_function_call(
         {
           if(
             called_arg.type().id() == ID_pointer &&
-            !called_arg.type().subtype().get_bool(ID_C_constant))
+            !to_pointer_type(called_arg.type())
+               .base_type()
+               .get_bool(ID_C_constant))
           {
             abstract_object_pointert pointer_value =
               abstract_state.eval(called_arg, ns);
@@ -339,7 +342,10 @@ void variable_sensitivity_domaint::transform_function_call(
               std::stack<exprt>(),
               nil_exprt(),
               abstract_state.abstract_object_factory(
-                called_arg.type().subtype(), ns, true, false),
+                to_pointer_type(called_arg.type()).base_type(),
+                ns,
+                true,
+                false),
               false);
           }
         }

src/goto-programs/remove_const_function_pointers.cpp

@@ -523,9 +523,10 @@ bool remove_const_function_pointerst::try_resolve_index_of(
     bool all_possible_const=true;
     for(const exprt &potential_array_expr : potential_array_exprs)
     {
-      all_possible_const=
+      all_possible_const =
         all_possible_const &&
-        is_const_type(potential_array_expr.type().subtype());
+        is_const_type(
+          to_array_type(potential_array_expr.type()).element_type());
 
       if(potential_array_expr.id()==ID_array)
       {

src/pointer-analysis/value_set.cpp

@@ -595,7 +595,12 @@ void value_sett::get_value_set_rec(
       // integer-to-pointer
 
       if(op.is_zero())
-        insert(dest, exprt(ID_null_object, expr_type.subtype()), mp_integer{0});
+      {
+        insert(
+          dest,
+          exprt(ID_null_object, to_type_with_subtype(expr_type).subtype()),
+          mp_integer{0});
+      }
       else
       {
         // see if we have something for the integer
@@ -674,11 +679,12 @@ void value_sett::get_value_set_rec(
 
       if(ptr_operand.has_value() && i.has_value())
       {
-        typet pointer_sub_type = ptr_operand->type().subtype();
-        if(pointer_sub_type.id()==ID_empty)
-          pointer_sub_type=char_type();
+        typet pointer_base_type =
+          to_pointer_type(ptr_operand->type()).base_type();
+        if(pointer_base_type.id() == ID_empty)
+          pointer_base_type = char_type();
 
-        auto size = pointer_offset_size(pointer_sub_type, ns);
+        auto size = pointer_offset_size(pointer_base_type, ns);
 
         if(!size.has_value() || (*size) == 0)
         {

src/pointer-analysis/value_set_dereference.cpp

@@ -205,7 +205,7 @@ exprt value_set_dereferencet::handle_dereference_base_case(
   const exprt &pointer,
   bool display_points_to_sets)
 { // type of the object
-  const typet &type=pointer.type().subtype();
+  const typet &type = to_pointer_type(pointer.type()).base_type();
 
   // collect objects the pointer may point to
   const std::vector<exprt> points_to_set =
@@ -335,8 +335,9 @@ bool value_set_dereferencet::dereference_type_compare(
   while(object_unwrapped->id() == ID_pointer &&
         dereference_unwrapped->id() == ID_pointer)
   {
-    object_unwrapped = &object_unwrapped->subtype();
-    dereference_unwrapped = &dereference_unwrapped->subtype();
+    object_unwrapped = &to_pointer_type(*object_unwrapped).base_type();
+    dereference_unwrapped =
+      &to_pointer_type(*dereference_unwrapped).base_type();
   }
   if(dereference_unwrapped->id() == ID_empty)
   {
@@ -494,27 +495,28 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
     const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
 
-    if(memory_symbol.type.subtype() == dereference_type)
+    if(to_array_type(memory_symbol.type).element_type() == dereference_type)
     {
       // Types match already, what a coincidence!
       // We can use an index expression.
 
       const index_exprt index_expr(
         symbol_expr,
         pointer_offset(pointer_expr),
-        memory_symbol.type.subtype());
+        to_array_type(memory_symbol.type).element_type());
 
       result.value=index_expr;
       result.pointer = address_of_exprt{index_expr};
     }
-    else if(
-      dereference_type_compare(
-        memory_symbol.type.subtype(), dereference_type, ns))
+    else if(dereference_type_compare(
+              to_array_type(memory_symbol.type).element_type(),
+              dereference_type,
+              ns))
     {
       const index_exprt index_expr(
         symbol_expr,
         pointer_offset(pointer_expr),
-        memory_symbol.type.subtype());
+        to_array_type(memory_symbol.type).element_type());
       result.value=typecast_exprt(index_expr, dereference_type);
       result.pointer =
         typecast_exprt{address_of_exprt{index_expr}, pointer_type};
@@ -753,13 +755,16 @@ bool value_set_dereferencet::memory_model_bytes(
 
   // See if we have an array of bytes already,
   // and we want something byte-sized.
-  auto from_type_subtype_size = pointer_offset_size(from_type.subtype(), ns);
+  auto from_type_element_type_size =
+    from_type.id() == ID_array
+      ? pointer_offset_size(to_array_type(from_type).element_type(), ns)
+      : optionalt<mp_integer>{};
 
   auto to_type_size = pointer_offset_size(to_type, ns);
 
   if(
-    from_type.id() == ID_array && from_type_subtype_size.has_value() &&
-    *from_type_subtype_size == 1 && to_type_size.has_value() &&
+    from_type.id() == ID_array && from_type_element_type_size.has_value() &&
+    *from_type_element_type_size == 1 && to_type_size.has_value() &&
     *to_type_size == 1 &&
     is_a_bv_type(to_array_type(from_type).element_type()) &&
     is_a_bv_type(to_type))