From 2ba794dbbc666bfa7664c60cba75c8837b442a6e Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 16 Feb 2018 15:00:49 +0000 Subject: [PATCH 1/2] Introduce fieldref_exprt to represent a field reference --- src/java_bytecode/java_bytecode_parse_tree.h | 17 +++++++++++++++++ src/java_bytecode/java_bytecode_parser.cpp | 5 ++--- src/util/irep_ids.def | 1 + 3 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index 8470d0cb864..bec8445d2f8 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -222,4 +222,21 @@ class java_bytecode_parse_treet } }; +/// Represents the argument of an instruction that uses a CONSTANT_Fieldref +/// This is used for example as an argument to a getstatic and putstatic +/// instruction +class fieldref_exprt : public exprt +{ +public: + fieldref_exprt( + const typet &type, + const irep_idt &component_name, + const irep_idt &class_name) + : exprt(ID_fieldref, type) + { + set(ID_class, class_name); + set(ID_component_name, component_name); + } +}; + #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 93dba637f5a..54d70bbfac5 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -537,9 +537,8 @@ void java_bytecode_parsert::rconstant_pool() symbol_typet class_symbol= java_classname(id2string(class_name_entry.s)); - exprt fieldref("fieldref", type); - fieldref.set(ID_class, class_symbol.get_identifier()); - fieldref.set(ID_component_name, name_entry.s); + fieldref_exprt fieldref( + type, name_entry.s, class_symbol.get_identifier()); it->expr=fieldref; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2cd85d63963..6c65022bcc9 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -840,6 +840,7 @@ IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) +IREP_ID_ONE(fieldref) #undef IREP_ID_ONE #undef IREP_ID_TWO From d2e10af10a5cf9f5de8b383e375a3c321137139a Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 22 Feb 2018 17:45:51 +0000 Subject: [PATCH 2/2] Remove the "fieldref" id Since this was never being read, it adds no value --- src/java_bytecode/java_bytecode_parse_tree.h | 2 +- src/util/irep_ids.def | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_parse_tree.h b/src/java_bytecode/java_bytecode_parse_tree.h index bec8445d2f8..bf5b36c5a2b 100644 --- a/src/java_bytecode/java_bytecode_parse_tree.h +++ b/src/java_bytecode/java_bytecode_parse_tree.h @@ -232,7 +232,7 @@ class fieldref_exprt : public exprt const typet &type, const irep_idt &component_name, const irep_idt &class_name) - : exprt(ID_fieldref, type) + : exprt(ID_empty_string, type) { set(ID_class, class_name); set(ID_component_name, component_name); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 6c65022bcc9..2cd85d63963 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -840,7 +840,6 @@ IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required) -IREP_ID_ONE(fieldref) #undef IREP_ID_ONE #undef IREP_ID_TWO