Merge pull request #3915 from thk123/use-fieldref-exprt

Use fieldref exprt

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -657,15 +657,15 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
 ///   components if necessary.
 static member_exprt to_member(
   const exprt &pointer,
-  const exprt &field_reference,
+  const fieldref_exprt &field_reference,
   const namespacet &ns)
 {
-  struct_tag_typet class_type(field_reference.get(ID_class));
+  struct_tag_typet class_type(field_reference.class_name());
 
   const exprt typed_pointer =
     typecast_exprt::conditional_cast(pointer, java_reference_type(class_type));
 
-  const irep_idt &component_name = field_reference.get(ID_component_name);
+  const irep_idt &component_name = field_reference.component_name();
 
   exprt accessed_object = checked_dereference(typed_pointer, class_type);
   const auto type_of = [&ns](const exprt &object) {
@@ -1559,7 +1559,8 @@ 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, ns));
+      results[0] = java_bytecode_promotion(
+        to_member(op[0], expr_dynamic_cast<fieldref_exprt>(arg0), ns));
     }
     else if(statement=="getstatic")
     {
@@ -1582,7 +1583,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="putfield")
     {
       PRECONDITION(op.size() == 2 && results.empty());
-      c = convert_putfield(arg0, op);
+      c = convert_putfield(expr_dynamic_cast<fieldref_exprt>(arg0), op);
     }
     else if(statement=="putstatic")
     {
@@ -2588,15 +2589,12 @@ code_blockt java_bytecode_convert_methodt::convert_putstatic(
 }
 
 code_blockt java_bytecode_convert_methodt::convert_putfield(
-  const exprt &arg0,
+  const fieldref_exprt &arg0,
   const exprt::operandst &op)
 {
   code_blockt block;
   save_stack_entries(
-    "stack_field",
-    block,
-    bytecode_write_typet::FIELD,
-    arg0.get(ID_component_name));
+    "stack_field", block, bytecode_write_typet::FIELD, arg0.component_name());
   block.add(code_assignt(to_member(op[0], arg0, ns), op[1]));
   return block;
 }

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -395,7 +395,8 @@ class java_bytecode_convert_methodt:public messaget
     codet &c,
     exprt::operandst &results);
 
-  code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op);
+  code_blockt
+  convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op);
 
   code_blockt convert_putstatic(
     const source_locationt &location,

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -311,16 +311,17 @@ static void infer_opaque_type_fields(
       if(instruction.statement == "getfield" ||
          instruction.statement == "putfield")
       {
-        const exprt &fieldref = instruction.args[0];
-        irep_idt class_symbol_id = fieldref.get(ID_class);
+        const fieldref_exprt &fieldref =
+          expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
+        irep_idt class_symbol_id = fieldref.class_name();
         const symbolt *class_symbol = symbol_table.lookup(class_symbol_id);
         INVARIANT(
           class_symbol != nullptr,
           "all types containing fields should have been loaded");
 
         const java_class_typet *class_type =
           &to_java_class_type(class_symbol->type);
-        const irep_idt &component_name = fieldref.get(ID_component_name);
+        const irep_idt &component_name = fieldref.component_name();
         while(!class_type->has_component(component_name))
         {
           if(class_type->get_is_stub())
@@ -582,12 +583,10 @@ static void create_stub_global_symbols(
         INVARIANT(
           instruction.args.size() > 0,
           "get/putstatic should have at least one argument");
-        irep_idt component = instruction.args[0].get_string(ID_component_name);
-        INVARIANT(
-          !component.empty(), "get/putstatic should specify a component");
-        irep_idt class_id = instruction.args[0].get_string(ID_class);
-        INVARIANT(
-          !class_id.empty(), "get/putstatic should specify a class");
+        const fieldref_exprt &field_ref =
+          expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
+        irep_idt component = field_ref.component_name();
+        irep_idt class_id = field_ref.class_name();
 
         // The final 'true' parameter here includes interfaces, as they can
         // define static fields.

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -337,6 +337,22 @@ class fieldref_exprt : public exprt
     set(ID_class, class_name);
     set(ID_component_name, component_name);
   }
+
+  irep_idt class_name() const
+  {
+    return get(ID_class);
+  }
+
+  irep_idt component_name() const
+  {
+    return get(ID_component_name);
+  }
 };
 
+template <>
+inline bool can_cast_expr<fieldref_exprt>(const exprt &base)
+{
+  return base.get(ID_class) != ID_nil && base.get(ID_component_name) != ID_nil;
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H