Merge pull request #8210 from tautschnig/cleanup/no-follow-jbmc

JBMC: Replace uses of namespacet::follow

Author: tautschnig

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -68,9 +68,8 @@ static java_class_typet
 followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
 {
   const pointer_typet &pointer_type = to_pointer_type(expr.type());
-  const java_class_typet &java_class_type = to_java_class_type(
-    namespacet{symbol_table}.follow(pointer_type.base_type()));
-  return java_class_type;
+  return to_java_class_type(namespacet{symbol_table}.follow_tag(
+    to_struct_tag_type(pointer_type.base_type())));
 }
 
 static bool
@@ -531,8 +530,8 @@ static code_with_references_listt assign_struct_components_from_json(
   const jsont &json,
   object_creation_infot &info)
 {
-  const java_class_typet &java_class_type =
-    to_java_class_type(namespacet{info.symbol_table}.follow(expr.type()));
+  const java_class_typet &java_class_type = to_java_class_type(
+    namespacet{info.symbol_table}.follow_tag(to_struct_tag_type(expr.type())));
   code_with_references_listt result;
   for(const auto &component : java_class_type.components())
   {
@@ -577,7 +576,7 @@ static code_with_references_listt assign_struct_from_json(
 {
   const namespacet ns{info.symbol_table};
   const java_class_typet &java_class_type =
-    to_java_class_type(ns.follow(expr.type()));
+    to_java_class_type(ns.follow_tag(to_struct_tag_type(expr.type())));
   code_with_references_listt result;
   if(is_java_string_type(java_class_type))
   {
@@ -642,8 +641,8 @@ static code_with_references_listt assign_enum_from_json(
 
   dereference_exprt values_struct{
     info.symbol_table.lookup_ref(values_name).symbol_expr()};
-  const auto &values_struct_type =
-    to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type()));
+  const auto &values_struct_type = namespacet{info.symbol_table}.follow_tag(
+    to_struct_tag_type(values_struct.type()));
   PRECONDITION(is_valid_java_array(values_struct_type));
   const member_exprt values_data = member_exprt{
     values_struct, "data", values_struct_type.components()[2].type()};

jbmc/src/java_bytecode/expr2java.cpp

@@ -105,7 +105,9 @@ std::string expr2javat::convert_struct(
   const exprt &src,
   unsigned &precedence)
 {
-  const typet &full_type=ns.follow(src.type());
+  const typet &full_type = src.type().id() == ID_struct_tag
+                             ? ns.follow_tag(to_struct_tag_type(src.type()))
+                             : src.type();
 
   if(full_type.id()!=ID_struct)
     return convert_norep(src, precedence);

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -409,9 +409,8 @@ static void instrument_get_monitor_count(
   PRECONDITION(f_code.arguments().size() == 1);
 
   const namespacet ns(symbol_table);
-  const auto &followed_type =
-    ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type());
-  const auto &object_type = to_struct_type(followed_type);
+  const auto &object_type = ns.follow_tag(to_struct_tag_type(
+    to_pointer_type(f_code.arguments()[0].type()).base_type()));
   code_assignt code_assign(
     f_code.lhs(),
     member_exprt(

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -667,7 +667,7 @@ static member_exprt to_member(
 
   exprt accessed_object = checked_dereference(typed_pointer);
   const auto type_of = [&ns](const exprt &object) {
-    return to_struct_type(ns.follow(object.type()));
+    return ns.follow_tag(to_struct_tag_type(object.type()));
   };
 
   // The field access is described as being against a particular type, but it

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -507,7 +507,8 @@ static void infer_opaque_type_fields(
                 "') should have an opaque superclass");
             const auto &superclass_type = class_type->bases().front().type();
             class_symbol_id = superclass_type.get_identifier();
-            class_type = &to_java_class_type(ns.follow(superclass_type));
+            class_type = &to_java_class_type(
+              ns.follow_tag(to_struct_tag_type(superclass_type)));
           }
         }
       }
@@ -1502,8 +1503,8 @@ bool java_bytecode_languaget::convert_single_method_code(
       // TODO(tkiley): ci_lazy_methods_neededt, but this needs further
       // TODO(tkiley): investigation
       namespacet ns{symbol_table};
-      const java_class_typet &underlying_type =
-        to_java_class_type(ns.follow(pointer_return_type->base_type()));
+      const java_class_typet &underlying_type = to_java_class_type(
+        ns.follow_tag(to_struct_tag_type(pointer_return_type->base_type())));
 
       if(!underlying_type.is_abstract())
         needed_lazy_methods->add_all_needed_classes(*pointer_return_type);

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -199,10 +199,8 @@ void java_object_factoryt::gen_pointer_target_init(
   PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
   const namespacet ns(symbol_table);
-  const typet &followed_target_type = ns.follow(target_type);
-  PRECONDITION(followed_target_type.id() == ID_struct);
-
-  const auto &target_class_type = to_java_class_type(followed_target_type);
+  const auto &target_class_type =
+    to_java_class_type(ns.follow_tag(to_struct_tag_type(target_type)));
   if(target_class_type.get_tag().starts_with("java::array["))
   {
     assignments.append(gen_nondet_array_init(
@@ -374,7 +372,7 @@ void initialize_nondet_string_fields(
 {
   namespacet ns(symbol_table);
   const struct_typet &struct_type =
-    to_struct_type(ns.follow(struct_expr.type()));
+    ns.follow_tag(to_struct_tag_type(struct_expr.type()));
   PRECONDITION(is_java_string_type(struct_type));
 
   // We allow type StringBuffer and StringBuilder to be initialized
@@ -481,9 +479,6 @@ void java_object_factoryt::gen_nondet_pointer_init(
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   const namespacet ns(symbol_table);
-  const typet &subtype = pointer_type.base_type();
-  const typet &followed_subtype = ns.follow(subtype);
-  PRECONDITION(followed_subtype.id() == ID_struct);
   const pointer_typet &replacement_pointer_type =
     pointer_type_selector.convert_pointer_type(
       pointer_type, generic_parameter_specialization_map, ns);
@@ -501,7 +496,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
       replacement_pointer_type,
-      ns.follow(replacement_pointer_type.base_type()));
+      ns.follow_tag(to_struct_tag_type(replacement_pointer_type.base_type())));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
       assignments, lifetime, replacement_pointer_type, depth, location);
@@ -529,7 +524,9 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
   // the pointer to NULL instead of recursively initializing the struct to which
   // it points.
-  const struct_typet &struct_type = to_struct_type(followed_subtype);
+  const struct_tag_typet &tag_type =
+    to_struct_tag_type(pointer_type.base_type());
+  const struct_typet &struct_type = ns.follow_tag(tag_type);
   const irep_idt &struct_tag = struct_type.get_tag();
 
   // If this is a recursive type of some kind AND the depth is exceeded, set
@@ -564,7 +561,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // ci_lazy_methodst::initialize_instantiated_classes.
   if(
     const auto class_type =
-      type_try_dynamic_cast<java_class_typet>(followed_subtype))
+      type_try_dynamic_cast<java_class_typet>(struct_type))
   {
     if(class_type->get_base("java::java.lang.Enum"))
     {
@@ -581,13 +578,13 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
   // emit to `update_in_place_assignments` code for in-place initialization of
   // the object pointed by `expr`, assuming that such object is of type
-  // `subtype`
+  // `tag_type`
   if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
   {
     gen_pointer_target_init(
       update_in_place_assignments,
       expr,
-      subtype,
+      tag_type,
       lifetime,
       depth,
       update_in_placet::MUST_UPDATE_IN_PLACE,
@@ -610,7 +607,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
   gen_pointer_target_init(
     non_null_inst,
     expr,
-    subtype,
+    tag_type,
     lifetime,
     depth,
     update_in_placet::NO_UPDATE_IN_PLACE,
@@ -773,7 +770,7 @@ void java_object_factoryt::gen_nondet_struct_init(
   const source_locationt &location)
 {
   const namespacet ns(symbol_table);
-  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
+  PRECONDITION(expr.type().id() == ID_struct_tag);
 
   typedef struct_typet::componentst componentst;
   const irep_idt &struct_tag=struct_type.get_tag();
@@ -1008,7 +1005,6 @@ void java_object_factoryt::gen_nondet_init(
 {
   const typet &type = override_type.has_value() ? *override_type : expr.type();
   const namespacet ns(symbol_table);
-  const typet &followed_type = ns.follow(type);
 
   if(type.id()==ID_pointer)
   {
@@ -1021,7 +1017,8 @@ void java_object_factoryt::gen_nondet_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
-      pointer_type, ns.follow(pointer_type.base_type()));
+      pointer_type,
+      ns.follow_tag(to_struct_tag_type(pointer_type.base_type())));
 
     gen_nondet_pointer_init(
       assignments,
@@ -1032,9 +1029,9 @@ void java_object_factoryt::gen_nondet_init(
       update_in_place,
       location);
   }
-  else if(followed_type.id() == ID_struct)
+  else if(type.id() == ID_struct_tag)
   {
-    const struct_typet struct_type = to_struct_type(followed_type);
+    const struct_typet struct_type = ns.follow_tag(to_struct_tag_type(type));
 
     // If we are about to initialize a generic class (as a superclass object
     // for a different object), add its concrete types to the map and delete
@@ -1388,8 +1385,8 @@ code_blockt gen_nondet_array_init(
   code_blockt statements;
 
   const namespacet ns(symbol_table);
-  const typet &type = ns.follow(to_pointer_type(expr.type()).base_type());
-  const struct_typet &struct_type = to_struct_type(type);
+  const struct_typet &struct_type =
+    ns.follow_tag(to_struct_tag_type(to_pointer_type(expr.type()).base_type()));
   const typet &element_type = static_cast<const typet &>(
     to_pointer_type(expr.type()).base_type().find(ID_element_type));
 
@@ -1492,7 +1489,8 @@ bool java_object_factoryt::gen_nondet_enum_init(
 
   // Access members (length and data) of $VALUES array
   dereference_exprt deref_expr(values.symbol_expr());
-  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
+  const auto &deref_struct_type =
+    ns.follow_tag(to_struct_tag_type(deref_expr.type()));
   PRECONDITION(is_valid_java_array(deref_struct_type));
   const auto &comps = deref_struct_type.components();
   const member_exprt length_expr(deref_expr, "length", comps[1].type());

jbmc/src/java_bytecode/java_pointer_casts.cpp

@@ -37,12 +37,11 @@ bool find_superclass_with_type(
   PRECONDITION(ptr.type().id() == ID_pointer);
   while(true)
   {
-    const typet ptr_base = ns.follow(to_pointer_type(ptr.type()).base_type());
-
-    if(ptr_base.id()!=ID_struct)
+    const typet &ptr_base = to_pointer_type(ptr.type()).base_type();
+    if(ptr_base.id() != ID_struct_tag)
       return false;
-
-    const struct_typet &base_struct=to_struct_type(ptr_base);
+    const struct_typet &base_struct =
+      ns.follow_tag(to_struct_tag_type(ptr_base));
 
     if(base_struct.components().empty())
       return false;
@@ -60,7 +59,11 @@ bool find_superclass_with_type(
 
     // Compare the real (underlying) type, as target_type is already a non-
     // symbolic type.
-    if(ns.follow(first_field_type)==target_type)
+    const typet &underlying_type =
+      first_field_type.id() == ID_struct_tag
+        ? ns.follow_tag(to_struct_tag_type(first_field_type))
+        : first_field_type;
+    if(underlying_type == target_type)
       return true;
   }
 }
@@ -88,8 +91,6 @@ exprt make_clean_pointer_cast(
     return typecast_exprt(ptr, target_type);
   }
 
-  const typet &target_base = ns.follow(target_type.base_type());
-
   exprt bare_ptr=ptr;
   while(bare_ptr.id()==ID_typecast)
   {
@@ -112,6 +113,10 @@ exprt make_clean_pointer_cast(
   // recorded on the pointer, not the pointee), so it may still be necessary
   // to use a cast to reintroduce the qualifier (for example, the base might
   // be recorded as a List, when we're looking for a List<E>)
+  const typet &target_base =
+    target_type.base_type().id() == ID_struct_tag
+      ? ns.follow_tag(to_struct_tag_type(target_type.base_type()))
+      : target_type.base_type();
   if(find_superclass_with_type(superclass_ptr, target_base, ns))
     return typecast_exprt::conditional_cast(superclass_ptr, target_type);
 

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -808,7 +808,8 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string(
   {
     // Initialise the supertype with the appropriate classid:
     namespacet ns(symbol_table);
-    const struct_typet &lhs_type = to_struct_type(ns.follow(deref.type()));
+    const struct_typet &lhs_type =
+      ns.follow_tag(to_struct_tag_type(deref.type()));
     auto zero_base_object = *zero_initializer(
       lhs_type.components().front().type(), source_locationt{}, ns);
     set_class_identifier(

jbmc/src/java_bytecode/java_string_literals.cpp

@@ -70,9 +70,9 @@ symbol_exprt get_or_create_string_literal_symbol(
   // Regardless of string refinement setting, at least initialize
   // the literal with @clsid = String
   struct_tag_typet jlo_symbol("java::java.lang.Object");
-  const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol));
+  const auto &jlo_struct = ns.follow_tag(jlo_symbol);
   struct_exprt jlo_init({}, jlo_symbol);
-  const auto &jls_struct = to_struct_type(ns.follow(string_type));
+  const auto &jls_struct = ns.follow_tag(string_type);
   java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String");
 
   // If string refinement *is* around, populate the actual

jbmc/src/java_bytecode/remove_java_new.cpp

@@ -145,7 +145,6 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   source_locationt location = rhs.source_location();
   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
   const auto object_size = size_of_expr(object_type, ns);
@@ -161,7 +160,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     goto_programt::make_assignment(code_assignt(lhs, malloc_expr), location);
   goto_programt::targett next = std::next(target);
 
-  const struct_typet &struct_type = to_struct_type(ns.follow(object_type));
+  const struct_typet &struct_type = ns.follow_tag(object_type);
 
   PRECONDITION(is_valid_java_array(struct_type));