Java 8 Lambdas

[Peter Anderson]

JPF folks,

I noticed that JPF now has support for Java 8. Does this include the byte codes necessary to use lambdas? If not, when do we anticipate this support begin available?

Thanks

Pete Anderson

[PETER C MEHLITZ]

yes, invokedynamic is supported. Theoretically, the only thing missing is user defined lambda factories.

-- Peter

[Peter Anderson]

I have run a couple of programs that use lambda function and JPF is throwing a null pointer exception in its internals. I assume that this is a bug that deals with lambdas because when I change them to anonymous inner classes they work just fine. If this is a bug, how can I help report it? Stack trace?

Thanks

Pete

[Nastaran Shafiei]

Hi Peter,

Can you please send me the lambda example that fails?

Thanks!

Nastaran

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Peter Anderson]

I have attached the file that fails. I have also attached the library needed to support that file. Below is the output that I get when I run the file within JPF. If you need anything else please let me know.

java.lang.NullPointerException

at gov.nasa.jpf.jvm.bytecode.VirtualInvocation.getInvokedMethod(VirtualInvocation.java:142)

at gov.nasa.jpf.jvm.bytecode.VirtualInvocation.execute(VirtualInvocation.java:76)

at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1890)

at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1848)

at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:733)

at gov.nasa.jpf.vm.VM.forward(VM.java:1719)

at gov.nasa.jpf.search.Search.forward(Search.java:580)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)

at gov.nasa.jpf.JPF.run(JPF.java:613)

at gov.nasa.jpf.JPF.start(JPF.java:190)

at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)

at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)

at java.lang.reflect.Method.invoke(Method.java:483)

at gov.nasa.jpf.tool.Run.call(Run.java:81)

at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)

[Nastaran Shafiei]

Hi Peter,

Thanks. Using your example, I was able to trackdown and fix the bug. In case you need the fix immediately attached you can find it. Otherwise, we will update the repository soon.

Thanks,

Nastaran

[Peter Anderson]

Thank you!

[Nicola Atzei]

Hi Nastaran,

I have a problem similar to the Peter's one (related to invoke dynamic and lambda expressions).

JPF version

JavaPathfinder core system v8.0 (rev 25+) - (C) 2005-2014 United States Government. All rights reserved.

The code that fails is

import java.util.Arrays;

public class Example {

    public static void main (String[] args) throws Exception {
       
        System.out.println(
                Arrays.toString(
                    Arrays.stream(new Integer[]{1,2,3,4,5,6,7,8,9,10})
                        .map( p -> p+1 )
                        .toArray(Integer[]::new)
                )
        );
    }
   
}

and the exeption is

java.lang.NullPointerException
    at gov.nasa.jpf.jvm.JVMClassInfo.<init>(JVMClassInfo.java:645)
    at gov.nasa.jpf.jvm.JVMClassInfo.createFuncObjClassInfo(JVMClassInfo.java:635)
    at gov.nasa.jpf.vm.ClassLoaderInfo.getResolvedFuncObjType(ClassLoaderInfo.java:457)
    at gov.nasa.jpf.vm.FunctionObjectFactory.getFunctionObject(FunctionObjectFactory.java:30)
    at gov.nasa.jpf.jvm.bytecode.INVOKEDYNAMIC.execute(INVOKEDYNAMIC.java:122)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)

    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)

    at java.lang.reflect.Method.invoke(Method.java:497)
    at gov.nasa.jpf.tool.Run.call(Run.java:80)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)

and finally my .jpf

target=Example

native_classpath+=./bin
classpath+=./bin/
sourcepath+=./src/

cg.enumerate_random = true

hope you can help me.
thanks

Nicola

[Nastaran Shafiei]

Hi Nicola,

I am working on fixing the bug. I’ll let you know once I have a fix.

Thanks,

Nastaran

[Nastaran Shafiei]

Hi Nicola,

I added support for the double colon operator in JPF. Now your example should run fine with the new version of jpf-core.

Thanks,

Nastaran

On May 30, 2015, at 12:03 PM, Nicola Atzei <atzei...@gmail.com> wrote:

[Nicola Atzei]

Thank you so much!
Best regards,

Nicola

[Nicola Atzei]

Hi Nastaran,

I have another problem on Java 8 lambdas.
There is a inconsistency between the official JVM and JVM_JPF. I explain you the problem with an example.

The JPF version is

JavaPathfinder core system v8.0 (rev 28+)

and the example that does not work as expected is

public class JPFLambda {
   
    public static void main (String[] args) {
       
        Foo foo = new Foo();
       
        new Foo().test(foo);
        System.out.println("---------------------------------");
        new Foo().test(foo);
    }
   
    public static void fooMethod(Foo foo, Consumer<Foo> consumer) {
        consumer.accept(foo);
    }
}

class Foo {
   
    public Foo test(Foo foo1) {

        System.out.println("this.hashCode(): "+this.hashCode());
        System.out.println("foo1.hashCode(): "+foo1.hashCode());
       
        JPFLambda.fooMethod(
                foo1,
                (x)-> {
                    System.out.println("[lambda] this.hashCode(): "+this.hashCode());
                    System.out.println("[lambda] x.hashCode(): "+x.hashCode());
                });
       
        return this;
    }
   
}

The output of the JVM (version 1.8.0_60 in my case) is

this.hashCode(): 705927765
foo1.hashCode(): 366712642
[lambda] this.hashCode(): 705927765
[lambda] x.hashCode(): 366712642
---------------------------------
this.hashCode(): 303563356
foo1.hashCode(): 366712642
[lambda] this.hashCode(): 303563356
[lambda] x.hashCode(): 366712642

while the output of the SUT in JPF is

this.hashCode(): 43666
foo1.hashCode(): 43667
[lambda] this.hashCode(): 43666
[lambda] x.hashCode(): 43667
---------------------------------
this.hashCode(): 43594
foo1.hashCode(): 43667
[lambda] this.hashCode(): 43666  // <-- instead of 43594
[lambda] x.hashCode(): 43667

As you can see, the problem is related to the call of this.hashCode() into the lambda expression.

thanks in advance

Nicola

Il giorno martedì 30 giugno 2015 05:34:51 UTC+2, nastaran ha scritto:

[Nastaran Shafiei]

Hi Nicola,

Thanks for reporting this issue. Yes, this is a bug and has something to do with the way we deal with free vriables within the lambda body. I fixed  the bug and will push the changes to the repo shortly.

Thanks,

Nastaran

[Nicola Atzei]

Thank you Nastaran, you have been very fast!

best regards,
Nicola

[Nicola Atzei]

Hi Nastaran,

sorry but I have a problem with lambdas serialization. As usual, an example is better than thousand words:

public class HelloWorld {
   
    static final Decoder base64Decoder = Base64.getDecoder();
    static final Encoder base64Encoder = Base64.getEncoder();
   
    public static void main(String[] args) throws IOException, ClassNotFoundException {
       
        String lambda = HelloWorld.serializeObjectToString((Serializable & Runnable)()->{ System.out.println("serial"); });
       
        ((Runnable) HelloWorld.deserializeObjectFromString(lambda)).run();
       
    }
   
    public static String serializeObjectToString(Object object) throws IOException {
       
        try (
                ByteArrayOutputStream arrayOutputStream = new ByteArrayOutputStream();
                ObjectOutputStream objectOutputStream = new ObjectOutputStream(arrayOutputStream);
                ) {
            objectOutputStream.writeObject(object);
            objectOutputStream.flush();
            return new String(base64Encoder.encode(arrayOutputStream.toByteArray()));
        }
    }

    private static Object deserializeObjectFromString(String objectString) throws IOException, ClassNotFoundException {
       
        try (
                ByteArrayInputStream arrayInputStream = new ByteArrayInputStream(base64Decoder.decode(objectString));
                ObjectInputStream objectInputStream = new ObjectInputStream(arrayInputStream)
                ) {
            return objectInputStream.readObject();
        }
    }
}

The output of JPF is

JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
HelloWorld.main()

====================================================== search started: 03/03/16 22.01

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ClassCastException: HelloWorld$$Lambda$0 cannot be cast to java.io.Serializable
        at HelloWorld.main(HelloWorld.java:38)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
        at HelloWorld.main(HelloWorld.java:38)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ClassCastException: HelloWorld$$Lambda$0..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=0,end=0
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=389,released=0,maxLive=0,gcCycles=0
instructions:       10548
max memory:         119MB
loaded code:        classes=68,methods=1567

====================================================== search finished: 03/03/16 22.01

whereas the JVM prints the output "serial" correctly.
Thanks in advance,

Nicola