Java frontend: support lambdas that implicitly box to Object

This broadens our support for lambdas with implicit boxing/unboxing conversions
to include those that use a method-reference to a method with type Object -> x
to satisfy a functional interface of type primitive -> x (requiring boxing the
parameter and then upcasting to Object), or a method with type x -> primitive
satisfying an interface of type x -> Object (requiring the same conversion on
the return value).

Author: smowton

jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class

@@ -0,0 +1,33 @@
+public class BoxingWithOtherConversions {
+
+  interface ObjectToObject {
+    Object accept(Object o);
+  }
+
+  interface IntToObject {
+    Object accept(int i);
+  }
+
+  // Check we can narrow a parameter type down to a primitive
+  // which should be boxed and then upcast to Object by the
+  // generated lambda:
+  public static void testNarrowParameterTypeToPrimitive() {
+    ObjectToObject o2o = i -> ((Integer)i) + 1;
+    IntToObject i2o = o2o::accept;
+    assert o2o.accept(1).equals(2);
+    assert i2o.accept(1).equals(2);
+    assert false;
+  }
+
+  interface ObjectToInt {
+    int accept(Object o);
+  }
+
+  public static void testBroadenReturnTypeToObject() {
+    ObjectToInt o2i = o -> ((Integer)o).intValue() + 1;
+    ObjectToObject o2o = o2i::accept;
+    assert o2o.accept(1).equals(2);
+    assert o2i.accept(1) == 2;
+    assert false;
+  }
+}

jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class

@@ -0,0 +1,8 @@
+CORE
+BoxingWithOtherConversions
+--function BoxingWithOtherConversions.testBroadenReturnTypeToObject --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.1\] line 29 assertion at file BoxingWithOtherConversions\.java line 29 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 21: SUCCESS
+\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.2\] line 30 assertion at file BoxingWithOtherConversions\.java line 30 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 33: SUCCESS
+\[java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V.assertion\.3\] line 31 assertion at file BoxingWithOtherConversions\.java line 31 function java::BoxingWithOtherConversions\.testBroadenReturnTypeToObject:\(\)V bytecode-index 39: FAILURE

jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class

@@ -0,0 +1,8 @@
+CORE
+BoxingWithOtherConversions
+--function BoxingWithOtherConversions.testNarrowParameterTypeToPrimitive --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.1\] line 17 assertion at file BoxingWithOtherConversions\.java line 17 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 21: SUCCESS
+\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.2\] line 18 assertion at file BoxingWithOtherConversions\.java line 18 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 34: SUCCESS
+\[java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V.assertion.3\] line 19 assertion at file BoxingWithOtherConversions\.java line 19 function java::BoxingWithOtherConversions\.testNarrowParameterTypeToPrimitive:\(\)V bytecode-index 40: FAILURE

jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class

@@ -662,17 +662,12 @@ exprt adjust_type_if_necessary(
   }
   else
   {
-    const irep_idt &boxed_type_id =
-      to_struct_tag_type(required_type.subtype()).get_identifier();
     const auto *primitive_type_info =
       get_java_primitive_type_info(original_type);
     INVARIANT(
       primitive_type_info != nullptr,
       "A Java non-pointer type involved in a type disagreement should"
       " be a primitive");
-    INVARIANT(
-      boxed_type_id == primitive_type_info->boxed_type_name,
-      "Boxed types are only convertable to their corresponding unboxed type");
 
     symbol_exprt fresh_local = create_and_declare_local(
       function_id, role + "_boxed", required_type, symbol_table, code_block);
@@ -682,7 +677,7 @@ exprt adjust_type_if_necessary(
     code_block.add(code_function_callt{
       fresh_local, boxed_type_factory_method.symbol_expr(), {expr}});
 
-    return std::move(fresh_local);
+    return typecast_exprt::conditional_cast(fresh_local, required_type);
   }
 }