Java 11 support for jpf-core

by Yuvaraj Anbarasan

About Java Pathfinder

Java Pathfinder (JPF) is a model checking tool for Java applications. JPF-core is the core structure of JPF. It is a Virtual Machine (VM) for Java bytecode which executes the system under test (SUT). While the execution semantics of Java bytecodes are clearly defined in Sun's Java virtual machine specifications, the semantics are hardwired in JPF - the VM instruction set is represented by a set of classes that can be replaced. JPF is a special VM. JPF itself is written in Java, so it is not as fast as your normal Java. That implies that JPF is VM which is running on top of another VM.

As JPF executes the SUT, it checks for certain properties which are given to JPF as input. Some of the properties that can be checked by JPF are unhandled exceptions, deadlocks, and user-defined assertions which are used to test properties of the code's behavior. After the execution of the SUT, JPF gives a detailed report on the properties which hold and verification artifacts that have been created by JPF for further analysis (like test cases).

Work summary

My task was to support JPF for java version 11 and 12.

Overview

The arrival of Java 9 introduced some interesting changes like the module system, handling strings, etc to the javac compiler and the Java internals. These changes caused various issues in JPF since a lot classes are dependent on the host JVM's implementation.

JPF can be viewed as a Java Virtual Machine (JVM) in itself. JPF has it's own implementation of the VM. Basically, JPF is a virtual machine (VM) running on top of the JVM. The class (.class) files at times are processed in two different ways in a JVM running JPF-core

  • as any other Java classes managed and executed by the host JVM (standard Java library classes, JPF implementation classes)
  • as "modeled" classes managed and processed (verified) by JPF

Each standard JVM supports a so called Java Native Interface (JNI), that is used to delegate execution from the Java level (i.e. JVM controlled bytecode) down into the (platform dependent) native layer (native method libraries). The primary goal is binary compatibility of native method libraries across all Java virtual machine implementations on a given platform.

Interestingly enough, there exists a analogous need to lower the "execution" level in JPF, from JPF controlled bytecode into JVM controlled bytecode. According to this analogy, the JPF specific interface is called Model Java interface (MJI), which is used to find or check mangled version of the native method when JPF encounters a native method.

JPF also has its own set of model classes which are used as a substitute for the JVM classes. The main reason for having model classes is that a lot of the functionalities can be implemented that the native methods have in simple Java code. Sometimes there exists a need to delegate the execution of a method to the host JVM and this is again done by declaring a function native using the native keyword. The native are invoked in the JVM using reflection, with the arguments drawn from the Model Java Interface environment (MJI).

Since the native method implementation of JPF is depenedent on the host JVM's implementation, a lot of issues occured when migrating JPF from java 8 to 11.

Pull Requests

#223

Added missing methods in native peer. Few methods were deprecated and new methods were introduced in java-12. This patch includes the missing methods and its implementation in native peer.

#227

Fixed native peer . Previously (in java 8 and lower versions), String values were stored as characters, and the string hash was computed as,

s[0]*31^(n-1) + s[1]*31^(n-2) + ... + s[n-1]
where s[i] was a character. This changed in java 9 and above versions, where s[i] is of type byte. Therefore, the existing logic didn't work since it tried to get char array instead of byte array. This PR fixed this issue by changing the logic to get byte array.

#232

#231

Added and implemented method in model class. method checks for by checking if the string offset is negative or greater than the string length.

#241

#238 #239

Since module system was introduced in java 9, the accessibilty of classes entirely depends on the modules instead of packages. Modularity adds a higher level of aggregation above packages. With module system, all the classes are dependent on the module info. Every class has its own module info. Module info contains details about class module. One such case which caused issue in JPF is .

inernally calls the class method which again calls class, and as a result of mutual dependency between the two classes, the call to was going into an infinite loop, causing a StackOverFlowError.

This issue occured because the logic in setting bootstrap method () to get enclosing lambda or class, was unable to partially resolve the classes. Hence everytime when enclosing class was not found, the class of again loaded if not already resolved. In this case, before Package class getting fully resolved, the Module class was called which again was not resolved. Hence resulted to infinte loop.

This issue was fixed by adding model class for Module class. Since the model classes are already resolved at JPF load time, when class calls class, the ClassLoader fetches the resolved model class.

Another issue related to class was, package version info initialization. A few fields related to Package were missing and were moved to the inner class of class. This issue was fixed by resolving class and initializing the fields in this class.

#242

#233

Added and implemented missing methods and in model and native peer classes

#245

was failing to fetch resource as the class path was missing module path. Fixed this issue by adding module path to class path.

#247

#246

Modified method logic. The method returns an . Previously, the method used an to store the resource URLs and converted the to , which was returned by the method. The URLs were not able to be added because of type mismatch which occured due to the changes in host JVM's implementation.

This issue was fixed by storing the resource URL's in an insted of storing it in an and return the instead the converting to and returning it.

#249

Removed model class for class and added logic to get partially resolved classes when seting bootstrap method (in).

Also, added method to model and native peer classes to get module name of a class. The method is implemented in the native peer to make use of the host JVM's . Using , and based on whether the resolved or loaded class is a JPF class or not, the module name was added to the class path in accordingly. This fixed the issue with method.

#257

#256

Added method to class native peer. The implementation of was changed since java 9. It leverages vector-based techniques to access and compare the contents of two arrays (to make the comparison efficient). To access the contents of the array, is used. This method uses Unsafe.getLong to get value of the array based on the offset value.

Since, the type of the array was not long, JPF was throwing an exception. This was becasue the offset value passed to method was the index of the array instead of the offset value. The offset value should have been,

((array Object's base index) - (offset of long type)) - ((array Object's base index) - (offset of array type (i.e, int, float, double, etc)))

Hence logic was not woking as expected. And since the method calculating is a host JVM class, the solution to this issue was to add and implement in native peer class. The native peer method, uses the type of the array instead of offset to return the right value.

#264

#261

was deprecated in Java 9. It can be replaced by . But the problem is that returns any constructor without regarding the access level. Hence, was not throwing any exception when instance of inaccessible constructors were created as JPF's implementaton of was not checking access levels of constructors.

Fixed this issue by adding logic to check access level of the caller class in native peer.

Conclusion

It was a great experience working for three months on my project for Java Pathfinder under Google Summer of Code. I sincerely thank my mentors and whose support, guidance and continuous encouragement helped me immensely in bringing this work where it stands.

Thanks, Google and Java Pathfinder for giving me this opportunity.