Test "gov.nasa.jpf.test.java.io.ObjectStreamTest and gov.nasa.jpf.test.java.io.testSimpleReadbackOk" Fails on Java 17

Question

Test "gov.nasa.jpf.test.java.io.ObjectStreamTest and gov.nasa.jpf.test.java.io.testSimpleReadbackOk" Fails on Java 17

eklaDFF opened this issue 3 months ago · 18 comments

While running the ./gradlew clean test on OpenJDK-17, gov.nasa.jpf.test.java.io.ObjectStreamTest and gov.nasa.jpf.test.java.io.testSimpleReadbackOk tests fails.

Here is the Standard Output :

running jpf with args:
JavaPathfinder core system v8.0 (rev 76cd506eb2d0de999cc263b3315b4f930c1505ad) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 20/06/24, 11:38 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: java.lang.System.getLogger(Ljava/lang/String;)Ljava/lang/System$Logger;
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:616)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testLambdaSerialization(ObjectStreamTest.java:143)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@27d
  call stack:
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:616)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testLambdaSerialization(ObjectStreamTest.java:143)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: java.lang.System...."

====================================================== search finished: 20/06/24, 11:38 pm
  running jpf with args:
JavaPathfinder core system v8.0 (rev 76cd506eb2d0de999cc263b3315b4f930c1505ad) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 20/06/24, 11:38 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: java.lang.System.getLogger(Ljava/lang/String;)Ljava/lang/System$Logger;
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:616)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@27d
  call stack:
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:616)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: java.lang.System...."

====================================================== search finished: 20/06/24, 11:38 pm

eklaDFF commented 3 months ago

PR #469

Answer 1 · 2024-06-20T18:31:40.000Z

@cyrille-artho
I do analysis on this error.

In java.lang.System, there is no method named with java.lang.System.getLogger(). getLogger() is quite complex in depth. Please look at this once yourself .

Answer 2 · 2024-06-24T06:48:25.000Z

Thanks for looking into this. It is unfortunate that the logger is needed to initialize the ObjectInputStream now, because our examples tend not to use it.
One option could be to implement a very simple logger, which logs everything to System.out unless logging is completely turned off. Another option is to return a dummy object or even null in getLogger. The latter is a good first step to see if the Logger instance is used anywhere at all.

Answer 3 · 2024-06-27T07:20:50.000Z

If returning null does not work, implement a dummy class that contains only empty methods to implement the interface System.Logger. Simply implement enough empty methods (max. 9) to the compiler sees that the interface is implemented and the code can compile and run. We don't need the actual logging functionality for our uses.

Answer 4 · 2024-06-27T14:24:11.000Z

Implemented these stuff in System.java.

public static Logger getLogger (String name){
    return new Logger() {
      @Override
      public String getName() {
        return null;
      }

      @Override
      public boolean isLoggable(Level level) {
        return false;
      }

      @Override
      public void log(Level level, ResourceBundle bundle, String msg, Throwable thrown) {

      }

      @Override
      public void log(Level level, ResourceBundle bundle, String format, Object... params) {

      }
    };
  }

  public interface Logger {

    public String getName();

    public enum Level {

    }

    public boolean isLoggable(Level level);

    public default void log(Level level, String msg) {

    }

    public default void log(Level level, Supplier<String> msgSupplier) {

    }

    public default void log(Level level, Object obj) {

    }

    public default void log(Level level, String msg, Throwable thrown) {

    }

    public default void log(Level level, Supplier<String> msgSupplier, Throwable thrown) {

    }

    public default void log(Level level, String format, Object... params) {

    }

    public void log(Level level, ResourceBundle bundle, String msg, Throwable thrown);

    public void log(Level level, ResourceBundle bundle, String format, Object... params);
  }

But the error is same as while returning null in place of dummy Logger

Error :

running jpf with args:
JavaPathfinder core system v8.0 (rev ba7891bcf8074e7481d9921ebd71dfaf7be172bf) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 27/06/24, 7:49 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.InternalError: null property: native.encoding
	at jdk.internal.util.StaticProperty.getProperty(StaticProperty.java:73)
	at jdk.internal.util.StaticProperty.<clinit>(StaticProperty.java:67)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:619)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@27d,java.lang.Class@338
  call stack:
	at jdk.internal.util.StaticProperty.<clinit>(StaticProperty.java:67)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:619)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.InternalError: null property: native.enc..."

====================================================== search finished: 27/06/24, 7:49 pm

Answer 5 · 2024-06-27T15:49:58.000Z

Thanks for adding this. As this new code fixes one part of the bigger problem, please make a pull request.

I have looked at what happens next: It seems that the property native.encoding was not used in Java 11 (it was null) but should be something like UTF-8 now.

JPF pre-initializes its set of properties from a configuration vm.sysprop.source (by making a copy); that setting defaults to SELECTED. This calls getSelectedSysPropsFromHost from the native peer for System, in src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.java:

String[] defKeys = {
        "path.separator",
        "line.separator",
        "file.separator",
        "user.name",
        "user.home",
        "user.dir",
        "user.home",
        "user.timezone",
        "user.country",
        "java.home",
        "java.version",
        "java.io.tmpdir",
        JAVA_CLASS_PATH
        //... and probably some more
        // <2do> what about -Dkey=value commandline options
      };

So it looks like simply adding "native.encoding" to that list will fix this error.

Answer 6 · 2024-06-28T06:04:37.000Z

As this new code fixes one part of the bigger problem, please make a pull request.-> PR #467

added `native.encoding' :

String[] defKeys = {
        "path.separator",
        "line.separator", 
        "file.separator",
        "user.name",
        "user.home",
        "user.dir",
        "user.home",
        "user.timezone",
        "user.country",
        "java.home",
        "java.version",
        "java.io.tmpdir",
        "native.encoding",
        JAVA_CLASS_PATH
        //... and probably some more
        // <2do> what about -Dkey=value commandline options
      };

New error :

running jpf with args:
JavaPathfinder core system v8.0 (rev 7b6099f399c5188d612481de5d433391d1916e21) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 28/06/24, 11:11 am
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.access.SharedSecrets.setJavaSecurityPropertiesAccess(Ljdk/internal/access/JavaSecurityPropertiesAccess;)V
	at java.security.Security.<clinit>(Security.java:89)
	at java.io.ObjectInputFilter$Config.lambda$static$0(ObjectInputFilter.java:623)
	at java.io.ObjectInputFilter$Config$0.run
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:622)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testLambdaSerialization(ObjectStreamTest.java:143)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@282,java.lang.Class@364
  call stack:
	at java.security.Security.<clinit>(Security.java:89)
	at java.io.ObjectInputFilter$Config.lambda$static$0(ObjectInputFilter.java:623)
	at java.io.ObjectInputFilter$Config$0.run(pc 0)
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:622)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testLambdaSerialization(ObjectStreamTest.java:143)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.acce..."

====================================================== search finished: 28/06/24, 11:11 am
  running jpf with args:
JavaPathfinder core system v8.0 (rev 7b6099f399c5188d612481de5d433391d1916e21) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 28/06/24, 11:11 am
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.access.SharedSecrets.setJavaSecurityPropertiesAccess(Ljdk/internal/access/JavaSecurityPropertiesAccess;)V
	at java.security.Security.<clinit>(Security.java:89)
	at java.io.ObjectInputFilter$Config.lambda$static$0(ObjectInputFilter.java:623)
	at java.io.ObjectInputFilter$Config$0.run
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:622)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  owned locks:java.lang.Class@282,java.lang.Class@364
  call stack:
	at java.security.Security.<clinit>(Security.java:89)
	at java.io.ObjectInputFilter$Config.lambda$static$0(ObjectInputFilter.java:623)
	at java.io.ObjectInputFilter$Config$0.run(pc 0)
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.io.ObjectInputFilter$Config.<clinit>(ObjectInputFilter.java:622)
	at java.io.ObjectInputStream.<init>(ObjectInputStream.java:390)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:88)
	at java.lang.reflect.Method.invoke(Method.java)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodException: jdk.internal.acce..."

====================================================== search finished: 28/06/24, 11:11 am

Answer 7 · 2024-06-29T23:07:54.000Z

Implemented jdk.internal.access.SharedSecrets.setJavaSecurityPropertiesAccess() method.

Then next problem arise where System.Logger.Level required enum values of Level which was empty earlier.

public enum Level {
      ALL(Integer.MIN_VALUE),
      TRACE(400),
      DEBUG(500),
      INFO(800),
      WARNING(900),
      ERROR(1000),
      OFF(Integer.MAX_VALUE);

      private final int severity;

      private Level(int severity) {
        this.severity = severity;
      }
    }

Then next problem arise where implementation of setJavaLangReflectAccess() and getJavaLangReflectAccess() were required.

Our next error stack is :

running jpf with args:
JavaPathfinder core system v8.0 (rev 7b6099f399c5188d612481de5d433391d1916e21) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 30/06/24, 4:27 am
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;
java.lang.NoSuchMethodError: java.util.WeakHashMap$Entry.refersTo(Ljava/lang/Object;)Z
	at java.util.WeakHashMap.matchesKey(WeakHashMap.java:288)
	at java.util.WeakHashMap.get(WeakHashMap.java:407)
	at java.lang.ClassValue$ClassValueMap.finishEntry(ClassValue.java:475)
	at java.lang.ClassValue.getFromHashMap(ClassValue.java:232)
	at java.lang.ClassValue.getFromBackup(ClassValue.java:210)
	at java.lang.ClassValue.get(ClassValue.java:116)
	at java.io.ClassCache.get(ClassCache.java:84)
	at java.io.ObjectStreamClass.lookup(ObjectStreamClass.java:363)
	at java.io.ObjectStreamClass.initNonProxy(ObjectStreamClass.java:579)
	at java.io.ObjectInputStream.readNonProxyDesc(ObjectInputStream.java:2051)
	at java.io.ObjectInputStream.readClassDesc(ObjectInputStream.java:1898)
	at java.io.ObjectInputStream.readOrdinaryObject(ObjectInputStream.java:2224)
	at java.io.ObjectInputStream.readObject0(ObjectInputStream.java:1733)
	at java.io.ObjectInputStream.readObject(ObjectInputStream.java:509)
	at java.io.ObjectInputStream.readObject(ObjectInputStream.java:467)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:89)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.AssertionError: serialization readback failed: java.lang.NoSuchMethodError: java.util.WeakHashMap$Entry.refersTo(Ljava/lang/Object;)Z
	at gov.nasa.jpf.util.test.TestJPF.fail(TestJPF.java:164)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testSimpleReadbackOk(ObjectStreamTest.java:99)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:650)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: serialization readback f..."

====================================================== search finished: 30/06/24, 4:27 am

Here problem is that there is not mention of java.util.WeakHashMap$Entry.refersTo() method in OpenJDK17 anywhere.

Answer 8 · 2024-06-30T13:25:39.000Z

Hi @cyrille-artho , please look into this.

Answer 9 · 2024-06-30T14:46:51.000Z

This looks strange: we don't have a model class (not to mention native peer) of WeakHashMap, so there should be no missing methods. Can you please make a PR with your changes that you have made so far, so I can try if I can reproduce the same stack trace locally?

Answer 10 · 2024-07-01T11:10:10.000Z

Thanks, I can reproduce the problem now. Still not sure about the cause. We don't have a model class for WeakHashMap or its super classes. Normally, model classes implement only some API functions, which explains why a NoSuchMethodException would occur. @pparizek , any ideas?

Answer 11 · 2024-07-01T11:45:15.000Z

The class WeakHashMap$Entry extends java.lang.ref.WeakReference and java.lang.ref.Reference, for which we have model classes in JPF.

Answer 12 · 2024-07-01T11:47:22.000Z

The method refersTo is in the JDK variant of java.lang.ref.Reference, but not in our model class.

Answer 13 · 2024-07-01T11:56:02.000Z

I see, thanks @pparizek . Reference.refersTo is a new method (in Java 17). It looks like our model class Reference works without a native peer, so perhaps refersTo can be implemented by simply comparing parameter obj with the "referent" ref (which is set by the constructor).

Answer 14 · 2024-07-01T20:30:32.000Z

Hi, implemented java.lang.ref.Reference.refersTo() as below (respecting the documentation) :

public boolean refersTo(Object o){
    if (o == null) {
      return ref == null;
    } else {
      return o.equals(ref);
    }
  }

Then we got errors like below :

running jpf with args:
JavaPathfinder core system v8.0 (rev b9c5d1178367979f2051481cb32228e1931cd0ad) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
gov.nasa.jpf.test.java.io.ObjectStreamTest.runTestMethod()

====================================================== search started: 02/07/24, 1:50 am
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToDoubles([BI[DII)V
[WARNING] orphan NativePeer method: java.io.ObjectInputStream.bytesToFloats([BI[FII)V
[WARNING] orphan NativePeer method: jdk.internal.reflect.Reflection.getCallerClass(I)Ljava/lang/Class;
java.lang.NoSuchMethodError: java.lang.Class.isRecord()Z
	at java.io.ObjectStreamClass.<init>(ObjectStreamClass.java:375)
	at java.io.ObjectStreamClass$Caches$1.computeValue(ObjectStreamClass.java:110)
	at java.io.ObjectStreamClass$Caches$1.computeValue(ObjectStreamClass.java:107)
	at java.io.ClassCache$1.computeValue(ClassCache.java:73)
	at java.io.ClassCache$1.computeValue(ClassCache.java:70)
	at java.lang.ClassValue.getFromHashMap(ClassValue.java:228)
	at java.lang.ClassValue.getFromBackup(ClassValue.java:210)
	at java.lang.ClassValue.get(ClassValue.java:116)
	at java.io.ClassCache.get(ClassCache.java:84)
	at java.io.ObjectStreamClass.lookup(ObjectStreamClass.java:363)
	at java.io.ObjectStreamClass.initNonProxy(ObjectStreamClass.java:579)
	at java.io.ObjectInputStream.readNonProxyDesc(ObjectInputStream.java:2051)
	at java.io.ObjectInputStream.readClassDesc(ObjectInputStream.java:1898)
	at java.io.ObjectInputStream.readOrdinaryObject(ObjectInputStream.java:2224)
	at java.io.ObjectInputStream.readObject0(ObjectInputStream.java:1733)
	at java.io.ObjectInputStream.readObject(ObjectInputStream.java:509)
	at java.io.ObjectInputStream.readObject(ObjectInputStream.java:467)
	at gov.nasa.jpf.test.java.io.ObjectStreamTest.testLambdaSerialization(ObjectStreamTest.java:144)
	at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
	at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)
        .
        ........

Here StackTrace tells that our model class do not have java.lang.Class.isRecord().

I do not how our jpf treats the Record classes. For a moment, implemented the java.lang.Class.isRecord() as below :

public boolean isRecord() {
    return false;
  }

And then both tests passes.

Answer 15 · 2024-07-02T07:27:53.000Z

Thanks. I think we need reference equality, not value equality, in refersTo. Please re-run the tests after changing o.equals(ref) to o == ref.

Answer 16 · 2024-07-02T08:09:24.000Z

public boolean refersTo(Object o){
    if (o == null) {
      return ref == null;
    } else {
      return o == ref;
    }
  }

Yes, it worked!

PR #472

Answer 17 · 2024-07-02T09:22:00.000Z

Great, thanks!