diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.class b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.class new file mode 100644 index 00000000000..c45226940b3 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.class differ diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java new file mode 100644 index 00000000000..8c4862a8b64 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java @@ -0,0 +1,6 @@ +interface InterfaceDeclaringEquals { + + public int f(int x); + + public boolean equals(Object other); +} diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.class b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.class new file mode 100644 index 00000000000..3e4498155f5 Binary files /dev/null and b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.class differ diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.java b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.java new file mode 100644 index 00000000000..ddab62b4a78 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.java @@ -0,0 +1,6 @@ +interface InterfaceWithDefaults { + + public int f(int x); + + public default int g() { return 1; } +} diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java b/jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java new file mode 100644 index 00000000000..15631be7792 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java @@ -0,0 +1,4 @@ +interface StubInterface { + + public int f(int x); +} diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.class b/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.class new file mode 100644 index 00000000000..de02a0144ad Binary files /dev/null and b/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.class differ diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.java b/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.java new file mode 100644 index 00000000000..a260e2b84ff --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.java @@ -0,0 +1 @@ +interface StubSuperinterface extends StubInterface {} diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/Test.class b/jbmc/regression/jbmc/lambda-unhandled-types/Test.class new file mode 100644 index 00000000000..a764627b92e Binary files /dev/null and b/jbmc/regression/jbmc/lambda-unhandled-types/Test.class differ diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/Test.java b/jbmc/regression/jbmc/lambda-unhandled-types/Test.java new file mode 100644 index 00000000000..b688b04f92f --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/Test.java @@ -0,0 +1,10 @@ +public class Test { + + public static void main() { + + StubInterface stubInterface = (x -> x); + StubSuperinterface stubSuperinterface = (x -> x); + InterfaceDeclaringEquals interfaceDeclaringEquals = (x -> x); + InterfaceWithDefaults interfaceWithDefaults = (x -> x); + } +} diff --git a/jbmc/regression/jbmc/lambda-unhandled-types/test.desc b/jbmc/regression/jbmc/lambda-unhandled-types/test.desc new file mode 100644 index 00000000000..1e072030e68 --- /dev/null +++ b/jbmc/regression/jbmc/lambda-unhandled-types/test.desc @@ -0,0 +1,16 @@ +CORE +Test.class +--function Test.main --verbosity 10 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +^ignoring invokedynamic at java::Test.main:\(\)V address 0 which produces a stub type java::StubInterface +^ignoring invokedynamic at java::Test.main:\(\)V address 6 which produces type java::StubSuperinterface which should have exactly one abstract method but actually has 0. +^ignoring invokedynamic at java::Test.main:\(\)V address 12 which produces type java::InterfaceDeclaringEquals which should have exactly one abstract method but actually has 2. +^ignoring invokedynamic at java::Test.main:\(\)V address 18 which produces type java::InterfaceWithDefaults which should have exactly one abstract method but actually has 2. +-- +-- +This exercises four cases that aren't currently supported: stub interfaces, stub +superinterfaces, interfaces that declare methods also declared on +java.lang.Object, and interfaces that provide default methods. All we require at +this point is that jbmc shouldn't crash when these are seen. diff --git a/jbmc/regression/jbmc/lambda1/B.class b/jbmc/regression/jbmc/lambda1/B.class index 8d177c6dc03..e3f12a58e08 100644 Binary files a/jbmc/regression/jbmc/lambda1/B.class and b/jbmc/regression/jbmc/lambda1/B.class differ diff --git a/jbmc/regression/jbmc/lambda1/B.java b/jbmc/regression/jbmc/lambda1/B.java index 21a3432c08b..83b8e7e30c2 100644 --- a/jbmc/regression/jbmc/lambda1/B.java +++ b/jbmc/regression/jbmc/lambda1/B.java @@ -1,9 +1,7 @@ public class B { - public int y; + public int y; - public static java.util.function.Function dmul = x -> x * 3.1415; + public static Function dmul = x -> x * 1.5; - public void set(int x) { - y = x; - } + public void set(int x) { y = x; } } diff --git a/jbmc/regression/jbmc/lambda1/BiFunction.class b/jbmc/regression/jbmc/lambda1/BiFunction.class new file mode 100644 index 00000000000..ed3db86e566 Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/BiFunction.class differ diff --git a/jbmc/regression/jbmc/lambda1/BiFunction.java b/jbmc/regression/jbmc/lambda1/BiFunction.java new file mode 100644 index 00000000000..475ea1d7df5 --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/BiFunction.java @@ -0,0 +1,5 @@ + +interface BiFunction { + + public To apply(From1 f1, From2 f2); +} diff --git a/jbmc/regression/jbmc/lambda1/C.class b/jbmc/regression/jbmc/lambda1/C.class index 44f19f094e6..cc581719903 100644 Binary files a/jbmc/regression/jbmc/lambda1/C.class and b/jbmc/regression/jbmc/lambda1/C.class differ diff --git a/jbmc/regression/jbmc/lambda1/CustomLambda.java b/jbmc/regression/jbmc/lambda1/CustomLambda.java index 1091fe62c46..6bf8f8f9f9c 100644 --- a/jbmc/regression/jbmc/lambda1/CustomLambda.java +++ b/jbmc/regression/jbmc/lambda1/CustomLambda.java @@ -1,4 +1,4 @@ @FunctionalInterface interface CustomLambda { - boolean is_ok(T t); + boolean is_ok(T t); } diff --git a/jbmc/regression/jbmc/lambda1/Function.class b/jbmc/regression/jbmc/lambda1/Function.class new file mode 100644 index 00000000000..7e6d3d58b1e Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/Function.class differ diff --git a/jbmc/regression/jbmc/lambda1/Function.java b/jbmc/regression/jbmc/lambda1/Function.java new file mode 100644 index 00000000000..956967fe34c --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/Function.java @@ -0,0 +1,5 @@ + +interface Function { + + public To apply(From f); +} diff --git a/jbmc/regression/jbmc/lambda1/Lambdatest$A.class b/jbmc/regression/jbmc/lambda1/Lambdatest$A.class index 0556baf0fb4..de4ae357b43 100644 Binary files a/jbmc/regression/jbmc/lambda1/Lambdatest$A.class and b/jbmc/regression/jbmc/lambda1/Lambdatest$A.class differ diff --git a/jbmc/regression/jbmc/lambda1/Lambdatest.class b/jbmc/regression/jbmc/lambda1/Lambdatest.class index 506d117020a..518e8992000 100644 Binary files a/jbmc/regression/jbmc/lambda1/Lambdatest.class and b/jbmc/regression/jbmc/lambda1/Lambdatest.class differ diff --git a/jbmc/regression/jbmc/lambda1/Lambdatest.java b/jbmc/regression/jbmc/lambda1/Lambdatest.java index 3dce340b8fd..311c67783c9 100644 --- a/jbmc/regression/jbmc/lambda1/Lambdatest.java +++ b/jbmc/regression/jbmc/lambda1/Lambdatest.java @@ -1,97 +1,185 @@ -import java.util.function.*; - public class Lambdatest { - class A { - int x; - } - - CustomLambda custom = x -> true; - BiFunction add = (x0, y0) -> x0.intValue() + y0; - int z = 10; - - A a; - B b = new B(); - - public Integer g(Float x, Integer y, BiFunction fun) { - return fun.apply(x, y); - } - - public int f(Float x, Integer y, Integer z) { - Integer tmp = add.apply(x, y); - Function mul = (a) -> a * tmp; - return mul.apply(z); - } - - public int i(int x) { - int z = 5; - Function foo = (a) -> a * z; - return foo.apply(x); - } - - public int j(int x) { - Function foo = (a) -> a * z; - return foo.apply(x); - } - - public int k(int x) { - a.x = 10; - - Function foo = (y) -> y * a.x; - return foo.apply(x); - } - - public int l(int x) { - b.y = 10; - Function foo = (y) -> { - int r = y * b.y; - b.set(r); - return r; - }; - b = new B(); - b.y = 14; - return foo.apply(x); - } - - public int m(int x) { - b.y = 10; - Function foo = (y) -> { - int r = y * b.y; - b.y = r; - return r; - }; - return foo.apply(x); - } - - // test static field of different class - public double d(Double x) { - return B.dmul.apply(x); + class A { + int x; + } + + CustomLambda custom = x -> true; + BiFunction add = (x0, y0) -> x0.intValue() + y0; + int z = 10; + + A a = new A(); + B b = new B(); + + public Integer captureNone(Float x, Integer y, + BiFunction fun) { + return fun.apply(x, y); + } + + public int captureReference(Float x, Integer y, Integer z) { + Integer tmp = add.apply(x, y); + Function mul = (a) -> a * tmp; + return mul.apply(z); + } + + public int captureInt(int x) { + int z = 5; + Function foo = (a) -> a * z; + return foo.apply(x); + } + + public int captureThisPrimitive(int x) { + Function foo = (a) -> a * z; + return foo.apply(x); + } + + public int captureThisReference(int x) { + a.x = 10; + + Function foo = (y) -> y * a.x; + return foo.apply(x); + } + + public int captureAndCall(int x) { + b.y = 10; + Function foo = (y) -> { + int r = y * b.y; + b.set(r); + return r; + }; + b = new B(); + b.y = 14; + return foo.apply(x); + } + + public int captureAndAssign(int x) { + b.y = 10; + Function foo = (y) -> { + int r = y * b.y; + b.y = r; + return r; + }; + return foo.apply(x); + } + + // test static field of different class + public double callStatic(Double x) { return B.dmul.apply(x); } + + public int capture2(Float a) { return add.apply(a, 1); } + + public boolean custom(Integer i) { return custom.is_ok(i); } + + public static void main(String[] args, int unknown) { + Lambdatest lt = new Lambdatest(); + if (unknown == 0) { + // should succeed + assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 3; + } else if (unknown == 1) { + // should fail + assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 4; + } else if (unknown == 2) { + assert lt.captureReference(1.0f, 2, 3) == 9; // should succeed + } else if (unknown == 3) { + assert lt.captureReference(1.0f, 2, 3) == 10; // should fail + } else if (unknown == 4) { + assert lt.captureInt(2) == 10; // should succeed + } else if (unknown == 5) { + assert lt.captureInt(2) == 11; // should fail + } else if (unknown == 6) { + assert lt.captureThisPrimitive(3) == 30; // should succeed + } else if (unknown == 7) { + assert lt.captureThisPrimitive(3) == 31; // should fail + } else if (unknown == 8) { + assert lt.captureThisReference(4) == 40; // should succeed + } else if (unknown == 9) { + assert lt.captureThisReference(4) == 41; // should fail + } else if (unknown == 10) { + assert lt.captureAndCall(5) == 70; // should succeed + assert lt.b.y == 70; // check side-effects of l method + } else if (unknown == 11) { + assert lt.captureAndCall(5) == 51; // should fail + } else if (unknown == 12) { + assert lt.captureAndAssign(6) == 60; // should succeed + assert lt.b.y == 60; // check side-effects of m method + } else if (unknown == 13) { + assert lt.captureAndAssign(6) == 61; // should fail + } else if (unknown == 14) { + assert lt.callStatic(7.0) == 10.5; // should succeed + } else if (unknown == 15) { + assert lt.callStatic(7.0) == 12; // should fail + } else if (unknown == 16) { + assert lt.capture2(8.0f) == 9; // should succeed + } else if (unknown == 17) { + assert lt.capture2(8.0f) == 10; // should fail + } else if (unknown == 18) { + assert lt.custom(9); // should succeed + } else if (unknown == 19) { + assert !lt.custom(9); // should fail + // Test array capture + } else if (unknown == 20) { + int array[] = new int[3]; + Function func = (x) -> x + array.length; + assert func.apply(2) == 5; // should succeed + } else if (unknown == 21) { + int array[] = new int[3]; + Function func = (x) -> x + array.length; + assert func.apply(2) == 6; // should fail + // Test reference array + } else if (unknown == 22) { + Integer array[] = new Integer[3]; + Function func = (x) -> x + array.length; + assert func.apply(2) == 5; // should succeed + } else if (unknown == 23) { + Integer array[] = new Integer[3]; + Function func = (x) -> x + array.length; + assert func.apply(2) == 6; // should fail + // Test outer class capture + } else if (unknown == 24) { + Outer outer = new Outer(); + outer.value = 42; + Outer.Inner inner = outer.new Inner(); + Function getter = inner.getOuterGetter(); + assert (getter.apply(0) == 42); // should succeed + } else if (unknown == 25) { + Outer outer = new Outer(); + outer.value = 42; + Outer.Inner inner = outer.new Inner(); + Function getter = inner.getOuterGetter(); + assert (getter.apply(0) != 42); // should fail + // Static intialized lambda + } else if (unknown == 26) { + assert StaticLambdas.id.apply(96) == 96; // should succeed + } else if (unknown == 27) { + assert StaticLambdas.id.apply(96) != 96; // should fail + // Reference equality of the captured object + } else if (unknown == 28) { + Object object = new Object(); + Function lambda = (x) -> object; + assert (lambda.apply(0) == object); // should succeed + } else if (unknown == 29) { + Object object = new Object(); + Function lambda = (x) -> object; + assert (lambda.apply(0) != object); // should fail } + } - public int capture2(Float a) { - return add.apply(a, 1); - } + static void lambdaCaptureNondet(Integer value) { + Function func = (x) -> value; + assert func.apply(0) == 42; + } +} - public boolean custom(Integer i) { - return custom.is_ok(i); - } +class StaticLambdas { + final static Function id = x -> x; +} - public static void main(String[] args) { - // Uses all of the above test functions, to ensure they are loaded under - // symex-driven loading: - - Lambdatest lt = new Lambdatest(); - lt.f(0.0f, 0, 0); - lt.i(0); - lt.j(0); - lt.k(0); - lt.l(0); - lt.m(0); - } +class Outer { + int value; + class Inner { + Function getOuterGetter() { return (x) -> value; } + } } class C implements CustomLambda { - public boolean is_ok(Integer i) { - return true; - } + public boolean is_ok(Integer i) { return true; } } diff --git a/jbmc/regression/jbmc/lambda1/Nondet.class b/jbmc/regression/jbmc/lambda1/Nondet.class new file mode 100644 index 00000000000..bda2a0180d3 Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/Nondet.class differ diff --git a/jbmc/regression/jbmc/lambda1/Nondet.java b/jbmc/regression/jbmc/lambda1/Nondet.java new file mode 100644 index 00000000000..b4f1914f5b6 --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/Nondet.java @@ -0,0 +1,16 @@ +public class Nondet { + int x; + int y; + public static void test(Nondet nondet) { + Function lambda = (z) -> nondet.x + nondet.y + z; + assert (lambda.apply(0) == 42); + } + public static void testPrimitiveArray(int[] ints) { + Function lambda = (index) -> ints[index]; + assert (lambda.apply(0) == 42); + } + public static void testReferenceArray(Nondet[] nondets) { + Function lambda = (index) -> nondets[index].x; + assert (lambda.apply(0) == 42); + } +} diff --git a/jbmc/regression/jbmc/lambda1/Outer$Inner.class b/jbmc/regression/jbmc/lambda1/Outer$Inner.class new file mode 100644 index 00000000000..110535a8785 Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/Outer$Inner.class differ diff --git a/jbmc/regression/jbmc/lambda1/Outer.class b/jbmc/regression/jbmc/lambda1/Outer.class new file mode 100644 index 00000000000..b7d2042b5aa Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/Outer.class differ diff --git a/jbmc/regression/jbmc/lambda1/StaticLambdas.class b/jbmc/regression/jbmc/lambda1/StaticLambdas.class new file mode 100644 index 00000000000..db47bec1bcc Binary files /dev/null and b/jbmc/regression/jbmc/lambda1/StaticLambdas.class differ diff --git a/jbmc/regression/jbmc/lambda1/nondet.desc b/jbmc/regression/jbmc/lambda1/nondet.desc new file mode 100644 index 00000000000..a688e63a75c --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/nondet.desc @@ -0,0 +1,9 @@ +CORE +Nondet.class +--function Nondet.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +line 6 assertion.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Check that objects created by the object factory can be captured by a lambda diff --git a/jbmc/regression/jbmc/lambda1/primitive_array.desc b/jbmc/regression/jbmc/lambda1/primitive_array.desc new file mode 100644 index 00000000000..f52cd3b1d20 --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/primitive_array.desc @@ -0,0 +1,10 @@ +CORE +Nondet.class +--function Nondet.testPrimitiveArray --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +line 10 assertion.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Check that primitive arrays created by the object factory can be +captured by a lambda diff --git a/jbmc/regression/jbmc/lambda1/reference_array.desc b/jbmc/regression/jbmc/lambda1/reference_array.desc new file mode 100644 index 00000000000..e7f56a2148c --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/reference_array.desc @@ -0,0 +1,10 @@ +CORE +Nondet.class +--function Nondet.testReferenceArray --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +line 14 assertion.*FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Check that reference arrays created by the object factory can be +captured by a lambda diff --git a/jbmc/regression/jbmc/lambda1/test.desc b/jbmc/regression/jbmc/lambda1/test.desc index f94b77de051..7c335cd8836 100644 --- a/jbmc/regression/jbmc/lambda1/test.desc +++ b/jbmc/regression/jbmc/lambda1/test.desc @@ -1,19 +1,37 @@ CORE Lambdatest.class ---verbosity 10 --show-goto-functions --function Lambdatest.main -lambda function reference lambda\$new\$0 in class \"Lambdatest\" -lambda function reference lambda\$new\$1 in class \"Lambdatest\" -lambda function reference lambda\$f\$2 in class \"Lambdatest\" -lambda function reference lambda\$i\$3 in class \"Lambdatest\" -lambda function reference lambda\$j\$4 in class \"Lambdatest\" -lambda function reference lambda\$k\$5 in class \"Lambdatest\" -lambda function reference lambda\$l\$6 in class \"Lambdatest\" -lambda function reference lambda\$m\$7 in class \"Lambdatest\" -lambda function reference lambda\$static\$0 in class \"B\" -^EXIT=0$ +--function Lambdatest.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +line 76 assertion.*SUCCESS$ +line 79 assertion.*FAILURE$ +line 81 assertion.*SUCCESS$ +line 83 assertion.*FAILURE$ +line 85 assertion.*SUCCESS$ +line 87 assertion.*FAILURE$ +line 89 assertion.*SUCCESS$ +line 91 assertion.*FAILURE$ +line 93 assertion.*SUCCESS$ +line 95 assertion.*FAILURE$ +line 97 assertion.*SUCCESS$ +line 98 assertion.*SUCCESS$ +line 100 assertion.*FAILURE$ +line 102 assertion.*SUCCESS$ +line 103 assertion.*SUCCESS$ +line 105 assertion.*FAILURE$ +line 107 assertion.*SUCCESS$ +line 109 assertion.*FAILURE$ +line 111 assertion.*SUCCESS$ +line 113 assertion.*FAILURE$ +line 115 assertion.*SUCCESS$ +line 117 assertion.*FAILURE$ +line 122 assertion.*SUCCESS$ +line 126 assertion.*FAILURE$ +line 131 assertion.*SUCCESS$ +line 135 assertion.*FAILURE$ +line 142 assertion.*SUCCESS$ +line 148 assertion.*FAILURE$ +line 151 assertion.*SUCCESS$ +line 153 assertion.*FAILURE$ +line 158 assertion.*SUCCESS$ +line 162 assertion.*FAILURE$ +^EXIT=10$ ^SIGNAL=0$ --- --- -Incompatible with symex-driven lazy loading because this test wants to process -everything in the given class, not the functions reachable from a particular -entry point, which is required for symex-driven loading. diff --git a/jbmc/regression/jbmc/lambda1/test_goto_functions.desc b/jbmc/regression/jbmc/lambda1/test_goto_functions.desc new file mode 100644 index 00000000000..8b45d833495 --- /dev/null +++ b/jbmc/regression/jbmc/lambda1/test_goto_functions.desc @@ -0,0 +1,14 @@ +CORE +Lambdatest.class +--verbosity 10 --show-goto-functions --function Lambdatest.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` +lambda function reference lambda\$new\$0 in class \"Lambdatest\" +lambda function reference lambda\$new\$1 in class \"Lambdatest\" +lambda function reference lambda\$captureReference\$2 in class \"Lambdatest\" +lambda function reference lambda\$captureInt\$3 in class \"Lambdatest\" +lambda function reference lambda\$captureThisPrimitive\$4 in class \"Lambdatest\" +lambda function reference lambda\$captureThisReference\$5 in class \"Lambdatest\" +lambda function reference lambda\$captureAndCall\$6 in class \"Lambdatest\" +lambda function reference lambda\$captureAndAssign\$7 in class \"Lambdatest\" +lambda function reference lambda\$static\$0 in class \"B\" +^EXIT=0$ +^SIGNAL=0$ diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 4cfb97b35fd..6003e5a382d 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -41,6 +41,7 @@ SRC = assignments_from_json.cpp \ java_trace_validation.cpp \ java_types.cpp \ java_utils.cpp \ + lambda_synthesis.cpp \ load_method_by_regex.cpp \ mz_zip_archive.cpp \ remove_exceptions.cpp \ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index de630a71dac..a8dbc42dacc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_string_literal_expr.h" #include "java_types.h" #include "java_utils.h" +#include "lambda_synthesis.h" #include "pattern.h" #include "remove_exceptions.h" @@ -94,6 +95,35 @@ static void assign_parameter_names( } } +void create_method_stub_symbol( + const irep_idt &identifier, + const irep_idt &base_name, + const irep_idt &pretty_name, + const typet &type, + const irep_idt &declaring_class, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + messaget log(message_handler); + + symbolt symbol; + symbol.name = identifier; + symbol.base_name = base_name; + symbol.pretty_name = pretty_name; + symbol.type = type; + symbol.type.set(ID_access, ID_private); + to_java_method_type(symbol.type).set_is_final(true); + symbol.value.make_nil(); + symbol.mode = ID_java; + assign_parameter_names( + to_java_method_type(symbol.type), symbol.name, symbol_table); + set_declaring_class(symbol, declaring_class); + + log.debug() << "Generating codet: new opaque symbol: method '" << symbol.name + << "'" << messaget::eom; + symbol_table.add(symbol); +} + static bool is_constructor(const irep_idt &method_name) { return id2string(method_name).find("") != std::string::npos; @@ -264,35 +294,18 @@ java_method_typet member_type_lazy( return to_java_method_type(*member_type_from_descriptor); } -/// Retrieves the symbol of the lambda method associated with the given -/// lambda method handle (bootstrap method). -/// \param lambda_method_handles: Vector of lambda method handles (bootstrap -/// methods) of the class where the lambda is called -/// \param index: Index of the lambda method handle in the vector -/// \return Symbol of the lambda method if the method handle has a known type -optionalt java_bytecode_convert_methodt::get_lambda_method_symbol( - const java_class_typet::java_lambda_method_handlest &lambda_method_handles, - const size_t index) -{ - const irept &lambda_method_handle = lambda_method_handles.at(index); - // If the lambda method handle has an unknown type, it does not refer to - // any symbol (it has an empty identifier) - if(!lambda_method_handle.id().empty()) - return symbol_table.lookup_ref(lambda_method_handle.id()); - return {}; -} - /// This creates a method symbol in the symtab, but doesn't actually perform /// method conversion just yet. The caller should call /// java_bytecode_convert_method later to give the symbol/method a body. -/// \param class_symbol: The class this method belongs to +/// \param class_symbol: The class this method belongs to. The method, if not +/// static, will be added to the class' list of methods. /// \param method_identifier: The fully qualified method name, including type /// descriptor (e.g. "x.y.z.f:(I)") /// \param m: The parsed method object to convert. /// \param symbol_table: The global symbol table (will be modified). /// \param message_handler: A message handler to collect warnings. void java_bytecode_convert_method_lazy( - const symbolt &class_symbol, + symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, @@ -384,6 +397,20 @@ void java_bytecode_convert_method_lazy( } symbol_table.add(method_symbol); + + if(!m.is_static) + { + class_typet::methodt new_method; + new_method.set_name(method_symbol.name); + new_method.set_base_name(method_symbol.base_name); + new_method.set_pretty_name(method_symbol.pretty_name); + new_method.set_access(member_type.get_access()); + new_method.type() = method_symbol.type; + + to_class_type(class_symbol.type) + .methods() + .emplace_back(std::move(new_method)); + } } static irep_idt get_method_identifier( @@ -577,8 +604,7 @@ void java_bytecode_convert_methodt::convert( if((!m.is_abstract) && (!m.is_native)) { code_blockt code(convert_parameter_annotations(m, method_type)); - code.append(convert_instructions( - m, to_java_class_type(class_symbol.type).lambda_method_handles())); + code.append(convert_instructions(m)); method_symbol.value = std::move(code); } } @@ -1007,9 +1033,8 @@ code_blockt java_bytecode_convert_methodt::convert_parameter_annotations( return code; } -code_blockt java_bytecode_convert_methodt::convert_instructions( - const methodt &method, - const java_class_typet::java_lambda_method_handlest &lambda_method_handles) +code_blockt +java_bytecode_convert_methodt::convert_instructions(const methodt &method) { const instructionst &instructions=method.instructions; @@ -1263,10 +1288,9 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( } else if(bytecode == BC_invokedynamic) { - // not used in Java if( - const auto res = convert_invoke_dynamic( - lambda_method_handles, i_it->source_location, arg0)) + const auto res = + convert_invoke_dynamic(i_it->source_location, i_it->address, arg0, c)) { results.resize(1); results[0] = *res; @@ -2096,6 +2120,30 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const( return results; } +static void adjust_invoke_argument_types( + const java_method_typet::parameterst ¶meters, + code_function_callt::argumentst &arguments) +{ + // do some type adjustment for the arguments, + // as Java promotes arguments + // Also cast pointers since intermediate locals + // can be void*. + INVARIANT( + parameters.size() == arguments.size(), + "for each parameter there must be exactly one argument"); + for(std::size_t i = 0; i < parameters.size(); i++) + { + const typet &type = parameters[i].type(); + if( + type == java_boolean_type() || type == java_char_type() || + type == java_byte_type() || type == java_short_type() || + type.id() == ID_pointer) + { + arguments[i] = typecast_exprt::conditional_cast(arguments[i], type); + } + } +} + void java_bytecode_convert_methodt::convert_invoke( source_locationt location, const irep_idt &statement, @@ -2173,24 +2221,7 @@ void java_bytecode_convert_methodt::convert_invoke( !use_this || arguments.front().type().id() == ID_pointer, "first argument must be a pointer"); - // do some type adjustment for the arguments, - // as Java promotes arguments - // Also cast pointers since intermediate locals - // can be void*. - INVARIANT( - parameters.size() == arguments.size(), - "for each parameter there must be exactly one argument"); - for(std::size_t i = 0; i < parameters.size(); i++) - { - const typet &type = parameters[i].type(); - if( - type == java_boolean_type() || type == java_char_type() || - type == java_byte_type() || type == java_short_type() || - type.id() == ID_pointer) - { - arguments[i] = typecast_exprt::conditional_cast(arguments[i], type); - } - } + adjust_invoke_argument_types(parameters, arguments); // do some type adjustment for return values exprt lhs = nil_exprt(); @@ -2224,23 +2255,15 @@ void java_bytecode_convert_methodt::convert_invoke( !(is_virtual && is_method_inherited(arg0.get(ID_C_class), arg0.get(ID_component_name)))) { - symbolt symbol; - symbol.name = invoked_method_id; - symbol.base_name = arg0.get(ID_C_base_name); - symbol.pretty_name = id2string(arg0.get(ID_C_class)).substr(6) + "." + - id2string(symbol.base_name) + "()"; - symbol.type = method_type; - symbol.type.set(ID_access, ID_private); - to_java_method_type(symbol.type).set_is_final(true); - symbol.value.make_nil(); - symbol.mode = ID_java; - assign_parameter_names( - to_java_method_type(symbol.type), symbol.name, symbol_table); - set_declaring_class(symbol, arg0.get(ID_C_class)); - - debug() << "Generating codet: new opaque symbol: method '" << symbol.name - << "'" << eom; - symbol_table.add(symbol); + create_method_stub_symbol( + invoked_method_id, + arg0.get(ID_C_base_name), + id2string(arg0.get(ID_C_class)).substr(6) + "." + + id2string(arg0.get(ID_C_base_name)) + "()", + method_type, + arg0.get(ID_C_class), + symbol_table, + get_message_handler()); } exprt function; @@ -2957,40 +2980,74 @@ code_blockt java_bytecode_convert_methodt::convert_astore( } optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( - const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, - const exprt &arg0) + std::size_t instruction_address, + const exprt &arg0, + codet &result_code) { const java_method_typet &method_type = to_java_method_type(arg0.type()); + const java_method_typet::parameterst ¶meters(method_type.parameters()); + const typet &return_type = method_type.return_type(); - const optionalt &lambda_method_symbol = get_lambda_method_symbol( - lambda_method_handles, - method_type.get_int(ID_java_lambda_method_handle_index)); - if(lambda_method_symbol.has_value()) - debug() << "Converting invokedynamic for lambda: " - << lambda_method_symbol.value().name << eom; - else - debug() << "Converting invokedynamic for lambda with unknown handle " - "type" - << eom; + // Note these must be popped regardless of whether we understand the lambda + // method or not + code_function_callt::argumentst arguments = pop(parameters.size()); - const java_method_typet::parameterst ¶meters(method_type.parameters()); + irep_idt synthetic_class_name = + lambda_synthetic_class_name(method_id, instruction_address); + + if(!symbol_table.has_symbol(synthetic_class_name)) + { + // We failed to parse the invokedynamic handle as a Java 8+ lambda; + // give up and return null. + const auto value = zero_initializer(return_type, location, ns); + if(!value.has_value()) + { + error().source_location = location; + error() << "failed to zero-initialize return type" << eom; + throw 0; + } + return value; + } - pop(parameters.size()); + // Construct an instance of the synthetic class created for this invokedynamic + // site: - const typet &return_type = method_type.return_type(); + irep_idt constructor_name = id2string(synthetic_class_name) + "."; - if(return_type.id() == ID_empty) - return {}; + const symbolt &constructor_symbol = ns.lookup(constructor_name); - const auto value = zero_initializer(return_type, location, ns); - if(!value.has_value()) + code_blockt result; + + // SyntheticType lambda_new = new SyntheticType; + const reference_typet ref_type = + java_reference_type(struct_tag_typet(synthetic_class_name)); + side_effect_exprt java_new_expr(ID_java_new, ref_type, location); + const exprt new_instance = tmp_variable("lambda_new", ref_type); + result.add(code_assignt(new_instance, java_new_expr, location)); + + // lambda_new.(capture_1, capture_2, ...); + // Add the implicit 'this' parameter: + arguments.insert(arguments.begin(), new_instance); + adjust_invoke_argument_types( + to_code_type(constructor_symbol.type).parameters(), arguments); + + code_function_callt constructor_call( + constructor_symbol.symbol_expr(), arguments); + constructor_call.add_source_location() = location; + result.add(constructor_call); + if(needed_lazy_methods) { - error().source_location = location; - error() << "failed to zero-initialize return type" << eom; - throw 0; + needed_lazy_methods->add_needed_method(constructor_symbol.name); + needed_lazy_methods->add_needed_class(synthetic_class_name); } - return value; + + result_code = std::move(result); + + if(return_type.id() == ID_empty) + return {}; + else + return new_instance; } void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr( diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 4fa21fc85dd..7df52892628 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -39,8 +39,17 @@ void java_bytecode_convert_method( const class_hierarchyt &class_hierarchy, bool threading_support); +void create_method_stub_symbol( + const irep_idt &identifier, + const irep_idt &base_name, + const irep_idt &pretty_name, + const typet &type, + const irep_idt &declaring_class, + symbol_table_baset &symbol_table, + message_handlert &message_handler); + void java_bytecode_convert_method_lazy( - const symbolt &class_symbol, + symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index ea6c9323d96..c10af8c214d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -289,10 +289,6 @@ class java_bytecode_convert_methodt:public messaget const address_mapt &amap, bool allow_merge = true); - optionalt get_lambda_method_symbol( - const java_class_typet::java_lambda_method_handlest &lambda_method_handles, - const size_t index); - // conversion void convert(const symbolt &class_symbol, const methodt &); @@ -300,9 +296,7 @@ class java_bytecode_convert_methodt:public messaget const methodt &method, const java_method_typet &method_type); - code_blockt convert_instructions( - const methodt &, - const java_class_typet::java_lambda_method_handlest &); + code_blockt convert_instructions(const methodt &); codet get_clinit_call(const irep_idt &classname); @@ -346,9 +340,10 @@ class java_bytecode_convert_methodt:public messaget &ret_instructions) const; optionalt convert_invoke_dynamic( - const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, - const exprt &arg0); + std::size_t instruction_address, + const exprt &arg0, + codet &result_code); code_blockt convert_astore( const irep_idt &statement, diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6a170274172..2d711a0df84 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_string_literal_expr.h" #include "java_string_literals.h" #include "java_utils.h" +#include "lambda_synthesis.h" #include "expr2java.h" #include "load_method_by_regex.h" @@ -739,6 +740,24 @@ bool java_bytecode_languaget::typecheck( } } + // Now add synthetic classes for every invokedynamic instruction found (it + // makes this easier that all interface types and their methods have been + // created above): + for(const auto &id_and_symbol : symbol_table) + { + const auto &symbol = id_and_symbol.second; + const auto &id = symbol.name; + if(can_cast_type(symbol.type) && method_bytecode.get(id)) + { + create_invokedynamic_synthetic_classes( + id, + method_bytecode.get(id)->get().method.instructions, + symbol_table, + synthetic_methods, + get_message_handler()); + } + } + // Now that all classes have been created in the symbol table we can populate // the class hierarchy: class_hierarchy(symbol_table); @@ -1062,6 +1081,15 @@ static void notify_static_method_calls( expr_dynamic_cast(fn_call->function()); needed_lazy_methods->add_needed_method(fn_sym.get_identifier()); } + else if( + it->id() == ID_side_effect && + to_side_effect_expr(*it).get_statement() == ID_function_call) + { + const auto &call_expr = to_side_effect_expr_function_call(*it); + const symbol_exprt &fn_sym = + expr_dynamic_cast(call_expr.function()); + needed_lazy_methods->add_needed_method(fn_sym.get_identifier()); + } } } } @@ -1173,6 +1201,14 @@ bool java_bytecode_languaget::convert_single_method( get_pointer_type_selector(), get_message_handler()); break; + case synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR: + writable_symbol.value = invokedynamic_synthetic_constructor( + function_id, symbol_table, get_message_handler()); + break; + case synthetic_method_typet::INVOKEDYNAMIC_METHOD: + writable_symbol.value = invokedynamic_synthetic_method( + function_id, symbol_table, get_message_handler()); + break; } // Notify lazy methods of static calls made from the newly generated // function: diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp new file mode 100644 index 00000000000..76f0ca81102 --- /dev/null +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -0,0 +1,507 @@ +/*******************************************************************\ + +Module: Java lambda code synthesis + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Java lambda code synthesis + +#include "lambda_synthesis.h" + +#include "java_bytecode_convert_method.h" +#include "java_bytecode_parse_tree.h" +#include "java_types.h" +#include "java_utils.h" +#include "synthetic_methods_map.h" + +#include +#include +#include +#include + +#include + +static std::string escape_symbol_special_chars(std::string input) +{ + for(auto &c : input) + { + if(c == '$' || c == ':' || c == '.') + c = '_'; + } + return input; +} + +irep_idt lambda_synthetic_class_name( + const irep_idt &method_identifier, + std::size_t instruction_address) +{ + return "java::lambda_synthetic_class$" + + escape_symbol_special_chars( + id2string(strip_java_namespace_prefix(method_identifier))) + + "$" + std::to_string(instruction_address); +} + +/// Retrieves the symbol of the lambda method associated with the given +/// lambda method handle (bootstrap method). +/// \param symbol_table: global symbol table +/// \param lambda_method_handles: Vector of lambda method handles (bootstrap +/// methods) of the class where the lambda is called +/// \param index: Index of the lambda method handle in the vector +/// \return Symbol of the lambda method if the method handle has a known type +static optionalt get_lambda_method_symbol( + const symbol_table_baset &symbol_table, + const java_class_typet::java_lambda_method_handlest &lambda_method_handles, + const size_t index) +{ + // Check if we don't have enough bootstrap methods to satisfy the requested + // lambda. This could happen if we fail to parse one of the methods, or if + // the class type is partly or entirely synthetic, such as the types created + // internally by the string solver. + if(index >= lambda_method_handles.size()) + return {}; + const irept &lambda_method_handle = lambda_method_handles.at(index); + // If the lambda method handle has an unknown type, it does not refer to + // any symbol (it has an empty identifier) + if(!lambda_method_handle.id().empty()) + return symbol_table.lookup_ref(lambda_method_handle.id()); + return {}; +} + +static optionalt lambda_method_name( + const symbol_tablet &symbol_table, + const irep_idt &method_identifier, + const java_method_typet &dynamic_method_type) +{ + const namespacet ns{symbol_table}; + const auto &method_symbol = ns.lookup(method_identifier); + const auto &declaring_class_symbol = + ns.lookup(*declaring_class(method_symbol)); + + const auto &class_type = to_java_class_type(declaring_class_symbol.type); + const auto &lambda_method_handles = class_type.lambda_method_handles(); + auto lambda_handle_index = + dynamic_method_type.get_int(ID_java_lambda_method_handle_index); + const auto lambda_method_symbol = get_lambda_method_symbol( + symbol_table, lambda_method_handles, lambda_handle_index); + if(lambda_method_symbol) + return lambda_method_symbol->name; + return {}; +} + +static optionalt interface_method_id( + const symbol_tablet &symbol_table, + const struct_tag_typet &functional_interface_tag, + const irep_idt &method_identifier, + const int instruction_address, + const messaget &log) +{ + const namespacet ns{symbol_table}; + const java_class_typet &implemented_interface_type = [&] { + const symbolt &implemented_interface_symbol = + ns.lookup(functional_interface_tag.get_identifier()); + return to_java_class_type(implemented_interface_symbol.type); + }(); + + if(implemented_interface_type.get_is_stub()) + { + log.debug() << "ignoring invokedynamic at " << method_identifier + << " address " << instruction_address + << " which produces a stub type " + << functional_interface_tag.get_identifier() << messaget::eom; + return {}; + } + else if(implemented_interface_type.methods().size() != 1) + { + log.debug() + << "ignoring invokedynamic at " << method_identifier << " address " + << instruction_address << " which produces type " + << functional_interface_tag.get_identifier() + << " which should have exactly one abstract method but actually has " + << implemented_interface_type.methods().size() + << ". Note default methods are not supported yet." << messaget::eom; + return {}; + } + return implemented_interface_type.methods().at(0).get_name(); +} + +symbolt synthetic_class_symbol( + const irep_idt &synthetic_class_name, + const irep_idt &lambda_method_name, + const struct_tag_typet &functional_interface_tag, + const java_method_typet &dynamic_method_type) +{ + java_class_typet synthetic_class_type; + // Tag = name without 'java::' prefix, matching the convention used by + // java_bytecode_convert_class.cpp + synthetic_class_type.set_tag( + strip_java_namespace_prefix(synthetic_class_name)); + synthetic_class_type.set_name(synthetic_class_name); + synthetic_class_type.set_synthetic(true); + synthetic_class_type.set( + ID_java_lambda_method_identifier, lambda_method_name); + struct_tag_typet base_tag("java::java.lang.Object"); + synthetic_class_type.add_base(base_tag); + synthetic_class_type.add_base(functional_interface_tag); + + // Add the class fields: + + { + java_class_typet::componentt base_field; + const irep_idt base_field_name("@java.lang.Object"); + base_field.set_name(base_field_name); + base_field.set_base_name(base_field_name); + base_field.set_pretty_name(base_field_name); + base_field.set_access(ID_private); + base_field.type() = base_tag; + synthetic_class_type.components().emplace_back(std::move(base_field)); + + std::size_t field_idx = 0; + for(const auto ¶m : dynamic_method_type.parameters()) + { + irep_idt field_basename = "capture_" + std::to_string(field_idx++); + + java_class_typet::componentt new_field; + new_field.set_name(field_basename); + new_field.set_base_name(field_basename); + new_field.set_pretty_name(field_basename); + new_field.set_access(ID_private); + new_field.type() = param.type(); + synthetic_class_type.components().emplace_back(std::move(new_field)); + } + } + + symbolt synthetic_class_symbol = type_symbolt{synthetic_class_type}; + synthetic_class_symbol.name = synthetic_class_name; + synthetic_class_symbol.mode = ID_java; + return synthetic_class_symbol; +} + +static symbolt constructor_symbol( + synthetic_methods_mapt &synthetic_methods, + const irep_idt &synthetic_class_name, + java_method_typet constructor_type) // dynamic_method_type +{ + symbolt constructor_symbol; + irep_idt constructor_name = id2string(synthetic_class_name) + "."; + constructor_symbol.name = constructor_name; + constructor_symbol.pretty_name = constructor_symbol.name; + constructor_symbol.base_name = ""; + constructor_symbol.mode = ID_java; + + synthetic_methods[constructor_name] = + synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR; + + constructor_type.set_is_constructor(); + constructor_type.return_type() = empty_typet(); + + size_t field_idx = 0; + for(auto ¶m : constructor_type.parameters()) + { + irep_idt param_basename = "param_" + std::to_string(field_idx++); + param.set_base_name(param_basename); + param.set_identifier( + id2string(constructor_name) + "::" + id2string(param_basename)); + } + + java_method_typet::parametert constructor_this_param; + constructor_this_param.set_this(); + constructor_this_param.set_base_name("this"); + constructor_this_param.set_identifier(id2string(constructor_name) + "::this"); + constructor_this_param.type() = + java_reference_type(struct_tag_typet(synthetic_class_name)); + + constructor_type.parameters().insert( + constructor_type.parameters().begin(), constructor_this_param); + + constructor_symbol.type = constructor_type; + set_declaring_class(constructor_symbol, synthetic_class_name); + return constructor_symbol; +} + +symbolt implemented_method_symbol( + synthetic_methods_mapt &synthetic_methods, + const symbolt &interface_method_symbol, + const struct_tag_typet &functional_interface_tag, + const irep_idt &synthetic_class_name) +{ + const std::string implemented_method_name = [&] { + std::string implemented_method_name = + id2string(interface_method_symbol.name); + const std::string &functional_interface_tag_str = + id2string(functional_interface_tag.get_identifier()); + INVARIANT( + has_prefix(implemented_method_name, functional_interface_tag_str), + "method names should be prefixed by their defining type"); + implemented_method_name.replace( + 0, + functional_interface_tag_str.length(), + id2string(synthetic_class_name)); + return implemented_method_name; + }(); + + symbolt implemented_method_symbol; + implemented_method_symbol.name = implemented_method_name; + synthetic_methods[implemented_method_symbol.name] = + synthetic_method_typet::INVOKEDYNAMIC_METHOD; + implemented_method_symbol.pretty_name = implemented_method_symbol.name; + implemented_method_symbol.base_name = interface_method_symbol.base_name; + implemented_method_symbol.mode = ID_java; + implemented_method_symbol.type = interface_method_symbol.type; + auto &implemented_method_type = to_code_type(implemented_method_symbol.type); + implemented_method_type.parameters()[0].type() = + java_reference_type(struct_tag_typet(synthetic_class_name)); + + size_t field_idx = 0; + for(auto ¶m : implemented_method_type.parameters()) + { + irep_idt param_basename = + field_idx == 0 ? "this" : "param_" + std::to_string(field_idx); + param.set_base_name(param_basename); + param.set_identifier( + id2string(implemented_method_name) + "::" + id2string(param_basename)); + + ++field_idx; + } + + set_declaring_class(implemented_method_symbol, synthetic_class_name); + return implemented_method_symbol; +} + +// invokedynamic will be called with operands that should be stored in a +// synthetic object implementing the interface type that it returns. For +// example, "invokedynamic f(a, b, c) -> MyInterface" should result in the +// creation of the synthetic class: +// public class SyntheticCapture implements MyInterface { +// private int a; +// private float b; +// private Other c; +// public SyntheticCapture(int a, float b, Other c) { +// this.a = a; this.b = b; this.c = c; +// } +// public void myInterfaceMethod(int d) { +// f(a, b, c, d); +// } +// } +// This method just creates the outline; the methods will be populated on +// demand via java_bytecode_languaget::convert_lazy_method. + +// Check that we understand the lambda method handle; if we don't then +// we will not create a synthetic class at all, and the corresponding +// invoke instruction will return null when eventually converted by +// java_bytecode_convert_method. +void create_invokedynamic_synthetic_classes( + const irep_idt &method_identifier, + const java_bytecode_parse_treet::methodt::instructionst &instructions, + symbol_tablet &symbol_table, + synthetic_methods_mapt &synthetic_methods, + message_handlert &message_handler) +{ + const messaget log{message_handler}; + + for(const auto &instruction : instructions) + { + if(strcmp(bytecode_info[instruction.bytecode].mnemonic, "invokedynamic")) + continue; + const auto &dynamic_method_type = + to_java_method_type(instruction.args.at(0).type()); + const auto lambda_method_name = ::lambda_method_name( + symbol_table, method_identifier, dynamic_method_type); + if(!lambda_method_name) + { + log.debug() << "ignoring invokedynamic at " << method_identifier + << " address " << instruction.address + << " with unknown handle type" << messaget::eom; + continue; + } + const auto &functional_interface_tag = to_struct_tag_type( + to_java_reference_type(dynamic_method_type.return_type()).subtype()); + const auto interface_method_id = ::interface_method_id( + symbol_table, + functional_interface_tag, + method_identifier, + instruction.address, + log); + if(!interface_method_id) + continue; + log.debug() << "identified invokedynamic at " << method_identifier + << " address " << instruction.address + << " for lambda: " << *lambda_method_name << messaget::eom; + const irep_idt synthetic_class_name = + lambda_synthetic_class_name(method_identifier, instruction.address); + symbol_table.add(constructor_symbol( + synthetic_methods, synthetic_class_name, dynamic_method_type)); + symbol_table.add(implemented_method_symbol( + synthetic_methods, + symbol_table.lookup_ref(*interface_method_id), + functional_interface_tag, + synthetic_class_name)); + symbol_table.add(synthetic_class_symbol( + synthetic_class_name, + *lambda_method_name, + functional_interface_tag, + dynamic_method_type)); + } +} + +static const symbolt &get_or_create_method_symbol( + const irep_idt &identifier, + const irep_idt &base_name, + const irep_idt &pretty_name, + const typet &type, + const irep_idt &declaring_class, + symbol_table_baset &symbol_table, + message_handlert &log) +{ + const auto *existing_symbol = symbol_table.lookup(identifier); + if(existing_symbol) + return *existing_symbol; + + create_method_stub_symbol( + identifier, + base_name, + pretty_name, + type, + declaring_class, + symbol_table, + log); + return symbol_table.lookup_ref(identifier); +} + +codet invokedynamic_synthetic_constructor( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + code_blockt result; + namespacet ns(symbol_table); + + const symbolt &function_symbol = ns.lookup(function_id); + const auto ¶meters = to_code_type(function_symbol.type).parameters(); + + const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol)); + const class_typet &class_type = to_class_type(class_symbol.type); + + const symbol_exprt this_param( + parameters.at(0).get_identifier(), parameters.at(0).type()); + const dereference_exprt deref_this(this_param); + + // Call super-constructor (always java.lang.Object): + const irep_idt jlo("java::java.lang.Object"); + const irep_idt jlo_constructor(id2string(jlo) + ".:()V"); + const auto jlo_reference = java_reference_type(struct_tag_typet(jlo)); + code_typet::parametert jlo_this_param{jlo_reference}; + jlo_this_param.set_this(); + + java_method_typet jlo_constructor_type( + code_typet::parameterst{jlo_this_param}, empty_typet()); + const auto &jlo_constructor_symbol = get_or_create_method_symbol( + jlo_constructor, + "", + jlo_constructor, + jlo_constructor_type, + jlo, + symbol_table, + message_handler); + code_function_callt super_constructor_call( + jlo_constructor_symbol.symbol_expr(), + code_function_callt::argumentst{typecast_exprt(this_param, jlo_reference)}); + result.add(super_constructor_call); + + // Store captured parameters: + auto field_iterator = std::next(class_type.components().begin()); + for(const auto ¶meter : parameters) + { + // Give the parameter its symbol: + parameter_symbolt param_symbol; + param_symbol.name = parameter.get_identifier(); + param_symbol.base_name = parameter.get_base_name(); + param_symbol.mode = ID_java; + param_symbol.type = parameter.type(); + symbol_table.add(param_symbol); + + if(parameter.get_this()) + continue; + + code_assignt assign_field( + member_exprt(deref_this, field_iterator->get_name(), parameter.type()), + symbol_exprt(parameter.get_identifier(), parameter.type())); + result.add(assign_field); + + ++field_iterator; + } + + return std::move(result); +} + +codet invokedynamic_synthetic_method( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler) +{ + // Call the bound method with the capture parameters, then the actual + // parameters. Note one of the capture params might be the `this` parameter + // of a virtual call -- that depends on whether the callee is a static or an + // instance method. + + code_blockt result; + namespacet ns(symbol_table); + + 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); + + const symbol_exprt this_param( + parameters.at(0).get_identifier(), parameters.at(0).type()); + const dereference_exprt deref_this(this_param); + + code_function_callt::argumentst lambda_method_args; + for(const auto &field : class_type.components()) + { + if(field.get_name() == "@java.lang.Object") + continue; + lambda_method_args.push_back( + member_exprt(deref_this, field.get_name(), field.type())); + } + + for(const auto ¶meter : parameters) + { + // Give the parameter its symbol: + parameter_symbolt param_symbol; + param_symbol.name = parameter.get_identifier(); + param_symbol.base_name = parameter.get_base_name(); + param_symbol.mode = ID_java; + param_symbol.type = parameter.type(); + symbol_table.add(param_symbol); + + if(parameter.get_this()) + continue; + + lambda_method_args.push_back(param_symbol.symbol_expr()); + } + + const auto &lambda_method_symbol = + ns.lookup(class_type.get(ID_java_lambda_method_identifier)); + + if(return_type != empty_typet()) + { + result.add(code_returnt(side_effect_expr_function_callt( + lambda_method_symbol.symbol_expr(), + lambda_method_args, + return_type, + source_locationt()))); + } + else + { + result.add(code_function_callt( + lambda_method_symbol.symbol_expr(), lambda_method_args)); + } + + return std::move(result); +} diff --git a/jbmc/src/java_bytecode/lambda_synthesis.h b/jbmc/src/java_bytecode/lambda_synthesis.h new file mode 100644 index 00000000000..af7da646fb5 --- /dev/null +++ b/jbmc/src/java_bytecode/lambda_synthesis.h @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Java lambda code synthesis + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Java lambda code synthesis + +#ifndef CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H +#define CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H + +#include +#include +#include + +class message_handlert; +class codet; +class symbol_table_baset; +class symbol_tablet; + +irep_idt lambda_synthetic_class_name( + const irep_idt &method_identifier, + std::size_t instruction_address); + +void create_invokedynamic_synthetic_classes( + const irep_idt &method_identifier, + const java_bytecode_parse_treet::methodt::instructionst &instructions, + symbol_tablet &symbol_table, + synthetic_methods_mapt &synthetic_methods, + message_handlert &message_handler); + +/// Create invokedynamic synthetic constructor +codet invokedynamic_synthetic_constructor( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler); + +/// Create invokedynamic synthetic method +codet invokedynamic_synthetic_method( + const irep_idt &function_id, + symbol_table_baset &symbol_table, + message_handlert &message_handler); + +#endif // CPROVER_JAVA_BYTECODE_LAMBDA_SYNTHESIS_H diff --git a/jbmc/src/java_bytecode/synthetic_methods_map.h b/jbmc/src/java_bytecode/synthetic_methods_map.h index 26645c67e00..67200b5a9de 100644 --- a/jbmc/src/java_bytecode/synthetic_methods_map.h +++ b/jbmc/src/java_bytecode/synthetic_methods_map.h @@ -36,7 +36,13 @@ enum class synthetic_method_typet /// A generated (synthetic) static initializer function for a stub type. /// Because we don't have the bytecode for a stub type (by definition), we /// generate a static initializer function to initialize its static fields. - STUB_CLASS_STATIC_INITIALIZER + STUB_CLASS_STATIC_INITIALIZER, + /// A generated constructor for a class capturing the parameters of an + /// invokedynamic instruction + INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR, + /// A generated method for a class capturing the parameters of an + /// invokedynamic instruction + INVOKEDYNAMIC_METHOD }; /// Maps method names on to a synthetic method kind. diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index ef2676574d3..8f042b85487 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -653,6 +653,7 @@ IREP_ID_TWO(implicit_generic_types, #implicit_generic_types) IREP_ID_ONE(type_variables) IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index) IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles) +IREP_ID_TWO(java_lambda_method_identifier, lambda_method_identifier) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)