Merge pull request #5352 from smowton/smowton/feature/default-methods

Java frontend: support default methods

Author: smowton

jbmc/regression/jbmc/default-methods/BothInterface.class

@@ -0,0 +1,56 @@
+public class Test extends Parent implements TestInterface, BothInterface {
+
+  public int parentInterfaceOverriddenByTest(int x) { return x + 7; }
+  public int testInterfaceOverriddenByTest(int x) { return x + 8; }
+
+  public static void testme() {
+
+    Test test = new Test();
+    assert test.testInterfaceNotOverridden(1) == 2;
+    assert test.testInterfaceOverriddenByTest(1) == 9;
+    assert test.parentInterfaceNotOverridden(1) == 4;
+    assert test.parentInterfaceOverriddenByParent(1) == 7;
+    assert test.parentInterfaceOverriddenByTest(1) == 8;
+    assert test.testInterfaceOverriddenByParent(1) == 11;
+    assert test.bothInterfaceOverriddenByParent(1) == 13;
+
+    // Check we made it here:
+    assert false;
+
+  }
+
+  public static void main(String[] args) { testme(); }
+
+}
+
+class Parent implements ParentInterface, BothInterface {
+
+  public int parentInterfaceOverriddenByParent(int x) { return x + 6; }
+  // Note this isn't an override here, as this class doesn't implement TestInterface,
+  // but it will become one when Test implements that interface.
+  public int testInterfaceOverriddenByParent(int x) { return x + 10; }
+  public int bothInterfaceOverriddenByParent(int x) { return x + 12; }
+
+}
+
+interface TestInterface {
+
+  default int testInterfaceNotOverridden(int x) { return x + 1; }
+  default int testInterfaceOverriddenByTest(int x) { return x + 2; }
+  default int testInterfaceOverriddenByParent(int x) { return x + 9; }
+
+}
+
+interface ParentInterface {
+
+  default int parentInterfaceNotOverridden(int x) { return x + 3; }
+  default int parentInterfaceOverriddenByParent(int x) { return x + 4; }
+  default int parentInterfaceOverriddenByTest(int x) { return x + 5; }
+
+}
+
+interface BothInterface {
+
+  default int bothInterfaceOverriddenByParent(int x) { return x + 11; }
+
+}

jbmc/regression/jbmc/default-methods/Parent.class

@@ -0,0 +1,13 @@
+CORE
+Test
+--function Test.testme
+line 9 assertion at file Test\.java line 9 function java::Test\.testme:\(\)V bytecode-index 14: SUCCESS
+line 10 assertion at file Test\.java line 10 function java::Test\.testme:\(\)V bytecode-index 25: SUCCESS
+line 11 assertion at file Test\.java line 11 function java::Test\.testme:\(\)V bytecode-index 36: SUCCESS
+line 12 assertion at file Test\.java line 12 function java::Test\.testme:\(\)V bytecode-index 47: SUCCESS
+line 13 assertion at file Test\.java line 13 function java::Test\.testme:\(\)V bytecode-index 58: SUCCESS
+line 14 assertion at file Test\.java line 14 function java::Test\.testme:\(\)V bytecode-index 69: SUCCESS
+line 15 assertion at file Test\.java line 15 function java::Test\.testme:\(\)V bytecode-index 80: SUCCESS
+line 18 assertion at file Test\.java line 18 function java::Test\.testme:\(\)V bytecode-index 86: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/default-methods/ParentInterface.class

@@ -546,8 +546,8 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
   if(!instantiated_classes.count(classname))
     return irep_idt();
 
-  resolve_inherited_componentt call_resolver{symbol_table};
-  const auto resolved_call = call_resolver(classname, call_basename, false);
+  auto resolved_call =
+    get_inherited_method_implementation(call_basename, classname, symbol_table);
 
   if(resolved_call)
     return resolved_call->get_full_component_identifier();

jbmc/regression/jbmc/default-methods/Test.class

@@ -3252,16 +3252,17 @@ 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.
 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();
 }
 

jbmc/regression/jbmc/default-methods/Test.java

@@ -52,8 +52,7 @@ class get_virtual_calleest
     const optionalt<symbol_exprt> &,
     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<symbol_exprt> &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);

jbmc/regression/jbmc/default-methods/TestInterface.class

@@ -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::inherited_componentt>
 resolve_inherited_componentt::operator()(
   const irep_idt &class_id,
   const irep_idt &component_name,
-  bool include_interfaces)
+  bool include_interfaces,
+  const std::function<bool(const symbolt &)> 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);
     }
@@ -102,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<resolve_inherited_componentt::inherited_componentt>
+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;
+}

jbmc/regression/jbmc/default-methods/test.desc

@@ -47,7 +47,10 @@ class resolve_inherited_componentt
   optionalt<inherited_componentt> operator()(
     const irep_idt &class_id,
     const irep_idt &component_name,
-    bool include_interfaces);
+    bool include_interfaces,
+    std::function<bool(const symbolt &)> user_filter = [](const symbolt &) {
+      return true;
+    });
 
   static irep_idt build_full_component_identifier(
     const irep_idt &class_name, const irep_idt &component_name);
@@ -56,4 +59,10 @@ class resolve_inherited_componentt
   const symbol_tablet &symbol_table;
 };
 
+optionalt<resolve_inherited_componentt::inherited_componentt>
+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