From e4f215c1cdc0bc6cd035054be412040499815831 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 23 Jan 2019 15:44:43 +0000 Subject: [PATCH 1/4] Add documentation to the member_of function --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 374fa6254a2..f276804db5e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -647,6 +647,14 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt) throw "unhandled java comparison instruction"; } +/// Build a member exprt for accessing a specific field that may come from a +/// base class. +/// \param pointer: The expression to access the field on. +/// \param fieldref: A getfield/setfield instruction produced by the bytecode +/// parser. +/// \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 &fieldref, const namespacet &ns) { From 09213d3171c620f195d22b7e82541ed2be4c0cbd Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 23 Jan 2019 15:45:24 +0000 Subject: [PATCH 2/4] Rename fieldref to clearer and lint-correct name --- .../java_bytecode/java_bytecode_convert_method.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index f276804db5e..4d29bf9ff9b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -650,20 +650,22 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt) /// Build a member exprt for accessing a specific field that may come from a /// base class. /// \param pointer: The expression to access the field on. -/// \param fieldref: A getfield/setfield instruction produced by the bytecode -/// parser. +/// \param field_reference: A getfield/setfield instruction produced by the +/// bytecode parser. /// \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 &fieldref, const namespacet &ns) +static member_exprt to_member( + const exprt &pointer, + const exprt &field_reference, + const namespacet &ns) { - struct_tag_typet class_type(fieldref.get(ID_class)); + struct_tag_typet class_type(field_reference.get(ID_class)); const exprt typed_pointer = typecast_exprt::conditional_cast(pointer, java_reference_type(class_type)); - const irep_idt &component_name = fieldref.get(ID_component_name); + const irep_idt &component_name = field_reference.get(ID_component_name); exprt accessed_object = checked_dereference(typed_pointer, class_type); From 659cc0bcd30faa2eedee312062df47aa1d03ef46 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 23 Jan 2019 15:59:39 +0000 Subject: [PATCH 3/4] Refactor member_of to make while loop clearer --- .../java_bytecode_convert_method.cpp | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 4d29bf9ff9b..74299a6f2de 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -668,28 +668,25 @@ static member_exprt to_member( const irep_idt &component_name = field_reference.get(ID_component_name); exprt accessed_object = checked_dereference(typed_pointer, class_type); + const auto type_of = [&ns](const exprt &object) { + return to_struct_type(ns.follow(object.type())); + }; // The field access is described as being against a particular type, but it // may in fact belong to any ancestor type. - while(1) + while(type_of(accessed_object).get_component(component_name).is_nil()) { - 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(); + const auto components = type_of(accessed_object).components(); INVARIANT( components.size() != 0, "infer_opaque_type_fields should guarantee that a member access has a " "corresponding field"); + // Base class access is always done through the first component accessed_object = member_exprt(accessed_object, components.front()); } + return member_exprt( + accessed_object, type_of(accessed_object).get_component(component_name)); } /// Find all goto statements in 'repl' that target 'old_label' and redirect them From b863377f1ae56f932ae89d6332948af0c4c2f162 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 23 Jan 2019 17:35:52 +0000 Subject: [PATCH 4/4] Remove deprecated call to make_typecast --- src/goto-programs/remove_virtual_functions.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index ec564b9c821..aa4863629c2 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -139,7 +139,7 @@ static void create_static_function_call( call_args[i].type().id() == ID_pointer, "where overriding function argument types differ, " "those arguments must be pointer-typed"); - call_args[i].make_typecast(need_type); + call_args[i] = typecast_exprt(call_args[i], need_type); } } }