From fd32f9bb7396b8d8cee6aefa99716a08cba5e39e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 13 Mar 2020 12:54:02 +0000 Subject: [PATCH 1/3] Resolve inherited component: support filtering by a user-specified condition --- src/goto-programs/resolve_inherited_component.cpp | 8 ++++++-- src/goto-programs/resolve_inherited_component.h | 5 ++++- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp index ace9bd78438..15e230d8324 100644 --- a/src/goto-programs/resolve_inherited_component.cpp +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -27,12 +27,15 @@ resolve_inherited_componentt::resolve_inherited_componentt( /// class specifier) /// \param include_interfaces: If true, consider inheritance from interfaces /// (parent types other than the first listed) +/// \param user_filter: Predicate that should return true for symbols that can +/// be returned. Those for which it returns false will be ignored. /// \return The concrete component that has been resolved optionalt resolve_inherited_componentt::operator()( const irep_idt &class_id, const irep_idt &component_name, - bool include_interfaces) + bool include_interfaces, + const std::function user_filter) { PRECONDITION(!class_id.empty()); PRECONDITION(!component_name.empty()); @@ -47,7 +50,8 @@ resolve_inherited_componentt::operator()( const irep_idt &full_component_identifier= build_full_component_identifier(current_class, component_name); - if(symbol_table.has_symbol(full_component_identifier)) + const symbolt *symbol = symbol_table.lookup(full_component_identifier); + if(symbol && user_filter(*symbol)) { return inherited_componentt(current_class, component_name); } diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h index 7805e765ba2..af28732abec 100644 --- a/src/goto-programs/resolve_inherited_component.h +++ b/src/goto-programs/resolve_inherited_component.h @@ -47,7 +47,10 @@ class resolve_inherited_componentt optionalt operator()( const irep_idt &class_id, const irep_idt &component_name, - bool include_interfaces); + bool include_interfaces, + std::function user_filter = [](const symbolt &) { + return true; + }); static irep_idt build_full_component_identifier( const irep_idt &class_name, const irep_idt &component_name); From bd4b15ed1df95fb2c1e7d393c4eb836deb1236a3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 13 Mar 2020 12:50:18 +0000 Subject: [PATCH 2/3] Add get-inherited-method utility This takes inheritance from interface default methods into account. --- .../resolve_inherited_component.cpp | 40 +++++++++++++++++++ .../resolve_inherited_component.h | 6 +++ 2 files changed, 46 insertions(+) diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp index 15e230d8324..e602c4f81c3 100644 --- a/src/goto-programs/resolve_inherited_component.cpp +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -106,3 +106,43 @@ irep_idt resolve_inherited_componentt::inherited_componentt:: return resolve_inherited_componentt::build_full_component_identifier( class_identifier, component_identifier); } + +/// Given a class and a component, identify the concrete method it is +/// resolved to. For example, a reference Child.abc refers to Child's method or +/// field if it exists, or else Parent.abc, and so on regarding Parent's +/// ancestors. If none are found, an empty string will be returned. +/// This looks first for non-abstract methods inherited from the first base +/// (i.e., for Java the superclass), then for non-abstract methods inherited +/// otherwise (for Java, interface default methods), then for any abstract +/// declaration. +/// \param classname: The name of the class the function is being called on +/// \param call_basename: The base name of the component (i.e. without the +/// class specifier) +/// \param symbol_table: Global symbol table +/// \return The concrete component that has been resolved +optionalt +get_inherited_method_implementation( + const irep_idt &call_basename, + const irep_idt &classname, + const symbol_tablet &symbol_table) +{ + resolve_inherited_componentt call_resolver{symbol_table}; + auto exclude_abstract_methods = [&](const symbolt &symbol) { + return !symbol.type.get_bool(ID_C_abstract); + }; + + auto resolved_call = + call_resolver(classname, call_basename, false, exclude_abstract_methods); + if(!resolved_call) + { + // Check for a default implementation: + resolved_call = + call_resolver(classname, call_basename, true, exclude_abstract_methods); + } + if(!resolved_call) + { + // Finally accept any abstract definition, which will likely get stubbed: + resolved_call = call_resolver(classname, call_basename, true); + } + return resolved_call; +} diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h index af28732abec..17d6e8add03 100644 --- a/src/goto-programs/resolve_inherited_component.h +++ b/src/goto-programs/resolve_inherited_component.h @@ -59,4 +59,10 @@ class resolve_inherited_componentt const symbol_tablet &symbol_table; }; +optionalt +get_inherited_method_implementation( + const irep_idt &call_basename, + const irep_idt &classname, + const symbol_tablet &symbol_table); + #endif // CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H From 1231e22e89e2e77fd9c536b978e352fa01dbeaec Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 13 Mar 2020 10:35:23 +0000 Subject: [PATCH 3/3] Java frontend: inherit default method implementations All areas of the codebase that resolve method implementations can now inherit a default method when neither a class nor any of its parents provide a definition. --- .../jbmc/default-methods/BothInterface.class | Bin 0 -> 289 bytes .../jbmc/default-methods/Parent.class | Bin 0 -> 617 bytes .../default-methods/ParentInterface.class | Bin 0 -> 499 bytes .../jbmc/default-methods/Test.class | Bin 0 -> 1618 bytes .../regression/jbmc/default-methods/Test.java | 56 ++++++++++++++++++ .../jbmc/default-methods/TestInterface.class | Bin 0 -> 490 bytes .../regression/jbmc/default-methods/test.desc | 13 ++++ jbmc/src/java_bytecode/ci_lazy_methods.cpp | 4 +- .../java_bytecode_convert_method.cpp | 7 ++- .../remove_virtual_functions.cpp | 35 +++-------- 10 files changed, 83 insertions(+), 32 deletions(-) create mode 100644 jbmc/regression/jbmc/default-methods/BothInterface.class create mode 100644 jbmc/regression/jbmc/default-methods/Parent.class create mode 100644 jbmc/regression/jbmc/default-methods/ParentInterface.class create mode 100644 jbmc/regression/jbmc/default-methods/Test.class create mode 100644 jbmc/regression/jbmc/default-methods/Test.java create mode 100644 jbmc/regression/jbmc/default-methods/TestInterface.class create mode 100644 jbmc/regression/jbmc/default-methods/test.desc diff --git a/jbmc/regression/jbmc/default-methods/BothInterface.class b/jbmc/regression/jbmc/default-methods/BothInterface.class new file mode 100644 index 0000000000000000000000000000000000000000..0b25dd2a3239fca7d3d67075644ceefc9a2a01a7 GIT binary patch literal 289 zcmY+9%}xSA5QMAOg_S?qc<{o3t6tz@Oo%s3NH!s0;>NSHyR8gaW|Ltc@=iVh2OhwO zGWG}uIdt{Zm+DI9`)7XuaE~~`RfH~~pH*&=7{~TqId(f|Me literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/default-methods/Parent.class b/jbmc/regression/jbmc/default-methods/Parent.class new file mode 100644 index 0000000000000000000000000000000000000000..a6800570ff0c4b13d5a7fbe727149b9835fe3264 GIT binary patch literal 617 zcmah_!A`giW}!I z81mq;(QyaD)3j;w_V3P+Z_ai@6$bs90TXHZM3WAAf|e%Kpv)+zk3YcP2^h%6gs51C zO)-}cuuces^VpymiO+~_P);8>nfo^av*N>8TuKO2F;P)~Lvn`AMK<=FO=X2magj}K N&ZfG;W-Fe4`xiNmXDa{z literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/default-methods/ParentInterface.class b/jbmc/regression/jbmc/default-methods/ParentInterface.class new file mode 100644 index 0000000000000000000000000000000000000000..b46fd08684179c2c2bc72e9015e9c1913b27b186 GIT binary patch literal 499 zcmaiw%}N7749EZ3uHCkN^yA<~LA>du>%oKIO+i>#TEXJk+1;p9)>)ZOi@uXj;K2v* zp~MUo#J1Q&lF2{GFJV5v-ai1Gq8FhPp-b3*R+f!RjAMJRavoG}IAd#dQLrI|N6B#_ z;j${2&`!1C!SpF(J5pIGN-wQ)Ro*JAef}ec?om$&-Sqk|`F*+$VU%@`$Z zwV>w(#EO7_)G!TuOu(D!T^5k0i+Nojnl(&)VS95`x0aYJ5X%;GT47nU3|?1^lD%P+ zC`NWkFWDmkU0a%^oA$hE>(-i<(;x2WmSyDgx;gcdDHK07-#bqyzo3W4PMfSJ(EYr> zNyke(5r{0>TJHG+ZOci3Iz~I2nqdkgQctqav>h!|(9HGBqHP)G`iN7JX020>@jBa- z@M_WCsC)h+rxIfPH^VBU`-GyaoWN+VQ0a4MvAAvJ^f`mO8eF2X`Z#X|t!Sfa*q|VR z76sEt3bY;;HCdH#*0PG0g7Zi!m|^H+=wi6aaD|}B8h2r3$FgzdD-&?sp1rS~B|(8PldLce3AjA*Wu3FyRGT9IN%60-9!u{|{UI#l`T zJDMDI_BzgqGNIy3RLbfcxeM;@@i2j7VWbno1X+f17?Gr-xRmb)@I2m!_x?vnyJ$*F zd+_<*AbbEnndP63xtYxYHR!fG^q}lEJM@rR-yT*2b@_@Ku4|8|5x2dT982JJBuFDf z^8o#W)bbF95XJ(Dv4#j9get_full_component_identifier(); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index fd22667eb84..2268df731fe 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -3252,7 +3252,7 @@ void java_bytecode_convert_method( } /// Returns true iff method \p methodid from class \p classname is -/// a method inherited from a class (and not an interface!) from which +/// a method inherited from a class or interface from which /// \p classname inherits, either directly or indirectly. /// \param classname: class whose method is referenced /// \param mangled_method_name: The particular overload of a given method. @@ -3260,8 +3260,9 @@ bool java_bytecode_convert_methodt::is_method_inherited( const irep_idt &classname, const irep_idt &mangled_method_name) const { - const auto inherited_method = get_inherited_component( - classname, mangled_method_name, symbol_table, false); + const auto inherited_method = get_inherited_method_implementation( + mangled_method_name, classname, symbol_table); + return inherited_method.has_value(); } diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 1b612a8b3da..6c473d23f80 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -52,8 +52,7 @@ class get_virtual_calleest const optionalt &, const irep_idt &, dispatch_table_entriest &, - dispatch_table_entries_mapt &, - const function_call_resolvert &) const; + dispatch_table_entries_mapt &) const; exprt get_method(const irep_idt &class_id, const irep_idt &component_name) const; }; @@ -510,14 +509,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( /// get_child_functions_rec("C", C.f, "f") /// -> [{"C", C.f}, {"B", C.f}, {"A", A.f}] /// \param entry_map: map of class identifiers to dispatch table entries -/// \param resolve_function_call`: function to resolve abstract method call void get_virtual_calleest::get_child_functions_rec( const irep_idt &this_id, const optionalt &last_method_defn, const irep_idt &component_name, dispatch_table_entriest &functions, - dispatch_table_entries_mapt &entry_map, - const function_call_resolvert &resolve_function_call) const + dispatch_table_entries_mapt &entry_map) const { auto findit=class_hierarchy.class_map.find(this_id); if(findit==class_hierarchy.class_map.end()) @@ -550,7 +547,8 @@ void get_virtual_calleest::get_child_functions_rec( } if(!function.symbol_expr.has_value()) { - const auto resolved_call = resolve_function_call(child, component_name); + const auto resolved_call = get_inherited_method_implementation( + component_name, child, symbol_table); if(resolved_call) { function.class_id = resolved_call->get_class_identifier(); @@ -566,12 +564,7 @@ void get_virtual_calleest::get_child_functions_rec( entry_map.emplace(child, function); get_child_functions_rec( - child, - function.symbol_expr, - component_name, - functions, - entry_map, - resolve_function_call); + child, function.symbol_expr, component_name, functions, entry_map); } } @@ -590,15 +583,8 @@ void get_virtual_calleest::get_functions( const std::string function_name_string(id2string(function_name)); INVARIANT(!class_id.empty(), "All virtual functions must have a class"); - resolve_inherited_componentt get_virtual_call_target{symbol_table}; - const function_call_resolvert resolve_function_call = - [&get_virtual_call_target]( - const irep_idt &class_id, const irep_idt &function_name) { - return get_virtual_call_target(class_id, function_name, false); - }; - - const auto resolved_call = - get_virtual_call_target(class_id, function_name, false); + auto resolved_call = + get_inherited_method_implementation(function_name, class_id, symbol_table); // might be an abstract function dispatch_table_entryt root_function(class_id); @@ -618,12 +604,7 @@ void get_virtual_calleest::get_functions( // iterate over all children, transitively dispatch_table_entries_mapt entry_map; get_child_functions_rec( - class_id, - root_function.symbol_expr, - function_name, - functions, - entry_map, - resolve_function_call); + class_id, root_function.symbol_expr, function_name, functions, entry_map); if(root_function.symbol_expr.has_value()) functions.push_back(root_function);