diff --git a/jbmc/regression/jbmc/lambda-boxing/Boolean.desc b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc new file mode 100644 index 00000000000..69b7c9d8516 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testBoolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.1\] line 73 assertion at file BoxingLambda\.java line 73 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 25: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.2\] line 74 assertion at file BoxingLambda\.java line 74 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 35: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.3\] line 75 assertion at file BoxingLambda\.java line 75 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 47: SUCCESS +\[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.4\] line 76 assertion at file BoxingLambda\.java line 76 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 53: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class new file mode 100644 index 00000000000..595e1c32578 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedBoolean.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedByte.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedByte.class new file mode 100644 index 00000000000..26136a93435 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedByte.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class new file mode 100644 index 00000000000..04a62a6d4df Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedCharacter.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class new file mode 100644 index 00000000000..274866094f8 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedFloat.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedFloat.class new file mode 100644 index 00000000000..9e374d57788 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedFloat.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class new file mode 100644 index 00000000000..120eda659ff Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedInteger.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class new file mode 100644 index 00000000000..8360e9315c9 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class new file mode 100644 index 00000000000..235a272437b Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesBoxedShort.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedBoolean.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedBoolean.class new file mode 100644 index 00000000000..6c5268f67ed Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedBoolean.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedByte.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedByte.class new file mode 100644 index 00000000000..b122c427ff7 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedByte.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class new file mode 100644 index 00000000000..990243e903a Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedCharacter.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class new file mode 100644 index 00000000000..dcd9dcb4b6d Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class new file mode 100644 index 00000000000..b7222a457aa Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedFloat.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class new file mode 100644 index 00000000000..f0c458d4839 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedInteger.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class new file mode 100644 index 00000000000..cb74f270447 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class new file mode 100644 index 00000000000..bf4c10a377e Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda$TakesUnboxedShort.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class new file mode 100644 index 00000000000..f1b83277ee2 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java new file mode 100644 index 00000000000..6a37fb9fbff --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BoxingLambda.java @@ -0,0 +1,171 @@ +public class BoxingLambda { + + interface TakesBoxedBoolean { + public Boolean accept(Boolean b); + } + + interface TakesUnboxedBoolean { + public boolean accept(boolean b); + } + + interface TakesBoxedByte { + public Byte accept(Byte b); + } + + interface TakesUnboxedByte { + public byte accept(byte b); + } + + interface TakesBoxedCharacter { + public Character accept(Character c); + } + + interface TakesUnboxedCharacter { + public char accept(char c); + } + + interface TakesBoxedDouble { + public Double accept(Double d); + } + + interface TakesUnboxedDouble { + public double accept(double d); + } + + interface TakesBoxedFloat { + public Float accept(Float f); + } + + interface TakesUnboxedFloat { + public float accept(float f); + } + + interface TakesBoxedInteger { + public Integer accept(Integer i); + } + + interface TakesUnboxedInteger { + public int accept(int i); + } + + interface TakesBoxedLong { + public Long accept(Long l); + } + + interface TakesUnboxedLong { + public long accept(long l); + } + + interface TakesBoxedShort { + public Short accept(Short s); + } + + interface TakesUnboxedShort { + public short accept(short s); + } + + public static void testBoolean() { + + TakesBoxedBoolean takesBoxed = b -> !b; + TakesUnboxedBoolean takesUnboxed = takesBoxed::accept; + TakesBoxedBoolean takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(true) == false; + assert takesUnboxed.accept(true) == false; + assert takesBoxedAgain.accept(true) == false; + assert false; + + } + + public static void testByte() { + + TakesBoxedByte takesBoxed = b -> (byte)(b + 1); + TakesUnboxedByte takesUnboxed = takesBoxed::accept; + TakesBoxedByte takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept((byte)1) == 2; + assert takesUnboxed.accept((byte)1) == 2; + assert takesBoxedAgain.accept((byte)1) == 2; + assert false; + + } + + public static void testCharacter() { + + TakesBoxedCharacter takesBoxed = c -> c == 'a' ? 'b' : 'a'; + TakesUnboxedCharacter takesUnboxed = takesBoxed::accept; + TakesBoxedCharacter takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept('a') == 'b'; + assert takesUnboxed.accept('a') == 'b'; + assert takesBoxedAgain.accept('a') == 'b'; + assert false; + + } + + public static void testDouble() { + + TakesBoxedDouble takesBoxed = d -> d + 1; + TakesUnboxedDouble takesUnboxed = takesBoxed::accept; + TakesBoxedDouble takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1.0) == 2.0; + assert takesUnboxed.accept(1.0) == 2.0; + assert takesBoxedAgain.accept(1.0) == 2.0; + assert false; + + } + + public static void testFloat() { + + TakesBoxedFloat takesBoxed = f -> f + 1; + TakesUnboxedFloat takesUnboxed = takesBoxed::accept; + TakesBoxedFloat takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1.0f) == 2.0f; + assert takesUnboxed.accept(1.0f) == 2.0f; + assert takesBoxedAgain.accept(1.0f) == 2.0f; + assert false; + + } + + public static void testInteger() { + + TakesBoxedInteger takesBoxed = i -> i + 1; + TakesUnboxedInteger takesUnboxed = takesBoxed::accept; + TakesBoxedInteger takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1) == 2; + assert takesUnboxed.accept(1) == 2; + assert takesBoxedAgain.accept(1) == 2; + assert false; + + } + + public static void testLong() { + + TakesBoxedLong takesBoxed = l -> l + 1; + TakesUnboxedLong takesUnboxed = takesBoxed::accept; + TakesBoxedLong takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept(1L) == 2L; + assert takesUnboxed.accept(1L) == 2L; + assert takesBoxedAgain.accept(1L) == 2L; + assert false; + + } + + public static void testShort() { + + TakesBoxedShort takesBoxed = s -> (short)(s + 1); + TakesUnboxedShort takesUnboxed = takesBoxed::accept; + TakesBoxedShort takesBoxedAgain = takesUnboxed::accept; + + assert takesBoxed.accept((short)1) == 2; + assert takesUnboxed.accept((short)1) == 2; + assert takesBoxedAgain.accept((short)1) == 2; + assert false; + + } + +} diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class new file mode 100644 index 00000000000..2bd41109fa0 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$IntToObject.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class new file mode 100644 index 00000000000..d8feafc013f Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToInt.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class new file mode 100644 index 00000000000..5483b2813f9 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions$ObjectToObject.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class new file mode 100644 index 00000000000..18019ef4125 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java new file mode 100644 index 00000000000..727a448bdf7 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BoxingWithOtherConversions.java @@ -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; + } +} diff --git a/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc b/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc new file mode 100644 index 00000000000..323f7e50e35 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/BroadenReturnTypeToObject.desc @@ -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 diff --git a/jbmc/regression/jbmc/lambda-boxing/Byte.desc b/jbmc/regression/jbmc/lambda-boxing/Byte.desc new file mode 100644 index 00000000000..988db9e9c02 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Byte.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.1\] line 86 assertion at file BoxingLambda\.java line 86 function java::BoxingLambda\.testByte:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.2\] line 87 assertion at file BoxingLambda\.java line 87 function java::BoxingLambda\.testByte:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.3\] line 88 assertion at file BoxingLambda\.java line 88 function java::BoxingLambda\.testByte:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testByte:\(\)V\.assertion\.4\] line 89 assertion at file BoxingLambda\.java line 89 function java::BoxingLambda\.testByte:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc b/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc new file mode 100644 index 00000000000..98cb8352af9 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/ByteToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testByteToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V\.assertion\.1\] line 26 assertion at file PrimitiveWideningWithBoxing\.java line 26 function java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V\.assertion\.2\] line 27 assertion at file PrimitiveWideningWithBoxing\.java line 27 function java::PrimitiveWideningWithBoxing\.testByteToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Character.desc b/jbmc/regression/jbmc/lambda-boxing/Character.desc new file mode 100644 index 00000000000..1488fef62df --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Character.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testCharacter --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.1\] line 99 assertion at file BoxingLambda\.java line 99 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.2\] line 100 assertion at file BoxingLambda\.java line 100 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.3\] line 101 assertion at file BoxingLambda\.java line 101 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testCharacter:\(\)V\.assertion\.4\] line 102 assertion at file BoxingLambda\.java line 102 function java::BoxingLambda\.testCharacter:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Double.desc b/jbmc/regression/jbmc/lambda-boxing/Double.desc new file mode 100644 index 00000000000..605b9f7c8d9 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Double.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.1\] line 112 assertion at file BoxingLambda\.java line 112 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.2\] line 113 assertion at file BoxingLambda\.java line 113 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.3\] line 114 assertion at file BoxingLambda\.java line 114 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testDouble:\(\)V\.assertion\.4\] line 115 assertion at file BoxingLambda\.java line 115 function java::BoxingLambda\.testDouble:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc b/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc new file mode 100644 index 00000000000..fdad63da3f0 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/DoubleToFloat.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testDoubleToFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V\.assertion\.1\] line 66 assertion at file PrimitiveWideningWithBoxing\.java line 66 function java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V\.assertion\.2\] line 67 assertion at file PrimitiveWideningWithBoxing\.java line 67 function java::PrimitiveWideningWithBoxing\.testDoubleToFloat:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Float.desc b/jbmc/regression/jbmc/lambda-boxing/Float.desc new file mode 100644 index 00000000000..e0062279f34 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Float.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.1\] line 125 assertion at file BoxingLambda\.java line 125 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.2\] line 126 assertion at file BoxingLambda\.java line 126 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.3\] line 127 assertion at file BoxingLambda\.java line 127 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testFloat:\(\)V\.assertion\.4\] line 128 assertion at file BoxingLambda\.java line 128 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc b/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc new file mode 100644 index 00000000000..be843d74d41 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/FloatToDouble.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testFloatToDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V\.assertion\.1\] line 44 assertion at file PrimitiveWideningWithBoxing\.java line 44 function java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V\.assertion\.2\] line 45 assertion at file PrimitiveWideningWithBoxing\.java line 45 function java::PrimitiveWideningWithBoxing\.testFloatToDouble:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc b/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc new file mode 100644 index 00000000000..1b2ac0969bd --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/IntToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testIntToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V\.assertion\.1\] line 38 assertion at file PrimitiveWideningWithBoxing\.java line 38 function java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V\.assertion\.2\] line 39 assertion at file PrimitiveWideningWithBoxing\.java line 39 function java::PrimitiveWideningWithBoxing\.testIntToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Integer.desc b/jbmc/regression/jbmc/lambda-boxing/Integer.desc new file mode 100644 index 00000000000..f0e61742adb --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Integer.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testInteger --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.1\] line 138 assertion at file BoxingLambda\.java line 138 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.2\] line 139 assertion at file BoxingLambda\.java line 139 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.3\] line 140 assertion at file BoxingLambda\.java line 140 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testInteger:\(\)V\.assertion\.4\] line 141 assertion at file BoxingLambda\.java line 141 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/Long.desc b/jbmc/regression/jbmc/lambda-boxing/Long.desc new file mode 100644 index 00000000000..ce8f0f79192 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Long.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.1\] line 151 assertion at file BoxingLambda\.java line 151 function java::BoxingLambda\.testLong:\(\)V bytecode-index 27: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.2\] line 152 assertion at file BoxingLambda\.java line 152 function java::BoxingLambda\.testLong:\(\)V bytecode-index 39: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.3\] line 153 assertion at file BoxingLambda\.java line 153 function java::BoxingLambda\.testLong:\(\)V bytecode-index 53: SUCCESS +\[java::BoxingLambda\.testLong:\(\)V\.assertion\.4\] line 154 assertion at file BoxingLambda\.java line 154 function java::BoxingLambda\.testLong:\(\)V bytecode-index 59: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc b/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc new file mode 100644 index 00000000000..f1e6c90c057 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToByte.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V\.assertion\.1\] line 72 assertion at file PrimitiveWideningWithBoxing\.java line 72 function java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V\.assertion\.2\] line 73 assertion at file PrimitiveWideningWithBoxing\.java line 73 function java::PrimitiveWideningWithBoxing\.testLongToByte:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc b/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc new file mode 100644 index 00000000000..cd2c541f4f1 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToInt.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V\.assertion\.1\] line 84 assertion at file PrimitiveWideningWithBoxing\.java line 84 function java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V\.assertion\.2\] line 85 assertion at file PrimitiveWideningWithBoxing\.java line 85 function java::PrimitiveWideningWithBoxing\.testLongToInt:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc b/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc new file mode 100644 index 00000000000..ee538f24a55 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/LongToShort.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testLongToShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V\.assertion\.1\] line 78 assertion at file PrimitiveWideningWithBoxing\.java line 78 function java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V bytecode-index 13: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V\.assertion\.2\] line 79 assertion at file PrimitiveWideningWithBoxing\.java line 79 function java::PrimitiveWideningWithBoxing\.testLongToShort:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc b/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc new file mode 100644 index 00000000000..3e030f2708a --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/NarrowParameterToPrimitive.desc @@ -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 diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class new file mode 100644 index 00000000000..1ae3abc9532 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ByteToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class new file mode 100644 index 00000000000..689faea2b5e Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$DoubleToDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$FloatToDouble.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$FloatToDouble.class new file mode 100644 index 00000000000..1c6dd6eb9cb Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$FloatToDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class new file mode 100644 index 00000000000..900fdb95cfa Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$IntToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$LongToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$LongToLong.class new file mode 100644 index 00000000000..4fa78ffb917 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$LongToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class new file mode 100644 index 00000000000..8c7d5b4fee3 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing$ShortToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.class b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.class new file mode 100644 index 00000000000..910a12599a5 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.class differ diff --git a/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java new file mode 100644 index 00000000000..0a0fc526362 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/PrimitiveWideningWithBoxing.java @@ -0,0 +1,88 @@ +public class PrimitiveWideningWithBoxing { + + // Tests for widening a parameter, accompanied by boxing and unboxing: + + public interface ByteToLong { + public Long accept(Byte b); + } + + public interface ShortToLong { + public Long accept(Short s); + } + + public interface IntToLong { + public Long accept(Integer i); + } + + public interface FloatToDouble { + public Double accept(Float f); + } + + public static long longToLong(long x) { return x + 1L; } + public static double doubleToDouble(double x) { return x + 1.0; } + + public static void testByteToLong() { + ByteToLong b2l = PrimitiveWideningWithBoxing::longToLong; + assert b2l.accept((byte)1) == 2L; + assert false; + } + + public static void testShortToLong() { + ShortToLong s2l = PrimitiveWideningWithBoxing::longToLong; + assert s2l.accept((short)1) == 2L; + assert false; + } + + public static void testIntToLong() { + IntToLong i2l = PrimitiveWideningWithBoxing::longToLong; + assert i2l.accept(1) == 2L; + assert false; + } + + public static void testFloatToDouble() { + FloatToDouble f2d = PrimitiveWideningWithBoxing::doubleToDouble; + assert f2d.accept(1.0f) == 2.0; + assert false; + } + + // Tests for widening a return value, accompanied by boxing and unboxing: + + public interface LongToLong { + public long accept(long l); + } + + public static Byte longToByte(Long l) { return (byte)(l + 1); } + public static Short longToShort(Long l) { return (short)(l + 1); } + public static Integer longToInt(Long l) { return (int)(l + 1); } + + public interface DoubleToDouble { + public double accept(double d); + } + + public static Float doubleToFloat(Double d) { return (float)(d + 1); } + + public static void testDoubleToFloat() { + DoubleToDouble d2d = PrimitiveWideningWithBoxing::doubleToFloat; + assert d2d.accept(1.0) == 2.0; + assert false; + } + + public static void testLongToByte() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToByte; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToShort() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToShort; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToInt() { + LongToLong l2l = PrimitiveWideningWithBoxing::longToInt; + assert l2l.accept(1L) == 2L; + assert false; + } + +} diff --git a/jbmc/regression/jbmc/lambda-boxing/Short.desc b/jbmc/regression/jbmc/lambda-boxing/Short.desc new file mode 100644 index 00000000000..7a969232ea7 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/Short.desc @@ -0,0 +1,9 @@ +CORE +BoxingLambda +--function BoxingLambda.testShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.1\] line 164 assertion at file BoxingLambda\.java line 164 function java::BoxingLambda\.testShort:\(\)V bytecode-index 26: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.2\] line 165 assertion at file BoxingLambda\.java line 165 function java::BoxingLambda\.testShort:\(\)V bytecode-index 37: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.3\] line 166 assertion at file BoxingLambda\.java line 166 function java::BoxingLambda\.testShort:\(\)V bytecode-index 50: SUCCESS +\[java::BoxingLambda\.testShort:\(\)V\.assertion\.4\] line 167 assertion at file BoxingLambda\.java line 167 function java::BoxingLambda\.testShort:\(\)V bytecode-index 56: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc b/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc new file mode 100644 index 00000000000..e147a202209 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-boxing/ShortToLong.desc @@ -0,0 +1,7 @@ +CORE +PrimitiveWideningWithBoxing +--function PrimitiveWideningWithBoxing\.testShortToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V\.assertion\.1\] line 32 assertion at file PrimitiveWideningWithBoxing\.java line 32 function java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V bytecode-index 15: SUCCESS +\[java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V\.assertion\.2\] line 33 assertion at file PrimitiveWideningWithBoxing\.java line 33 function java::PrimitiveWideningWithBoxing\.testShortToLong:\(\)V bytecode-index 21: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class new file mode 100644 index 00000000000..e5bc44b5db1 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntToVoid.class differ diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class new file mode 100644 index 00000000000..88e17290fb0 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-void-return-type/Test$IntegerToVoid.class differ diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test$ObjectToVoid.class b/jbmc/regression/jbmc/lambda-void-return-type/Test$ObjectToVoid.class new file mode 100644 index 00000000000..3c231466358 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-void-return-type/Test$ObjectToVoid.class differ diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test.class b/jbmc/regression/jbmc/lambda-void-return-type/Test.class new file mode 100644 index 00000000000..8f97e53a051 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-void-return-type/Test.class differ diff --git a/jbmc/regression/jbmc/lambda-void-return-type/Test.java b/jbmc/regression/jbmc/lambda-void-return-type/Test.java new file mode 100644 index 00000000000..f6d32102cd2 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-void-return-type/Test.java @@ -0,0 +1,31 @@ +public class Test { + + public int lastArgument = 0; + public int intToInt(int x) { lastArgument = x; return x + 1; } + public Integer intToInteger(int x) { lastArgument = x; return x + 1; } + public Object intToObject(int x) { lastArgument = x; return -1; } + + public interface IntToVoid { + void consume(int x); + } + + public static void test() { + Test t = new Test(); + + IntToVoid intToVoid = t::intToInt; + intToVoid.consume(5); + assert t.lastArgument == 5; + + IntToVoid intToVoid2 = t::intToInteger; + intToVoid2.consume(10); + assert t.lastArgument == 10; + + IntToVoid intToVoid3 = t::intToObject; + intToVoid3.consume(15); + assert t.lastArgument == 15; + + assert false; // Check we got here + + } + +} diff --git a/jbmc/regression/jbmc/lambda-void-return-type/test.desc b/jbmc/regression/jbmc/lambda-void-return-type/test.desc new file mode 100644 index 00000000000..0d0d6f858eb --- /dev/null +++ b/jbmc/regression/jbmc/lambda-void-return-type/test.desc @@ -0,0 +1,9 @@ +CORE +Test +--function Test.test --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +^EXIT=10$ +^SIGNAL=0$ +\[java::Test\.test:\(\)V\.assertion\.1\] line 17 assertion at file Test\.java line 17 function java::Test\.test:\(\)V bytecode-index 22: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.2\] line 21 assertion at file Test\.java line 21 function java::Test\.test:\(\)V bytecode-index 41: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.3\] line 25 assertion at file Test\.java line 25 function java::Test\.test:\(\)V bytecode-index 60: SUCCESS +\[java::Test\.test:\(\)V\.assertion\.4\] line 27 assertion at file Test\.java line 27 function java::Test\.test:\(\)V bytecode-index 66: FAILURE diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc new file mode 100644 index 00000000000..52ac3ebd739 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/ByteToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testByteToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testByteToLong:\(\)V.assertion\.1\] line 26 assertion at file Test\.java line 26 function java::Test\.testByteToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testByteToLong:\(\)V.assertion\.2\] line 27 assertion at file Test\.java line 27 function java::Test\.testByteToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc b/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc new file mode 100644 index 00000000000..d0efe27dff6 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/DoubleToFloat.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testDoubleToFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testDoubleToFloat:\(\)V.assertion\.1\] line 66 assertion at file Test\.java line 66 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testDoubleToFloat:\(\)V.assertion\.2\] line 67 assertion at file Test\.java line 67 function java::Test\.testDoubleToFloat:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc b/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc new file mode 100644 index 00000000000..ad120047795 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/FloatToDouble.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testFloatToDouble --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testFloatToDouble:\(\)V.assertion\.1\] line 44 assertion at file Test\.java line 44 function java::Test\.testFloatToDouble:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testFloatToDouble:\(\)V.assertion\.2\] line 45 assertion at file Test\.java line 45 function java::Test\.testFloatToDouble:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc new file mode 100644 index 00000000000..6d54e0e12fe --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/IntToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testIntToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testIntToLong:\(\)V.assertion\.1\] line 38 assertion at file Test\.java line 38 function java::Test\.testIntToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testIntToLong:\(\)V.assertion\.2\] line 39 assertion at file Test\.java line 39 function java::Test\.testIntToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc new file mode 100644 index 00000000000..42ba4d87cc5 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToByte.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToByte --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToByte:\(\)V.assertion\.1\] line 72 assertion at file Test\.java line 72 function java::Test\.testLongToByte:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToByte:\(\)V.assertion\.2\] line 73 assertion at file Test\.java line 73 function java::Test\.testLongToByte:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc new file mode 100644 index 00000000000..d29ecc6bf9d --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToInt.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToInt:\(\)V.assertion\.1\] line 84 assertion at file Test\.java line 84 function java::Test\.testLongToInt:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToInt:\(\)V.assertion\.2\] line 85 assertion at file Test\.java line 85 function java::Test\.testLongToInt:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc b/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc new file mode 100644 index 00000000000..5fe3458c69d --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/LongToShort.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testLongToShort --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testLongToShort:\(\)V.assertion\.1\] line 78 assertion at file Test\.java line 78 function java::Test\.testLongToShort:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testLongToShort:\(\)V.assertion\.2\] line 79 assertion at file Test\.java line 79 function java::Test\.testLongToShort:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc b/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc new file mode 100644 index 00000000000..a43c99ea32c --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/ShortToLong.desc @@ -0,0 +1,7 @@ +CORE +Test +--function Test\.testShortToLong --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +\[java::Test\.testShortToLong:\(\)V.assertion\.1\] line 32 assertion at file Test\.java line 32 function java::Test\.testShortToLong:\(\)V bytecode-index 13: SUCCESS +\[java::Test\.testShortToLong:\(\)V.assertion\.2\] line 33 assertion at file Test\.java line 33 function java::Test\.testShortToLong:\(\)V bytecode-index 19: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class new file mode 100644 index 00000000000..344354de37a Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ByteToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$DoubleToDouble.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$DoubleToDouble.class new file mode 100644 index 00000000000..590fe667e1d Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$DoubleToDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$FloatToDouble.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$FloatToDouble.class new file mode 100644 index 00000000000..a96f2b21085 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$FloatToDouble.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$IntToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$IntToLong.class new file mode 100644 index 00000000000..ecf01b900cd Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$IntToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$LongToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$LongToLong.class new file mode 100644 index 00000000000..b5086c6c26a Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$LongToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToInt.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToInt.class new file mode 100644 index 00000000000..dde34c477ad Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToInt.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class new file mode 100644 index 00000000000..9a489d6c422 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test$ShortToLong.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test.class b/jbmc/regression/jbmc/lambda-widening-conversions/Test.class new file mode 100644 index 00000000000..9bf53f2037c Binary files /dev/null and b/jbmc/regression/jbmc/lambda-widening-conversions/Test.class differ diff --git a/jbmc/regression/jbmc/lambda-widening-conversions/Test.java b/jbmc/regression/jbmc/lambda-widening-conversions/Test.java new file mode 100644 index 00000000000..e986553b5ba --- /dev/null +++ b/jbmc/regression/jbmc/lambda-widening-conversions/Test.java @@ -0,0 +1,88 @@ +public class Test { + + // Tests for widening a parameter: + + public interface ByteToLong { + public long accept(byte b); + } + + public interface ShortToLong { + public long accept(short s); + } + + public interface IntToLong { + public long accept(int i); + } + + public interface FloatToDouble { + public double accept(float f); + } + + public static long longToLong(long x) { return x + 1L; } + public static double doubleToDouble(double x) { return x + 1.0; } + + public static void testByteToLong() { + ByteToLong b2l = Test::longToLong; + assert b2l.accept((byte)1) == 2L; + assert false; + } + + public static void testShortToLong() { + ShortToLong s2l = Test::longToLong; + assert s2l.accept((short)1) == 2L; + assert false; + } + + public static void testIntToLong() { + IntToLong i2l = Test::longToLong; + assert i2l.accept(1) == 2L; + assert false; + } + + public static void testFloatToDouble() { + FloatToDouble f2d = Test::doubleToDouble; + assert f2d.accept(1.0f) == 2.0; + assert false; + } + + // Tests for widening a return value: + + public interface LongToLong { + public long accept(long l); + } + + public static byte longToByte(long l) { return (byte)(l + 1); } + public static short longToShort(long l) { return (short)(l + 1); } + public static int longToInt(long l) { return (int)(l + 1); } + + public interface DoubleToDouble { + public double accept(double d); + } + + public static float doubleToFloat(double d) { return (float)(d + 1); } + + public static void testDoubleToFloat() { + DoubleToDouble d2d = Test::doubleToFloat; + assert d2d.accept(1.0) == 2.0; + assert false; + } + + public static void testLongToByte() { + LongToLong l2l = Test::longToByte; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToShort() { + LongToLong l2l = Test::longToShort; + assert l2l.accept(1L) == 2L; + assert false; + } + + public static void testLongToInt() { + LongToLong l2l = Test::longToInt; + assert l2l.accept(1L) == 2L; + assert false; + } + +} diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 1ebe0f7b032..8a72fb858e2 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -544,8 +544,7 @@ static code_with_references_listt assign_struct_components_from_json( { const auto member_json = [&]() -> jsont { if( - is_primitive_wrapper_type_name(id2string( - strip_java_namespace_prefix(java_class_type.get_name()))) && + is_primitive_wrapper_type_id(java_class_type.get_name()) && id2string(component_name) == "value") { return get_untyped_primitive(json); diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index d91a5a00cae..6690c8799a6 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -38,6 +38,77 @@ bool is_java_string_type(const struct_typet &struct_type) struct_type.has_component("data"); } +const java_boxed_type_infot * +get_boxed_type_info_by_name(const irep_idt &type_name) +{ + static std::unordered_map type_info_by_name = + { + {"java::java.lang.Boolean", + {"java::java.lang.Boolean.booleanValue:()Z", java_boolean_type()}}, + {"java::java.lang.Byte", + {"java::java.lang.Byte.byteValue:()B", java_byte_type()}}, + {"java::java.lang.Character", + {"java::java.lang.Character.charValue:()C", java_char_type()}}, + {"java::java.lang.Double", + {"java::java.lang.Double.doubleValue:()D", java_double_type()}}, + {"java::java.lang.Float", + {"java::java.lang.Float.floatValue:()F", java_float_type()}}, + {"java::java.lang.Integer", + {"java::java.lang.Integer.intValue:()I", java_int_type()}}, + {"java::java.lang.Long", + {"java::java.lang.Long.longValue:()J", java_long_type()}}, + {"java::java.lang.Short", + {"java::java.lang.Short.shortValue:()S", java_short_type()}}, + }; + + auto found = type_info_by_name.find(type_name); + return found == type_info_by_name.end() ? nullptr : &found->second; +} + +const java_primitive_type_infot * +get_java_primitive_type_info(const typet &maybe_primitive_type) +{ + static std::unordered_map + type_info_by_primitive_type = { + {java_boolean_type(), + {"java::java.lang.Boolean", + "java::java.lang.Boolean.valueOf:(Z)Ljava/lang/Boolean;"}}, + {java_byte_type(), + {"java::java.lang.Byte", + "java::java.lang.Byte.valueOf:(B)Ljava/lang/Byte;"}}, + {java_char_type(), + {"java::java.lang.Character", + "java::java.lang.Character.valueOf:(C)" + "Ljava/lang/Character;"}}, + {java_double_type(), + {"java::java.lang.Double", + "java::java.lang.Double.valueOf:(D)" + "Ljava/lang/Double;"}}, + {java_float_type(), + {"java::java.lang.Float", + "java::java.lang.Float.valueOf:(F)" + "Ljava/lang/Float;"}}, + {java_int_type(), + {"java::java.lang.Integer", + "java::java.lang.Integer.valueOf:(I)" + "Ljava/lang/Integer;"}}, + {java_long_type(), + {"java::java.lang.Long", + "java::java.lang.Long.valueOf:(J)Ljava/lang/Long;"}}, + {java_short_type(), + {"java::java.lang.Short", + "java::java.lang.Short.valueOf:(S)" + "Ljava/lang/Short;"}}}; + + auto found = type_info_by_primitive_type.find(maybe_primitive_type); + return found == type_info_by_primitive_type.end() ? nullptr : &found->second; +} + +bool is_primitive_wrapper_type_id(const irep_idt &id) +{ + return get_boxed_type_info_by_name(id) != nullptr; +} + bool is_primitive_wrapper_type_name(const std::string &type_name) { static const std::unordered_set primitive_wrapper_type_names = { diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 91644e4e88c..ee4767c409a 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -32,8 +32,42 @@ bool java_is_array_type(const typet &type); /// and in particular may not have length and data fields. bool is_java_string_type(const struct_typet &struct_type); +/// Return type for get_java_primitive_type_info +struct java_primitive_type_infot +{ + /// Name, including java:: prefix, of the corresponding boxed type + const irep_idt boxed_type_name; + /// 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; +}; + +/// If \p primitive_type is a Java primitive type, return information about it, +/// otherwise return null +const java_primitive_type_infot * +get_java_primitive_type_info(const typet &maybe_primitive_type); + +/// Return type for get_boxed_type_info_by_name +struct java_boxed_type_infot +{ + /// Name of the function defined on the boxed type that returns the boxed + /// value + const irep_idt unboxing_function_name; + /// Primitive type that this boxed type contains + const typet corresponding_primitive_type; +}; + +/// If \p type_name is a Java boxed type tag, return information about it, +/// otherwise return null +const java_boxed_type_infot * +get_boxed_type_info_by_name(const irep_idt &type_name); + +/// Returns true iff the argument is the symbol-table identifier of a Java +/// primitive wrapper type (for example, java::java.lang.Byte) +bool is_primitive_wrapper_type_id(const irep_idt &id); + /// Returns true iff the argument is the fully qualified name of a Java -/// primitive wrapper type. +/// primitive wrapper type (for example, java.lang.Byte) bool is_primitive_wrapper_type_name(const std::string &type_name); void generate_class_stub( diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 1e5975a8aad..49443eed7f0 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -610,6 +610,88 @@ static symbol_exprt instantiate_new_object( return new_instance_var; } +/// If \p expr needs (un)boxing to satisfy \p required_type, add the required +/// symbols to \p symbol_table and code to \p code_block, then return an +/// expression giving the adjusted expression. Otherwise return \p expr +/// unchanged. \p role is a suggested name prefix for any temporary variable +/// needed; \p function_id is the id of the function any created code it +/// added to. +exprt box_or_unbox_type_if_necessary( + exprt expr, + const typet &required_type, + code_blockt &code_block, + symbol_table_baset &symbol_table, + const irep_idt &function_id, + const std::string &role) +{ + const typet &original_type = expr.type(); + const bool original_is_pointer = can_cast_type(original_type); + const bool required_is_pointer = can_cast_type(required_type); + + if(original_is_pointer == required_is_pointer) + { + return expr; + } + + // One is a pointer, the other a primitive -- box or unbox as necessary, and + // check the types are consistent: + if(original_is_pointer) + { + const irep_idt &boxed_type_id = + to_struct_tag_type(original_type.subtype()).get_identifier(); + const auto *boxed_type_info = get_boxed_type_info_by_name(boxed_type_id); + INVARIANT( + boxed_type_info != nullptr, + "Only boxed primitive types should participate in a pointer vs." + " primitive type disagreement"); + + symbol_exprt fresh_local = create_and_declare_local( + function_id, role + "_unboxed", required_type, symbol_table, code_block); + const symbolt &unboxing_function_symbol = + symbol_table.lookup_ref(boxed_type_info->unboxing_function_name); + code_block.add(code_function_callt{ + fresh_local, unboxing_function_symbol.symbol_expr(), {expr}}); + + return std::move(fresh_local); + } + else + { + 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"); + + symbol_exprt fresh_local = create_and_declare_local( + function_id, role + "_boxed", required_type, symbol_table, code_block); + const symbolt &boxed_type_factory_method = + symbol_table.lookup_ref(primitive_type_info->boxed_type_factory_method); + + code_block.add(code_function_callt{ + fresh_local, boxed_type_factory_method.symbol_expr(), {expr}}); + + return std::move(fresh_local); + } +} + +/// Box or unbox expr as per \ref box_or_unbox_type_if_necessary, then cast the +/// result to \p required_type. If the source is legal Java that should mean a +/// pointer upcast or primitive widening conversion, but this is not checked. +exprt adjust_type_if_necessary( + exprt expr, + const typet &required_type, + code_blockt &code_block, + symbol_table_baset &symbol_table, + const irep_idt &function_id, + const std::string &role) +{ + return typecast_exprt::conditional_cast( + box_or_unbox_type_if_necessary( + expr, required_type, code_block, symbol_table, function_id, role), + required_type); +} + /// Create the body for the synthetic method implementing an invokedynamic /// method. For most lambdas this means creating a simple function body like /// TR new_synthetic_method(T1 param1, T2 param2, ...) { @@ -642,7 +724,6 @@ codet invokedynamic_synthetic_method( const symbolt &function_symbol = ns.lookup(function_id); const auto &function_type = to_code_type(function_symbol.type); const auto ¶meters = function_type.parameters(); - const auto &return_type = function_type.return_type(); const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol)); const java_class_typet &class_type = to_java_class_type(class_symbol.type); @@ -707,12 +788,37 @@ codet invokedynamic_synthetic_method( else callee = lambda_method_symbol.symbol_expr(); - if(return_type != empty_typet() && !is_constructor_lambda) + // Adjust boxing if required: + const code_typet &callee_type = to_code_type(lambda_method_symbol.type); + const auto &callee_parameters = callee_type.parameters(); + const auto &callee_return_type = callee_type.return_type(); + INVARIANT( + callee_parameters.size() == lambda_method_args.size(), + "should have args for every parameter"); + for(unsigned i = 0; i < callee_parameters.size(); ++i) + { + lambda_method_args[i] = adjust_type_if_necessary( + std::move(lambda_method_args[i]), + callee_parameters[i].type(), + result, + symbol_table, + function_id, + "param" + std::to_string(i)); + } + + if(function_type.return_type() != empty_typet() && !is_constructor_lambda) { symbol_exprt result_local = create_and_declare_local( - function_id, "return_value", return_type, symbol_table, result); + function_id, "return_value", callee_return_type, symbol_table, result); result.add(code_function_callt(result_local, callee, lambda_method_args)); - result.add(code_returnt{result_local}); + exprt adjusted_local = adjust_type_if_necessary( + result_local, + function_type.return_type(), + result, + symbol_table, + function_id, + "retval"); + result.add(code_returnt{adjusted_local}); } else { @@ -722,8 +828,8 @@ codet invokedynamic_synthetic_method( if(is_constructor_lambda) { // Return the newly-created object. - result.add(code_returnt{ - typecast_exprt::conditional_cast(lambda_method_args.at(0), return_type)}); + result.add(code_returnt{typecast_exprt::conditional_cast( + lambda_method_args.at(0), function_type.return_type())}); } return std::move(result);