Synthesise lambda classes

jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java

@@ -0,0 +1,6 @@
+interface InterfaceDeclaringEquals {
+
+  public int f(int x);
+
+  public boolean equals(Object other);
+}

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; }
+}

jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java

@@ -0,0 +1,4 @@
+interface StubInterface {
+
+  public int f(int x);
+}

jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.java

@@ -0,0 +1 @@
+interface StubSuperinterface extends StubInterface {}

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);
+  }
+}

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.

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<Double, Double> dmul = x -> x * 3.1415;
+  public static Function<Double, Double> dmul = x -> x * 1.5;
 
-    public void set(int x) {
-        y = x;
-    }
+  public void set(int x) { y = x; }
 }

jbmc/regression/jbmc/lambda1/BiFunction.java

@@ -0,0 +1,5 @@
+
+interface BiFunction<From1, From2, To> {
+
+  public To apply(From1 f1, From2 f2);
+}

jbmc/regression/jbmc/lambda1/CustomLambda.java

@@ -1,4 +1,4 @@
 @FunctionalInterface
 interface CustomLambda<T> {
-    boolean is_ok(T t);
+  boolean is_ok(T t);
 }

jbmc/regression/jbmc/lambda1/Function.java

@@ -0,0 +1,5 @@
+
+interface Function<From, To> {
+
+  public To apply(From f);
+}

jbmc/regression/jbmc/lambda1/Lambdatest.java

@@ -1,97 +1,185 @@
-import java.util.function.*;
-
 public class Lambdatest {
 
-    class A {
-        int x;
-    }
-
-    CustomLambda<Integer> custom = x -> true;
-    BiFunction<Float, Integer, Integer> add = (x0, y0) -> x0.intValue() + y0;
-    int z = 10;
-
-    A a;
-    B b = new B();
-
-    public Integer g(Float x, Integer y, BiFunction<Float, Integer, Integer> fun) {
-        return fun.apply(x, y);
-    }
-
-    public int f(Float x, Integer y, Integer z) {
-        Integer tmp = add.apply(x, y);
-        Function<Integer, Integer> mul = (a) -> a * tmp;
-        return mul.apply(z);
-    }
-
-    public int i(int x) {
-        int z = 5;
-        Function<Integer, Integer> foo = (a) -> a * z;
-        return foo.apply(x);
-    }
-
-    public int j(int x) {
-        Function<Integer, Integer> foo = (a) -> a * z;
-        return foo.apply(x);
-    }
-
-    public int k(int x) {
-        a.x = 10;
-
-        Function<Integer, Integer> foo = (y) -> y * a.x;
-        return foo.apply(x);
-    }
-
-    public int l(int x) {
-        b.y = 10;
-        Function<Integer, Integer> 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<Integer, Integer> 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<Integer> custom = x -> true;
+  BiFunction<Float, Integer, Integer> 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<Float, Integer, Integer> fun) {
+    return fun.apply(x, y);
+  }
+
+  public int captureReference(Float x, Integer y, Integer z) {
+    Integer tmp = add.apply(x, y);
+    Function<Integer, Integer> mul = (a) -> a * tmp;
+    return mul.apply(z);
+  }
+
+  public int captureInt(int x) {
+    int z = 5;
+    Function<Integer, Integer> foo = (a) -> a * z;
+    return foo.apply(x);
+  }
+
+  public int captureThisPrimitive(int x) {
+    Function<Integer, Integer> foo = (a) -> a * z;
+    return foo.apply(x);
+  }
+
+  public int captureThisReference(int x) {
+    a.x = 10;
+
+    Function<Integer, Integer> foo = (y) -> y * a.x;
+    return foo.apply(x);
+  }
+
+  public int captureAndCall(int x) {
+    b.y = 10;
+    Function<Integer, Integer> 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<Integer, Integer> 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<Integer, Integer> func = (x) -> x + array.length;
+      assert func.apply(2) == 5; // should succeed
+    } else if (unknown == 21) {
+      int array[] = new int[3];
+      Function<Integer, Integer> 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<Integer, Integer> func = (x) -> x + array.length;
+      assert func.apply(2) == 5; // should succeed
+    } else if (unknown == 23) {
+      Integer array[] = new Integer[3];
+      Function<Integer, Integer> 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<Integer, Integer> 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<Integer, Integer> 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<Integer, Object> lambda = (x) -> object;
+      assert (lambda.apply(0) == object); // should succeed
+    } else if (unknown == 29) {
+      Object object = new Object();
+      Function<Integer, Object> 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<Integer, Integer> func = (x) -> value;
+    assert func.apply(0) == 42;
+  }
+}
 
-    public boolean custom(Integer i) {
-        return custom.is_ok(i);
-    }
+class StaticLambdas {
+  final static Function<Integer, Integer> 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<Integer, Integer> getOuterGetter() { return (x) -> value; }
+  }
 }
 
 class C implements CustomLambda<Integer> {
-    public boolean is_ok(Integer i) {
-        return true;
-    }
+  public boolean is_ok(Integer i) { return true; }
 }

jbmc/regression/jbmc/lambda1/Nondet.java

@@ -0,0 +1,16 @@
+public class Nondet {
+  int x;
+  int y;
+  public static void test(Nondet nondet) {
+    Function<Integer, Integer> lambda = (z) -> nondet.x + nondet.y + z;
+    assert (lambda.apply(0) == 42);
+  }
+  public static void testPrimitiveArray(int[] ints) {
+    Function<Integer, Integer> lambda = (index) -> ints[index];
+    assert (lambda.apply(0) == 42);
+  }
+  public static void testReferenceArray(Nondet[] nondets) {
+    Function<Integer, Integer> lambda = (index) -> nondets[index].x;
+    assert (lambda.apply(0) == 42);
+  }
+}

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

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