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);