Merge pull request #6618 from diffblue/typet_subtype_const2

kroening · web-flow · commit a702e770fc70 · 2022-05-24T11:43:51.000+01:00
remove uses of typet::subtype() const
diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/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");
         }
       }
diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/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;
 }
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/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;
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/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;
     });
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/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
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/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());
 
diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/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())
     {
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/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);
 
diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/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;
 
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/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;
 
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
@@ -574,13 +574,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
       to_pointer_type(type).base_type().id() == ID_code &&
       to_pointer_type(expr.type()).base_type().id() == ID_code)
     {
-      code_typet code1=to_code_type(expr.type().subtype());
+      code_typet code1 = to_code_type(to_pointer_type(expr.type()).base_type());
       assert(!code1.parameters().empty());
       code_typet::parametert this1=code1.parameters()[0];
       INVARIANT(this1.get_this(), "first parameter should be `this'");
       code1.parameters().erase(code1.parameters().begin());
 
-      code_typet code2=to_code_type(type.subtype());
+      code_typet code2 = to_code_type(to_pointer_type(type).base_type());
       assert(!code2.parameters().empty());
       code_typet::parametert this2=code2.parameters()[0];
       INVARIANT(this2.get_this(), "first parameter should be `this'");
@@ -1118,7 +1118,7 @@ bool cpp_typecheckt::reference_related(
   assert(!is_reference(expr.type()));
 
   typet from=follow(expr.type());
-  typet to=follow(type.subtype());
+  typet to = follow(to_reference_type(type).base_type());
 
   // need to check #c_type
   if(from.get(ID_C_c_type)!=to.get(ID_C_c_type))
@@ -1667,7 +1667,7 @@ bool cpp_typecheckt::const_typecast(
     if(!expr.get_bool(ID_C_lvalue))
       return false;
 
-    if(new_expr.type()!=type.subtype())
+    if(new_expr.type() != to_reference_type(type).base_type())
       return false;
 
     address_of_exprt address_of(expr, to_pointer_type(type));
@@ -1710,21 +1710,21 @@ bool cpp_typecheckt::dynamic_typecast(
 
   if(is_reference(type))
   {
-    if(type.subtype().id() != ID_struct_tag)
+    if(to_reference_type(type).base_type().id() != ID_struct_tag)
       return false;
   }
   else if(type.id()==ID_pointer)
   {
     if(type.find(ID_to_member).is_not_nil())
       return false;
 
-    if(type.subtype().id()==ID_empty)
+    if(to_pointer_type(type).base_type().id() == ID_empty)
     {
       if(!e.get_bool(ID_C_lvalue))
         return false;
       UNREACHABLE; // currently not supported
     }
-    else if(type.subtype().id() == ID_struct_tag)
+    else if(to_pointer_type(type).base_type().id() == ID_struct_tag)
     {
       if(e.get_bool(ID_C_lvalue))
       {
@@ -1863,7 +1863,7 @@ bool cpp_typecheckt::static_typecast(
     if(reference_binding(e, type, new_expr, rank))
       return true;
 
-    typet subto=follow(type.subtype());
+    typet subto = follow(to_pointer_type(type).base_type());
     typet from=follow(e.type());
 
     if(subto.id()==ID_struct && from.id()==ID_struct)
@@ -1875,7 +1875,7 @@ bool cpp_typecheckt::static_typecast(
       qual_from.read(e.type());
 
       c_qualifierst qual_to;
-      qual_to.read(type.subtype());
+      qual_to.read(to_pointer_type(type).base_type());
 
       if(!qual_to.is_subset_of(qual_from))
         return false;
@@ -1945,8 +1945,8 @@ bool cpp_typecheckt::static_typecast(
   {
     if(type.find(ID_to_member).is_nil() && e.type().find(ID_to_member).is_nil())
     {
-      typet to=follow(type.subtype());
-      typet from=follow(e.type().subtype());
+      typet to = follow(to_pointer_type(type).base_type());
+      typet from = follow(to_pointer_type(e.type()).base_type());
 
       if(from.id()==ID_empty)
       {
@@ -1979,7 +1979,9 @@ bool cpp_typecheckt::static_typecast(
       type.find(ID_to_member).is_not_nil() &&
       e.type().find(ID_to_member).is_not_nil())
     {
-      if(type.subtype()!=e.type().subtype())
+      if(
+        to_pointer_type(type).base_type() !=
+        to_pointer_type(e.type()).base_type())
         return false;
 
       const struct_typet &from_struct = to_struct_type(
@@ -1998,8 +2000,12 @@ bool cpp_typecheckt::static_typecast(
       type.find(ID_to_member).is_nil() &&
       e.type().find(ID_to_member).is_not_nil())
     {
-      if(type.subtype() != e.type().subtype())
+      if(
+        to_pointer_type(type).base_type() !=
+        to_pointer_type(e.type()).base_type())
+      {
         return false;
+      }
 
       const struct_typet &from_struct = to_struct_type(
         follow(static_cast<const typet &>(e.type().find(ID_to_member))));
diff --git a/src/cpp/expr2cpp.cpp b/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;
 }
diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp
@@ -201,7 +201,7 @@ size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
   if(t.id() != ID_pointer)
     return 0;
   else
-    return pointer_depth(t.subtype()) + 1;
+    return pointer_depth(to_pointer_type(t).base_type()) + 1;
 }
 
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp

Original file line number	Diff line number	Diff line change
`@@ -174,7 +174,7 @@ void ci_lazy_methods_neededt::gather_field_types(`
`174`	`174`	`gather_field_types(field.type(), ns);`
`175`	`175`	`else if(field.type().id() == ID_pointer)`
`176`	`176`	`{`
`177`		`- if(field.type().subtype().id() == ID_struct_tag)`
	`177`	`+ if(to_pointer_type(field.type()).base_type().id() == ID_struct_tag)`
`178`	`178`	`{`
`179`	`179`	`add_all_needed_classes(to_pointer_type(field.type()));`
`180`	`180`	`}`
`@@ -186,7 +186,7 @@ void ci_lazy_methods_neededt::gather_field_types(`
`186`	`186`	`// We should therefore only be skipping pointers such as the uint16t*`
`187`	`187`	`// in our internal String representation.`
`188`	`188`	`INVARIANT(`
`189`		`- field.type().subtype().id() != ID_struct,`
	`189`	`+ to_pointer_type(field.type()).base_type().id() != ID_struct,`
`190`	`190`	`"struct types should be referred to by symbol at this stage");`
`191`	`191`	`}`
`192`	`192`	`}`
Original file line number	Diff line number	Diff line change
`@@ -340,13 +340,13 @@ std::string expr2javat::convert_java_new(const exprt &src)`
`340`	`340`	`convert(static_cast<const exprt &>(src.find(ID_size)));`
`341`	`341`
`342`	`342`	`dest+=' ';`
`343`		`- dest+=convert(src.type().subtype());`
	`343`	`+ dest += convert(to_pointer_type(src.type()).base_type());`
`344`	`344`	`dest+='[';`
`345`	`345`	`dest+=tmp_size;`
`346`	`346`	`dest+=']';`
`347`	`347`	`}`
`348`	`348`	`else`
`349`		`- dest="new "+convert(src.type().subtype());`
	`349`	`+ dest = "new " + convert(to_pointer_type(src.type()).base_type());`
`350`	`350`
`351`	`351`	`return dest;`
`352`	`352`	`}`
Original file line number	Diff line number	Diff line change
`@@ -600,7 +600,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)`
`600`	`600`	`get_class_refs_rec(c.type());`
`601`	`601`	`}`
`602`	`602`	`else if(src.id()==ID_pointer)`
`603`		`- get_class_refs_rec(src.subtype());`
	`603`	`+ get_class_refs_rec(to_pointer_type(src).base_type());`
`604`	`604`	`}`
`605`	`605`
`606`	`606`	`/// For each of the given annotations, get a reference to its class and`
Original file line number	Diff line number	Diff line change
`@@ -97,7 +97,9 @@ std::string java_qualifierst::as_string() const`
`97`	`97`	`for(const java_annotationt &annotation : annotations)`
`98`	`98`	`{`
`99`	`99`	`out << '@';`
`100`		`- out << annotation.get_type().subtype().get(ID_identifier);`
	`100`	`+ out << to_reference_type(annotation.get_type())`
	`101`	`+ .base_type()`
	`102`	`+ .get(ID_identifier);`
`101`	`103`
`102`	`104`	`if(!annotation.get_values().empty())`
`103`	`105`	`{`