Ensure member_exprt's type matches the addressed component

Previously we created the expression with the partial type given at the
access site (i.e. as part of the
get/setfield bytecode), but this lacked any generic type information,
which the actual component *did* have.
The member expression could therefore be type-inconsistent with the
object is addressed. Since it's no longer
necessary to make the expression approximately and later fix it up in
typecheck_expr, let's just get it right
the first time, including giving it the right type.

Author: smowton

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -641,20 +641,39 @@ 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)
+static member_exprt
+to_member(const exprt &pointer, const exprt &fieldref, const namespacet &ns)
 {
   struct_tag_typet class_type(fieldref.get(ID_class));
 
-  const typecast_exprt pointer2(pointer, java_reference_type(class_type));
+  const exprt typed_pointer =
+    typecast_exprt::conditional_cast(pointer, java_reference_type(class_type));
 
-  dereference_exprt obj_deref=checked_dereference(pointer2, class_type);
+  const irep_idt &component_name = fieldref.get(ID_component_name);
 
-  const member_exprt member_expr(
-    obj_deref,
-    fieldref.get(ID_component_name),
-    fieldref.type());
+  exprt accessed_object = checked_dereference(typed_pointer, class_type);
 
-  return member_expr;
+  // The field access is described as being against a particular type, but it
+  // may in fact belong to any ancestor type.
+  while(1)
+  {
+    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();
+    INVARIANT(
+      components.size() != 0,
+      "infer_opaque_type_fields should guarantee that a member access has a "
+      "corresponding field");
+
+    accessed_object = member_exprt(accessed_object, components.front());
+  }
 }
 
 /// Find all goto statements in 'repl' that target 'old_label' and redirect them
@@ -1530,7 +1549,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="getfield")
     {
       PRECONDITION(op.size() == 1 && results.size() == 1);
-      results[0]=java_bytecode_promotion(to_member(op[0], arg0));
+      results[0] = java_bytecode_promotion(to_member(op[0], arg0, ns));
     }
     else if(statement=="getstatic")
     {
@@ -2543,7 +2562,7 @@ code_blockt java_bytecode_convert_methodt::convert_putfield(
     block,
     bytecode_write_typet::FIELD,
     arg0.get(ID_component_name));
-  block.add(code_assignt(to_member(op[0], arg0), op[1]));
+  block.add(code_assignt(to_member(op[0], arg0, ns), op[1]));
   return block;
 }
 
@@ -2918,8 +2937,7 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   if(return_type.id() == ID_empty)
     return {};
 
-  const auto value =
-    zero_initializer(return_type, location, namespacet(symbol_table));
+  const auto value = zero_initializer(return_type, location, ns);
   if(!value.has_value())
   {
     error().source_location = location;

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -43,6 +43,7 @@ class java_bytecode_convert_methodt:public messaget
     bool threading_support)
     : messaget(_message_handler),
       symbol_table(symbol_table),
+      ns(symbol_table),
       max_array_length(_max_array_length),
       throw_assertion_error(throw_assertion_error),
       threading_support(threading_support),
@@ -69,6 +70,7 @@ class java_bytecode_convert_methodt:public messaget
 
 protected:
   symbol_table_baset &symbol_table;
+  namespacet ns;
   const size_t max_array_length;
   const bool throw_assertion_error;
   const bool threading_support;

jbmc/src/java_bytecode/java_bytecode_typecheck.h

@@ -69,7 +69,6 @@ class java_bytecode_typecheckt:public typecheckt
   void typecheck_code(codet &);
   void typecheck_type(typet &);
   void typecheck_expr_symbol(symbol_exprt &);
-  void typecheck_expr_member(member_exprt &);
   void typecheck_expr_java_new(side_effect_exprt &);
   void typecheck_expr_java_new_array(side_effect_exprt &);
 

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -52,8 +52,6 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
     else if(statement==ID_java_new_array)
       typecheck_expr_java_new_array(to_side_effect_expr(expr));
   }
-  else if(expr.id()==ID_member)
-    typecheck_expr_member(to_member_expr(expr));
 }
 
 void java_bytecode_typecheckt::typecheck_expr_java_new(side_effect_exprt &expr)
@@ -120,46 +118,3 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
     expr.type()=symbol.type;
   }
 }
-
-void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
-{
-  // The member might be in a parent class or an opaque class, which we resolve
-  // here.
-  const irep_idt component_name=expr.get_component_name();
-
-  while(1)
-  {
-    typet base_type(ns.follow(expr.struct_op().type()));
-
-    if(base_type.id()!=ID_struct)
-      break; // give up
-
-    struct_typet &struct_type=
-      to_struct_type(base_type);
-
-    if(struct_type.has_component(component_name))
-      return; // done
-
-    // look at parent
-    struct_typet::componentst &components=
-      struct_type.components();
-
-    if(components.empty())
-      break;
-
-    const struct_typet::componentt &c=components.front();
-
-    member_exprt m(expr.struct_op(), c.get_name(), c.type());
-    m.add_source_location()=expr.source_location();
-
-    expr.struct_op()=m;
-  }
-
-  warning().source_location=expr.source_location();
-  warning() << "failed to find field `"
-            << component_name << "` in class hierarchy" << eom;
-
-  // We replace by a non-det of same type
-  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
-  expr.swap(nondet);
-}