Merge pull request #5363 from smowton/smowton/feature/generic-lambda-boxing

Java frontend: support lambda autoboxing involving generics

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,