Skip to content

Fix class loading order to support any extension#587

Open
Mahmoud-Khawaja wants to merge 1 commit intojavapathfinder:masterfrom
Mahmoud-Khawaja:model-classes-fix
Open

Fix class loading order to support any extension#587
Mahmoud-Khawaja wants to merge 1 commit intojavapathfinder:masterfrom
Mahmoud-Khawaja:model-classes-fix

Conversation

@Mahmoud-Khawaja
Copy link
Copy Markdown
Contributor

No description provided.

@Mahmoud-Khawaja
Copy link
Copy Markdown
Contributor Author

Hi @cyrille-artho ,

This is more elegant solution that adding a new config in init in ClassLoaderInfo. I was thinking first about adding vm.model_class_priority but to be honest it sounded like adding stuff rather than fixing the main issue. I think this is a good solution so far. the main issue was when we tried to override a model class that already existed in jpf core (such as java.lang.Math or java.lang.String) it wouldn't work because the order of search

jpf was searching for classes in the following order:
1 classpath (application classes)
2 vm.boot_classpath (jpf-core model classes)
3 jrt classes

so here is the thing
in the old code we had

// loading class path first
pathElements = getPathElements(conf, "classpath", appId); 


// then load vm.boot_classpath (jpf-core)
pathElements = getPathElements(conf, "vm.boot_classpath", appId);

but in the new code we are looking for all properties named *.boot_classpath if it found something like our test ext
jpf-test.boot_classpath it will load it first before anythingelse and add it to the class path.

I've tested that on my machine and it works good now

in jpf-test ext in Math.java model class

i have a function abs that should that should return 999 regardless the parameter

    public static int abs(int a) {
        return 999;  // wrong on purpose
    }

when i test that

java -jar ../jpf-core/build/RunJPF.jar TestMath.jpf
public class TestMath {
    public static void main(String[] args) {
        int absVal = Math.abs(-42);

        System.out.println(absVal); // should be 99
    }
}

it will result


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

====================================================== search started: 1/11/26, 7:23 AM
999

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

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=496,released=24,maxLive=0,gcCycles=1
instructions:       9160
max memory:         250MB
loaded code:        classes=80,methods=1658

====================================================== search finished: 1/11/26, 7:23 AM

which means that its using the function in my model class. same thing for string model class. Now, I think this will be helpful to fix the same issue we had with jpf-nas months ago. Please Let me know what you think about that

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant