javapathfinder / jpf-core

JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.
528 stars 334 forks source link

VM.getSavedProperty("os.name") not supported #495

Open cyrille-artho opened 1 month ago

cyrille-artho commented 1 month ago

Some properties have to be set at the time when the VM is initialized; this is not the case for os.name. If a class later calls VM.getSavedProperty("os.name"), the result is an IllegalArgumentException because the property has not been set.

cyrille-artho commented 1 month ago

Example to reproduce problem:

public class Test {
  public static void main(String[] args) {
    System.out.println(jdk.internal.misc.VM.getSavedProperty("os.name"));
  }
}

Run with bin/jpf +classpath=. Test.

Harsh4902 commented 3 weeks ago
Properties props = new Properties();
props.setProperty("os.name","Linux");
VM.saveAndRemoveProperties(props);

I have added these lines to ensure that savedProps variable of jdk.internal.misc.VM class is initialized, and I got the results.

JavaPathfinder core system v8.0 (rev a16b929e0aae442552277e0be3ae86e2666b0b10) - (C) 2005-2014 United States Government. All rights reserved.

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

====================================================== search started: 9/12/24, 5:28 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Linux

====================================================== 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=617,released=35,maxLive=0,gcCycles=1
instructions:       11482
max memory:         62MB
loaded code:        classes=108,methods=2221
cyrille-artho commented 3 weeks ago

Great! Please see where in the VM initialization you can add such code (using the union of the existing properties and the new "os.name" property).

cyrille-artho commented 3 weeks ago

We want to use the results of the host JVM's System.getProperty to set the same value on the properties map of the JPF VM.

cyrille-artho commented 3 weeks ago

There is a mechanism for this in the native peer of System, in src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.java, getSelectedSysPropsFromHost. This is the default behavior, but "os.name" is currently missing there; try adding it there, perhaps this will resolve this issue.

cyrille-artho commented 1 week ago

There is a type mismatch in the multi process VM, maybe somewhere in initialize. Try finding out where there is a difference w.r.t. system properties between src/main/gov/nasa/jpf/vm/SingleProcessVM.java and src/main/gov/nasa/jpf/vm/MultiProcessVM.java.