diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 74299a6f2de..938ec646f04 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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(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(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; } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 94202ee9d65..eefd2c77a8b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/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, diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 89405927ff3..5bb0f861d5d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -311,8 +311,9 @@ 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(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, @@ -320,7 +321,7 @@ static void infer_opaque_type_fields( 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(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. diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 78f9b86b14e..99e03329b87 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/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(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