Challenges running java.util.logging.Logger.getLogger in JPF

[copumpkin]

I have this super minimal reproduction:

public class Input {
  public static void main(String[] args) {
    System.out.println("-------- In main!");

    java.util.logging.Logger.getLogger("blah");
  }
}

I'm running it against the java-10-gradle branch (a816054) and the first thing I get when calling that is:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: Calling java.lang.Thread.<init>(Ljava/lang/ThreadGroup;Ljava/lang/Runnable;Ljava/lang/String;JZ)V
	at java.util.logging.LogManager$Cleaner.<init>(LogManager.java:261)
	at java.util.logging.LogManager.<init>(LogManager.java:301)
	at java.util.logging.LogManager.<init>(LogManager.java:294)
	at java.util.logging.LogManager$1.run(LogManager.java:248)
	at java.util.logging.LogManager$1.run(LogManager.java:223)
	at java.security.AccessController.doPrivileged(AccessController.java:34)
	at java.util.logging.LogManager.<clinit>(LogManager.java:223)
	at java.util.logging.Logger.demandLogger(Logger.java:648)
	at java.util.logging.Logger.getLogger(Logger.java:717)
	at java.util.logging.Logger.getLogger(Logger.java:701)
	at Input.main(Input.java:5)

So I added an extra method with an (ignored) boolean to here:

jpf-core/src/classes/modules/java.base/java/lang/Thread.java

Lines 118 to 121 in a816054

	public Thread (ThreadGroup group, Runnable target, String name) {
	this(group, target, name, 0L);
	}

I then ran into a similar issue from java.security.AccessController and added another dummy overload there.

That got me past the initial issue, but now I'm stuck here:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native jdk.internal.misc.VM.initializeFromArchive
	at jdk.internal.misc.VM.initializeFromArchive(gov.nasa.jpf.vm.JPF_jdk_internal_misc_VM)
	at java.util.ImmutableCollections$SetN.<clinit>(ImmutableCollections.java:583)
	at java.util.Set.of(Set.java:502)
	at java.nio.file.spi.FileSystemProvider.<clinit>(FileSystemProvider.java:428)
	at sun.nio.fs.DefaultFileSystemProvider.<clinit>(DefaultFileSystemProvider.java:35)
	at java.nio.file.FileSystems.getDefault(FileSystems.java:185)
	at java.nio.file.Path.of(Path.java:147)
	at java.nio.file.Paths.get(Paths.java:69)
	at java.util.logging.LogManager.getConfigurationFileName(LogManager.java:1389)
	at java.util.logging.LogManager.readConfiguration(LogManager.java:1375)
	at java.util.logging.LogManager.readPrimordialConfiguration(LogManager.java:445)
	at java.util.logging.LogManager$2.run(LogManager.java:394)
	at java.security.AccessController.doPrivileged(AccessController.java:39)
	at java.util.logging.LogManager.ensureLogManagerInitialized(LogManager.java:382)
	at java.util.logging.LogManager.getLogManager(LogManager.java:430)
	at java.util.logging.Logger.demandLogger(Logger.java:648)
	at java.util.logging.Logger.getLogger(Logger.java:717)
	at java.util.logging.Logger.getLogger(Logger.java:701)
	at Input.main(Input.java:5)

Which doesn't seem to be as easy to fix as the two above. Anyone have hints for how to get past this?

[quadhier]

Considering that JDK's implementation of logging API involves interactions with the module system which JPF doesn't fully support yet and core functions of Logger are easy to simulate, creating a model class for java.util.logging.Logger might be a good choice to support logging API.

[Rohan-here]

is somebody working on this? I would like to pick it up

[d1vyanshu-kumar]

Hello @cyrille-artho @copumpkin,
it seems like no one is working on this issue. I'll start working on it now.

[cyrille-artho]

Yes, whenever there is no concrete discussion on a solution attempt for a given issue, this means that nobody is working on it.

[d1vyanshu-kumar]

@cyrille-artho I am attempting to replicate this issue on my local machine, but I encountered the following error.

Steps taken to reproduce the issue:

1. Checked out commit a816054:

   git checkout a816054

2. Created Input.java.
3. Compiled the Java file.
4. Created a JPF configuration file (Input.jpf).
5. Ran Java PathFinder (JPF):

   java -jar build/RunJPF.jar Input.jpf

Observed output:

[SEVERE] JPF configuration error: error instantiating class gov.nasa.jpf.vm.OVHeap for entry "vm.heap.class":
> exception in gov.nasa.jpf.vm.OVHeap(gov.nasa.jpf.Config,gov.nasa.jpf.vm.KernelState):
>> java.lang.NoClassDefFoundError: sun/misc/SharedSecrets
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated

Analysis:

Upon investigating, I found that sun.misc.SharedSecrets was available in Java 8 but was removed in Java 9 and later. This appears to be the root cause of JPF failing when attempting to access internal Java APIs.

I ran the same steps using Java 8, and JPF executed successfully.
Could you please provide guidance on this?
Thank you!

[cyrille-artho]

The main branch of jpf-core is meant to run with Java 11. We still have an older version on branch java-8, but we don't develop that anymore. Please try using OpenJDK 11.