Jar.jpf demo run failed

[qingmuAdore]

env: openJdk 11.0.1

log detail:

* DELEGATING -> java.util.jar.JarFile.<clinit>
* DELEGATING -> java.util.jar.JarFile.<init>
* DELEGATING -> java.util.jar.JarFile.entries
WARNING: the class class java.util.jar.JarFile$$Lambda$40/0x0000000800208c40 is ignored!
* DELEGATING -> java.util.zip.ZipFile.ensureOpen
* DELEGATING -> java.util.zip.ZipFile.getZipEntry
otf - getZipEntry__Ljava_lang_String_2_3BILjava_util_function_Function_2__Ljava_util_zip_ZipEntry_2
Disconnected from the target VM, address: 'localhost:58263', transport: 'socket'
Exception in thread "main" ---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.util.zip.ZipFile.getZipEntry
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:186)
	at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
	at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1910)
	at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1861)
	at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
	at gov.nasa.jpf.vm.VM.forward(VM.java:1721)
	at gov.nasa.jpf.search.Search.forward(Search.java:937)
	at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
	at gov.nasa.jpf.JPF.run(JPF.java:613)
	at com.huawei.runner.JarApp.main(JarApp.java:38)
Caused by: java.lang.reflect.InvocationTargetException
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at OTF_JPF_java_util_zip_ZipFile.getZipEntry__Ljava_lang_String_2_3BILjava_util_function_Function_2__Ljava_util_zip_ZipEntry_2(OTF_JPF_java_util_zip_ZipFile.java:84)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:566)
	at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
	... 9 more
Caused by: java.lang.NullPointerException
	at java.base/java.util.zip.ZipFile.getZipEntry(ZipFile.java:674)
	... 19 more

WARNING: the class class java.util.jar.JarFile$$Lambda$40/0x0000000800208c40 is ignored!
The problem is that classloaderInfo cannot match the class. As a result, the func value is null in the getZipEntry method.

private ZipEntry getZipEntry(String name, byte[] bname, int pos,
                                 Function<String, ? extends ZipEntry> func) {
        ...
        ZipEntry e = func.apply(name);    //throw NullPointerException

[cyrille-artho]

Hi,
We have work in progress in jpf-core, but it is not active at the moment: javapathfinder/jpf-core#483

[qingmuAdore]

@cyrille-artho Thanks for your reply.

Yes, I also see the issue.
We may encounter many problems similar to JarFile. jpf-nhandler is a very good extension to solve the problem that SUT may crash due to dependency libraries.

My problem should be that jpf-nhandler does not support lambda expression objects. Because it is a dynamic class, so ClassLoaderInfo cannot match.

Could you please help me solve this problem? Thanks very much.

[qingmuAdore]

@cyrille-artho

I replaced the unmatched class with Object.class. Run successfully, and you can evaluate if it's feasible.

JVM2JPFConverter.java

  protected ClassInfo getJPFCls (Class<?> JVMCls, MJIEnv env) throws ConversionException{
    ClassInfo JPFCls = null;
    int JPFClsRef = Integer.MIN_VALUE;

    if (JVMCls != null){
      // retrieving the integer representing the Class in JPF
      try {
        JPFCls = ClassLoaderInfo.getCurrentResolvedClassInfo(JVMCls.getName()); 
      }catch (ClassInfoException ex){
        // use Object.class replace not match class 
        JPFCls = ClassLoaderInfo.getCurrentResolvedClassInfo(Object.class.getName());
      }
    ....

[cyrille-artho]

Thank you for your suggestion. I see that using Object, being the base class of everything, may sometimes work as a stand-in for the actual type. However, if we later try to call a method or access a field of that class, that will fail (unless Object already supports it).
Your suggestion also catches an exception that is meant to signal an internal error (an incorrect class name).
Can you please show a test that fails without your change and works with it? Perhaps it is possible to recover from a failed class lookup in a different way? If not, it would help to understand under which conditions your workaround is suitable.

[cyrille-artho]

The easiest way to share your setting is to make a pull request against the current version of jpf-nhandler.