Comments (18)
eklaDFF
commented on August 30, 2024
@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 .
from jpf-core.
cyrille-artho
commented on August 30, 2024
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.
from jpf-core.
cyrille-artho
commented on August 30, 2024
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.
from jpf-core.
eklaDFF
commented on August 30, 2024
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
from jpf-core.
cyrille-artho
commented on August 30, 2024
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.
from jpf-core.
eklaDFF
commented on August 30, 2024
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
from jpf-core.
eklaDFF
commented on August 30, 2024
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.
from jpf-core.
eklaDFF
commented on August 30, 2024
Hi @cyrille-artho , please look into this.
from jpf-core.
cyrille-artho
commented on August 30, 2024
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?
from jpf-core.
eklaDFF
commented on August 30, 2024
PR #469
from jpf-core.
cyrille-artho
commented on August 30, 2024
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?
from jpf-core.
pparizek
commented on August 30, 2024
The class WeakHashMap$Entry extends java.lang.ref.WeakReference and java.lang.ref.Reference, for which we have model classes in JPF.
from jpf-core.
pparizek
commented on August 30, 2024
The method refersTo is in the JDK variant of java.lang.ref.Reference, but not in our model class.
from jpf-core.
cyrille-artho
commented on August 30, 2024
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).
from jpf-core.
eklaDFF
commented on August 30, 2024
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.
from jpf-core.
cyrille-artho
commented on August 30, 2024
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.
from jpf-core.
eklaDFF
commented on August 30, 2024
public boolean refersTo(Object o){
if (o == null) {
return ref == null;
} else {
return o == ref;
}
}
Yes, it worked!
PR #472
from jpf-core.
cyrille-artho
commented on August 30, 2024
Great, thanks!
from jpf-core.
Related Issues (20)
- java.lang.NoSuchMethodError: java.lang.String.getBytes([BIIBI) HOT 13
- cannot find native jdk.internal.misc.CDS.isDumpingClassList0 HOT 43
- StringIndexOutOfBoundsException HOT 5
- `java.net.URI.toURI` broken
- Java 17: BufferMismatch now depends on native code: JPF crashes (missing native peer) if byte buffers differ
- `BufferTest.testCharBufferConstructor` uses random bytes HOT 96
- Test "gov.nasa.jpf.test.java.concurrent.SemaphoreTest" fails on OpenJDK-17 HOT 16
- Assistance Needed with Deadlock Detection in JPF HOT 5
- "gov.nasa.jpf.test.java.concurrent.CountDownLatchTest" and "gov.nasa.jpf.test.java.concurrent.ExecutorServiceTest" fails on Java-17 HOT 16
- "gov.nasa.jpf.test.java.concurrent.ConcurrentSkipListMapTest" fails on Java-17 HOT 6
- Add support for package metadata in `JarClassFileContainer`
- Investigate `java.lang.invoke.MethodHandles$Lookup.findVarHandle` HOT 19
- NullPointerException in `java.util.jar.JarFile.getEntry0` method HOT 5
- Compiler warnings under Java 17 HOT 35
- java.lang.NoSuchMethodException: SharedSecrets.setJavaNetInetAddressAccess HOT 4
- Need Implementation of `JarFile`
- "record" feature in jpf-core/java-17 HOT 39
- "Sealed Class and Interface" feature of "OpenJDK-17" on JPF/java-17 HOT 9
- NumericValueChecker incorrectly reports out-of-range error
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from jpf-core.