Model Class Loading

[Mahmoud-Khawaja]

I created a minimal test extension to diagnose the model class loading issue. Here are my findings. Please also check this repository: https://github.com/Mahmoud-Khawaja/jpf-test.

You can test it on your machine, but make sure to modify the site.properties file first.

jpf-core = PATH
jpf-test = PATH
extensions = ${jpf-core}

build the jar

gradle buildJars

and

java -jar ~/Downloads/nas/jpf-core/build/RunJPF.jar TestMath.jpf

you will get this output

avaPathfinder core system v8.0 (rev 7a901f73eec280ee2a3a14ff57a0ad4269b7baee) - (C) 2005-2014 United States Government. All rights reserved.


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

====================================================== search started: 10/3/25, 8:13 AM
=== Testing JPF Math Model ===
[JPF-TEST] Math.max() called via peer: 10, 20
[JPF-TEST] Math.min() called via peer: 16, 34
[JPF-TEST] Math.min() called via peer: 34, 21
Math.max(10, 20) = 20
[JPF-TEST] Math.min() called via peer: 10, 20
[JPF-TEST] Math.min() called via peer: 16, 34
[JPF-TEST] Math.min() called via peer: 34, 21
Math.min(10, 20) = 10
[JPF-TEST] Math.sqrt() called via peer: 16.0
[JPF-TEST] Math.min() called via peer: 16, 34
[JPF-TEST] Math.max() called via peer: 0, -2
[JPF-TEST] Math.min() called via peer: 1, 1
[JPF-TEST] Math.min() called via peer: 34, 21
Math.sqrt(16.0) = 4.0
[JPF-TEST] Math.min() called via peer: 16, 34
[JPF-TEST] Math.min() called via peer: 34, 18
Math.abs(-42) = 42
FAILURE: Standard Math class loaded (model not working)
(Method getModelInfo() not found)
=== Test Complete ===

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=4,visited=0,backtracked=4,end=1
search:             maxDepth=4,constraints=0
choice generators:  thread=4 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=3), data=0
heap:               new=1331,released=54,maxLive=1252,gcCycles=4
instructions:       154856
max memory:         250MB
loaded code:        classes=101,methods=2474

====================================================== search finished: 10/3/25, 8:13 AM

as we can see here Peer classes load correctly - I see diagnostic output [JPF-TEST] Math.max() called via peer: 10, 20 proving the native peer methods execute

Model classes do not load - The diagnostic method Math.getModelInfo() throws NoSuchMethodError, meaning JPF is using the standard JDK java.lang.Math instead of my model class

[cyrille-artho]

Thank you for creating this example. While compilation does not succeed for me due to an undeclared dependency, I still get all the necessary artifacts to run the test. I get the same behavior.
At the moment, Math.class is not part of the module java.base, so perhaps this is why it is not recognized as a replacement for the built-in library class.

[cyrille-artho]

Check build.gradle in jpf-core, which uses --patch-module to produce class files that replace built-in library classes.
It also uses --add-reads. Try to make the configuration as similar as possible to the one in jpf-core.

[Mahmoud-Khawaja]

Hi Cryille,
I think i found something here. The issue that we still loading Math from the java run time system even though the structure is correct. I tried to look at what classes that jpf-core provides

and i found this

finn@lenovo:~/Downloads/nas/jpf-test$ jar tf ~/Downloads/nas/jpf-core/build/jpf-classes.jar | grep "java.base/java/lang"       
modules/java.base/java/lang/
modules/java.base/java/lang/ClassLoader$EnumerationAdapter.class
modules/java.base/java/lang/invoke/
modules/java.base/java/lang/invoke/JPFFieldVarHandle.class
modules/java.base/java/lang/String.class
modules/java.base/java/lang/System.class
modules/java.base/java/lang/StackFrameInfo.class
modules/java.base/java/lang/ThreadLocal.class
modules/java.base/java/lang/System$2.class
modules/java.base/java/lang/StackTraceElement.class
modules/java.base/java/lang/annotation/
modules/java.base/java/lang/annotation/Retention.class
modules/java.base/java/lang/annotation/Inherited.class
modules/java.base/java/lang/ThreadLocal$SuppliedThreadLocal.class
modules/java.base/java/lang/Thread$Permit.class
modules/java.base/java/lang/Thread.class
modules/java.base/java/lang/reflect/
modules/java.base/java/lang/reflect/Method.class
modules/java.base/java/lang/reflect/InvocationTargetException.class
modules/java.base/java/lang/reflect/Proxy.class
modules/java.base/java/lang/reflect/AccessibleObject.class
modules/java.base/java/lang/reflect/Field.class
modules/java.base/java/lang/reflect/Constructor.class
modules/java.base/java/lang/ThreadGroup.class
modules/java.base/java/lang/ThreadLocal$Entry.class
modules/java.base/java/lang/System$1.class
modules/java.base/java/lang/String$CaseInsensitiveComparator.class
modules/java.base/java/lang/InheritableThreadLocal.class
modules/java.base/java/lang/Thread$UncaughtExceptionHandler.class
modules/java.base/java/lang/Throwable.class
modules/java.base/java/lang/Object.class
modules/java.base/java/lang/ClassLoader.class
modules/java.base/java/lang/ref/
modules/java.base/java/lang/ref/Reference.class
modules/java.base/java/lang/ref/WeakReference.class
modules/java.base/java/lang/ref/ReferenceQueue.class
modules/java.base/java/lang/Thread$State.class
modules/java.base/java/lang/Class.class
java.base/java/lang/
java.base/java/lang/ClassLoader$EnumerationAdapter.class
java.base/java/lang/invoke/
java.base/java/lang/invoke/JPFFieldVarHandle.class
java.base/java/lang/String.class
java.base/java/lang/System.class
java.base/java/lang/StackFrameInfo.class
java.base/java/lang/ThreadLocal.class
java.base/java/lang/System$2.class
java.base/java/lang/StackTraceElement.class
java.base/java/lang/annotation/
java.base/java/lang/annotation/Retention.class
java.base/java/lang/annotation/Inherited.class
java.base/java/lang/ThreadLocal$SuppliedThreadLocal.class
java.base/java/lang/Thread$Permit.class
java.base/java/lang/Thread.class
java.base/java/lang/reflect/
java.base/java/lang/reflect/Method.class
java.base/java/lang/reflect/InvocationTargetException.class
java.base/java/lang/reflect/Proxy.class
java.base/java/lang/reflect/AccessibleObject.class
java.base/java/lang/reflect/Field.class
java.base/java/lang/reflect/Constructor.class
java.base/java/lang/ThreadGroup.class
java.base/java/lang/ThreadLocal$Entry.class
java.base/java/lang/System$1.class
java.base/java/lang/String$CaseInsensitiveComparator.class
java.base/java/lang/InheritableThreadLocal.class
java.base/java/lang/Thread$UncaughtExceptionHandler.class
java.base/java/lang/Throwable.class
java.base/java/lang/Object.class
java.base/java/lang/ClassLoader.class
java.base/java/lang/ref/
java.base/java/lang/ref/Reference.class
java.base/java/lang/ref/WeakReference.class
java.base/java/lang/ref/ReferenceQueue.class
java.base/java/lang/Thread$State.class
java.base/java/lang/Class.class

I suspect the answer is we cant really Load it because jpf core actaully doesnt provide Math model class which means that the jpf class loader is configured always to load Math from JRT.

as you can see in the log it provides model classes for object, string, Thread and some other classes but there is no Math.
What we're tryina do is unsolvable for Math class. What I'm thinking now is to try to test some other class like String, Object . of course I'm not gonna implement the whole class its gonna a be very simplified version just to see if what im thinking of is correct

[cyrille-artho]

I had not noticed before that the model classes are duplicated in the JAR file, even in jpf-core. The file is not very large, but having classes both in java.base and also in modules/java.base makes it hard to debug this type of problem.
Maybe we look at jpf-core first and try to clean up the build so only one of these two copies is used? That will make it easier to see what is going on.
In the case of jpf-nas, something is not correct in the build because Math is missing; I assume that the model class loading itself would work if that class is present.

[Mahmoud-Khawaja]

Hello Cyrille,
Sorry for late updates I was very busy for the last week. I actaully implemented a minimal string class ( Please check my ext https://github.com/Mahmoud-Khawaja/jpf-test ). and somehow it also failed to load the model class. however it should work cause we have it in jpf-classes.jar. I tried to print the class loading log for both math and string and here is what I found

finn@lenovo:~/Downloads/nas/jpf-test$ java -jar ~/Downloads/nas/jpf-core/build/RunJPF.jar TestMath.jpf | grep -E "(Testing|SUCCESS|FAILURE|Model info|loading class java.lang.Math)"
=== Testing JPF Math Model ===
[INFO] loading class java.lang.Math from jrt:/java.base/java/lang/Math.class
SUCCESS: Peer classes working (see [JPF-TEST] messages above)

as we know math should load from the jrt which is expected cause we dont have it in the whitelist in jpf-classes.jar thats why we need a peer for it.
but for the string this is what we have:

finn@lenovo:~/Downloads/nas/jpf-test$ java -jar ~/Downloads/nas/jpf-core/build/RunJPF.jar TestString.jpf | grep -E "(Testing|SUCCESS|FAILURE|Model info|loading class java.lang.String)"
[INFO] loading class java.lang.String from jar:file:/home/finn/Downloads/nas/jpf-core/build/jpf-classes.jar!/java.base/java/lang/String.class
[INFO] loading class java.lang.String$CaseInsensitiveComparator from jar:file:/home/finn/Downloads/nas/jpf-core/build/jpf-classes.jar!/java.base/java/lang/String$CaseInsensitiveComparator.class
=== Testing JPF String Model ===
[INFO] loading class java.lang.StringBuilder from jrt:/java.base/java/lang/StringBuilder.class
[INFO] loading class java.lang.StringLatin1 from jrt:/java.base/java/lang/StringLatin1.class
FAILURE: Standard String class loaded

it doesn't load the model class from my extention it loads String class in jpf core. you can also notice that StringBuilder are being loaded from the jrt cause its not in the jar

[INFO] loading class java.lang.String from jar:file:/home/finn/Downloads/nas/jpf-core/build/jpf-classes.jar!/java.base/java/lang/String.class

I'm not sure if there is a way to load the class that we have in jpf-test instead of loading it from jpf-core. there has to be a way to override that but I don't know how to do it yet.

Any ideas about how we can do it?

also, regarding the duplication in java.base and in modules/java.base I don't know if its intentional I haven't looked at it yet.

[cyrille-artho]

Hi,
I currently can't build your project jpf-test because it assumes jpf-core to be in a hard-coded path (relative to the user's home). The convention for extensions is that jpf-core is in ../jpf-core. I think this worked in an earlier version; can you please try to adapt this?
Also, please copy the output of jar tf build/jpf-test.jar so I can see if the model class is part of the runtime; this is what currently is missing in jpf-nas.

[cyrille-artho]

Please try the following to simplify build.gradle a bit:

1. Use a more portable way of detecting the parent directory and the location of jpf-core.
2. Compile the classes once and include them in the JAR file once.
   This will likely not solve the issue of reproducing the build but at least reduce the number of steps in the build file and simplify the debugging slightly.

[Sameersawant77]

I have cloned the test extension locally to verify this issue. The output of jar tf build/jpf-test.jar is

META-INF/
META-INF/MANIFEST.MF
gov/
gov/nasa/
gov/nasa/jpf/
gov/nasa/jpf/vm/
gov/nasa/jpf/vm/JPF_java_lang_Math.class