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

eklaDFF · 2024-06-20T18:25:46Z

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

The text was updated successfully, but these errors were encountered:

eklaDFF · 2024-06-20T18:31:40Z

@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 .

cyrille-artho · 2024-06-24T06:48:25Z

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.

cyrille-artho · 2024-06-27T07:20:50Z

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.

eklaDFF · 2024-06-27T14:24:11Z

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

cyrille-artho · 2024-06-27T15:49:58Z

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.

eklaDFF · 2024-06-28T06:04:37Z

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

eklaDFF · 2024-06-29T23:07:54Z

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.

eklaDFF · 2024-06-30T13:25:39Z

Hi @cyrille-artho , please look into this.

cyrille-artho · 2024-06-30T14:46:51Z

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?

eklaDFF · 2024-06-30T20:42:14Z

PR #469

cyrille-artho · 2024-07-01T11:10:10Z

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?

pparizek · 2024-07-01T11:45:15Z

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

pparizek · 2024-07-01T11:47:22Z

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

cyrille-artho · 2024-07-01T11:56:02Z

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).

eklaDFF · 2024-07-01T20:30:32Z

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.

cyrille-artho · 2024-07-02T07:27:53Z

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.

eklaDFF · 2024-07-02T08:09:24Z

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

Yes, it worked!

PR #472

cyrille-artho · 2024-07-02T09:22:00Z

Great, thanks!

cyrille-artho closed this as completed Jul 2, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

eklaDFF commented Jun 20, 2024 •

edited

Loading

eklaDFF commented Jun 20, 2024

cyrille-artho commented Jun 24, 2024 •

edited

Loading

cyrille-artho commented Jun 27, 2024

eklaDFF commented Jun 27, 2024

cyrille-artho commented Jun 27, 2024

eklaDFF commented Jun 28, 2024

eklaDFF commented Jun 29, 2024

eklaDFF commented Jun 30, 2024

cyrille-artho commented Jun 30, 2024

eklaDFF commented Jun 30, 2024

cyrille-artho commented Jul 1, 2024

pparizek commented Jul 1, 2024

pparizek commented Jul 1, 2024

cyrille-artho commented Jul 1, 2024

eklaDFF commented Jul 1, 2024 •

edited

Loading

cyrille-artho commented Jul 2, 2024

eklaDFF commented Jul 2, 2024 •

edited

Loading

cyrille-artho commented Jul 2, 2024

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

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

Comments

eklaDFF commented Jun 20, 2024 • edited Loading

eklaDFF commented Jun 20, 2024

cyrille-artho commented Jun 24, 2024 • edited Loading

cyrille-artho commented Jun 27, 2024

eklaDFF commented Jun 27, 2024

cyrille-artho commented Jun 27, 2024

eklaDFF commented Jun 28, 2024

eklaDFF commented Jun 29, 2024

eklaDFF commented Jun 30, 2024

cyrille-artho commented Jun 30, 2024

eklaDFF commented Jun 30, 2024

cyrille-artho commented Jul 1, 2024

pparizek commented Jul 1, 2024

pparizek commented Jul 1, 2024

cyrille-artho commented Jul 1, 2024

eklaDFF commented Jul 1, 2024 • edited Loading

cyrille-artho commented Jul 2, 2024

eklaDFF commented Jul 2, 2024 • edited Loading

cyrille-artho commented Jul 2, 2024

eklaDFF commented Jun 20, 2024 •

edited

Loading

cyrille-artho commented Jun 24, 2024 •

edited

Loading

eklaDFF commented Jul 1, 2024 •

edited

Loading

eklaDFF commented Jul 2, 2024 •

edited

Loading