Merge pull request #3901 from thk123/clean-member-of

Clean member of

Author: Thomas Kiley

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -647,39 +647,46 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
   throw "unhandled java comparison instruction";
 }
 
-static member_exprt
-to_member(const exprt &pointer, const exprt &fieldref, const namespacet &ns)
+/// Build a member exprt for accessing a specific field that may come from a
+/// base class.
+/// \param pointer: The expression to access the field on.
+/// \param field_reference: A getfield/setfield instruction produced by the
+///   bytecode parser.
+/// \param ns: Global namespace
+/// \return A member expression accessing the field, through base class
+///   components if necessary.
+static member_exprt to_member(
+  const exprt &pointer,
+  const exprt &field_reference,
+  const namespacet &ns)
 {
-  struct_tag_typet class_type(fieldref.get(ID_class));
+  struct_tag_typet class_type(field_reference.get(ID_class));
 
   const exprt typed_pointer =
     typecast_exprt::conditional_cast(pointer, java_reference_type(class_type));
 
-  const irep_idt &component_name = fieldref.get(ID_component_name);
+  const irep_idt &component_name = field_reference.get(ID_component_name);
 
   exprt accessed_object = checked_dereference(typed_pointer, class_type);
+  const auto type_of = [&ns](const exprt &object) {
+    return to_struct_type(ns.follow(object.type()));
+  };
 
   // The field access is described as being against a particular type, but it
   // may in fact belong to any ancestor type.
-  while(1)
+  while(type_of(accessed_object).get_component(component_name).is_nil())
   {
-    struct_typet object_type =
-      to_struct_type(ns.follow(accessed_object.type()));
-    auto component = object_type.get_component(component_name);
-
-    if(component.is_not_nil())
-      return member_exprt(accessed_object, component);
-
-    // Component not present: check the immediate parent type.
-
-    const auto &components = object_type.components();
+    const auto components = type_of(accessed_object).components();
     INVARIANT(
       components.size() != 0,
       "infer_opaque_type_fields should guarantee that a member access has a "
       "corresponding field");
 
+    // Base class access is always done through the first component
     accessed_object = member_exprt(accessed_object, components.front());
   }
+  return member_exprt(
+    accessed_object, type_of(accessed_object).get_component(component_name));
 }
 
 /// Find all goto statements in 'repl' that target 'old_label' and redirect them

src/goto-programs/remove_virtual_functions.cpp

@@ -139,7 +139,7 @@ static void create_static_function_call(
         call_args[i].type().id() == ID_pointer,
         "where overriding function argument types differ, "
         "those arguments must be pointer-typed");
-      call_args[i].make_typecast(need_type);
+      call_args[i] = typecast_exprt(call_args[i], need_type);
     }
   }
 }