-
Notifications
You must be signed in to change notification settings - Fork 280
Complete Java lambda support [TG-11760] #5350
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
Complete Java lambda support [TG-11760] #5350
Conversation
@@ -426,7 +426,8 @@ void java_bytecode_convert_classt::convert( | |||
lambda_entry.second.is_unknown_handle() | |||
? class_type.add_unknown_lambda_method_handle() | |||
: class_type.add_lambda_method_handle( | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref)); | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
⛏️ ID_java + "::"
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
not sure - "java::" is quite a common string - probably makes more sense to pull out a ID_java_prefix than hide a few of them with this
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also unchanged by this PR
for(const auto &method : methods) | ||
{ | ||
const auto &name = method.get_name(); | ||
static irep_idt equals = "equals"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const
?
cc0baa7
to
f2bd2ae
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In a couple of places you allow the name of the method to match the name of the method found in the functional interface, but afaict you don't have any tests for this scenario, can they be added.
Couple of minor points but looks good
@@ -426,7 +426,8 @@ void java_bytecode_convert_classt::convert( | |||
lambda_entry.second.is_unknown_handle() | |||
? class_type.add_unknown_lambda_method_handle() | |||
: class_type.add_lambda_method_handle( | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref)); | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
not sure - "java::" is quite a common string - probably makes more sense to pull out a ID_java_prefix than hide a few of them with this
@@ -426,7 +426,8 @@ void java_bytecode_convert_classt::convert( | |||
lambda_entry.second.is_unknown_handle() | |||
? class_type.add_unknown_lambda_method_handle() | |||
: class_type.add_lambda_method_handle( | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref)); | |||
"java::" + id2string(lambda_entry.second.lambda_method_ref), |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also unchanged by this PR
} | ||
if(!ns.lookup(name).type.get_bool(ID_C_abstract)) | ||
continue; | ||
if(result.has_value() && name != *result) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is it allowed for a functional interface to have two unimplemented methods with the same name?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These are mangled names (since we expect to find them in ns
); renamed to clarify.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure - but I don't understand why an interface would be allowed to have two methods with the same mangled name? I mean - surely that is just impossible? I.e. in what circumstances is result.has_value() && name == *result
?
jbmc/regression/jbmc/lambda-interface-declaring-equals/InterfaceDeclaringEquals.java
Show resolved
Hide resolved
b132efd
to
4b58a79
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Still a little confused about the check for the mangled name - happy to chat in slack if easier to explain
lambda_method_handle.handle_type = | ||
method_handle_typet::LAMBDA_METHOD_HANDLE; | ||
|
||
return lambda_method_handle; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
💡 Given that this could happen - it might make sense to output a warning, or even an invariant
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oops approved too early - could you have a look at the gaps in testing highlighted by code cov, in particular:
- 🚫 a test for with an interface that contains two methods
- 🚫 a test for an interface with one method, and inherits another
- ❓ a test for a constructor? - I thought I'd seen this, but there is a whole untested function:
instantiate_new_object
- 💡 and ideally something to cover this line: https://codecov.io/gh/diffblue/cbmc/compare/c6082355bde3657bdfdefde8eff16a2813684b54...4b58a793061915277cf8255c628f94bff27414af/diff#D32-1244
This paves the way for supporting multiple lambda method kinds, e.g. newinvokespecial lambdas which instantiate and construct a type.
Previously we failed to detect a functional interface when the abstract method being implemented was inherited, or the interface also declared methods which are defined on java.lang.Object such as toString.
Usually an intermediate synthetic method is created by javac, but sometimes it can use a direct reference to a method, which we would previously have failed to spot. For example, Callable c = x -> x + 1 will generate a synthetic private method housing the body of the lambda, but Callable c = SomeClass::someCallable may not generate one but rather directly use SomeClass.someCallable as the lambda target. Whether this happens in practice depends on the compiler.
These encode a lambda that instantiates and constructs an instance of some type without using an intermediate method.
These compile down to direct references to a static, virtual and interface method (i.e. to method reference kinds REF_invokeStatic, REF_invokeVirtual and REF_invokeInterface as described at https://docs.oracle.com/javase/9/docs/api/java/lang/invoke/MethodHandleInfo.html)
To support these we store lambda descriptors in the same form as virtual method references, using class_method_descriptor_exprt, lowering it to a symbol_exprt if we have a known callee. This is also the first form of synthetic method to produce a virtual method call, hence the alteration of notify_static_method_calls to tolerate them.
They are method handles not references, and their varieties are kinds not types
…_callt This is currently dead code, so replace it with an invariant describing the situation.
Along with the basename already stored on class_typet::methodt, this means we can compare two Java methods for name and descriptor compatibility without having to parse the composite method identifier.
…ral methods For example, if Intf1 declares int f(int) and so does Intf2, then Merge which implements both Intf1 and Intf2 is a functional interface.
9fcd9b9
to
8525cab
Compare
8525cab
to
9e6eee5
Compare
"that has changed, remove this invariant. Also note that " | ||
"as of the time of writing remove_virtual_functions did " | ||
"not support this form of function call."); | ||
// needed_lazy_methods->add_needed_method(fn_sym->get_identifier()); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
⛏️ remove or comment with #if 0
…xplicitly abstracting methods It's possible to make a functional interface by taking a parent or parents that have more than one abstract method, then inheriting default definitions or making definitions yourself so that only one abstract method remains, and so the interface becomes functional. Similarly you can re-declare a method as abstract even if a parent made a default definition. This commit adds support for all of these cases and tests them.
9e6eee5
to
af9104f
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5350 +/- ##
===========================================
+ Coverage 68.16% 68.17% +0.01%
===========================================
Files 1170 1170
Lines 96450 96535 +85
===========================================
+ Hits 65743 65817 +74
- Misses 30707 30718 +11
Continue to review full report at Codecov.
|
Requested changes applied; diff is now entirely covered apart from errors that should now be unreachable
This adds the various missing pieces of Java lambda support:
this::f
orsomeInterface::method
)newinvokespecial
lambda binding, used forSomeType::new
, which means we must both instantiate and call the constructorequals
orhashCode