Java frontend: support lambda autoboxing against generic types

It's possible to use a primitive-typed method-reference to implement an appropriately
specialised generic functional interface (e.g. something that takes an integer can satisfy
Consumer<Byte> by direct method reference without needing to introduce a stub method to do
the conversion).

Here we implement that by unboxing using the java.lang.Number interface where necessary, thereby
catching all valid widening numeric casts at the same time (Short.intValue for example will
do the widening and deliver the required primitive type). When boxing we always box to the
primitive type's corresponding boxed type, as this is all the compiler seems to allow (i.e. it
won't allow satisfying Producer<Long> using a function that returns an int, even though that is
type-safe).

Note this solution uses virtual dispatch a little more often than is needed: in some simple cases
the class file contains enough information to know that the Object we're unboxing must in practice
be an Integer (for example) and so no dispatch is necessary. That doesn't account for all cases
where a generic interface is implemented however, so I did not pursue this possibility.

Author: smowton

jbmc/regression/jbmc/lambda-generic-boxing/Test$TakesInt.class

@@ -0,0 +1,66 @@
+public class Test {
+
+  interface TakesT<T> {
+    public Object take(T t);
+  }
+
+  interface YieldsT<T> {
+    public T yield();
+  }
+
+  interface TakesInt {
+    public Object take(int i);
+  }
+
+  interface TakesLong {
+    public Object take(long l);
+  }
+
+  interface YieldsInt {
+    public int yield();
+  }
+
+  public static Object takesLong(long l) { return l; }
+
+  public static short yieldsShort() { return (short)1; }
+
+  public static void test() {
+
+    // Implement a generic interface using a primitive-typed function
+    // that requires us to unbox the Short then widen it:
+    TakesT<Short> takesShort = Test::takesLong;
+    assert takesShort.take((short)1).equals(1L);
+
+    // Surprisingly, the following case doesn't compile despite
+    // being type-safe and symmetrical to the one above:
+    // YieldsT<Long> yieldsLong = Test::yieldsShort;
+
+    // So instead, here's a simpler case, that just requires us
+    // to box the return value, not widen it then box:
+    YieldsT<Short> yieldsShort = Test::yieldsShort;
+    assert yieldsShort.yield() == (short)1;
+
+    // Now test the reverse: using an instantiated generic to
+    // implement a primitive-typed interface:
+
+    TakesT<Long> takesLong = x -> x + 1;
+    // Again this doesn't compile:
+    // TakesInt takesInt = takesLong::take;
+    // So here's a simpler example that only boxes to implement the
+    // primitive interface, rather than boxes then widens:
+    TakesLong takesPrimitiveLong = takesLong::take;
+    assert takesPrimitiveLong.take(1L).equals(2L);
+
+    // And finally, using an instantiated generic to satisfy a primitive
+    // return value. This one does work with the conversion requiring both
+    // to unbox the value and to widen it.
+    YieldsT<Short> yieldsShortGeneric = () -> (short)1;
+    YieldsInt yieldsInt = yieldsShortGeneric::yield;
+    assert yieldsInt.yield() == 1;
+
+    // Check we got to the end:
+    assert false;
+
+  }
+
+}

jbmc/regression/jbmc/lambda-generic-boxing/Test$TakesLong.class

@@ -0,0 +1,10 @@
+CORE
+Test
+--function Test.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+\[java::Test\.test:\(\)V\.assertion\.1\] line 32 assertion at file Test\.java line 32 function java::Test\.test:\(\)V bytecode-index 15: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.2\] line 41 assertion at file Test\.java line 41 function java::Test\.test:\(\)V bytecode-index 29: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.3\] line 52 assertion at file Test\.java line 52 function java::Test\.test:\(\)V bytecode-index 50: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.4\] line 59 assertion at file Test\.java line 59 function java::Test\.test:\(\)V bytecode-index 68: SUCCESS
+\[java::Test\.test:\(\)V\.assertion\.5\] line 62 assertion at file Test\.java line 62 function java::Test\.test:\(\)V bytecode-index 74: FAILURE
+^EXIT=10$
+^SIGNAL=0$

jbmc/regression/jbmc/lambda-generic-boxing/Test$TakesT.class

@@ -72,33 +72,41 @@ get_java_primitive_type_info(const typet &maybe_primitive_type)
     type_info_by_primitive_type = {
       {java_boolean_type(),
        {"java::java.lang.Boolean",
-        "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;"}},
+        "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;",
+        "java::java.lang.Boolean.booleanValue:()Z"}},
       {java_byte_type(),
        {"java::java.lang.Byte",
-        "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;"}},
+        "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;",
+        "java::java.lang.Number.byteValue:()B"}},
       {java_char_type(),
        {"java::java.lang.Character",
         "java::java.lang.Character.valueOf:(C)"
-        "Ljava/lang/Character;"}},
+        "Ljava/lang/Character;",
+        "java::java.lang.Character.charValue:()C"}},
       {java_double_type(),
        {"java::java.lang.Double",
         "java::java.lang.Double.valueOf:(D)"
-        "Ljava/lang/Double;"}},
+        "Ljava/lang/Double;",
+        "java::java.lang.Number.doubleValue:()D"}},
       {java_float_type(),
        {"java::java.lang.Float",
         "java::java.lang.Float.valueOf:(F)"
-        "Ljava/lang/Float;"}},
+        "Ljava/lang/Float;",
+        "java::java.lang.Number.floatValue:()F"}},
       {java_int_type(),
        {"java::java.lang.Integer",
         "java::java.lang.Integer.valueOf:(I)"
-        "Ljava/lang/Integer;"}},
+        "Ljava/lang/Integer;",
+        "java::java.lang.Number.intValue:()I"}},
       {java_long_type(),
        {"java::java.lang.Long",
-        "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;"}},
+        "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;",
+        "java::java.lang.Number.longValue:()J"}},
       {java_short_type(),
        {"java::java.lang.Short",
         "java::java.lang.Short.valueOf:(S)"
-        "Ljava/lang/Short;"}}};
+        "Ljava/lang/Short;",
+        "java::java.lang.Number.shortValue:()S"}}};
 
   auto found = type_info_by_primitive_type.find(maybe_primitive_type);
   return found == type_info_by_primitive_type.end() ? nullptr : &found->second;

jbmc/regression/jbmc/lambda-generic-boxing/Test$YieldsInt.class

@@ -40,6 +40,11 @@ struct java_primitive_type_infot
   /// Full identifier of the boxed type's factory method that takes the
   /// corresponding primitive as its sole argument
   const irep_idt boxed_type_factory_method;
+  /// Full identifier of the most general boxed-type method that yields this
+  /// type. For most primitives that means the corresponding method on
+  /// java.lang.Number; for Character and Boolean it means the method on their
+  /// specific boxed type.
+  const irep_idt unboxing_function_name;
 };
 
 /// If \p primitive_type is a Java primitive type, return information about it,