Use fieldref_expr to make the parsing more precise

Author: thk123

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -655,15 +655,17 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt)
 /// \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_instruction, const namespacet &ns)
+static member_exprt to_member(
+  const exprt &pointer,
+  const fieldref_exprt &field_instruction,
+  const namespacet &ns)
 {
-  struct_tag_typet class_type(field_instruction.get(ID_class));
+  struct_tag_typet class_type(field_instruction.field_of_class());
 
   const exprt typed_pointer =
     typecast_exprt::conditional_cast(pointer, java_reference_type(class_type));
 
-  const irep_idt &component_name = field_instruction.get(ID_component_name);
+  const irep_idt &component_name = field_instruction.component_name();
 
   exprt accessed_object = checked_dereference(typed_pointer, class_type);
   const auto type_of = [&](const exprt &object) {
@@ -1560,7 +1562,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")
     {
@@ -1583,7 +1586,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")
     {
@@ -2592,15 +2595,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.field_of_class();
         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.field_of_class();
 
         // The final 'true' parameter here includes interfaces, as they can
         // define static fields.

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -341,6 +341,22 @@ class fieldref_exprt : public exprt
     set(ID_class, class_name);
     set(ID_component_name, component_name);
   }
+
+  irep_idt field_of_class() 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