Skip to content

Java frontend: support default methods #5352

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
May 21, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file not shown.
Binary file added jbmc/regression/jbmc/default-methods/Parent.class
Binary file not shown.
Binary file not shown.
Binary file added jbmc/regression/jbmc/default-methods/Test.class
Binary file not shown.
56 changes: 56 additions & 0 deletions jbmc/regression/jbmc/default-methods/Test.java
Original file line number Diff line number Diff line change
@@ -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; }

}
Binary file not shown.
13 changes: 13 additions & 0 deletions jbmc/regression/jbmc/default-methods/test.desc
Original file line number Diff line number Diff line change
@@ -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$
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/ci_lazy_methods.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
7 changes: 4 additions & 3 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

Expand Down
35 changes: 8 additions & 27 deletions src/goto-programs/remove_virtual_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
};
Expand Down Expand Up @@ -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())
Expand Down Expand Up @@ -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();
Expand All @@ -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);
}
}

Expand All @@ -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);
Expand All @@ -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);
Expand Down
48 changes: 46 additions & 2 deletions src/goto-programs/resolve_inherited_component.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand All @@ -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);
}
Expand Down Expand Up @@ -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;
}
11 changes: 10 additions & 1 deletion src/goto-programs/resolve_inherited_component.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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